Generation of Isabelle/HOL Theory Focused on Proving Verification Conditions of PoST Programs and Based on Derived Requirement Patterns

Process-oriented programming is an approach to the development of control software based on the concept of a hyper-automation – a set of communicating processes that are extended finite state machines. PoST language is a process-oriented extension of ST language from the IEC 61131-3 standard. Control software is often safety-critical and requires formal verification. Deductive verification is a formal verification method in which requirements are formalized as logical formulas, and logical inference is used to establish compliance of a program with its requirements. A loop invariant must be specified for each loop in the program. Temporal requirements are formalized as control loop invariants in deductive verification of process-oriented programs. However, these requirements where a specified program is considered as a black box are not sufficient to prove verification conditions generated by deductive verification of poST programs, and extra invariants related to the semantics of the program being verified are added to control loop invariants. Earlier, we developed a pattern-based approach to automation of deductive verification of process-oriented programs. This approach allows defining requirement patterns using basic ones and automatically generating corresponding extra invariant patterns and lemmas needed for proving program correctness. We developed a requirement pattern language that allows one to define requirement patterns. In this paper, we present a generator of a theory for Isabelle/HOL. This theory contains generated requirement and extra invariant patterns definitions as well as lemmas. These patterns are used to specify requirements and extra invariants, and lemmas are used in proving verification conditions.