Partial Automation of Verification Condition Proving for Reflex Programs (Draft)

Abstract

Process-Oriented Programming is a software development approach that emphasizes the management of control systems through abstractions of processes and their states, enabling these systems to be described in terms of real physical processes. This native description of control is particularly important for industrial systems consisting of hundreds or thousands of processes. For such systems, safety is critical. To ensure the reliability and safety of these systems, formal verification methods must be applied. One such method is deductive verification, which involves formalizing programs and their requirements as logical formulas, known as verification conditions. Proving these conditions confirms that the program meets its requirements. The automatic generation of verification conditions is performed by a specialized software tool called a verification condition generator. We previously proposed a verification condition generator for the Reflex language. However, it generates too many verification conditions, making their manual proof impossible. This paper proposes modifications to the verification condition generator aimed at automating the proof of some of these conditions. These modifications include introducing an annotation language to describe requirements in a structured form, generating invariants based on the program structure, and using SMT solvers for the preliminary attempt to solve the verification conditions.