Подход к автоматизации дедуктивной верификации процесс-ориентированных программ, основанный на шаблонах: шаблоны, леммы и алгоритмы

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

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

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

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

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

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.

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

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

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

9. E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, and others, Handbook of model checking, vol. 10. Springer, 2018.

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

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

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

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

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

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

16. J. Stark and A. Ireland, “Invariant discovery via failed proof attempts,” in International Workshop on Logic Programming Synthesis and Transformation, 1998, pp. 271–288.

17. K. R. M. Leino and F. Logozzo, “Loop invariants on demand,” in Asian Symposium on Programming Languages and Systems, 2005, pp. 119–134.

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

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

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

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

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

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

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

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

26. A. Naumchev, “Seamless object-oriented requirements,” in Proceedings of the International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON), 2019, pp. 0743–0748.

27. A. Gupta and A. Rybalchenko, “Invgen: An efficient invariant generator,” in Proceedings of the Computer Aided Verification, 2009, pp. 634–640.

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

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

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