Шаблоны требований, возникающих при дедуктивной верификации процесс-ориентированных программ, и примеры их использования

Requirements patterns in deductive verification of process-oriented programs and examples of their use

Article's language
English
Abstract
Process-oriented programming is a promising approach to the development of control software. Control software often has high reliability requirements. Formal verification methods, in particular deductive verification, are used to prove the correctness of such programs regarding the requirements. Previously, a temporal requirements language was developed to specify temporal requirements for deductive verification of process-oriented programs. It was also shown that a significant part of the requirements falls into a small number of classes. Requirements patterns was developed for these classes. In this paper, we present a collection of process-oriented programs and requirements for them. Requirements are formalized in the temporal requirements language and classified according the set of patterns. We also define a new requirement pattern. These results can be used in the research of formal verification methods for process-oriented programs, in particular in the research of methods of proving verification conditions.
DOI
10.31144/si.2307-6410.2023.n22.p11-20
Pages
11-20
File
Number