maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2023-4-308-339LDUGESmais-1823Research ArticleTheory of SoftwareLTL-спецификация для разработки и верификации управляющих программLTL-specification for development and verification of control programshttps://orcid.org/0009-0000-6893-6137НейзовМаксим ВячеславовичNeyzovMaxim V.neyzov.max@gmail.comhttps://orcid.org/0000-0003-0500-306XКузьминЕгор ВладимировичKuzminEgor V.kuzmin@uniyar.ac.ruИнститут автоматики и электрометрии СО РАНРоссияInstitute of Automation and Electrometry SB RASRussian FederationЯрославский государственный университет им. П.Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian Federation202311122023304308339Copyright © Нейзов М.В., Кузьмин Е.В., 20232023Нейзов М.В., Кузьмин Е.В.Neyzov M.V., Kuzmin E.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1823

Настоящая работа продолжает цикл статей по разработке и верификации управляющих программ на основе LTL"=спецификации. Суть подхода заключается в описании поведения программ с помощью формул линейной темпоральной логики LTL специального вида. Полученная LTL"=спецификация может быть непосредственно верифицирована с помощью инструмента проверки модели. Далее по LTL"=спецификации однозначно строится код программы на императивном языке программирования. Перевод спецификации в программу осуществляется по шаблону. Новизна работы состоит в предложении двух LTL"=спецификаций нового вида — декларативной и императивной, а также в более строгом формальном обосновании данного подхода к разработке и верификации программ. Выполнен переход на более современный инструмент верификации конечных и бесконечных систем — nuXmv. Предлагается описывать поведение управляющих программ в декларативном стиле. Для этого предназначена декларативная LTL"=спецификация, которая задаёт размеченную систему переходов как формальную модель поведения программы. Данный способ описания поведения является достаточно выразительным — доказана теорема о Тьюринг"=полноте декларативной LTL"=спецификации. Далее для построения кода программы на императивном языке декларативная LTL"=спецификация преобразуется в эквивалентную императивную LTL"=спецификацию. Доказана теорема об эквивалентности, которая гарантирует, что обе спецификации задают одно и то же поведение. Императивная LTL"=спецификация транслируется в императивный код программы по представленному шаблону. Декларативная LTL"=спецификация, которая подвергается верификации, и построенная по ней управляющая программа гарантированно задают одно и то же поведение в виде соответствующей системы переходов. Таким образом, при верификации используется модель, адекватная реальному поведению управляющей программы.

This work continues the series of articles on development and verification of control programs based on the LTL-specification. The essence of the approach is to describe the behavior of programs using formulas of linear temporal logic LTL of a special form. The developed LTL-specification can be directly verified by using a model checking tool. Next, according to the LTL-specification, the program code in the imperative programming language is unambiguously built. The translation of the specification into the program is carried out using a template. The novelty of the work consists in the proposal of two LTL-specifications of a new form — declarative and imperative, as well as in a more strict formal justification for this approach to program development and verification. A transition has been made to a more modern verification tool for finite and infinite systems — nuXmv. It is proposed to describe the behavior of control programs in a declarative style. For this purpose, a declarative LTL-specification is intended, which defines a labelled transition system as a formal model of program behavior. This method of describing behavior is quite expressive — the theorem on the Turing completeness of the declarative LTL-specification is proved. Next, to construct program code in an imperative language, the declarative LTL-specification is converted into an equivalent imperative LTL-specification. An equivalence theorem is proved, which guarantees that both specifications specify the same behavior. The imperative LTL-specification is translated into imperative program code according to the presented template. The declarative LTL-specification, which is subject to verification, and the control program built on it are guaranteed to specify the same behavior in the form of a corresponding transition system. Thus, during verification, a model is used that is adequate to the real behavior of the control program.

управляющее программное обеспечениедекларативная LTL-спецификацияимперативная LTL-спецификацияполная система переходовпсевдополная система переходовсчётчиковая машина Минскогопроверка моделиверификатор nuXmvПЛК-программаязык STcontrol softwaredeclarative LTL-specificationimperative LTL-specificationmodel checkingcomplete transition systempseudo-complete transition systemMinsky counter machinenuXmv verifierPLC programST languageГосзадание ИАиЭ СО РАН, проект № 122031600173-8; ЯрГУ (проект VIP-016).State task IAaE SB RAS, project No. 122031600173-8; Yaroslavl State University (project VIP-016).ReferencesS. 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.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.E. A. Lee and S. A. Seshia, Introduction to Embedded Systems -- A Cyber-Physical Systems Approach, 2nd ed. MIT Press, 2017.E. A. Lee and S. A. Seshia, Introduction to Embedded Systems -- A Cyber-Physical Systems Approach, 2nd ed. MIT Press, 2017.E. A. Parr, Programmable Controllers. An Engineer’s Guide, 3rd ed. Newnes, 2003.E. A. Parr, Programmable Controllers. An Engineer’s Guide, 3rd ed. Newnes, 2003.V. N. Lifshic and L. E. Sadovskii, “Algebraic Models of Computing Machines,” UMN, vol. 27, no. 3(165), pp. 79–125, 1972.V. N. Lifshic and L. E. Sadovskii, “Algebraic Models of Computing Machines,” UMN, vol. 27, no. 3(165), pp. 79–125, 1972.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.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.N. I. Polikarpova and A. A. Shalyto, Automata-Based Programming, 2nd ed. Spb.: Piter, 2011.N. I. Polikarpova and A. A. Shalyto, Automata-Based Programming, 2nd ed. Spb.: Piter, 2011.D. Harel and A. Pnueli, “On the Development of Reactive Systems,” in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477–498.D. Harel and A. Pnueli, “On the Development of Reactive Systems,” in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477–498.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.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.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.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.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.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.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.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.E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed. Springer Publishing Company, Incorporated, 2018.E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed. Springer Publishing Company, Incorporated, 2018.Y. G. Karpov, Model checking. Verification of Parallel and Distributed Program Systems. BHV-Peterburg, 2010.Y. G. Karpov, Model checking. Verification of Parallel and Distributed Program Systems. BHV-Peterburg, 2010.S. Velder, M. Lukin, A. Shalyto, and B. Yaminov, Verification of Automata-Based Programs. Spb Science, 2011.S. Velder, M. Lukin, A. Shalyto, and B. Yaminov, Verification of Automata-Based Programs. Spb Science, 2011.E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002.E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.E. V. Kuzmin, “LTL-Specification of Counter Machines,” Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104–119, 2021.E. V. Kuzmin, “LTL-Specification of Counter Machines,” Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104–119, 2021.E. V. Kuzmin, “LTL-Specification of Bounded Counter Machines,” Modeling and Analysis of Information Systems, vol. 29, no. 1, pp. 44–59, 2022.E. V. Kuzmin, “LTL-Specification of Bounded Counter Machines,” Modeling and Analysis of Information Systems, vol. 29, no. 1, pp. 44–59, 2022.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.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.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.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.“IEC 61131-3:2013 Programmable controllers -- Part 3: Programming languages.” [Online]. Available: https://webstore.iec.ch/publication/4552.“IEC 61131-3:2013 Programmable controllers -- Part 3: Programming languages.” [Online]. Available: https://webstore.iec.ch/publication/4552.A. Pnueli, “The Temporal Logic of Programs,” in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), 1977, pp. 46–57.A. Pnueli, “The Temporal Logic of Programs,” in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), 1977, pp. 46–57.M. L. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, 1967.M. L. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, 1967.R. Schroeppel, “A Two Counter Machine Cannot Calculate $2^N$,” Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972.R. Schroeppel, “A Two Counter Machine Cannot Calculate $2^N$,” Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972.E. V. Kuzmin, Counter Machines. Yaroslavl State University, 2010.E. V. Kuzmin, Counter Machines. Yaroslavl State University, 2010.

The authors declare that there are no conflicts of interest present.