Автоматизация доказательства условий корректности в системе дедуктивной верификации poST-программ

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

1. IEC, “IEC 61131-3: 2013 programmable controllers-Part 3: programming languages.” 2013. Available: https://webstore.iec.ch/publication/4552

2. 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.

3. 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.

4. 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.

5. 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.

6. 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.

7. 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.

8. 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.

9. 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.

10. L. C. Paulson, T. Nipkow, and M. Wenzel, “From LCF to Isabelle/HOL,” Formal Aspects of Computing, vol. 31, pp. 675–698, 2019.

11. 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.

12. 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.

13. 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.

14. L. C. Paulson, “The foundation of a generic theorem prover,” Journal of Automated Reasoning, vol. 5, pp. 363–397, 1989.

15. L. Bettini, Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd, 2016.

16. 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.

17. 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.

18. 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.

19. 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.

20. 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.

21. J.-C. Filli^atre and A. Paskevich, “Why3 — where programs meet provers,” in European Symposium on Programming, 2013, pp. 125–128.

22. 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.

23. M. Johansson, “Lemma discovery for induction: a survey,” in Proceedings of the Intelligent Computer Mathematics: 12th International Conference, Springer, 2019, pp. 125–139.

24. M. Aderhold, “Improvements in formula generalization,” in Proceedings of the International Conference on Automated Deduction, 2007, pp. 231–246.

25. 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.

26. 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.

27. 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.

28. 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.