Application of Formal Methods to Verify Industrial Control Code (Theta4PLCverif)

The European Organization for Nuclear Research (CERN) is one of the world's largest physics laboratory. Many safety critical control systems of its advanced machinery are operated by programmable logic controllers (PLCs). The purpose of the collaboration between CERN and the Fault Tolerant Systems Research Group (FTSRG) of BME is the formal verification of software running on such PLCs. Formal verification techniques (such as model checking) can give mathematically precise proofs that the software meets certain requirements (e.g., assertions never fail).

PLCverif is a tool developed at CERN, supporting the formal verification of software running on PLCs. It works by translating the source code of PLC programs and the requirement to the input language of different model checking tools, and reporting their result to the user in a clean manner, which requires no deep knowledge in formal methods.

The first phase of the project aimed at designing the architecture for the new version of PLCverif. An important feature of the new tool is that its internal model allows it to be easily extended by different model checkers as backends.

The purpose of the second phase was to integrate the Theta verification tool as a backend in PLCverif. Theta is a generic, modular and configurable model checking framework developed at FTSRG. It includes various state-of-the-art algorithms and some novel ideas as well. Theta was successfully integrated into PLCverif in this phase and an extensive benchmarking session on 90 input PLC programs concluded that it can verify all of them.

BME provided novel algorithms to help to scale the verification to more complex programs. The collaboration presents a step towards provable safe control systems that is of utmost importance for such critical control systems.