LTL-Specification for Development and Verification of Control Programs

Abstract

This work continues the series of articles on the development and verification of control programs based on the LTL-specification. The approach consists in describing the behavior of programs by special form of linear temporal logic (LTL) formulae. The developed LTL-specification can be directly verified with the help of a model-checking tool. Next, according to the LTL-specification, a program code is unambiguously built in the imperative programming language. The specification is translated into the program using a template. The novelty of the work is the proposal of two new LTL-specifications, which are declarative and imperative, as well as in a stricter formal justification of this approach to program development and verification. A transition is made to nuXmv, a more advanced verification tool for finite and infinite systems. It is proposed to describe the behavior of control programs in a declarative manner. For this purpose, a declarative LTL-specification is intended, which defines a transition system as a formal model of program behavior. This behavior description method is quite expressive—the theorem on the Turing completeness of the declarative LTL-specification is proved. Next, to build a program code in the imperative language, the declarative LTL-specification is converted to an equivalent imperative LTL-specification. An equivalence theorem is proved, which guarantees that both specifications determine the same behavior. The imperative LTL-specification is translated into an imperative program code according to the presented template. The declarative LTL-specification, which undergoes verification, and the control program based on it are guaranteed to determine the same behavior in the form of a corresponding transition system. Thus, in the verification a model coherent with the actual behavior of the control program is used.