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/

[1] D. J. Smith, K. G. Simpson, The Safety Critical Systems Handbook, Butterworth-Heinemann, 5th, 2020

[2] V. D'Silva, D. Kroening, G. Weissenbacher, “A Survey of Automated Techniques for Formal Software Verification”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27 (2008), 1165–1178 | DOI

[3] S. Oks et al, “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook”, Information Systems Frontiers, 2022 | DOI

[4] E. Lee, S. Seshia, Introduction to Embedded Systems A Cyber-Physical Systems Approach, 2nd, MIT Press, 2017 | MR | Zbl

[5] M. Neyzov, E. Kuzmin, “LTL-specification for Development and Verification of Control Programs”, Modeling and Analysis of Information Systems, 30:4 (2023), 308–339 (in Russian) | DOI

[6] D. Harel, A. Pnueli, “On the Development of Reactive Systems”, Logics and Models of Concurrent Systems, 13 (1985), 477–498 | DOI | MR | Zbl

[7] A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends”, Current Trends in Concurrency, 224, Springer, 1986, 510–584 | DOI | MR

[8] IEC 61131-3:2013 Programmable controllers Part 3: Programming languages https://webstore.iec.ch/publication/4552

[9] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 1st, Springer Publishing Company, Incorporated, 2018 | MR | Zbl

[10] E. M. Clarke, O. Grumberg, D. Peled, Verification of Program Models: Model Checking, translated from English to Russian, MCNMO, 2002, 416 pp.

[11] D. Beyer, A. Podelski, “Software model checking: 20 years and beyond”, Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, Springer, 2022, 554–582 | DOI | MR

[12] nuXmv home, https://nuxmv.fbk.eu/

[13] IEC 61131-1:2003 Programmable controllers Part 1: General information https://webstore.iec.ch/publication/4550

[14] B. Alpern, F. B. Schneider, “Defining Liveness”, Information Processing Letters, 21:4 (1985), 181–185 | DOI | MR | Zbl

[15] Z. Manna, A. Pnueli, “A Hierarchy of Temporal Properties”, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, 1990, 377–410 | DOI

[16] Spot home, https://spot.lre.epita.fr/

[17] nuXmv User Manual, https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf

[18] D. Park, “Concurrency and Automata on Infinite Sequences”, Theoretical Computer Science: 5th GI-Conference Karlsruhe, Lecture Notes in Computer Science, 104, 1981, 167–183 | DOI | Zbl