maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2024-2-120-141mais-1849Research ArticleTheory of SoftwareВерификация декларативной LTL-спецификации поведения управляющих программVerification of declarative LTL-specification of control programs behaviorhttps://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 Federation202413062024312120141Copyright © Нейзов М.В., Кузьмин Е.В., 20242024Нейзов М.В., Кузьмин Е.В.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/1849

Статья продолжает цикл трудов по разработке и верификации управляющих программ на основе LTL-спецификаций специального вида. Ранее была предложена декларативная LTL-спецификация, позволяющая описывать поведение управляющих программ и выполнять построение по ней программного кода на императивном языке ST для программируемых логических контроллеров. Данная LTL-спецификация может быть непосредственно верифицирована на предмет соответствия заданным темпоральным свойствам методом проверки модели (model checking) с помощью инструмента символьной верификации nuXmv. При этом не требуется переводить LTL-формулы спецификации в другой формализм — SMV-спецификацию (код на входном языке инструмента nuXmv). Цель настоящей работы состоит в исследовании альтернативных способов представления модели поведения программы, соответствующей декларативной LTL-спецификации, при её верификации в рамках инструментального средства nuXmv. В статье выполняются преобразования декларативной LTL-спецификации в различные SMV-спецификации с сопутствующими изменениями постановки задачи верификации, что приводит к значительному снижению временных затрат при проверке темпоральных свойств с использованием инструмента nuXmv. Ускорение верификации обусловлено сокращением пространства состояний проверяемой модели. Полученные в результате предложенных преобразований SMV-спецификации задают одинаковые или бисимуляционно эквивалентные системы переходов, обеспечивая неизменность результатов верификации при замене одной SMV-спецификации на другую.

The article continues the series of works on development and verification of control programs based on LTL-specifications of a special type. Previously, it was proposed a declarative LTL-specification, which allows describing the behavior of control programs and building program code based on it in the imperative ST-language for programmable logic controllers. The LTL-specification can be directly verified for compliance with specified temporal properties by the model checking method using the nuXmv symbolic verification tool. In general, it is not required translating LTL-formulas of the specification into another formalism — an SMV-specification (code in the input language of the nuXmv tool). The purpose of this work is to explore alternative ways of representing a program behavior model corresponding to the declarative LTL-specification during its verification within the nuXmv tool. In the article, we transform the declarative LTL-specification into various SMV-specifications with accompanying changes of formulation of the verification problem, what leads to a significant reduction in time costs when checking temporal properties by using the nuXmv tool. The acceleration of verification is due to the reduction of the state space of a model being verified. The SMV-specifications obtained as a result of the proposed transformations specify identical or bisimulationally equivalent transition systems. It is ensuring the same verification results when replacing one SMV-specification with another.

управляющее программное обеспечениеПЛК-программадекларативная LTL-спецификацияимперативная LTL-спецификацияполная система переходовпсевдополная система переходовпространство состоянийпроверка моделиверификатор nuXmvSMV-спецификациябисимуляционная эквивалентностьбисимуляцияcontrol softwarePLC programdeclarative LTL-specificationimperative LTL-specificationcomplete transition systempseudo-complete transition systemstate spacemodel checkingnuXmv verifierSMV-specificationbisimulation equivalencebisimulationГосзадание ИАиЭ СО РАН, проект No 122031600173-8; ЯрГУ (проект VIP-016).State task IAaE SB RAS, project No. 122031600173-8; Yaroslavl State University (project VIP-016).ReferencesD. J. Smith and K. G. L. Simpson, The Safety Critical Systems Handbook, 5th ed. Butterworth-Heinemann, 2020.D. J. Smith and K. G. L. Simpson, The Safety Critical Systems Handbook, 5th ed. Butterworth-Heinemann, 2020.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, doi: 10.1109/TCAD.2008.923410.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, doi: 10.1109/TCAD.2008.923410.S. Oks et al., “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook,” Information Systems Frontiers, 2022, doi: 10.1007/s10796-022-10252-x.S. Oks et al., “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook,” Information 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.M. V. Neyzov and E. V. Kuzmin, “LTL-specification for Development and Verification of Control Programs,” Modeling and Analysis of Information Systems, vol. 30, no. 4, pp. 308–339, 2023, doi: 10.18255/1818-1015-2023-4-308-339.M. V. Neyzov and E. V. Kuzmin, “LTL-specification for Development and Verification of Control Programs,” Modeling and Analysis of Information Systems, vol. 30, no. 4, pp. 308–339, 2023, doi: 10.18255/1818-1015-2023-4-308-339.D. Harel and A. Pnueli, “On the Development of Reactive Systems,” in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477–498, doi: 10.1007/978-3-642-82453-1_17.D. Harel and A. Pnueli, “On the Development of Reactive Systems,” in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477–498, doi: 10.1007/978-3-642-82453-1_17.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, doi: 10.1007/BFb0027047.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, doi: 10.1007/BFb0027047.“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.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.E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002, p. 416.E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002, p. 416.D. Beyer and A. Podelski, “Software model checking: 20 years and beyond,” in Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, Springer, 2022, pp. 554–582.D. Beyer and A. Podelski, “Software model checking: 20 years and beyond,” in Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, Springer, 2022, pp. 554–582.“nuXmv Home.” [Online]. Available: https://nuxmv.fbk.eu/.“nuXmv Home.” [Online]. Available: https://nuxmv.fbk.eu/.“IEC 61131-1:2003 Programmable controllers -- Part 1: General information.” [Online]. Available: https://webstore.iec.ch/publication/4550.“IEC 61131-1:2003 Programmable controllers -- Part 1: General information.” [Online]. Available: https://webstore.iec.ch/publication/4550.B. Alpern and F. B. Schneider, “Defining Liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181–185, 1985, doi: 10.1016/0020-0190(85)90056-0.B. Alpern and F. B. Schneider, “Defining Liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181–185, 1985, doi: 10.1016/0020-0190(85)90056-0.Z. Manna and A. Pnueli, “A Hierarchy of Temporal Properties,” in Proceedings of the ninth annual ACM symposium on Principles of distributed computing, 1990, pp. 377–410, doi: 10.1145/93385.93442.Z. Manna and A. Pnueli, “A Hierarchy of Temporal Properties,” in Proceedings of the ninth annual ACM symposium on Principles of distributed computing, 1990, pp. 377–410, doi: 10.1145/93385.93442.“Spot Home.” [Online]. Available: https://spot.lre.epita.fr/.“Spot Home.” [Online]. Available: https://spot.lre.epita.fr/.“nuXmv User Manual.” [Online]. Available: https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf.“nuXmv User Manual.” [Online]. Available: https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf.D. Park, “Concurrency and Automata on Infinite Sequences,” in Theoretical Computer Science: 5th GI-Conference Karlsruhe, 1981, vol. 104, pp. 167–183, doi: 10.1007/BFb0017309.D. Park, “Concurrency and Automata on Infinite Sequences,” in Theoretical Computer Science: 5th GI-Conference Karlsruhe, 1981, vol. 104, pp. 167–183, doi: 10.1007/BFb0017309.

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