Software model checking has recently started to be applied in the verification of programmable logic controller (PLC) programs. It works efficiently when the number of input variables is limited, their interaction is small and, thus, the number of states the program can reach is not large. As observed in the large code base of the CERN industrial PLC applications, this is usually not the case: it thus leads to the well-known state-space explosion problem, making it impossible to perform model checking. One of the main reasons that causes state-space explosion is the inclusion of numeric variables due to the wide range of values they can take. In this paper, we propose an approach to discretize PLC input numeric variables (modelled as non-deterministic). This discretization is complemented with a set of transformations on the control-flow automaton that models the PLC program so that no extra behaviours are added. This approach is then quantitatively evaluated with a set of empirical tests using the PLC model checking framework PLCverif and three different state-of-the-art model checkers (CBMC, nuXmv, and Theta), showing beneficial results for BDD-based model checkers.

The complexity and quality needs of PLC-based control system software have largely increased. Formal specification methods can help to cope with these needs. Besides formal verification, another benefit of a formal specification language is the possibility to provide automatic generation of the final source code. This paper overviews PLCspecif, our formal specification language for PLC programs and presents a code generation method for the language. The result of the code generator is a Structured Text (ST) code that not only corresponds to the formal semantics of the specification, but is also configurable, readable, understandable, and follows development conventions and standards. The code generation method shows that PLC-specif is applicable and well-adapted to the PLC domain.

Programmable logic controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the correctness of safety-critical software, but is still underused in industry due to the complexity of building and managing formal models of real applications. In this paper, we propose a general methodology to perform automated model checking of complex properties expressed in temporal logics [e.g., computation tree logic (CTL) and linear temporal logic (LTL)] on PLC programs. This methodology is based on an intermediate model (IM) meant to transform PLC programs written in various standard languages [structured text (ST), sequential function chart (SFC), etc.] to different modeling languages of verification tools. We present the syntax and semantics of the IM, and the transformation rules of the ST and SFC languages to the nuXmv model checker passing through the IM. Finally, two real cases studies of the European Organization for Nuclear Research (CERN) PLC programs, written mainly in the ST language, are presented to illustrate and validate the proposed approach.

Testing of critical PLC (Programmable Logic Controller) programs remains a challenging task for control system engineers as it can rarely be automated. This paper proposes a model based approach which uses the BIP (Behavior, Interactions and Priorities) framework to perform automated testing of PLC programs developed with the UNICOS (UNified Industrial COntrol System) framework. This paper defines the translation procedure and rules from UNICOS to BIP which can be fully automated in order to hide the complexity of the underlying model from the control engineers. The approach is illustrated and validated through the study of a water treatment process.