Bringing Automated Formal Verification to PLC Program Development

Automation is the field of engineering that deals with the development of control systems for operating systems such as industrial processes, railways, machinery or aircraft without human intervention. In most of the cases, a failure in these control systems can cause a disaster in terms of economic losses, environmental damages or human losses. For that reason, providing safe, reliable and robust control systems is a first priority goal for control engineers. Ideally, control engineers should be able to guarantee that both software and hardware fulfill the design requirements. This is an enormous challenge in which industry and academia have been working and making progresses in the last decades. This thesis focuses on one particular type of control systems that operates industrial processes, the PLC (Programmable Logic Controller) - based control systems. Moreover it targets one of the main challenges for these systems, guaranteeing that PLC programs are compliant with their specifications. Traditionally in industry, PLC programs are checked using testing techniques. Testing consists in checking the requirements on the real system. Although these testing techniques have achieved good results in different kind of systems, they have some well-known drawbacks such as the difficulty to check safety and liveness properties (e.g. ensuring a forbidden output value combination should never occur). This thesis proposes an alternative for checking PLC programs. A methodology based on formal verification techniques, which can complement the testing techniques to guarantee that a PLC program is compliant with the specifications. Formal verification is a technique meant to prove the correctness of a system by using formal methods. One of the most popular formal verification techniques is model checking, which consists in checking a formalized requirement in a formal model of the system. Comparing model checking with testing, model checking explores all the possible combinations of the state space in the formal model to guarantee that the formal requirement is satisfied. Formal verification and in particular model checking appears to be a very appropriate technique for this goal. However, the industrial automation community has not adopted yet this approach to verify PLC code, even if some standards, like the IEC 61508, highly recommend the use of formal methods for Safety Instrumented Systems. This is due to following challenges for control engineers: (1) the difficulty of building formal models representing real-life PLC programs, (2) the difficulty of using specification formalisms to express the requirements and finally, (3) when creating formal models out of real-life software, the number of combinations can be huge and model checking tools may not be able to handle the state space, thus cannot evaluate the given requirement. This research deals with these three main challenges and tries to fill the gap between the industrial automation and the formal verification communities. The thesis proposes a general methodology for applying automated formal verification to PLC programs and any complexity related to formal methods is hidden from control engineers. In this methodology, formal models are built automatically out of the PLC programs. The model transformations are divided in two parts: PLC programs, from the IEC 61131 standard, are translated to an Intermediate Model (IM), which is the central piece of this methodology. The IM is then transformed to the input modeling languages of different verification tools (e.g. nuXmv, UPPAAL or BIP). This modeling strategy simplifies the model transformations and makes the integration of new verification tools easier. Regarding the requirements formalization, this methodology provides a solution that allows control engineers to express the requirements in a simple and natural language based on patterns with well-defined semantics. Then, these requirements are translated to temporal logic formalisms as they are the most common formalisms used by the verification tools. Regarding the state space explosion problem, this methodology provides a set of reduction and abstraction techniques that are applied to the IM. These techniques are a fundamental part of the methodology, as they make the verification of real-life PLC programs, which usually have huge state spaces, possible. The methodology has been applied to real-life PLC programs developed at CERN. These experimental results have demonstrated the usability of this methodology by control engineers with no experience in formal methods.