Geodesic
Ltl-specification for development and verification of control programs
Modelirovanie i analiz informacionnyh sistem, Tome 30 (2023) no. 4, pp. 308-339

Voir la notice de l'article provenant de la source Math-Net.Ru

This work continues the series of articles on development and verification of control programs based on the LTL-specification. The essence of the approach is to describe the behavior of programs using formulas of linear temporal logic LTL of a special form. The developed LTL-specification can be directly verified by using a model checking tool. Next, according to the LTL-specification, the program code in the imperative programming language is unambiguously built. The translation of the specification into the program is carried out using a template. The novelty of the work consists in the proposal of two LTL-specifications of a new form — declarative and imperative, as well as in a more strict formal justification for this approach to program development and verification. A transition has been made to a more modern verification tool for finite and infinite systems — nuXmv. It is proposed to describe the behavior of control programs in a declarative style. For this purpose, a declarative LTL-specification is intended, which defines a labelled transition system as a formal model of program behavior. This method of describing behavior is quite expressive — the theorem on the Turing completeness of the declarative LTL-specification is proved. Next, to construct program code in an imperative language, the declarative LTL-specification is converted into an equivalent imperative LTL-specification. An equivalence theorem is proved, which guarantees that both specifications specify the same behavior. The imperative LTL-specification is translated into imperative program code according to the presented template. The declarative LTL-specification, which is subject to verification, and the control program built on it are guaranteed to specify the same behavior in the form of a corresponding transition system. Thus, during verification, a model is used that is adequate to the real behavior of the control program.
Keywords: control software, declarative LTL-specification, imperative LTL-specification, model checking, complete transition system, pseudo-complete transition system, Minsky counter machine, nuXmv verifier, PLC program, ST language. 
@article{MAIS_2023_30_4_a1,
     author = {M. V. Neyzov and E. V. Kuzmin},
     title = {Ltl-specification for development and verification of control programs},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {308--339},
     publisher = {mathdoc},
     volume = {30},
     number = {4},
     year = {2023},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2023_30_4_a1/}
}
TY  - JOUR
AU  - M. V. Neyzov
AU  - E. V. Kuzmin
TI  - Ltl-specification for development and verification of control programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2023
SP  - 308
EP  - 339
VL  - 30
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2023_30_4_a1/
LA  - ru
ID  - MAIS_2023_30_4_a1
ER  - 
%0 Journal Article
%A M. V. Neyzov
%A E. V. Kuzmin
%T Ltl-specification for development and verification of control programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2023
%P 308-339
%V 30
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2023_30_4_a1/
%G ru
%F MAIS_2023_30_4_a1
M. V. Neyzov; E. V. Kuzmin. Ltl-specification for development and verification of control programs. Modelirovanie i analiz informacionnyh sistem, Tome 30 (2023) no. 4, pp. 308-339. http://geodesic.mathdoc.fr/item/MAIS_2023_30_4_a1/