Preview

Modeling and Analysis of Information Systems

Advanced search

Verification of declarative LTL-specification of control programs behavior

https://doi.org/10.18255/1818-1015-2024-2-120-141

Abstract

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.

About the Authors

Maxim V. Neyzov
Institute of Automation and Electrometry SB RAS
Russian Federation


Egor V. Kuzmin
P.G. Demidov Yaroslavl State University
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

Views: 315


Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)