Formalization of Process-oriented Programs in poST Using Isabelle/HOL

To develop reliable control systems running on embedded devices, we advice to use domain specified languages. They abstract away the underlying hardware and provide the necessary syntactic sugar to conveniently describe the most useful control constructs. In addition, such languages can provide toolsets for proving the correctness of programs in them against given formal requirements. In this paper, we consider a partial solution of such a problem related to the formalization of the control code. In our case, syntactic sugar lies in extending the IEC 61131–3 standard for industrial automation languages with explicit statefulness and focusing on logical decomposition of code into processes. The aim of the present paper is to provide approaches and methods for transforming imperative programs in such a promising poST (process-oriented structured text) language into a functional representation for their further proofs using the Isabelle/HOL system. In our solution, we provide insight into three parts of the formalization: (1) the creation of basic data types constituting the original code model, (2) transformation of the poST code model into special representation for execution, and (3) a group of inductive definitions constructing the process of execution. The results represent a complete solution in the form of a formal functional model for the execution of poST programs and then can be used to form and prove theorems based on the model.