Pattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithms

I. M. Chernenko ; I. S. Anureev

Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 4, pp. 384-425.

Résumé

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.

Détail

Keywords: deductive verification, temporal requirements, requirement pattern, loop invariant, control software, process-oriented programming.

Bibliographie

[1] V. E. Zyubin, “Hyper-automaton: A model of control algorithms”, Proceedings of the Siberian Conference on Control and Communications, IEEE, 2007, 51–57 | DOI

[2] V. E. Zyubin, A. S. Rozov, I. S. Anureev, N. O. Garanina, V. Vyatkin, “poST: A process-oriented extension of the IEC 61131-3 structured text language”, IEEE Access, 10 (2022), 35238–35250 | DOI

[3] IEC, IEC 61131-3: 2013 programmable controllers-Part 3: Programming languages, International Standard, 2013 https://webstore.iec.ch/publication/4552

[4] R.Hähnle, M. Huisman, “Deductive software verification: From-pen-and-paper proofs to industrial tools”, Computing and Software Science: State of the Art and Perspectives, 2019, 345–373 | DOI | Zbl

[5] I. Anureev, N. Garanina, T. Liakh, A. Rozov, V. Zyubin, S. Gorlatch, “Two-step deductive verification of control software using reflex”, Perspectives of System Informatics, 2019, 50–63 | DOI

[6] I. Chernenko, I. S. Anureev, N. O. Garanina, S. M. Staroletov, “A temporal requirements language for deductive verification of process-oriented programs”, Proceedings of the IEEE 23rd International Conference of Young Professionals in Electron Devices and Materials (EDM), IEEE, 2022, 657–662

[7] I. Chernenko, “Requirements patterns in deductive verification of process-oriented programs and examples of their use”, System Informatics, 22 (2023), 11–20 | DOI

[8] L. C. Paulson, T. Nipkow, M. Wenzel, “From LCF to Isabelle/HOL”, Formal Aspects of Computing, 31 (2019), 675–698 | DOI | MR | Zbl

[9] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem et al, Handbook of model checking, 10, Springer, 2018 | MR

[10] D. Matichuk, T. Murray, M. Wenzel, “Eisbach: A proof method language for Isabelle”, Journal of Automated Reasoning, 56:3 (2016), 261–282 | DOI | MR | Zbl

[11] I. M. Chernenko, I. S. Anureev, N. O. Garanina, “Requirement patterns in deductive verification of poST programs”, Modeling and Analysis of Information Systems, 31:1 (2024), 6–31 (in Russian) | DOI

[12] P. Cousot, R. Cousot, “Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints”, Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977, 238–252

[13] N. Suzuki, K. Ishihata, “Implementation of an array bound checker”, Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977, 132–143

[14] M. A. Colón, S. Sankaranarayanan, H. B. Sipma, “Linear invariant generation using non-linear constraint solving”, Computer Aided Verification, Springer, 2003, 420–432 | DOI | MR | Zbl

[15] L. Kovács, “Reasoning algebraically about P-solvable loops”, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2008, 249–264 | MR | Zbl

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

[17] K. R. M. Leino, F. Logozzo, “Loop invariants on demand”, Asian Symposium on Programming Languages and Systems, Springer, 2005, 119–134 | Zbl

[18] M. D. Ernst, J. Cockrell, W. G. Griswold, D. Notkin, “Dynamically discovering likely program invariants to support program evolution”, Proceedings of the 21st International Conference on Software engineering, 1999, 213–224 | DOI

[19] X. Si, H. Dai, M. Raghothaman, M. Naik, L. Song, “Learning loop invariants for program verification”, Advances in Neural Information Processing Systems, 31 (2018)

[20] C. A. Furia, B. Meyer, S. Velder, “Loop invariants: Analysis, classification, and examples”, ACM Computing Surveys (CSUR), 46:3 (2014), 1–51 | DOI | MR

[21] J. Breck, J. Cyphert, Z. Kincaid, T. Reps, “Templates and recurrences: Better together”, Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020, 688–702 | DOI

[22] S. Srivastava, S. Gulwani, J. S. Foster, “Template-based program verification and program synthesis”, International Journal on Software Tools for Technology Transfer, 15 (2013), 497–518 | DOI

[23] Z. Manna et al, “STeP: The Stanford temporal prover”, Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, Springer, 1995, 793–794 | DOI

[24] C. Belo Lourenço, D. Cousineau, F. Faissole, C. Marché, D. Mentré, H. Inoue, “Automated formal analysis of temporal properties of Ladder programs”, International Journal on Software Tools for Technology Transfer, 24:6 (2022), 977–997 | DOI

[25] A. Blanchard, F. Loulergue, N. Kosmatov, “Towards full proof automation in Frama-C using auto-active verification”, NASA Formal Methods Symposium, Springer, 2019, 88–105 | DOI

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

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

[28] D. Beyer, T. A. Henzinger, R. Majumdar, A. Rybalchenko, “Invariant synthesis for combined theories”, International Workshop on Verification, Model Checking, and Abstract Interpretation, Springer, 2007, 378–394 | DOI | MR | Zbl

[29] A. Mekki, M. Ghazel, A. Toguyeni, “Patterns-based assistance for temporal requirement specification”, Proceedings of the International Conference on Software Engineering Research and Practice (SERP), 2011, 40893006

[30] M. B. Dwyer, G. S. Avrunin, J. C. Corbett, “Patterns in property specifications for finite-state verification”, Proceedings of the 21st International Conference on Software Engineering, 1999, 411–420 | DOI