LTL-specification for development and verification of control programs

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.

1. S. Oks, M. Jalowski, M. Lechner, and others, “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook,” Inf. Systems Frontiers, 2022, doi: 10.1007/s10796-022-10252-x.

2. E. A. Lee and S. A. Seshia, Introduction to Embedded Systems -- A Cyber-Physical Systems Approach, 2nd ed. MIT Press, 2017.

3. E. A. Parr, Programmable Controllers. An Engineer’s Guide, 3rd ed. Newnes, 2003.

4. V. N. Lifshic and L. E. Sadovskii, “Algebraic Models of Computing Machines,” UMN, vol. 27, no. 3(165), pp. 79–125, 1972.

5. K.-Y. Cai, T. Y. Chen, and T. H. Tse, “Towards Research on Software Cybernetics,” in Proceedings of 7th IEEE International on High-assurance Systems Engineering (HASE 2002), 2002, pp. 240–241.

6. N. I. Polikarpova and A. A. Shalyto, Automata-Based Programming, 2nd ed. Spb.: Piter, 2011.

7. D. Harel and A. Pnueli, “On the Development of Reactive Systems,” in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477–498.

8. A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends,” in Current Trends in Concurrency, 1986, vol. 224, pp. 510–584.

9. A. Maurya and D. Kumar, “Reliability of safety‐critical systems: A state‐of‐the‐art review,” Quality and Reliability Engineering International, vol. 36, no. 7, pp. 2547–2568, 2020.

10. N. Rajabli, F. Flammini, R. Nardone, and V. Vittorini, “Software Verification and Validation of Safe Autonomous Cars: A Systematic Literature Review,” in IEEE Access, 2021, vol. 9, pp. 4797–4819.

11. V. D'Silva, D. Kroening, and G. Weissenbacher, “A Survey of Automated Techniques for Formal Software Verification,” in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008, vol. 27, no. 7, pp. 1165–1178.

12. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed. Springer Publishing Company, Incorporated, 2018.

13. Y. G. Karpov, Model checking. Verification of Parallel and Distributed Program Systems. BHV-Peterburg, 2010.

14. S. Velder, M. Lukin, A. Shalyto, and B. Yaminov, Verification of Automata-Based Programs. Spb Science, 2011.

15. E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002.

16. E. V. Kuzmin and V. A. Sokolov, “Modeling, Specification and Construction of PLC-programs,” Modeling and Analysis of Information Systems, vol. 20, no. 2, pp. 104–120, 2013.

17. E. V. Kuzmin and V. A. Sokolov, “Modeling, Specification and Construction of PLC-programs,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 554–563, 2014.

18. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC-programs by LTL-specification,” Modeling and Analysis of Information Systems, vol. 20, no. 4, pp. 5–22, 2013.

19. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC-Programs by LTL-Specification,” Automatic Control and Computer Sciences, vol. 49, no. 7, pp. 453–465, 2015.

20. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC LD-programs by LTL-specification,” Modeling and Analysis of Information Systems, vol. 20, no. 6, pp. 78–94, 2013.

21. E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, “Construction and Verification of PLC LD Programs by the LTL Specification,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 424–436, 2014.

22. D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, “Construction of PLC IL-programs by LTL-specification,” Modeling and Analysis of Information Systems, vol. 21, no. 2, pp. 26–38, 2014.

23. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors,” Modeling and Analysis of Information Systems, vol. 21, no. 4, pp. 75–90, 2014.

24. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “Modeling a Consistent Behavior of PLC-Sensors,” Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 602–614, 2014.

25. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification,” Modeling and Analysis of Information Systems, vol. 22, no. 4, pp. 507–520, 2015.

26. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, “On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification,” Automatic Control and Computer Sciences, vol. 50, pp. 510–519, 2016.

27. D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, “Construction of CFC-programs by LTL-specification,” Modeling and Analysis of Information Systems, vol. 23, no. 2, pp. 173–184, 2016.

28. D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, “Construction of CFC-Programs by LTL-Specification,” Automatic Control and Computer Sciences, vol. 51, pp. 567–575, 2017.

29. E. V. Kuzmin, “LTL-Specification of Counter Machines,” Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104–119, 2021.

30. E. V. Kuzmin, “LTL-Specification of Bounded Counter Machines,” Modeling and Analysis of Information Systems, vol. 29, no. 1, pp. 44–59, 2022.

31. E. V. Kuzmin and V. A. Sokolov, “On Construction and Verification of PLC-Programs,” Modeling and Analysis of Information Systems, vol. 19, no. 4, pp. 25–36, 2012.

32. E. V. Kuzmin and V. A. Sokolov, “On Construction and Verification of PLC Programs,” Automatic Control and Computer Sciences, vol. 47, no. 7, pp. 443–451, 2013.

33. “IEC 61131-3:2013 Programmable controllers -- Part 3: Programming languages.” [Online]. Available: https://webstore.iec.ch/publication/4552.

34. A. Pnueli, “The Temporal Logic of Programs,” in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), 1977, pp. 46–57.

35. M. L. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, 1967.

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

37. E. V. Kuzmin, Counter Machines. Yaroslavl State University, 2010.