Temporal logic for programmable logic controllers

N. O. Garanina ; I. S. Anureev ; V. E. Zyubin ; S. M. Staroletov ; T. V. Liakh ; A. S. Rozov ; S. P. Gorlatch

Modelirovanie i analiz informacionnyh sistem, Tome 27 (2020) no. 4, pp. 412-427.

Résumé

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.

Détail

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

Bibliographie

[1] I. Anureev, “Operacionnaya semantica annotirovannih Re-ex programm”, Modelirovanie i analiz informacionnyh sistem, 26:6 (2019), 181–192 | MR

[2] I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, “Towards safe cyber-physical systems: the Reflex language and its transformational semantics”, IEEE International Siberian Conference on Control and Communications, IEEE, 2019, 18–20

[3] E. Brinksma, A. Mader, “Verification and Optimization of a PLC Control Schedule”, SPIN Model Checking and Software Verification, SPIN 2000, LNCS, 1885, Springer, 2000, 73–92 | Zbl

[4] V. Gourcuff, O. de Smet, J. M. Faure, “Improving large-sized PLC programs verification using abstractions”, IFAC Proceedings Volumes, 41:2 (2008), 5101–5106 | DOI

[5] A. Mader, “A Classification of PLC Models and Applications”, Discrete Event Systems, SECS, 569, Springer, 2000, 239–246 | MR

[6] H. Wan, G. Chen, X. Song, M. Gu, “Formalization and Verification of PLC Timers in Coq”, Proc. of 33rd Annual IEEE International Computer Software and Applications Conference, IEEE, 2009, 315–323

[7] J. Yoo, S. Cha, E. Jee, “A Verification Framework for FBD Based Software in Nuclear Power Plants”, Proc. of 15th Asia-Pacific Software Engineering Conference, IEEE, 2008, 385–392

[8] D. Bulavskij, V. Zyubin, N. Karlson, V. Krivoruchko, V. Mironov, “An Automated Control System for a Silicon Single-Crystal Growth Furnace”, Optoelectronics, instrumentation, and data processing, 32:2 (1996), 25–30

[9] P. G. Kovadlo, A. Lubkov, A. Bevzov, and et al, “Automation system for the large solar vacuum telescope”, Optoelectronics, Instrumentation and Data processing, 52 (2016), 187–195 | DOI

[10] A. Gupta, V. Kahlon, S. Qadeer, T. Touili, “Model Checking Concurrent Programs”, Handbook of Model Checking, ch. 18, Springer International Publishing, 2018, 573–577 | DOI | MR

[11] E. M. Clarke, T. A. Henzinger, H. Veith, “Introduction to Model Checking”, Handbook of Model Checking, ch. 1, Springer International Publishing, 2018, 1–13 | MR

[12] H. Dierks, “PLC-automata: A new class of implementable real-time automata”, International AMAST Workshop on Aspects of Real-Time Systems and Concurrent and Distributed Software, Lecture Notes in Computer Science, 1231, Springer, 1997, 111–125 | DOI

[13] T. Ovatman, “An overview of model checking practices on verification of PLC Software”, Software Systems Modeling, 4:15 (2016), 937–960 | DOI

[14] E. Kuzmin, D. Ryabukhin, V. A. Sokolov, “On the expressiveness of the approach to constructing PLC-programs by LTL-specification”, Automatic Control and Computer Sciences, 7:50 (2016), 510–519 | DOI | MR

[15] M. Zhang, “Towards automated safety vetting of PLC code in real-world plants”, IEEE Symposium on Security and Privacy, IEEE, 2019, 522–538

[16] A. Rajeev, T. Henzinger, “A really temporal logic”, Journal of the ACM, 41:1 (1994), 181–203 | DOI | MR

[17] J. Xiong, “A User-Friendly Verification Approach for IEC 61131-3 PLC Programs”, Electronics, 4:9 (2020)

[18] B. Beckert, “Regression verification for programmable logic controller software”, International Conference on Formal Engineering Methods, 9407, Lecture Notes in Computer Science, Springer, 2015 | MR

[19] O. Ljungkrantz, “An empirical study of control logic specifications for programmable logic controllers”, Empirical Software Engineering, 3:19 (2014), 655–677 | DOI

[20] O. Ljungkrantz, K. Akesson, M. Fabian, C. Yuan, “A formal specification language for PLC-based control logic”, 8th IEEE International Conference on Industrial Informatics, IEEE, 2010, 1067–1072

[21] O. Maler, D. Nickovic, “Monitoring temporal properties of continuous signals”, Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, 2004, 152–166 | DOI | Zbl

[22] N. Garanina, I. Anureev, V. Zyubin, A. Rozov, T. Liakh, S. Gorlatch, “Reasoning about Programmable Logic Controllers”, System Informatics, 17 (2020), 33–42

[23] G. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003