RUS  ENG
Full version
JOURNALS // Modelirovanie i Analiz Informatsionnykh Sistem // Archive

Model. Anal. Inform. Sist., 2020 Volume 27, Number 4, Pages 412–427 (Mi mais725)

Theory of computing

Temporal logic for programmable logic controllers

N. O. Garaninaa, I. S. Anureeva, V. E. Zyubinb, S. M. Staroletovc, T. V. Liakhb, A. S. Rozovb, S. P. Gorlatchd

a A. P. Ershov Institute of Informatics Systems (IIS), Siberian Branch of the Russian Academy of Sciences, 6, Acad. Lavrentjev ave., Novosibirsk 630090, Russia
b Institute of Automation and Electrometry SB RAS, 1 Academician Koptyug ave., Novosibirsk 630090, Russia
c Polzunov Altai State Technical University, 46 Lenina ave., Barnaul 656038, Russia
d University of Munster, 2 Schlossplatz, Munster 48149, Germany

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 describe the transition system taking into account this specificity and reason both in terms of state transitions within a cycle and in terms of larger state transitions according to the scan-cyclic semantics. We propose a formal PLC model as a hyperprocess transition system and temporal cycle-LTL logic based on LTL logic for formulating PLC property. A feature of the cycle-LTL logic is the possibility of viewing the scan cycle in two ways: as the effect of the environment (in particular, the control object) on the control system and as the effect of the control system on the environment. For both cases we introduce modified LTL temporal operators. We also define special modified LTL temporal operators to specify inside properties of scan cycles. We describe the translation of formulas of cycle-LTL into formulas of LTL, and prove its correctness. This implies the possibility ofmodel checking requirements expressed in logic cycle-LTL, by using well-known model checking tools with LTL as specification logic, e.g., Spin. We give the illustrative examples of requirements expressed in the cycle-LTL logic.

Keywords: formal verification, temporal logics, transition systems, programmable logic controllers (PLC).

UDC: 004.822, 681.51

MSC: 68N30

Received: 12.11.2020
Revised: 12.12.2020
Accepted: 16.12.2020

DOI: 10.18255/1818-1015-2020-4-412-427



Bibliographic databases:


© Steklov Math. Inst. of RAS, 2024