maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2024-4-384-425mais-1896Research ArticleTheory of ComputingПодход к автоматизации дедуктивной верификации процесс-ориентированных программ, основанный на шаблонах: шаблоны, леммы и алгоритмыPattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithmshttps://orcid.org/0000-0001-7675-8449ЧерненкоИван МихайловичChernenkoIvan M.cheriv98@mail.ruhttps://orcid.org/0000-0001-9574-128XАнуреевИгорь СергеевичAnureevIgor S.anureev@gmail.comИнститут автоматики и электрометрии СО РАНРоссияInstitute of Automation and Electrometry SB RASRussian Federation202413122024314384425Copyright © Черненко И.М., Ануреев И.С., 20242024Черненко И.М., Ануреев И.С.Chernenko I.M., 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/1896

Процесс-ориентированное программирование — это подход к разработке управляющего программного обеспечения, в котором программа определяется как набор взаимодействующих процессов. PoST — это процесс-ориентированный язык, который является расширением языка ST из стандарта IEC 61131-3. В области разработки управляющего программного обеспечения формальная верификация играет важную роль вследствие необходимости обеспечения высокой надежности такого программного обеспечения. Дедуктивная верификация — это метод формальной верификации, в котором программа и требования к ней представляются в виде логических формул, а для доказательства того, что программа удовлетворяет требованиям, используется логический вывод. К управляющему программному обеспечению часто предъявляются темпоральные требования. Мы формализуем такие требования для процесс-ориентированных программ в виде инвариантов цикла управления. Но инварианты цикла управления, представляющие требования, недостаточны для доказательства корректности программы. Поэтому мы добавляем дополнительные инварианты, которые содержат вспомогательную информацию. В данной статье рассматривается проблема автоматизации дедуктивной верификации процесс-ориентированных программ. Предложен подход, в котором темпоральные требования задаются с использованием шаблонов требований, которые строятся из базовых шаблонов. Для каждого шаблона требований определяются соответствующий шаблон дополнительных инвариантов и леммы. В статье описан предлагаемый подход и схемы базовых и производных шаблонов требований. Рассмотрены схемы базовых шаблонов дополнительных инвариантов, схемы лемм, определяемых для базовых шаблонов, а также набор базовых шаблонов и леммы для них. Определены схема производных шаблонов дополнительных инвариантов и схемы лемм, определяемых для производных шаблонов. Представлены алгоритмы построения производных шаблонов дополнительных инвариантов и лемм для них, а также метод доказательства этих лемм. Рассмотрены схемы доказательства условий корректности. Предложенный подход демонстрируется на примере. Также проведен анализ связанных работ.

Process-oriented programming is an approach to developing control software in which a program is defined as a set of interacting processes. PoST is a process-oriented language, which is an extension of the ST language from the IEC 61131-3 standard. In the field of control software development, formal verification plays an important role due to the need to ensure high reliability of such software. Deductive verification is a formal verification method in which a program and its requirements are represented as logical formulas, and logical inference is used to prove that the program satisfies the requirements. Control software often has temporal requirements. We formalize such requirements for process-oriented programs as control loop invariants. However, control loop invariants that represent requirements are not sufficient to prove the correctness of the program. Therefore, we add extra invariants containing auxiliary information. This paper considers the problem of automating deductive verification of process-oriented programs. An approach is proposed in which temporal requirements are specified using requirement patterns which are constructed from basic patterns. For each requirement pattern, a corresponding extra invariant pattern and lemmas are defined. In this paper, the proposed approach and schemes of basic and derived requirement patterns are described. The schemes of basic extra invariant patterns, schemes of lemmas defined for basic patterns, and a set of basic patterns and lemmas for them are considered. The scheme of derived extra invariant patterns and schemes of lemmas defined for derived patterns are defined. The algorithms for constructing derived extra invariant patterns and lemmas for them, as well as methods for proving these lemmas are presented. The schemes of proving verification conditions are considered. The proposed approach is demonstrated with an example. The analysis of related works has also been carried out.

дедуктивная верификациятемпоральные требованияшаблон требованийинвариант циклауправляющее программное обеспечениепроцесс-ориентированное программированиеdeductive verificationtemporal requirementsrequirement patternloop invariantcontrol 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 Proceedings of the 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 Proceedings of the 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.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.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.R. H"ahnle and M. Huisman, “Deductive software verification: from pen-and-paper proofs to industrial tools,” Computing and Software Science: State of the Art and Perspectives, pp. 345–373, 2019.R. H"ahnle and M. Huisman, “Deductive software verification: from pen-and-paper proofs to industrial tools,” Computing and Software Science: State of the Art and Perspectives, pp. 345–373, 2019.I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, and S. Gorlatch, “Two-Step Deductive Verification of Control Software Using Reflex,” in 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 Perspectives of System Informatics, 2019, pp. 50–63, doi: 10.1007/978-3-030-37487-7_5.I. Chernenko, I. S. Anureev, N. O. Garanina, and S. M. Staroletov, “A temporal requirements language for deductive verification of process-oriented programs,” in Proceedings of the IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 657–662.I. Chernenko, I. S. Anureev, N. O. Garanina, and S. M. Staroletov, “A temporal requirements language for deductive verification of process-oriented programs,” in Proceedings of the IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 657–662.I. M. Chernenko, “Requirements patterns in deductive verification of process-oriented programs and examples of their use,” System Informatics, no. 22, pp. 11–20, 2023.I. M. Chernenko, “Requirements patterns in deductive verification of process-oriented programs and examples of their use,” System Informatics, no. 22, pp. 11–20, 2023.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.E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of model checking, vol. 10. Springer, 2018.E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of model checking, vol. 10. Springer, 2018.D. Matichuk, T. Murray, and M. Wenzel, “Eisbach: A Proof Method Language for Isabelle,” Journal of Automated Reasoning, vol. 56, no. 3, pp. 261–282, 2016, doi: 10.1007/s10817-015-9360-2.D. Matichuk, T. Murray, and M. Wenzel, “Eisbach: A Proof Method Language for Isabelle,” Journal of Automated Reasoning, vol. 56, no. 3, pp. 261–282, 2016, doi: 10.1007/s10817-015-9360-2.I. M. Chernenko, I. S. Anureev, and N. O. Garanina, “Requirement patterns in deductive verification of poST programs,” Modeling and Analysis of Information Systems, vol. 31, no. 1, pp. 6–31, 2024.I. M. Chernenko, I. S. Anureev, and N. O. Garanina, “Requirement patterns in deductive verification of poST programs,” Modeling and Analysis of Information Systems, vol. 31, no. 1, pp. 6–31, 2024.P. Cousot and R. Cousot, “Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977, pp. 238–252.P. Cousot and R. Cousot, “Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints,” in Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977, pp. 238–252.N. Suzuki and K. Ishihata, “Implementation of an array bound checker,” in Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977, pp. 132–143.N. Suzuki and K. Ishihata, “Implementation of an array bound checker,” in Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977, pp. 132–143.M. A. Col'on, S. Sankaranarayanan, and H. B. Sipma, “Linear invariant generation using non-linear constraint solving,” in Computer Aided Verification, 2003, pp. 420–432.M. A. Col'on, S. Sankaranarayanan, and H. B. Sipma, “Linear invariant generation using non-linear constraint solving,” in Computer Aided Verification, 2003, pp. 420–432.L. Kov'acs, “Reasoning algebraically about P-solvable loops,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 249–264.L. Kov'acs, “Reasoning algebraically about P-solvable loops,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 249–264.J. Stark and A. Ireland, “Invariant discovery via failed proof attempts,” in International Workshop on Logic Programming Synthesis and Transformation, 1998, pp. 271–288.J. Stark and A. Ireland, “Invariant discovery via failed proof attempts,” in International Workshop on Logic Programming Synthesis and Transformation, 1998, pp. 271–288.K. R. M. Leino and F. Logozzo, “Loop invariants on demand,” in Asian Symposium on Programming Languages and Systems, 2005, pp. 119–134.K. R. M. Leino and F. Logozzo, “Loop invariants on demand,” in Asian Symposium on Programming Languages and Systems, 2005, pp. 119–134.M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin, “Dynamically discovering likely program invariants to support program evolution,” in Proceedings of the 21st International Conference on Software engineering, 1999, pp. 213–224.M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin, “Dynamically discovering likely program invariants to support program evolution,” in Proceedings of the 21st International Conference on Software engineering, 1999, pp. 213–224.X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song, “Learning loop invariants for program verification,” Advances in Neural Information Processing Systems, vol. 31, 2018.X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song, “Learning loop invariants for program verification,” Advances in Neural Information Processing Systems, vol. 31, 2018.C. A. Furia, B. Meyer, and S. Velder, “Loop invariants: Analysis, classification, and examples,” ACM Computing Surveys (CSUR), vol. 46, no. 3, pp. 1–51, 2014.C. A. Furia, B. Meyer, and S. Velder, “Loop invariants: Analysis, classification, and examples,” ACM Computing Surveys (CSUR), vol. 46, no. 3, pp. 1–51, 2014.J. Breck, J. Cyphert, Z. Kincaid, and T. Reps, “Templates and recurrences: better together,” in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020, pp. 688–702.J. Breck, J. Cyphert, Z. Kincaid, and T. Reps, “Templates and recurrences: better together,” in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020, pp. 688–702.S. Srivastava, S. Gulwani, and J. S. Foster, “Template-based program verification and program synthesis,” International Journal on Software Tools for Technology Transfer, vol. 15, pp. 497–518, 2013.S. Srivastava, S. Gulwani, and J. S. Foster, “Template-based program verification and program synthesis,” International Journal on Software Tools for Technology Transfer, vol. 15, pp. 497–518, 2013.Z. Manna et al., “STeP: The Stanford temporal prover,” in Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995, pp. 793–794.Z. Manna et al., “STeP: The Stanford temporal prover,” in Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995, pp. 793–794.C. Belo Lourencco, D. Cousineau, F. Faissole, C. March'e, D. Mentr'e, and H. Inoue, “Automated formal analysis of temporal properties of Ladder programs,” International Journal on Software Tools for Technology Transfer, vol. 24, no. 6, pp. 977–997, 2022.C. Belo Lourencco, D. Cousineau, F. Faissole, C. March'e, D. Mentr'e, and H. Inoue, “Automated formal analysis of temporal properties of Ladder programs,” International Journal on Software Tools for Technology Transfer, vol. 24, no. 6, pp. 977–997, 2022.A. Blanchard, F. Loulergue, and N. Kosmatov, “Towards full proof automation in Frama-C using auto-active verification,” in NASA Formal Methods Symposium, 2019, pp. 88–105.A. Blanchard, F. Loulergue, and N. Kosmatov, “Towards full proof automation in Frama-C using auto-active verification,” in NASA Formal Methods Symposium, 2019, pp. 88–105.A. Naumchev, “Seamless object-oriented requirements,” in Proceedings of the International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON), 2019, pp. 0743–0748.A. Naumchev, “Seamless object-oriented requirements,” in Proceedings of the International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON), 2019, pp. 0743–0748.A. Gupta and A. Rybalchenko, “Invgen: An efficient invariant generator,” in Proceedings of the Computer Aided Verification, 2009, pp. 634–640.A. Gupta and A. Rybalchenko, “Invgen: An efficient invariant generator,” in Proceedings of the Computer Aided Verification, 2009, pp. 634–640.D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, “Invariant synthesis for combined theories,” in International Workshop on Verification, Model Checking, and Abstract Interpretation, 2007, pp. 378–394.D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, “Invariant synthesis for combined theories,” in International Workshop on Verification, Model Checking, and Abstract Interpretation, 2007, pp. 378–394.A. Mekki, M. Ghazel, and A. Toguyeni, “Patterns-Based Assistance for Temporal Requirement Specification,” in Proceedings of the International Conference on Software Engineering Research and Practice (SERP), 2011, p. 40893006.A. Mekki, M. Ghazel, and A. Toguyeni, “Patterns-Based Assistance for Temporal Requirement Specification,” in Proceedings of the International Conference on Software Engineering Research and Practice (SERP), 2011, p. 40893006.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.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.

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