Formal Verification of PLC-Code

Date: Thursday, May 26, 2011
Speaker: Sebastian Biallas
Venue: TU Vienna

188/2 – @ 17.00

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 huge 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 model checker [mc]square, 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 techniques that make the verification of real world PLCs programs feasible.

Posted in RiSE Seminar