Bringing Automated Model Checking to PLC Program Development - A CERN Case Study

Verification of critical software is a high priority but a challenging task for industrial control systems. Model checking appears to be an appropriate approach for this purpose. However, this technique is not widely used in industry yet, due to some obstacles. The main obstacles encountered when trying to apply formal verification techniques at industrial installations are the difficulty of creating models out of PLC programs and defining formally the specification requirements. In addition, models produced out of real-life programs have a huge state space, thus preventing the verification due to performance issues. Our work at CERN (European Organization for Nuclear Research) focuses on developing efficient automatic verification methods for industrial critical installations based on PLC (Programmable Logic Controller) control systems. In this paper, we present a tool generating automatically formal models out of PLC code. The tool implements a general methodology which can support several input languages, like the PLC programming languages defined in the IEC 61131 standard, as well as the model formalisms of different model checker tools. The tool supports the three main stages of model checking: system modelization, requirement formalization and counterexample analysis. In addition, a verification case study of a PLC program, written in Structured Text (ST) language implemented at CERN is described. The paper shows that the verification process is automatized and supported by the proposed tool, thus its difficulty is completely hidden for the control engineer.