Development of Verification Condition Generator for Process-Oriented Programs in PoST Language

The process-oriented paradigm is an approach to the development of control software. The poST language is a process-oriented extension of the ST language from the IEC 61131–3 family. In many control systems, control software is safety-critical. This requires the use of formal verification of such software, one of the methods of which is deductive verification. In deductive verification, the requirements for a program are formalized as annotations (formulas of some logical language). These annotations are added to the program, and the resulting annotated program is reduced to verification conditions - logical formulas. This method assumes that if all the verification conditions are true, then the program is considered to be correct. To automate the generation of verification conditions, verification systems have a special component - a verification condition generator. Verification condition generators were developed for various programming languages, but they have not yet been developed for the poST language. This paper presents a verification condition generator for poST programs with the output in the format of the generic proof assistant Isabelle/HOL.