A Temporal Logic for Programmable Logic Controllers

— We investigate the formal verification of the control software of critical systems, i.e., the verification of the compliance of the designed system with the requirements. The most important class of control software consists of programs for programmable logic controllers (PLCs). A special feature of PLC programs is the scan cycle: (1) the inputs are read, (2) the PLC states are changed, and (3) the outputs are written. Therefore, for formal verification of PLC programs, for example by model checking, it is necessary to be able to describe transition systems that take into account this specificity. In addition, it is required to determine properties of systems that model PLC programs, both with respect to transitions within the cycle as well as larger transitions in accordance with the semantics of the scan cycle. In this paper, we introduce a formal model of a PLC program as a system of hyperprocess transitions and the temporal cycle-LTL logic based on the LTL logic for formalizing the properties of the PLC. A special feature of the cycle-LTL logic is the ability to consider the properties of control systems in two ways: as an impact of the environment on the control system and as an impact of the control system on the environment. We define modifications of the standard temporal operators of the LTL logic for each of these cases, as well as for properties inside the scan cycle. Examples of requirements defined in our logic are considered. The translation of cycle-LTL formulas into LTL formulas is described and its correctness is proved. Thereby we demonstrate the possibility of reducing the problem of verification by model checking for the requirements defined in the cycle-LTL logic to the model checking problem for the requirements defined in the standard LTL logic.