maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2024-1-32-53mais-1837Research ArticleTheory of SoftwareВерификация моделей программ на процесс-ориентированном расширении языка Structured Text стандарта IEC 61131-3Model checking programs in process-oriented IEC 61131-3 Structured Texthttps://orcid.org/0000-0001-9734-3808ГаранинаНаталья ОлеговнаGaraninaNatalia O.garanina@iis.nsk.suhttps://orcid.org/0000-0001-5183-9736СтаролетовСергей МихайловичStaroletovSergey M.serg_soft@mail.ruhttps://orcid.org/0000-0002-8198-3197ЗюбинВладимир ЕвгеньевичZyubinVladimir E.zyubin@iae.nsk.suhttps://orcid.org/0000-0001-9574-128XАнуреевИгорь СергеевичAnureevIgor S.anureev@iis.nsk.suИнститут автоматики и электрометрии СО РАНРоссияInstitute of Automation and Electrometry SB RASRussian Federation2024280320243113253Copyright © Гаранина Н.О., Старолетов С.М., Зюбин В.Е., Ануреев И.С., 20242024Гаранина Н.О., Старолетов С.М., Зюбин В.Е., Ануреев И.С.Garanina N.O., Staroletov S.M., Zyubin V.E., Anureev I.S.Данная работа распространяется под лицензией 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/1837

Процессно-ориентированное программирование — это парадигма, основанная на концепции процесса. Каждый процесс представляет собой конечный автомат. Эта парадигма предназначена для разработчиков ПЛК (программируемых логических контроллеров) для написания программного обеспечения с поддержкой Индустрии 4.0. Язык poST является многообещающим процессно-ориентированным расширением языка структурированного текста (ST) МЭК 61131-3, предназначенным для обеспечения концептуальной согласованности исходного кода ПЛК с технологическим описанием управляемого процесса. Этот язык сочетает в себе преимущества программирования на основе конечных автоматов со стандартным синтаксисом языка ST. Мы предлагаем трансформационную семантику poST, заданную правилами перевода операторов языка poST в Promela — входной язык средства проверки моделей SPIN. Следуя этим правилам, наш транслятор, основанный на технологии Xtext, строит модель Promela для программы poST. Основной вклад нашей статьи — это трансформационная семантика poST и метод автоматической генерации кода Promela из программ управления PoST. Полученная модель Promela готова к проверке с помощью системы верификации моделей SPIN на соответствие требованиям к исходной программе poST, выраженных в терминах линейной темпоральной логики LTL. В статье мы приводим обзор связанных работ, а также краткое описание языков poST и Promela. Представленные далее правила трансляции poST в Promela покрывают операторы потока управления, конструкции создания процессов и управления их состояниями, а также операторы для таймаутов. Отдельно определены сервисные процессы для моделирования внешней среды и задания высокоуровневых LTL спецификаций. Затем мы останавливаемся на основных идеях реализации транслятора poST в Promela, и далее иллюстрируем наш подход на примере системы управления потреблением и производством электроэнергии, в том числе из возобновляемых источников.

The process-oriented programming is a paradigm based on the process concept where each process is a concurrent finite state machine inside. The paradigm is intended for PLC (programmable logic controllers) developers to write Industry 4.0-enabled software. The poST language is a promising process-oriented extension of the IEC 61131-3 Structured Text (ST) language designed to provide a conceptual consistency of the PLC source code with technological description of the process under control. This language combines the advantages of FSM-based programming with the standard syntax of the ST language. We propose transformational semantics of poST providing rules for translation of poST language statements to Promela — the input language of the SPIN model checker. Following these semantic rules, our Xtext-based translator outputs a Promela model for the poST program. Our contribution is the poST transformational semantics and the method for automatic generation of the Promela code from poST control programs. The resulting Promela program is ready to be verified with SPIN model checker against linear temporal logic requirements to the source poST program. In the paper we provide an overview of related work, as well as a brief description of the poST and Promela languages. Further, the Promela poST translation rules cover control flow statements, process creation and state management constructs, and timeout management. Then we define service processes for modeling the external environment and managing high-level LTL specifications. Then we present the main ideas of implementing the translator poST to Promela. We also illustrate our approach using the example of a system for managing electricity consumption and production, including renewable sources.

управляющее программное обеспечениепроверка моделейпроцесс-ориентированное программированиеLTLSPINStructured Textcontrol softwaremodel checkingprocess-oriented programmingLTLSPINStructured TextГосзадание ИАиЭ СО РАН, проект No 122031600173-8, госзадание No АААА-А19-119120290056-0.State task IAaE SB RAS, project No. 122031600173-8, state task No. AAAA-A19-119120290056-0.ReferencesIEC, “IEC 61131-3: 2013 Programmable controllers-Part 3: programming languages.” 2013, [Online]. Available: https://webstore.iec.ch/publication/4552.IEC, “IEC 61131-3: 2013 Programmable controllers-Part 3: programming languages.” 2013, [Online]. Available: https://webstore.iec.ch/publication/4552.T. M. Antonsen, PLC Controls with Structured Text (ST), V3: IEC 61131-3 and best practice ST programming. Books on Demand, 2020.T. M. Antonsen, PLC Controls with Structured Text (ST), V3: IEC 61131-3 and best practice ST programming. Books on Demand, 2020.V. E. Zyubin, “Hyper-automaton: a Model of Control Algorithms,” in 2007 Siberian Conference on Control and Communications, 2007, pp. 51–57, doi: 10.1109/SIBCON.2007.371297.V. E. Zyubin, “Hyper-automaton: a Model of Control Algorithms,” in 2007 Siberian Conference on Control and Communications, 2007, pp. 51–57, doi: 10.1109/SIBCON.2007.371297.V. E. Zyubin, A. S. Rozov, I. S. Anureev, N. O. Garanina, and V. Vyatkin, “poST: A Process-Oriented Extension of the IEC 61131-3 Structured Text Language,” IEEE Access, vol. 10, pp. 35238–35250, 2022, doi: 10.1109/ACCESS.2022.3157601.V. E. Zyubin, A. S. Rozov, I. S. Anureev, N. O. Garanina, and V. Vyatkin, “poST: A Process-Oriented Extension of the IEC 61131-3 Structured Text Language,” IEEE Access, vol. 10, pp. 35238–35250, 2022, doi: 10.1109/ACCESS.2022.3157601.G. J. Holzmann, The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts, 2003.G. J. Holzmann, The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts, 2003.L. Schneider and D. Schultes, “Evaluating Swift-to-Kotlin and Kotlin-to-Swift transpilers,” in Proceedings of the 9th IEEE/ACM International Conference on Mobile Software Engineering and Systems, 2022, pp. 102–106.L. Schneider and D. Schultes, “Evaluating Swift-to-Kotlin and Kotlin-to-Swift transpilers,” in Proceedings of the 9th IEEE/ACM International Conference on Mobile Software Engineering and Systems, 2022, pp. 102–106.E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of model checking. Springer, 2018.E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of model checking. Springer, 2018.T. Ovatman, “An overview of model checking practices on verification of PLC software,” Software & Systems Modeling, vol. 4, no. 15, pp. 937–960, 2016.T. Ovatman, “An overview of model checking practices on verification of PLC software,” Software & Systems Modeling, vol. 4, no. 15, pp. 937–960, 2016.E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 8, no. 2, pp. 244–263, 1986.E. M. Clarke, E. A. Emerson, and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 8, no. 2, pp. 244–263, 1986.C. A. R. Hoare, “Communicating sequential processes,” Communications of the ACM, vol. 21, no. 8, pp. 666–677, 1978.C. A. R. Hoare, “Communicating sequential processes,” Communications of the ACM, vol. 21, no. 8, pp. 666–677, 1978.N. O. Garanina, S. M. Staroletov, V. E. Zyubin, and I. S. Anureev, “Model Checking Programs in Process-Oriented IEC 61131-3 Structured Text,” System Informatics, vol. 22, pp. 21–30, 2023, doi: 10.31144/si.2307-6410.2023.n22.p21-30.N. O. Garanina, S. M. Staroletov, V. E. Zyubin, and I. S. Anureev, “Model Checking Programs in Process-Oriented IEC 61131-3 Structured Text,” System Informatics, vol. 22, pp. 21–30, 2023, doi: 10.31144/si.2307-6410.2023.n22.p21-30.M. Weissmann, S. Bedenk, C. Buckl, and A. Knoll, “Model checking industrial robot systems,” in Model Checking Software. SPIN 2011, 2011, pp. 161–176.M. Weissmann, S. Bedenk, C. Buckl, and A. Knoll, “Model checking industrial robot systems,” in Model Checking Software. SPIN 2011, 2011, pp. 161–176.P. Cousot, “Abstract interpretation,” ACM Computing Surveys, vol. 28, no. 2, pp. 324–328, 1996, doi: 10.1145/234528.234740.P. Cousot, “Abstract interpretation,” ACM Computing Surveys, vol. 28, no. 2, pp. 324–328, 1996, doi: 10.1145/234528.234740.S. Leue and G. Holzmann, “v-Promela: A visual, object-oriented language for SPIN,” in Proceedings of the 2nd IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, 1999, pp. 14–23.S. Leue and G. Holzmann, “v-Promela: A visual, object-oriented language for SPIN,” in Proceedings of the 2nd IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, 1999, pp. 14–23.M. Benerecetti et al., “From dynamic state machines to Promela,” in International Symposium on Model Checking Software, 2019, pp. 56–73.M. Benerecetti et al., “From dynamic state machines to Promela,” in International Symposium on Model Checking Software, 2019, pp. 56–73.B. Lion, S. Chouali, and F. Arbab, “Compiling Protocols to Promela and Verifying their LTL Properties,” in Proceedings of 21st MODELS Workshops, 2018, pp. 31–39.B. Lion, S. Chouali, and F. Arbab, “Compiling Protocols to Promela and Verifying their LTL Properties,” in Proceedings of 21st MODELS Workshops, 2018, pp. 31–39.A. Klarl, “From Helena ensemble specifications to Promela verification models,” in Model Checking Software. SPIN 2015, 2015, pp. 39–45.A. Klarl, “From Helena ensemble specifications to Promela verification models,” in Model Checking Software. SPIN 2015, 2015, pp. 39–45.N. Dilley and J. Lange, “Bounded verification of message-passing concurrency in Go using Promela and SPIN,” in Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, 2010, pp. 34–45, doi: 10.4204/EPTCS.314.4.N. Dilley and J. Lange, “Bounded verification of message-passing concurrency in Go using Promela and SPIN,” in Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, 2010, pp. 34–45, doi: 10.4204/EPTCS.314.4.N. Dilley and J. Lange, “Automated Verification of Go Programs via Bounded Model Checking,” in 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2021, pp. 1016–1027.N. Dilley and J. Lange, “Automated Verification of Go Programs via Bounded Model Checking,” in 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2021, pp. 1016–1027.E. Brinksma, A. Mader, and A. Fehnker, “Verification and optimization of a PLC control schedule,” International Journal on Software Tools for Technology Transfer, vol. 4, no. 1, pp. 21–33, 2002, doi: 10.1007/s10009-002-0079-0.E. Brinksma, A. Mader, and A. Fehnker, “Verification and optimization of a PLC control schedule,” International Journal on Software Tools for Technology Transfer, vol. 4, no. 1, pp. 21–33, 2002, doi: 10.1007/s10009-002-0079-0.M. Xia, M. Sun, G. Luo, and X. Zhao, “Design and implementation of automatic verification for PLC systems,” in IEEE 12th International Conference on Cognitive Informatics and Cognitive Computing, 2013, pp. 374–379.M. Xia, M. Sun, G. Luo, and X. Zhao, “Design and implementation of automatic verification for PLC systems,” in IEEE 12th International Conference on Cognitive Informatics and Cognitive Computing, 2013, pp. 374–379.P. Liu, G. Luo, M. Xia, and M. He, “Automatic verification of event-driven control programs: a case study,” in The Fourth International Workshop on Advanced Computational Intelligence, 2011, pp. 249–256.P. Liu, G. Luo, M. Xia, and M. He, “Automatic verification of event-driven control programs: a case study,” in The Fourth International Workshop on Advanced Computational Intelligence, 2011, pp. 249–256.T. Liakh, R. Sorokin, D. Akifev, S. Patil, and V. Vyatkin, “Formal model of IEC 61499 execution trace in FBME IDE,” in IEEE 20th International Conference on Industrial Informatics (INDIN), 2022, pp. 588–593.T. Liakh, R. Sorokin, D. Akifev, S. Patil, and V. Vyatkin, “Formal model of IEC 61499 execution trace in FBME IDE,” in IEEE 20th International Conference on Industrial Informatics (INDIN), 2022, pp. 588–593.V. Shatrov and V. Vyatkin, “Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV,” in IEEE 19th International Conference on Industrial Informatics (INDIN), 2021, pp. 1–6.V. Shatrov and V. Vyatkin, “Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV,” in IEEE 19th International Conference on Industrial Informatics (INDIN), 2021, pp. 1–6.A. Ebnenasir, “Formalizing Ladder Logic Programs and Timing Charts for Fault Impact Analysis and Verification of Fault Tolerance,” Michigan Technological University, CS-TR-23-01, Jan. 2023.A. Ebnenasir, “Formalizing Ladder Logic Programs and Timing Charts for Fault Impact Analysis and Verification of Fault Tolerance,” Michigan Technological University, CS-TR-23-01, Jan. 2023.A. Mader, “A Classification of PLC Models and Applications,” Discrete Event Systems: Analysis and Control, vol. 569, pp. 239–246, 2000.A. Mader, “A Classification of PLC Models and Applications,” Discrete Event Systems: Analysis and Control, vol. 569, pp. 239–246, 2000.N. O. Garanina et al., “A Temporal Logic for Programmable Logic Controllers,” Automatic Control and Computer Sciences, vol. 55, no. 7, pp. 763–775, 2021, doi: 10.3103/S0146411621070038.N. O. Garanina et al., “A Temporal Logic for Programmable Logic Controllers,” Automatic Control and Computer Sciences, vol. 55, no. 7, pp. 763–775, 2021, doi: 10.3103/S0146411621070038.M. Eysholdt and H. Behrens, “Xtext: implement your language faster than the quick and dirty way,” in Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion, 2010, pp. 307–309.M. Eysholdt and H. Behrens, “Xtext: implement your language faster than the quick and dirty way,” in Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion, 2010, pp. 307–309.D. Steinberg, F. Budinsky, E. Merks, and M. Paternostro, EMF: Eclipse modeling framework. Pearson Education, 2008.D. Steinberg, F. Budinsky, E. Merks, and M. Paternostro, EMF: Eclipse modeling framework. Pearson Education, 2008.“ANTLR: A predicated-LL(k) parser generator,” Software: Practice and Experience, vol. 25, no. 7, pp. 789–810, 1995.“ANTLR: A predicated-LL(k) parser generator,” Software: Practice and Experience, vol. 25, no. 7, pp. 789–810, 1995.D. Lepri, E. 'Abrah'am, and P. C. "Olveczky, “Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories,” Science of Computer Programming, vol. 99, pp. 128–192, 2015.D. Lepri, E. 'Abrah'am, and P. C. "Olveczky, “Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories,” Science of Computer Programming, vol. 99, pp. 128–192, 2015.N. Rhodes and J. McKeehan, Palm OS programming: the developer's guide. O'Reilly Media, Inc., 2002.N. Rhodes and J. McKeehan, Palm OS programming: the developer's guide. O'Reilly Media, Inc., 2002.R. Miles and K. Hamilton, Learning UML 2.0: a pragmatic introduction to UML. O'Reilly Media, Inc., 2006.R. Miles and K. Hamilton, Learning UML 2.0: a pragmatic introduction to UML. O'Reilly Media, Inc., 2006.

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