Темпоральная логика для программируемых логических контроллеров

Мы исследуем формальную верификацию управляющего программного обеспечения критических систем, т. е. проверку соответствия функционирования проектируемой системы предъявленным требованиям. Важнейший класс управляющего программного обеспечения составляют программы для программируемых логических контроллеров (ПЛК). Особенностью программ ПЛК является цикл управления: 1) считываются входы, 2) изменяются состояния ПЛК и 3) записываются выходы. Поэтому для формальной верификации программ ПЛК нужна возможность описывать учитывающие эту специфику системы переходов, а также определять свойства систем, моделирующих программы ПЛК, как относительно переходов внутри цикла, так и относительно более крупных переходов в соответствии с семантикой цикла управления. Мы предлагаем формальную модель программы ПЛК как систему переходов гиперпроцессов и темпоральную логику cycle-LTL для формализации свойств ПЛК. Особенностью логики cycle-LTL является возможность рассматривать свойства систем управления двояким образом: воздействие окружения на систему управления и воздействие системы управления на окружение. Мы определяем модификации стандартных темпоральных операторов логики LTL для каждого из этих случаев, а также для свойств внутри цикла управления. Рассмотрены примеры требований, определенных в нашей логике. Описана трансляция формул cycle-LTL в формулы LTL и показана её корректность. Доказана возможность сведения задачи верификации методом проверки моделей для требований, определенных в логике cycle-LTL, к задаче верификации требований, определенных в стандартной логике LTL.

1. I. Anureev, «Operacionnaya semantica annotirovannih Reflex programm», Modelirovanie i analiz informacionnyh sistem, vol. 26, no. 6, pp. 181-192, 2019.

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

3. E. Brinksma and A. Mader, «Verification and Optimization of a PLC Control Schedule», in SPIN 2000 - SPIN Model Checking and Software Verification, ser. LNCS, vol. 1885, Springer, 2000, pp. 73-92.

4. V. Gourcuff, O. de Smet, and J.-M. Faure, «Improving large-sized PLC programs verification using abstractions», IFAC Proceedings Volumes, vol. 41, no. 2, pp. 5101-5106, 2008.

5. A. Mader, «A Classification of PLC Models and Applications», in Discrete Event Systems, ser. SECS, vol. 569, Springer, 2000, pp. 239-246.

6. H. Wan, G. Chen, X. Song, and M. Gu, «Formalization and Verification of PLC Timers in Coq», in Proc. of 33rd Annual IEEE International Computer Software and Applications Conference, IEEE, 2009, pp. 315-323.

7. J. Yoo, S. Cha, and E. Jee, «A Verification Framework for FBD Based Software in Nuclear Power Plants», in Proc. of 15th Asia-Pacific Software Engineering Conference, IEEE, 2008, pp. 385-392.

8. D. Bulavskij, V. Zyubin, N. Karlson, V. Krivoruchko, and V. Mironov, «An Automated Control System for a Silicon Single-Crystal Growth Furnace», Optoelectronics, instrumentation, and data processing, vol. 32, no. 2, pp. 25-30, 1996.

9. P. G. Kovadlo, A. Lubkov, A. Bevzov, and et al., «Automation system for the large solar vacuum telescope», Optoelectronics, Instrumentation and Data processing, vol. 52, pp. 187-195, 2016.

10. A. Gupta, V. Kahlon, S. Qadeer, and T. Touili, Handbook of Model Checking. Springer International Publishing, 2018, ch. 18. Model Checking Concurrent Programs, pp. 573-577.

11. E. M. Clarke, T. A. Henzinger, and H. Veith, Handbook of Model Checking. Springer International Publishing, 2018, ch. 1. Introduction to Model Checking, pp. 1-13.

12. H. Dierks, «PLC-automata: A new class of implementable real-time automata», in International AMAST Workshop on Aspects of Real-Time Systems and Concurrent and Distributed Software, vol. 1231, Springer, 1997, pp. 111-125.

13. T. Ovatman, «An overview of model checking practices on verification of PLC software», Software & Systems Modeling, vol. 4, no. 15, pp. 937-960, 2016.

14. E. Kuzmin, D. Ryabukhin, and V. A. Sokolov, «On the expressiveness of the approach to constructing PLC-programs by LTL-specification», Automatic Control and Computer Sciences, vol. 7, no. 50, pp. 510-519, 2016.

15. M. Zhang, «Towards automated safety vetting of PLC code in real-world plants», in IEEE Symposium on Security and Privacy, IEEE, 2019, pp. 522-538.

16. A. Rajeev and T. Henzinger, «A really temporal logic», Journal of the ACM, vol. 41, no. 1, pp. 181-203, 1994.

17. J. Xiong, «A User-Friendly Verification Approach for IEC 61131-3 PLC Programs», Electronics, vol. 4, no. 9, 2020.

18. B. Beckert, «Regression verification for programmable logic controller software», in International Conference on Formal Engineering Methods, vol. 9407, Springer, 2015.

19. O. Ljungkrantz, «An empirical study of control logic specifications for programmable logic controllers», Empirical Software Engineering, vol. 3, no. 19, pp. 655-677, 2014.

20. O. Ljungkrantz, K. Akesson, M. Fabian, and C. Yuan, «A formal specification language for PLC-based control logic», in 8th IEEE International Conference on Industrial Informatics, IEEE, 2010, pp. 1067-1072.

21. O. Maler and D. Nickovic, «Monitoring temporal properties of continuous signals», Formal Techniques, Modellingand Analysis of Timed and Fault-Tolerant Systems, pp. 152-166, 2004.

22. N. Garanina, I. Anureev, V. Zyubin, A. Rozov, T. Liakh, and S. Gorlatch, «Reasoning about Programmable Logic Controllers», System Informatics, vol. 17, pp. 33-42, 2020.

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