LTL-спецификация для разработки и верификации управляющих программ
https://doi.org/10.18255/1818-1015-2023-4-308-339
EDN: LDUGES
Аннотация
Настоящая работа продолжает цикл статей по разработке и верификации управляющих программ на основе LTL"=спецификации. Суть подхода заключается в описании поведения программ с помощью формул линейной темпоральной логики LTL специального вида. Полученная LTL"=спецификация может быть непосредственно верифицирована с помощью инструмента проверки модели. Далее по LTL"=спецификации однозначно строится код программы на императивном языке программирования. Перевод спецификации в программу осуществляется по шаблону. Новизна работы состоит в предложении двух LTL"=спецификаций нового вида — декларативной и императивной, а также в более строгом формальном обосновании данного подхода к разработке и верификации программ. Выполнен переход на более современный инструмент верификации конечных и бесконечных систем — nuXmv. Предлагается описывать поведение управляющих программ в декларативном стиле. Для этого предназначена декларативная LTL"=спецификация, которая задаёт размеченную систему переходов как формальную модель поведения программы. Данный способ описания поведения является достаточно выразительным — доказана теорема о Тьюринг"=полноте декларативной LTL"=спецификации. Далее для построения кода программы на императивном языке декларативная LTL"=спецификация преобразуется в эквивалентную императивную LTL"=спецификацию. Доказана теорема об эквивалентности, которая гарантирует, что обе спецификации задают одно и то же поведение. Императивная LTL"=спецификация транслируется в императивный код программы по представленному шаблону. Декларативная LTL"=спецификация, которая подвергается верификации, и построенная по ней управляющая программа гарантированно задают одно и то же поведение в виде соответствующей системы переходов. Таким образом, при верификации используется модель, адекватная реальному поведению управляющей программы.
Ключевые слова
MSC2020: 68N30
Об авторах
Максим Вячеславович НейзовРоссия
Егор Владимирович Кузьмин
Россия
Список литературы
1. S. Oks, M. Jalowski, M. Lechner, and others, “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook,” Inf. Systems Frontiers, 2022, doi: 10.1007/s10796-022-10252-x.
2. E. A. Lee and S. A. Seshia, Introduction to Embedded Systems -- A Cyber-Physical Systems Approach, 2nd ed. MIT Press, 2017.
3. E. A. Parr, Programmable Controllers. An Engineer’s Guide, 3rd ed. Newnes, 2003.
4. V. N. Lifshic and L. E. Sadovskii, “Algebraic Models of Computing Machines,” UMN, vol. 27, no. 3(165), pp. 79–125, 1972.
5. K.-Y. Cai, T. Y. Chen, and T. H. Tse, “Towards Research on Software Cybernetics,” in Proceedings of 7th IEEE International on High-assurance Systems Engineering (HASE 2002), 2002, pp. 240–241.
6. N. I. Polikarpova and A. A. Shalyto, Automata-Based Programming, 2nd ed. Spb.: Piter, 2011.
7. D. Harel and A. Pnueli, “On the Development of Reactive Systems,” in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477–498.
8. A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends,” in Current Trends in Concurrency, 1986, vol. 224, pp. 510–584.
9. A. Maurya and D. Kumar, “Reliability of safety‐critical systems: A state‐of‐the‐art review,” Quality and Reliability Engineering International, vol. 36, no. 7, pp. 2547–2568, 2020.
10. N. Rajabli, F. Flammini, R. Nardone, and V. Vittorini, “Software Verification and Validation of Safe Autonomous Cars: A Systematic Literature Review,” in IEEE Access, 2021, vol. 9, pp. 4797–4819.
11. V. D'Silva, D. Kroening, and G. Weissenbacher, “A Survey of Automated Techniques for Formal Software Verification,” in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008, vol. 27, no. 7, pp. 1165–1178.
12. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed. Springer Publishing Company, Incorporated, 2018.
13. Y. G. Karpov, Model checking. Verification of Parallel and Distributed Program Systems. BHV-Peterburg, 2010.
14. S. Velder, M. Lukin, A. Shalyto, and B. Yaminov, Verification of Automata-Based Programs. Spb Science, 2011.
15. E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002.
16. E. V. Kuzmin and V. A. Sokolov, “Modeling, Specification and Construction of PLC-programs,” Modeling and Analysis of Information Systems, vol. 20, no. 2, pp. 104–120, 2013.
17. E. V. Kuzmin and V. A. Sokolov, “Modeling, Specification and Construction of PLC-programs,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 554–563, 2014.
18. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC-programs by LTL-specification,” Modeling and Analysis of Information Systems, vol. 20, no. 4, pp. 5–22, 2013.
19. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC-Programs by LTL-Specification,” Automatic Control and Computer Sciences, vol. 49, no. 7, pp. 453–465, 2015.
20. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC LD-programs by LTL-specification,” Modeling and Analysis of Information Systems, vol. 20, no. 6, pp. 78–94, 2013.
21. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC LD Programs by the LTL Specification,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 424–436, 2014.
22. D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, “Construction of PLC IL-programs by LTL-specification,” Modeling and Analysis of Information Systems, vol. 21, no. 2, pp. 26–38, 2014.
23. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors,” Modeling and Analysis of Information Systems, vol. 21, no. 4, pp. 75–90, 2014.
24. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 602–614, 2014.
25. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification,” Modeling and Analysis of Information Systems, vol. 22, no. 4, pp. 507–520, 2015.
26. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification,” Automatic Control and Computer Sciences, vol. 50, pp. 510–519, 2016.
27. D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, “Construction of CFC-programs by LTL-specification,” Modeling and Analysis of Information Systems, vol. 23, no. 2, pp. 173–184, 2016.
28. D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, “Construction of CFC-Programs by LTL-Specification,” Automatic Control and Computer Sciences, vol. 51, pp. 567–575, 2017.
29. E. V. Kuzmin, “LTL-Specification of Counter Machines,” Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104–119, 2021.
30. E. V. Kuzmin, “LTL-Specification of Bounded Counter Machines,” Modeling and Analysis of Information Systems, vol. 29, no. 1, pp. 44–59, 2022.
31. E. V. Kuzmin and V. A. Sokolov, “On Construction and Verification of PLC-Programs,” Modeling and Analysis of Information Systems, vol. 19, no. 4, pp. 25–36, 2012.
32. E. V. Kuzmin and V. A. Sokolov, “On Construction and Verification of PLC Programs,” Automatic Control and Computer Sciences, vol. 47, no. 7, pp. 443–451, 2013.
33. “IEC 61131-3:2013 Programmable controllers -- Part 3: Programming languages.” [Online]. Available: https://webstore.iec.ch/publication/4552.
34. A. Pnueli, “The Temporal Logic of Programs,” in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), 1977, pp. 46–57.
35. M. L. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, 1967.
36. R. Schroeppel, “A Two Counter Machine Cannot Calculate $2^N$,” Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972.
37. E. V. Kuzmin, Counter Machines. Yaroslavl State University, 2010.
Рецензия
Для цитирования:
Нейзов М.В., Кузьмин Е.В. LTL-спецификация для разработки и верификации управляющих программ. Моделирование и анализ информационных систем. 2023;30(4):308-339. https://doi.org/10.18255/1818-1015-2023-4-308-339. EDN: LDUGES
For citation:
Neyzov M.V., Kuzmin E.V. LTL-specification for development and verification of control programs. Modeling and Analysis of Information Systems. 2023;30(4):308-339. (In Russ.) https://doi.org/10.18255/1818-1015-2023-4-308-339. EDN: LDUGES