Рассуждения о программируемых логических контроллерах

Reasoning about Programmable Logic Controllers

Article's language
English
Abstract
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.
DOI
10.31144/si.2307-6410.2020.n17.p33-42
UDK
Pages
33-42
File
Number