Verification of declarative LTL-specification of control programs behavior
https://doi.org/10.18255/1818-1015-2024-2-120-141
Abstract
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.
About the Authors
Maxim V. NeyzovRussian Federation
Egor V. Kuzmin
Russian Federation
References
1. D. J. Smith and K. G. L. Simpson, The Safety Critical Systems Handbook, 5th ed. Butterworth-Heinemann, 2020.
2. 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, doi: 10.1109/TCAD.2008.923410.
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: 10.1007/s10796-022-10252-x.
4. E. A. Lee and S. A. Seshia, Introduction to Embedded Systems -- A Cyber-Physical Systems Approach, 2nd ed. MIT Press, 2017.
5. M. V. Neyzov and E. V. Kuzmin, “LTL-specification for Development and Verification of Control Programs,” Modeling and Analysis of Information Systems, vol. 30, no. 4, pp. 308–339, 2023, doi: 10.18255/1818-1015-2023-4-308-339.
6. D. Harel and A. Pnueli, “On the Development of Reactive Systems,” in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477–498, doi: 10.1007/978-3-642-82453-1_17.
7. 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, doi: 10.1007/BFb0027047.
8. “IEC 61131-3:2013 Programmable controllers -- Part 3: Programming languages.” [Online]. Available: https://webstore.iec.ch/publication/4552.
9. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed. Springer Publishing Company, Incorporated, 2018.
10. E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002, p. 416.
11. D. Beyer and A. Podelski, “Software model checking: 20 years and beyond,” in Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, Springer, 2022, pp. 554–582.
12. “nuXmv Home.” [Online]. Available: https://nuxmv.fbk.eu/.
13. “IEC 61131-1:2003 Programmable controllers -- Part 1: General information.” [Online]. Available: https://webstore.iec.ch/publication/4550.
14. B. Alpern and F. B. Schneider, “Defining Liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181–185, 1985, doi: 10.1016/0020-0190(85)90056-0.
15. Z. Manna and A. Pnueli, “A Hierarchy of Temporal Properties,” in Proceedings of the ninth annual ACM symposium on Principles of distributed computing, 1990, pp. 377–410, doi: 10.1145/93385.93442.
16. “Spot Home.” [Online]. Available: https://spot.lre.epita.fr/.
17. “nuXmv User Manual.” [Online]. Available: https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf.
18. D. Park, “Concurrency and Automata on Infinite Sequences,” in Theoretical Computer Science: 5th GI-Conference Karlsruhe, 1981, vol. 104, pp. 167–183, doi: 10.1007/BFb0017309.
Review
For citations:
Neyzov M.V., Kuzmin E.V. Verification of declarative LTL-specification of control programs behavior. Modeling and Analysis of Information Systems. 2024;31(2):120-141. (In Russ.) https://doi.org/10.18255/1818-1015-2024-2-120-141