Automation of proving verification conditions in deductive verification system for poST programs

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.

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.