|
This article is cited in 2 scientific papers (total in 2 papers)
Theory of software
Ltl-specification for development and verification of control programs
M. V. Neyzova, E. V. Kuzminb a Institute of Automation and Electrometry SB RAS, 1 Academician Koptyug ave., Novosibirsk 630090, Russia
b P.G. Demidov Yaroslavl State University, 14 Sovetskaya str., Yaroslavl 150003, Russia
Abstract:
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.
Received: 06.11.2023 Revised: 20.11.2023 Accepted: 22.11.2023
Citation:
M. V. Neyzov, E. V. Kuzmin, “Ltl-specification for development and verification of control programs”, Model. Anal. Inform. Sist., 30:4 (2023), 308–339
Linking options:
https://www.mathnet.ru/eng/mais806 https://www.mathnet.ru/eng/mais/v30/i4/p308
|
Statistics & downloads: |
Abstract page: | 34 | Full-text PDF : | 5 | References: | 6 |
|