Geodesic
Ltl-specification for development and verification of control programs
Modelirovanie i analiz informacionnyh sistem, Tome 30 (2023) no. 4, pp. 308-339.

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

This work continues the series of articles on development and verification of control programs based on the LTL-specification. The essence of the approach is to describe the behavior of programs using formulas of linear temporal logic LTL of a special form. The developed LTL-specification can be directly verified by using a model checking tool. Next, according to the LTL-specification, the program code in the imperative programming language is unambiguously built. The translation of the specification into the program is carried out using a template. The novelty of the work consists in the proposal of two LTL-specifications of a new form — declarative and imperative, as well as in a more strict formal justification for this approach to program development and verification. A transition has been made to a more modern verification tool for finite and infinite systems — nuXmv. It is proposed to describe the behavior of control programs in a declarative style. For this purpose, a declarative LTL-specification is intended, which defines a labelled transition system as a formal model of program behavior. This method of describing behavior is quite expressive — the theorem on the Turing completeness of the declarative LTL-specification is proved. Next, to construct program code in an imperative language, the declarative LTL-specification is converted into an equivalent imperative LTL-specification. An equivalence theorem is proved, which guarantees that both specifications specify the same behavior. The imperative LTL-specification is translated into imperative program code according to the presented template. The declarative LTL-specification, which is subject to verification, and the control program built on it are guaranteed to specify the same behavior in the form of a corresponding transition system. Thus, during verification, a model is used that is adequate to the real behavior of the control program.
Keywords: control software, declarative LTL-specification, imperative LTL-specification, model checking, complete transition system, pseudo-complete transition system, Minsky counter machine, nuXmv verifier, PLC program, ST language. 
@article{MAIS_2023_30_4_a1,
     author = {M. V. Neyzov and E. V. Kuzmin},
     title = {Ltl-specification for development and verification of control programs},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {308--339},
     publisher = {mathdoc},
     volume = {30},
     number = {4},
     year = {2023},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2023_30_4_a1/}
}
TY  - JOUR
AU  - M. V. Neyzov
AU  - E. V. Kuzmin
TI  - Ltl-specification for development and verification of control programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2023
SP  - 308
EP  - 339
VL  - 30
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2023_30_4_a1/
LA  - ru
ID  - MAIS_2023_30_4_a1
ER  - 
%0 Journal Article
%A M. V. Neyzov
%A E. V. Kuzmin
%T Ltl-specification for development and verification of control programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2023
%P 308-339
%V 30
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2023_30_4_a1/
%G ru
%F MAIS_2023_30_4_a1
M. V. Neyzov; E. V. Kuzmin. Ltl-specification for development and verification of control programs. Modelirovanie i analiz informacionnyh sistem, Tome 30 (2023) no. 4, pp. 308-339. http://geodesic.mathdoc.fr/item/MAIS_2023_30_4_a1/

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

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

[3] E. A. Parr, Programmable Controllers. An Engineer's Guide, 3rd ed., Newnes, 2003, 448 pp.

[4] V. Lifshic, L. Sadovskii, “Algebraic Models of Computing Machines”, UMN, 27:3 (165) (1972), 79–125 (in Russian)

[5] K.-Y. Cai, T. Chen, T. Tse, “Towards Research on Software Cybernetics”, Proceedings of 7th IEEE International on High-assurance Systems Engineering, HASE 2002, IEEE Computer Society Press, 2002, 240–241

[6] N. Polikarpova, A. Shalyto, Automata-Based Programming, 2nd ed., Piter, Spb., 2011, 176 pp. (in Russian)

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

[8] 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

[9] A. Maurya, D. Kumar, “Reliability of safety-critical systems: A state-of-the-art review”, Quality and Reliability Engineering International, 36:7 (2020), 2547–2568 | DOI

[10] N. Rajabli, F. Flammini, R. Nardone, V. Vittorini, “Software Verification and Validation of Safe Autonomous Cars: A Systematic Literature Review”, IEEE Access, 9 (2021), 4797–4819 | DOI

[11] 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

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

[13] Y. G. Karpov, Model checking, Verification of Parallel and Distributed Program Systems, BHV-Peterburg, 2010, 560 pp. (in Russian)

[14] S. Velder, M. Lukin, A. Shalyto, B. Yaminov, Verification of Automata-Based Programs, Spb Science, 2011, 244 pp. (in Russian)

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

[16] E. Kuzmin, V. Sokolov, “Modeling, Specification and Construction of PLC-programs”, Modeling and Analysis of Information Systems, 20:2 (2013), 104–120 (in Russian) | DOI

[17] E. Kuzmin, D. Ryabukhin, V. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification”, Modeling and Analysis of Information Systems, 22:4 (2015), 507–520 (in Russian) | DOI | MR

[18] E. Kuzmin, D. Ryabukhin, V. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification”, Automatic Control and Computer Sciences, 50 (2016), 510–519 | DOI

[19] D. Ryabukhin, E. Kuzmin, V. Sokolov, “Construction of CFC-programs by LTL-specification”, Modeling and Analysis of Information Systems, 23:2 (2016), 173–184 (in Russian) | DOI | MR

[20] D. Ryabukhin, E. Kuzmin, V. Sokolov, “Construction of CFC-Programs by LTL-Specification”, Automatic Control and Computer Sciences, 51 (2017), 567–575 | DOI

[21] E. Kuzmin, “LTL-Specification of Counter Machines”, Modeling and Analysis of Information Systems, 28:1 (2021), 104–119 (in Russian) | DOI | MR | Zbl

[22] E. Kuzmin, “LTL-Specification of Bounded Counter Machines”, Modeling and Analysis of Information Systems, 29:1 (2022), 44–59 (in Russian) | DOI | MR | Zbl

[23] E. Kuzmin, V. Sokolov, “On Construction and Verification of PLC-Programs”, Modeling and Analysis of Information Systems, 19:4 (2012), 25–36 (in Russian) | DOI

[24] E. Kuzmin, V. Sokolov, “On Construction and Verification of PLC Programs”, Automatic Control and Computer Sciences, 47:7 (2013), 443–451 | DOI

[25] E. Kuzmin, V. Sokolov, “Modeling, Specification and Construction of PLC-programs”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563 | DOI

[26] E. Kuzmin, V. Sokolov, D. Ryabukhin, “Construction and Verification of PLC-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:4 (2013), 5–22 (in Russian) | DOI

[27] E. Kuzmin, V. Sokolov, D. Ryabukhin, “Construction and Verification of PLC-Programs by LTL-Specification”, Automatic Control and Computer Sciences, 49:7 (2015), 453–465 | DOI

[28] E. Kuzmin, V. Sokolov, D. Ryabukhin, “Construction and Verification of PLC LD-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:6 (2013), 78–94 (in Russian) | DOI

[29] E. Kuzmin, V. Sokolov, D. Ryabukhin, “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, 48:7 (2014), 424–436 | DOI

[30] D. Ryabukhin, E. Kuzmin, V. Sokolov, “Construction of PLC IL-programs by LTL-specification”, Modeling and Analysis of Information Systems, 21:2 (2014), 26–38 (in Russian) | DOI | MR

[31] E. Kuzmin, D. Ryabukhin, V. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90 (in Russian) | DOI

[32] E. Kuzmin, D. Ryabukhin, V. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614 | DOI

[33] IEC 61131-3.2013 Programmable controllers – Part 3: Programming languages, International Standard https://webstore.iec.ch/publication/4552

[34] A. Pnueli, “The Temporal Logic of Programs”, 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, IEEE Computer Society Press, 1977, 46–57

[35] M. Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, 1967, 317 pp. | Zbl

[36] R. Schroeppel, A Two Counter Machine Cannot Calculate $2^N$, Artificial Intelligence Memo #257, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972, 32 pp.

[37] E. V. Kuzmin, Counter Machines, in Russian, Yaroslavl State University, Yaroslavl, 2010, 127 pp.