Подход к автоматизации дедуктивной верификации процесс-ориентированных программ, основанный на шаблонах

Pattern-based approach to automation of deductive verification of process-oriented programs

Article's language
English
Abstract
Process-oriented programming is an approach to the development of control software in which a program is defined as a set of interacting processes. PoST is a process-oriented language that extends ST language from the IEC 61131-3 standard. In the field of control software development, formal verification plays an important role because of the need to ensure the high reliability of such software. Deductive verification is a formal verification method in which a program and requirements for it are presented in the form of logical formulas and logical inference is used to prove that the program satisfies the requirements. Control software is often subject to temporal requirements. We formalize such requirements for process-oriented programs in the form of control loop invariants. But control loop invariants representing requirements are not sufficient for proving program correctness. Therefore, we add extra invariants that contain auxiliary information. This paper addresses the problem of automating deductive verification of process-oriented programs. We propose an approach in which temporal requirements are specified using requirement patterns that are constructed from basic patterns. For each requirement pattern the corresponding extra invariant pattern and lemmas are defined. The proposed approach allows us to make the deductive verification of process-oriented programs more automated.
DOI
10.31144/si.2307-6410.2024.n25.p11-28
Pages
11-28
File
Number