maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2026-2-150-175mais-2091Research ArticleTheory of SoftwareАвтоматизация доказательства условий корректности в системе дедуктивной верификации poST-программAutomation of proving verification conditions in deductive verification system for poST programshttps://orcid.org/0000-0001-7675-8449ЧерненкоИван МихайловичChernenkoIvan M.chernenkoim@iae.nsk.suhttps://orcid.org/0000-0001-9574-128XАнуреевИгорь СергеевичAnureevIgor S.anureev@gmail.comИнститут автоматики и электрометрии СО РАНРоссияInstitute of Automation and Electrometry SB RASRussian Federation202618062026332150175Copyright © Черненко И.М., Ануреев И.С., 20262026Черненко И.М., Ануреев И.С.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/2091

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

Process-oriented programming is an approach to developing control software where a program is structured as a set of processes. PoST is a process-oriented extension of ST language from the IEC 61131-3 standard. Since control systems often have high reliability requirements, formal verification of their software plays an important role. One formal verification method is deductive verification, which involves building a formal specification, generating verification conditions, and proving them. We use the Isabelle/HOL theorem prover for the proof step. Only the generation of verification conditions is fully automated. Deductive verification itself is labor-intensive, so automating it as much as possible is desirable. Control software involves temporal requirements, which in deductive verification of process-oriented programs are expressed as control loop invariants. However, these requirements are insufficient invariants, making it necessary to introduce extra invariants that carry auxiliary information about the program. An earlier approach to proving verification conditions used patterns for both the requirements and the extra invariants, with pattern-specific lemmas satisfying predefined schemas used in the proofs. This paper looks at automating the proof of both the verification conditions and the lemmas used in those proofs. We describe the previously proposed approach to automating deductive verification and give an introduction to Isabelle/HOL. Revised schemas for patterns and lemmas are presented, along with an algorithm for generating lemma proofs. We discuss the implementation of this algorithm and of the previously developed algorithm for generating verification condition proofs. The proposed approach is demonstrated with an example. A review of related work is provided.

дедуктивная верификациятемпоральные требованияшаблон требованийинвариант циклауправляющее программное обеспечениепроцесс-ориентированное программированиеdeductive verificationtemporal requirementsrequirement patternloop invariantcontrol softwareprocess-oriented programmingИАиЭ СО РАН (проект № 125022803031-1)IAaE SB RAS (project No. 125022803031-1)ReferencesIEC, “IEC 61131-3: 2013 programmable controllers-Part 3: programming languages.” 2013. Available: https://webstore.iec.ch/publication/4552IEC, “IEC 61131-3: 2013 programmable controllers-Part 3: programming languages.” 2013. Available: https://webstore.iec.ch/publication/4552F. Basile, P. Chiacchio, and D. Gerbasio, “On the implementation of industrial automation systems based on PLC,” IEEE Transactions on Automation Science and Engineering, vol. 10, no. 4, pp. 990–1003, 2012.F. Basile, P. Chiacchio, and D. Gerbasio, “On the implementation of industrial automation systems based on PLC,” IEEE Transactions on Automation Science and Engineering, vol. 10, no. 4, pp. 990–1003, 2012.V. E. Zyubin, “Hyper-automaton: A model of control algorithms,” in Proceedings of the 2007 Siberian Conference on Control and Communications, IEEE, 2007, pp. 51–57. doi: 10.1109/SIBCON.2007.371297.V. E. Zyubin, “Hyper-automaton: A model of control algorithms,” in Proceedings of the 2007 Siberian Conference on Control and Communications, IEEE, 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.P. Ovsiannikova, I. Buzhinsky, A. Pakonen, and V. Vyatkin, “Oeritte: User-friendly counterexample explanation for model checking,” IEEE Access, vol. 9, pp. 61383–61397, 2021.P. Ovsiannikova, I. Buzhinsky, A. Pakonen, and V. Vyatkin, “Oeritte: User-friendly counterexample explanation for model checking,” IEEE Access, vol. 9, pp. 61383–61397, 2021.D. Gurov, P. Herber, and I. Schaefer, “Automated Verification of Embedded Control Software: Track Introduction,” in Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2020, pp. 235–239.D. Gurov, P. Herber, and I. Schaefer, “Automated Verification of Embedded Control Software: Track Introduction,” in Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2020, pp. 235–239.E. M. Clarke, W. Klieber, M. Nov'avcek, and P. Zuliani, “Model checking and the state explosion problem,” in LASER Summer School on Software Engineering, Springer, 2011, pp. 1–30.E. M. Clarke, W. Klieber, M. Nov'avcek, and P. Zuliani, “Model checking and the state explosion problem,” in LASER Summer School on Software Engineering, Springer, 2011, pp. 1–30.I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, and S. Gorlatch, “Two-step deductive verification of control software using Reflex,” in Proceedings of the International Andrei Ershov Memorial Conference on Perspectives of System Informatics, 2019, pp. 50–63.I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, and S. Gorlatch, “Two-step deductive verification of control software using Reflex,” in Proceedings of the International Andrei Ershov Memorial Conference on Perspectives of System Informatics, 2019, pp. 50–63.L. De Moura and N. Bjorner, “Z3: An efficient SMT solver,” in Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 337–340.L. De Moura and N. Bjorner, “Z3: An efficient SMT solver,” in Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 337–340.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 and I. S. Anureev, “Pattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithms,” Modeling and Analysis of Information Systems, vol. 31, no. 4, pp. 384–425, 2024, doi: 10.18255/1818-1015-2024-4-384-425.I. M. Chernenko and I. S. Anureev, “Pattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithms,” Modeling and Analysis of Information Systems, vol. 31, no. 4, pp. 384–425, 2024, doi: 10.18255/1818-1015-2024-4-384-425.I. Chernenko and I. Anureev, “Generation of Isabelle/HOL Theory Focused on Proving Verification Conditions of PoST Programs and Based on Derived Requirement Patterns,” in Proceedings of the 26th International Conference of Young Professionals in Electron Devices and Materials (EDM), 2025, pp. 1480–1485.I. Chernenko and I. Anureev, “Generation of Isabelle/HOL Theory Focused on Proving Verification Conditions of PoST Programs and Based on Derived Requirement Patterns,” in Proceedings of the 26th International Conference of Young Professionals in Electron Devices and Materials (EDM), 2025, pp. 1480–1485.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 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 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2022, pp. 657–662.L. C. Paulson, “The foundation of a generic theorem prover,” Journal of Automated Reasoning, vol. 5, pp. 363–397, 1989.L. C. Paulson, “The foundation of a generic theorem prover,” Journal of Automated Reasoning, vol. 5, pp. 363–397, 1989.L. Bettini, Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd, 2016.L. Bettini, Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd, 2016.F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, “Frama-C: A software analysis perspective,” Formal Aspects of Computing, vol. 27, no. 3, pp. 573–609, 2015.F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, “Frama-C: A software analysis perspective,” Formal Aspects of Computing, vol. 27, no. 3, pp. 573–609, 2015.E. Cohen et al., “VCC: A practical system for verifying concurrent C,” in Proceedings of the Theorem Proving in Higher Order Logics: 22nd International Conference, 2009, pp. 23–42.E. Cohen et al., “VCC: A practical system for verifying concurrent C,” in Proceedings of the Theorem Proving in Higher Order Logics: 22nd International Conference, 2009, pp. 23–42.M. Barnett, M. F"ahndrich, K. R. M. Leino, P. M"uller, W. Schulte, and H. Venter, “Specification and verification: the Spec# experience,” Communications of the ACM, vol. 54, no. 6, pp. 81–91, 2011.M. Barnett, M. F"ahndrich, K. R. M. Leino, P. M"uller, W. Schulte, and H. Venter, “Specification and verification: the Spec# experience,” Communications of the ACM, vol. 54, no. 6, pp. 81–91, 2011.N. Kosmatov, C. March'e, Y. Moy, and J. Signoles, “Static versus dynamic verification in Why3, Frama-C and SPARK 2014,” in Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2016, pp. 461–478.N. Kosmatov, C. March'e, Y. Moy, and J. Signoles, “Static versus dynamic verification in Why3, Frama-C and SPARK 2014,” in Proceedings of the International Symposium on Leveraging Applications of Formal Methods, 2016, pp. 461–478.K. R. M. Leino and V. W"ustholz, “The Dafny Integrated Development Environment,” in Proceedings of the 1st Workshop on Formal Integrated Development Environment, 2014, pp. 3–15. doi: 10.4204/EPTCS.149.2.K. R. M. Leino and V. W"ustholz, “The Dafny Integrated Development Environment,” in Proceedings of the 1st Workshop on Formal Integrated Development Environment, 2014, pp. 3–15. doi: 10.4204/EPTCS.149.2.J.-C. Filli^atre and A. Paskevich, “Why3 — where programs meet provers,” in European Symposium on Programming, 2013, pp. 125–128.J.-C. Filli^atre and A. Paskevich, “Why3 — where programs meet provers,” in European Symposium on Programming, 2013, pp. 125–128.M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino, “Boogie: A modular reusable verifier for object-oriented programs,” in Proceedings of the International Symposium on Formal Methods for Components and Objects, Springer, 2005, pp. 364–387.M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino, “Boogie: A modular reusable verifier for object-oriented programs,” in Proceedings of the International Symposium on Formal Methods for Components and Objects, Springer, 2005, pp. 364–387.M. Johansson, “Lemma discovery for induction: a survey,” in Proceedings of the Intelligent Computer Mathematics: 12th International Conference, Springer, 2019, pp. 125–139.M. Johansson, “Lemma discovery for induction: a survey,” in Proceedings of the Intelligent Computer Mathematics: 12th International Conference, Springer, 2019, pp. 125–139.M. Aderhold, “Improvements in formula generalization,” in Proceedings of the International Conference on Automated Deduction, 2007, pp. 231–246.M. Aderhold, “Improvements in formula generalization,” in Proceedings of the International Conference on Automated Deduction, 2007, pp. 231–246.Y. Nagashima and J. Parsert, “Goal-oriented conjecturing for Isabelle/HOL,” in Proceedings of the Intelligent Computer Mathematics: 11th International Conference, 2018, pp. 225–231.Y. Nagashima and J. Parsert, “Goal-oriented conjecturing for Isabelle/HOL,” in Proceedings of the Intelligent Computer Mathematics: 11th International Conference, 2018, pp. 225–231.O. Montano-Rivas, R. McCasland, L. Dixon, and A. Bundy, “Scheme-based synthesis of inductive theories,” in Proceedings of the Mexican International Conference on Artificial Intelligence, 2010, pp. 348–361.O. Montano-Rivas, R. McCasland, L. Dixon, and A. Bundy, “Scheme-based synthesis of inductive theories,” in Proceedings of the Mexican International Conference on Artificial Intelligence, 2010, pp. 348–361.Y. Nagashima, Z. Xu, N. Wang, D. S. Goc, and J. Bang, “Template-Based Conjecturing for Automated Induction in Isabelle/HOL,” in Proceedings of the International Conference on Fundamentals of Software Engineering, 2023, pp. 112–125.Y. Nagashima, Z. Xu, N. Wang, D. S. Goc, and J. Bang, “Template-Based Conjecturing for Automated Induction in Isabelle/HOL,” in Proceedings of the International Conference on Fundamentals of Software Engineering, 2023, pp. 112–125.M. Johansson, D. Ros'en, N. Smallbone, and K. Claessen, “Hipster: Integrating theory exploration in a proof assistant,” in Proceedings of the International Conference on Intelligent Computer Mathematics, 2014, pp. 108–122.M. Johansson, D. Ros'en, N. Smallbone, and K. Claessen, “Hipster: Integrating theory exploration in a proof assistant,” in Proceedings of the International Conference on Intelligent Computer Mathematics, 2014, pp. 108–122.

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