Formal Verification of PLC-Code

Speaker

Sebastian Biallas
(Informatik 11)

Title Formal Verification of PLC-Code
When 02.05.2012, 10:00
Where Room 5052
Abstract Programmable Logic Controllers (PLCs) are industrial control systems used as control devices in the automation industry and for monitoring of safety critical infrastructure. Since they are often used in safety critical environments, where a failure might have serious effects for human health or the environment, formal verification of their programs is advised. This strive for functional correctness combined with having small, well-structured programs, makes PLCs a very interesting platform for the application of formal methods.

In this talk, I will give a short introduction to PLCs and their programming modes. Then, I will turn to the ArcadePLC tool, which is developed at the Embedded Software Laboratory at the RWTH Aachen and allows for the verification of PLC programs. I will discuss current progress and obstacles and detail some of our abstraction techniques that make the verification of real world PLCs programs feasible.

Slides