Control systems that are used in areas such as nuclear reactors, chemical plants, railway signaling, and aircraft are safety-critical systems. Failure on these systems can cause injuries, death, or damage to the environment and property. These systems must use control systems that have gone through an extensive and thorough verification process. Programmable logic controllers (PLCs) are digital control systems that are widely used in safety-critical systems. These control systems must often be verified with respect to a specification. There are several ways of doing that and formal verification techniques is one of them.
The PLC programming standard, IEC 61131-3, is widely accepted in the industry. PLC programmers who develop control systems for safety-critical systems often need to verify the logic of the PLCs by using formal methods such as model checking. Translating from a PLC programming language to the input language of a model checker takes times and is error-prone. It also needs to be done frequently if the PLC is often modified.
In this master’s thesis we develop and evaluate a compiler that can automatically translate PLC programs in function block diagrams (FBD), one of five industry standard PLC programming languages, to the input language of the model checker NuSMV. We will compile a PLC program from a case study suggested by the company DNV GL. The case study will used as a validation of the compiler. The efficiency and performance of the PLC-NuSMV compiler will also be evaluated.
| supervisors | Martin Steffen, Ingrid Yu, Yingyue Li |
| IFI links | abstract, thesis, presentation |
| code repository | bitbucket |