maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2024-1-6-31mais-1836Research ArticleTheory of SoftwareШаблоны требований в дедуктивной верификации poST-программRequirement patterns in deductive verification of poST Programshttps://orcid.org/0000-0001-7675-8449ЧерненкоИван МихайловичChernenkoIvan M.cheriv98@mail.ruhttps://orcid.org/0000-0001-9574-128XАнуреевИгорь СергеевичAnureevIgor S.anureev@gmail.comhttps://orcid.org/0000-0001-9734-3808ГаранинаНаталья ОлеговнаGaraninaNatalia O.garanina@iis.nsk.suИнститут автоматики и электрометрии СО РАНРоссияInstitute of Automation and Electrometry SB RASRussian Federation202428032024311631Copyright © Черненко И.М., Ануреев И.С., Гаранина Н.О., 20242024Черненко И.М., Ануреев И.С., Гаранина Н.О.Chernenko I.M., Anureev I.S., Garanina N.O.Данная работа распространяется под лицензией 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/1836

Процесс-ориентированное программирование — один из подходов к разработке управляющего программного обеспечения. Процесс-ориентированная программа определяется как последовательность процессов. Каждый процесс представляется набором именованных состояний, содержащих программный код, которые задают логику поведения процесса. Выполнение программы заключается в последовательном исполнении этих процессов в их текущих состояниях на каждой итерации цикла управления. Процессы могут взаимодействовать через изменение состояний друг друга и через разделяемые переменные. Статья является развитием метода классификации темпоральных требований к процесс-ориентированным программам с целью упростить и автоматизировать дедуктивную верификацию таких программ. Метод состоит из следующих шагов. На первом шаге требования формализуются на специализированном языке DV-TRL, варианте типизированной логики предикатов первого порядка с набором интерпретированных типов и предикатных и функциональных символов, позволяющем отражать специфические понятия систем управления в процесс-ориентированной парадигме. На втором шаге формализованные требования разбиваются на классы, каждый из которых определяется шаблоном — параметрической формулой языка DV-TRL, причем условия корректности, порождаемые для процесс-ориентированных программ относительно требований, удовлетворяющих одному шаблону, имеют одну и ту же схему доказательства. На третьем шаге разрабатываются соответствующие схемы доказательства. В статье мы сначала даём краткое введение в язык poST, процесс-ориентированное расширение языка ST стандарта МЭК 61131-3. Далее определяется язык DV-TRL. Мы также приводим коллекцию требований на естественном языке для нескольких систем управления. Затем мы определяем шаблоны, позволяющие полностью покрыть все требования этой коллекции и для каждого из шаблонов приводим пример формализованного требования из коллекции и описываем схему доказательства условий корректности для этого шаблона. Статистика распределения требований из коллекции по шаблонам выявляет наиболее востребованные шаблоны. Мы также провели анализ связанных работ.

Process-oriented programming is one of the approaches to developing control software. A process-oriented program is defined as a sequence of processes. Each process is represented by a set of named states containing program code that define the logic of the process's behavior. Program execution is sequential execution of each of these processes in their current states at every iteration of the control cycle. Processes can interact through changing each other's states and shared variables. The paper expands a method for classifying temporal requirements for process-oriented programs in order to simplify and automate the deductive verification of such programs. The method consists of the following steps. At the first step, the requirements are formalized in a specialized language DV-TRL, a variant of typed first-order predicate logic with a set of interpreted types and predicate and functional symbols, that reflect specific concepts of control systems in a process-oriented paradigm. At the second step, the formalized requirements are divided into classes, each of which is defined by a pattern — a parametric formula of the DV-TRL language. The correctness conditions generated for process-oriented programs regarding requirements satisfying the same pattern have the same proof scheme. At the third step, appropriate proof schemes are developed. In our paper, we first give a brief introduction to the poST language, a process-oriented extension to the ST language of the IEC 61131-3 standard. Next, the DV-TRL language is defined. We also provide a collection of natural language requirements for several control systems. Then we define patterns that fully cover all the requirements of this collection. For each of these patterns we give an example of a formalized requirement from the collection and describe a scheme for proving the correctness conditions for this pattern. Statistics on the distribution of requirements from the collection across patterns reveals the most popular patterns. We also analyzed related works.

дедуктивная верификациятемпоральные требованияшаблоны требованийуправляющее программное обеспечениепроцесс-ориентированное программированиеdeductive verificationtemporal requirementsrequirement patternscontrol softwareprocess-oriented programmingГосзадание ИАиЭ СО РАН, проект No 122031600173-8.State task IAaE SB RAS, project No. 122031600173-8.ReferencesV. 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.I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, and S. Gorlatch, “Two-step deductive verification of control software using Reflex,” in International Andrei Ershov Memorial Conference on Perspectives of System Informatics, 2019, pp. 50–63, doi: 10.1007/978-3-030-37487-7_5.I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, and S. Gorlatch, “Two-step deductive verification of control software using Reflex,” in International Andrei Ershov Memorial Conference on Perspectives of System Informatics, 2019, pp. 50–63, doi: 10.1007/978-3-030-37487-7_5.V. E. Zyubin, T. V. Liakh, and A. S. Rozov, “Reflex language: a practical notation for cyber-physical systems,” System Informatics, no. 12, pp. 85–104, 2018.V. E. Zyubin, T. V. Liakh, and A. S. Rozov, “Reflex language: a practical notation for cyber-physical systems,” System Informatics, no. 12, pp. 85–104, 2018.C. Paulin-Mohring, “Introduction to the Coq proof-assistant for practical software verification,” in LASER Summer School on Software Engineering, Springer, 2011, pp. 45–95.C. Paulin-Mohring, “Introduction to the Coq proof-assistant for practical software verification,” in LASER Summer School on Software Engineering, Springer, 2011, pp. 45–95.I. Chernenko, I. S. Anureev, N. O. Garanina, and S. M. Staroletov, “A Temporal Requirements Language for Deductive Verification of Process-Oriented Programs,” in IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 657–662, doi: 10.1109/EDM55285.2022.9855145.I. Chernenko, I. S. Anureev, N. O. Garanina, and S. M. Staroletov, “A Temporal Requirements Language for Deductive Verification of Process-Oriented Programs,” in IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 657–662, doi: 10.1109/EDM55285.2022.9855145.I. M. Chernenko and I. S. Anureev, “Development of Verification Condition Generator for Process-Oriented Programs in poST Language,” in IEEE 24th International Conference of Young Professionals in Electron Devices and Materials (EDM), 2023, pp. 1760–1765, doi: 10.1109/EDM58354.2023.10225217.I. M. Chernenko and I. S. Anureev, “Development of Verification Condition Generator for Process-Oriented Programs in poST Language,” in IEEE 24th International Conference of Young Professionals in Electron Devices and Materials (EDM), 2023, pp. 1760–1765, doi: 10.1109/EDM58354.2023.10225217.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, 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, 2022, doi: 10.1109/ACCESS.2022.3157601.IEC, “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.L. C. Paulson, T. Nipkow, and M. Wenzel, “From LCF to Isabelle/HOL,” Formal Aspects of Computing, vol. 31, pp. 675–698, 2019.L. C. Paulson, T. Nipkow, and M. Wenzel, “From LCF to Isabelle/HOL,” Formal Aspects of Computing, vol. 31, pp. 675–698, 2019.I. M. Chernenko, “Requirements patterns in deductive verification of process-oriented programs and examples of their use,” System Informatics, no. 22, 2023, doi: 10.31144/si.2307-6410.2023.n22.p11-20.I. M. Chernenko, “Requirements patterns in deductive verification of process-oriented programs and examples of their use,” System Informatics, no. 22, 2023, doi: 10.31144/si.2307-6410.2023.n22.p11-20.J.-C. Filli^atre, “Deductive software verification,” International Journal on Software Tools for Technology Transfer, vol. 13, pp. 397–403, 2011, doi: 10.1007/s10009-011-0211-0.J.-C. Filli^atre, “Deductive software verification,” International Journal on Software Tools for Technology Transfer, vol. 13, pp. 397–403, 2011, doi: 10.1007/s10009-011-0211-0.D. Gurov, P. Herber, and I. Schaefer, “Automated Verification of Embedded Control Software,” in International Symposium on Leveraging Applications of Formal Methods, 2020, pp. 235–239, doi: 10.1007/978-3-030-61467-6_15.D. Gurov, P. Herber, and I. Schaefer, “Automated Verification of Embedded Control Software,” in International Symposium on Leveraging Applications of Formal Methods, 2020, pp. 235–239, doi: 10.1007/978-3-030-61467-6_15.D. Gurov, C. Lidstr"om, M. Nyberg, and J. Westman, “Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report,” in Critical Systems: Formal Methods and Automated Verification, 2017, pp. 3–18.D. Gurov, C. Lidstr"om, M. Nyberg, and J. Westman, “Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report,” in Critical Systems: Formal Methods and Automated Verification, 2017, pp. 3–18.C. B. Lourencco, D. Cousineau, F. Faissole, C. March'e, D. Mentr'e, and H. Inoue, “Automated Verification of Temporal Properties of Ladder Programs,” in Formal Methods for Industrial Critical Systems, 2021, pp. 21–38.C. B. Lourencco, D. Cousineau, F. Faissole, C. March'e, D. Mentr'e, and H. Inoue, “Automated Verification of Temporal Properties of Ladder Programs,” in Formal Methods for Industrial Critical Systems, 2021, pp. 21–38.Z. Manna et al., “An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems,” in Tool Support for System Specification, Development and Verification, 1999, pp. 174–188, doi: 10.1007/978-3-7091-6355-9_13.Z. Manna et al., “An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems,” in Tool Support for System Specification, Development and Verification, 1999, pp. 174–188, doi: 10.1007/978-3-7091-6355-9_13.S. Yamane, “Deductive verification method of real-time safety properties for embedded assembly programs,” Electronics, vol. 8, no. 10, p. 1163, 2019.S. Yamane, “Deductive verification method of real-time safety properties for embedded assembly programs,” Electronics, vol. 8, no. 10, p. 1163, 2019.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.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.Z. Manna and A. Pnueli, The temporal logic of reactive and concurrent systems: Specification. Springer New York, NY, 1992.Z. Manna and A. Pnueli, The temporal logic of reactive and concurrent systems: Specification. Springer New York, NY, 1992.M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, “Patterns in Property Specifications for Finite-State Verification,” in Proceedings of the 21st International Conference on Software Engineering, 1999, pp. 411–420, doi: 10.1145/302405.302672.M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, “Patterns in Property Specifications for Finite-State Verification,” in Proceedings of the 21st International Conference on Software Engineering, 1999, pp. 411–420, doi: 10.1145/302405.302672.L. Grunske, “Specification patterns for probabilistic quality properties,” in Proceedings of the 30th international conference on Software engineering, 2008, pp. 31–40, doi: 10.1145/1368088.1368094.L. Grunske, “Specification patterns for probabilistic quality properties,” in Proceedings of the 30th international conference on Software engineering, 2008, pp. 31–40, doi: 10.1145/1368088.1368094.S. Konrad and B. H. C. Cheng, “Real-Time Specification Patterns,” in Proceedings of the 27th International Conference on Software Engineering, 2005, pp. 372–381, doi: 10.1145/1062455.1062526.S. Konrad and B. H. C. Cheng, “Real-Time Specification Patterns,” in Proceedings of the 27th International Conference on Software Engineering, 2005, pp. 372–381, doi: 10.1145/1062455.1062526.A. Mekki, M. Ghazel, and A. Toguy'eni, “Assisting Temporal Requirement Specification,” Computer Technology and Application, vol. 3, no. 1, pp. 47–55, 2012.A. Mekki, M. Ghazel, and A. Toguy'eni, “Assisting Temporal Requirement Specification,” Computer Technology and Application, vol. 3, no. 1, pp. 47–55, 2012.O. Mondragon, A. Q. Gates, and S. Roach, “Prospec: Support for elicitation and formal specification of software properties,” Electronic Notes in Theoretical Computer Science, vol. 89, no. 2, pp. 67–88, 2003, doi: 10.1016/S1571-0661(04)81043-0.O. Mondragon, A. Q. Gates, and S. Roach, “Prospec: Support for elicitation and formal specification of software properties,” Electronic Notes in Theoretical Computer Science, vol. 89, no. 2, pp. 67–88, 2003, doi: 10.1016/S1571-0661(04)81043-0.S. Salamah, A. Gates, and V. Kreinovich, “Validated Templates for Specification of Complex LTL Formulas,” Journal of Systems and Software, vol. 85, no. 8, pp. 1915–1929, 2012, doi: 10.1016/j.jss.2012.02.041.S. Salamah, A. Gates, and V. Kreinovich, “Validated Templates for Specification of Complex LTL Formulas,” Journal of Systems and Software, vol. 85, no. 8, pp. 1915–1929, 2012, doi: 10.1016/j.jss.2012.02.041.D. Bianculli, C. Ghezzi, C. Pautasso, and P. Senti, “Specification patterns from research to industry: A case study in service-based applications,” in 34th International Conference on Software Engineering (ICSE), 2012, pp. 968–976, doi: 10.1109/ICSE.2012.6227125.D. Bianculli, C. Ghezzi, C. Pautasso, and P. Senti, “Specification patterns from research to industry: A case study in service-based applications,” in 34th International Conference on Software Engineering (ICSE), 2012, pp. 968–976, doi: 10.1109/ICSE.2012.6227125.S. Halle, R. Villemaire, and O. Cherkaoui, “Specifying and Validating Data-Aware Temporal Web Service Properties,” IEEE Transactions on Software Engineering, vol. 35, no. 5, pp. 669–683, 2009, doi: 10.1109/TSE.2009.29.S. Halle, R. Villemaire, and O. Cherkaoui, “Specifying and Validating Data-Aware Temporal Web Service Properties,” IEEE Transactions on Software Engineering, vol. 35, no. 5, pp. 669–683, 2009, doi: 10.1109/TSE.2009.29.A. Post, I. Menzel, and A. Podelski, “Applying Restricted English Grammar on Automotive Requirements—Does it Work? A Case Study,” in Requirements Engineering: Foundation for Software Quality, 2011, pp. 166–180.A. Post, I. Menzel, and A. Podelski, “Applying Restricted English Grammar on Automotive Requirements—Does it Work? A Case Study,” in Requirements Engineering: Foundation for Software Quality, 2011, pp. 166–180.M. Autili, L. Grunske, M. Lumpe, P. Pelliccione, and A. Tang, “Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar,” IEEE Transactions on Software Engineering, vol. 41, no. 7, pp. 620–638, 2015, doi: 10.1109/TSE.2015.2398877.M. Autili, L. Grunske, M. Lumpe, P. Pelliccione, and A. Tang, “Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar,” IEEE Transactions on Software Engineering, vol. 41, no. 7, pp. 620–638, 2015, doi: 10.1109/TSE.2015.2398877.A. N. Getmanova, N. O. Garanina, S. M. Staroletov, V. E. Zyubin, and I. S. Anureev, “Semantic Classification of Event Driven Temporal Logic Requirements,” in IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 663–668, doi: 10.1109/EDM55285.2022.9855053.A. N. Getmanova, N. O. Garanina, S. M. Staroletov, V. E. Zyubin, and I. S. Anureev, “Semantic Classification of Event Driven Temporal Logic Requirements,” in IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 663–668, doi: 10.1109/EDM55285.2022.9855053.V. Zyubin, I. Anureev, N. Garanina, S. Staroletov, A. Rozov, and T. Liakh, “Event-Driven Temporal Logic Pattern for Control Software Requirements Specification,” in International Conference on Fundamentals of Software Engineering, 2021, pp. 92–107.V. Zyubin, I. Anureev, N. Garanina, S. Staroletov, A. Rozov, and T. Liakh, “Event-Driven Temporal Logic Pattern for Control Software Requirements Specification,” in International Conference on Fundamentals of Software Engineering, 2021, pp. 92–107.

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