학술논문
Development of Verification Condition Generator for Process-Oriented Programs in PoST Language
Document Type
Conference
Author
Source
2023 IEEE 24th International Conference of Young Professionals in Electron Devices and Materials (EDM) Young Professionals in Electron Devices and Materials (EDM), 2023 IEEE 24th International Conference of. :1760-1765 Jun, 2023
Subject
Language
ISSN
2325-419X
Abstract
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.