Conformance checking for programmable logic controller programs and specifications

Verification of industrial control systems' software is an important task, as the cost of failure in these systems is typically high. Formal verification methods can complement the currently used testing techniques, especially if requirements are formally specified. Behavioural specifications can be used to perform conformance checking against the implementation. However, the typical conformance relations are often more sensitive to differences than the controlled processes in case of many control systems, resulting in counterexamples during verification that are considered as false positives in practice. To overcome this issue, we introduce conformance relations adapted to control systems based on programmable logic controllers (PLCs) with different levels of permissibility. The relations can be selected by the control engineers, depending on the required compliance levels. Defining the new relations and a model checking-based method to check them makes conformance checking a powerful tool for the verification of industrial control systems.

I. Introduction

Industrial control systems (ICS) often rely on programmable logic controllers (PLCs). PLCs are robust industrial computers performing various control tasks. The typical execution schema of a PLC is cyclic: the user-defined program is executed in an infinite loop (so-called PLC or scan cycle). At the beginning of the loop the physical inputs are read, then the program is executed using these stable input values. At the end of each loop the physical outputs are assigned which are then stable until the end of the next cycle. The duration of the scan cycle may vary in most of the PLCs.