Верификация декларативной LTL-спецификации поведения управляющих программ

Статья продолжает цикл трудов по разработке и верификации управляющих программ на основе LTL-спецификаций специального вида. Ранее была предложена декларативная LTL-спецификация, позволяющая описывать поведение управляющих программ и выполнять построение по ней программного кода на императивном языке ST для программируемых логических контроллеров. Данная LTL-спецификация может быть непосредственно верифицирована на предмет соответствия заданным темпоральным свойствам методом проверки модели (model checking) с помощью инструмента символьной верификации nuXmv. При этом не требуется переводить LTL-формулы спецификации в другой формализм — SMV-спецификацию (код на входном языке инструмента nuXmv). Цель настоящей работы состоит в исследовании альтернативных способов представления модели поведения программы, соответствующей декларативной LTL-спецификации, при её верификации в рамках инструментального средства nuXmv. В статье выполняются преобразования декларативной LTL-спецификации в различные SMV-спецификации с сопутствующими изменениями постановки задачи верификации, что приводит к значительному снижению временных затрат при проверке темпоральных свойств с использованием инструмента nuXmv. Ускорение верификации обусловлено сокращением пространства состояний проверяемой модели. Полученные в результате предложенных преобразований SMV-спецификации задают одинаковые или бисимуляционно эквивалентные системы переходов, обеспечивая неизменность результатов верификации при замене одной SMV-спецификации на другую.

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.