|
This article is cited in 1 scientific paper (total in 1 paper)
Theory of software
Verification of declarative LTL-specification of control programs behavior
M. V. Neyzova, E. V. Kuz'minb a Institute of Automation and Electrometry SB RAS, Novosibirsk, Russia
b P.G. Demidov Yaroslavl State University, Yaroslavl, Russia
Abstract:
The article continues the series of works on development and verification of control programs based on LTL-specifications of a special type. Previously, it was proposed a declarative LTL-specification, which allows describing the behavior of control programs and building program code based on it in the imperative ST-language for programmable logic controllers. The LTL-specification can be directly verified for compliance with specified temporal properties by the model checking method using the nuXmv symbolic verification tool. In general, it is not required translating LTL-formulas of the specification into another formalism — an SMV-specification (code in the input language of the nuXmv tool).
The purpose of this work is to explore alternative ways of representing a program behavior model corresponding to the declarative LTL-specification during its verification within the nuXmv tool.
In the article, we transform the declarative LTL-specification into various SMV-specifications with accompanying changes of formulation of the verification problem, what leads to a significant reduction in time costs when checking temporal properties by using the nuXmv tool. The acceleration of verification is due to the reduction of the state space of a model being verified. The SMV-specifications obtained as a result of the proposed transformations specify identical or bisimulationally equivalent transition systems. It is ensuring the same verification results when replacing one SMV-specification with another.
Keywords:
control software, PLC program, declarative LTL-specification, imperative LTL-specification, complete transition system, pseudo-complete transition system, state space, model checking, nuXmv verifier, SMV-specification, bisimulation equivalence, bisimulation.
Received: 03.05.2024 Revised: 17.05.2024 Accepted: 22.05.2024
Citation:
M. V. Neyzov, E. V. Kuz'min, “Verification of declarative LTL-specification of control programs behavior”, Model. Anal. Inform. Sist., 31:2 (2024), 120–141
Linking options:
https://www.mathnet.ru/eng/mais819 https://www.mathnet.ru/eng/mais/v31/i2/p120
|
Statistics & downloads: |
Abstract page: | 5 | References: | 2 |
|