REASONING ABOUT PROGRAMMABLE LOGIC CONTROLLERS
Natalia Olegovna Garanina, Igor Sergeevich Anureev, Vladimir Evgenievich Zyubin, Andrei Rozov, Tatiana Liakh, Sergei Gorlatch · System Informatics · 2020
We address the formal verification of the control software of critical systems, i.e., ensuring the absence of design errors in a system with respect to requirements. Control systems are usually based on industrial controllers, also known as Programmable Logic Controllers (PLCs). A specific feature of a PLC is a scan cycle: 1) the inputs are read, 2) the PLC states change, and 3) the outputs are written. Therefore, in order to formally verify PLC, e.g., by model checking, it is necessary to reason both in terms of state transitions within a cycle and in terms of larger state transitions according to the scan-cyclic semantics. We develop a formalization of PLC as a hyperprocess transition system and an LTL-based temporal logic cycle-LTL for reasoning about PLC.