Geodesic
Verification of declarative LTL-specification of control programs behavior
Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 2, pp. 120-141

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

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
Mots-clés : bisimulation equivalence, bisimulation. 
@article{MAIS_2024_31_2_a0,
     author = {M. V. Neyzov and E. V. Kuz'min},
     title = {Verification of declarative {LTL-specification} of control programs behavior},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {120--141},
     publisher = {mathdoc},
     volume = {31},
     number = {2},
     year = {2024},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2024_31_2_a0/}
}
TY  - JOUR
AU  - M. V. Neyzov
AU  - E. V. Kuz'min
TI  - Verification of declarative LTL-specification of control programs behavior
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2024
SP  - 120
EP  - 141
VL  - 31
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2024_31_2_a0/
LA  - ru
ID  - MAIS_2024_31_2_a0
ER  - 
%0 Journal Article
%A M. V. Neyzov
%A E. V. Kuz'min
%T Verification of declarative LTL-specification of control programs behavior
%J Modelirovanie i analiz informacionnyh sistem
%D 2024
%P 120-141
%V 31
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2024_31_2_a0/
%G ru
%F MAIS_2024_31_2_a0
M. V. Neyzov; E. V. Kuz'min. Verification of declarative LTL-specification of control programs behavior. Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 2, pp. 120-141. http://geodesic.mathdoc.fr/item/MAIS_2024_31_2_a0/