Requirement Patterns in Isabelle/HOL for Deductive Verification of Process-oriented Programs

One of the main ways to ensure the correctness of programs is deductive verification. This method is based on formalizing the program and its requirements as logical formulas. If these formulas are proven, the program is considered correct regarding the requirements. The process of proving these formulas is very complicated and so requires attempts at automatization or simplifying. Programs created within a process-oriented paradigm are operating in a control loop, which means that they are launched once in a certain period. This adds its specificity to requirement formulas and program properties, as they have to be formulated as loop invariants. Such form severely complicates proving. This paper introduces requirements patterns formulated as Isabelle/HOL lemmas and based on analysis of requirements to several control programs. These patterns are designed to simplify the proving and in more easy cases completely automate it. Analysis of pattern usage showed that proofs become shorter, more structured and less complex.