Welcome to My Research!
You may have access to the free features available through My Research. You can save searches, save documents, create alerts and more. Please log in through your library or institution to check if you have access.
Translate this article into 20 different languages!
If you log in through your library or institution you might have access to this article in multiple languages.
Get access to 20+ different citations styles
Styles include MLA, APA, Chicago and many more. This feature may be available for free if you log in through your library or institution.
Looking for a PDF of this document?
You may have access to it for free by logging in through your library or institution.
Want to save this document?
You may have access to different export options including Google Drive and Microsoft OneDrive and citation management tools like RefWorks and EasyBib. Try logging in through your library or institution to get access to these tools.
- Preview Available
- Scholarly Journal
LTL-Specification for Development and Verification of Control Programs
LTL-Specification for Development and Verification of Control ProgramsWe're sorry, there is no preview available.
Try and log in through your library or institution to see if they have access.
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.
