Использование симметрии при программировании и верификации арбитра ресурсов

Большое пространство состояний программ затрудняет или делает невозможной их непосредственную верификацию методом проверки модели (model checking). Наличие симметрии в программе достаточно часто позволяет упростить модель и сократить её пространство состояний, что приводит к значительному снижению времени верификации. Классический подход состоит в обнаружении группы симметрии и построении на её основе фактормодели — упрощённой модели для верификации. Однако не все инструменты имеют поддержку симметрии, а инструменты с такой поддержкой не всегда справляются с поставленной задачей, так как поиск подходящей группы симметрии является вычислительно сложной задачей.

В работе предлагается альтернативный классическому подход к разработке программ, основанный на явном выделении симметрии. В программе выделяется ядро — координационный центр, который работает с учётом симметрии и отвечает за выполнимость заданных темпоральных свойств. Ядро координирует вычисления, вынесенные за его пределы — в обвязку ядра. В связи с этим ядро имеет небольшое пространство состояний, заменяет собой фактормодель и может быть верифицировано инструментом проверки модели без поддержки симметрии. Обвязка не может вмешиваться в работу верифицированного ядра и нарушать его свойства. Подход продемонстрирован на примере разработки и верификации арбитра ресурсов марсохода. Арбитр координирует доступ n процессов к m ресурсам, где n и m — натуральные числа. Используются язык программирования C/C++ и инструмент проверки модели Spin. Модель поведения ядра автоматически извлекается верификатором Spin из C-кода. Проверке подлежат темпоральные свойства, выраженные с помощью линейной темпоральной логики LTL.

1. D. Harel and A. Pnueli, “On the Development of Reactive Systems”, in Logics and Models of Concurrent Systems, vol. 13, 1985, pp. 477–498. doi: 10.1007/978-3-642-82453-1_17.

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

3. K. Schneider, J. Shabolt, and J. G. Taylor, Verification of Reactive Systems: Formal Methods and Algorithms (Texts in Theoretical Computer Science), 1st edition. Springer, 2004, isbn: 978-3-540-00296-3. doi: 10.1007/978-3-662-10778-2.

4. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st edition. Springer, 2018, p. 1212, isbn: 978-3-319-10574-1. doi: 10.1007/978-3-319-10575-8.

5. E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002, p. 416, translated from English to Russian, isbn: 5-94057-054-2.

6. C. Baier and J.-P. Katoen, Principles of Model Checking. MIT Press, 2008, p. 975, isbn: 978-0-262-02649-9.

7. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Progress on the State Explosion Problem in Model Checking”, in Informatics: 10 Years Back, 10 Years Ahead, ser. LNCS, vol. 2000, 2001, pp. 176–194. doi: 10.1007/3-540-44577-3_12.

8. E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla, “Symmetry Reductions in Model Checking”, in Computer Aided Verification, 1998, pp. 147–158. doi: 10.1007/BFb0028741.

9. E. M. Clarke, R. Enders, T. Filkorn, and S. Jha, “Exploiting Symmetry in Temporal Logic Model Checking”, Formal Methods in System Design, vol. 9, no. 1–2, pp. 77–104, 1996. doi:10.1007/BF00625969.

10. A. Miller, A. Donaldson, and M. Calder, “Symmetry in Temporal Logic Model Checking”, ACM Computing Surveys, vol. 38, no. 3, pp. 1–36, 2006. doi: 10.1145/1132960.1132962.

11. E. A. Emerson and A. P. Sistla, “Symmetry and Model Checking”, Formal Methods in System Design, vol. 9, no. 1, pp. 105–131, 1996. doi: 10.1007/BF00625970.

12. S. Barner and O. Grumberg, “Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking”, in International Conference on Computer Aided Verification, 2002, pp. 93–106. doi: 10.1007/3-540-45657-0_8.

13. D. Tang, S. Malik, A. Gupta, and C. N. Ip, “Symmetry Reduction in SAT-Based Model Checking”, in International Conference on Computer Aided Verification, ser. LNCS, vol. 3576, 2005, pp. 125–138. doi: 10.1007/11513988_12.

14. A. P. Sistla, “Employing Symmetry Reductions in Model Checking”, Computer Languages, Systems & Structures, vol. 30, no. 3-4, pp. 99–137, 2004. doi: 10.1016/j.cl.2004.02.002.

15. C. N. Ip and D. L. Dill, “Better Verification Through Symmetry”, in Computer Hardware Description Languages and their Applications, 1993, pp. 97–111. doi: 10.1016/B978-0-444-81641-2.50012-5.

16. S. J. Zhang, J. Sun, C. Sun, Y. Liu, J. Ma, and J. S. Dong, Symmetry Detection for Model Checking, 2013.

17. M. Leuschel and T. Massart, “Efficient Approximate Verification of B and Z Models via Symmetry Markers”, Annals of Mathematics and Artificial Intelligence, vol. 59, no. 1, pp. 81–106, 2010. doi: 10.1007/s10472-010-9208-8.

18. A. P. Sistla, V. Gyuris, and E. A. Emerson, “SMC: A Symmetry-Based Model Checker for Verification of Safety and Liveness Properties”, ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 9, no. 2, pp. 133–166, 2000. doi: 10.1145/350887.350891.

19. A. P. Sistla and P. Godefroid, “Symmetry and Reduced Symmetry in Model Checking”, ACM Transactions on Programming Languages and Systems, vol. 26, no. 4, pp. 702–734, 2004. doi: 10.1145/1011508.1011511.

20. A. F. Donaldson and A. Miller, “Automatic Symmetry Detection for Model Checking Using Computational Group Theory”, in International Symposium on Formal Methods, 2005, pp. 481–496. doi: 10.1007/11526841_32.

21. I. Valkov, A. F. Donaldson, and A. Miller, “Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking”, in International Symposium on Model Checking Software, Springer, 2024, pp. 49–66. doi: 10.1007/978-3-031-66149-5_3.

22. A. F. Donaldson and A. Miller, “Exact and Approximate Strategies for Symmetry Reduction in Model Checking”, in International Symposium on Formal Methods, 2006, pp. 541–556. doi: 10.1007/11813040_

23. T. Gibson-Robinson and G. Lowe, “Symmetry Reduction in CSP Model Checking”, International Journal on Software Tools for Technology Transfer, vol. 21, no. 5, pp. 567–605, 2019. doi:10.1007/s10009-019-00516-4.

24. M. M. Jaghoori, M. Sirjani, M. R. Mousavi, E. Khamespanah, and A. Movaghar, “Symmetry and Partial Order Reduction Techniques in Model Checking Rebeca”, Acta Informatica, vol. 47, no. 1, pp. 33–66, 2010. doi: 10.1007/s00236-009-0111-x.

25. M. Leuschel, M. Butler, C. Spermann, and E. Turner, “Symmetry Reduction for B by Permutation Flooding”, in International Conference of B Users, vol. 4355, 2007, pp. 79–93. doi: 10.1007/11955757_9.

26. L. Antuña, D. Araiza-Illan, S. Campos, and K. Eder, “Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms”, in Towards Autonomous Robotic Systems, vol. 9287, 2015, pp. 26–37. doi: 10.1007/978-3-319-22416-9_4.

27. I. Buzhinsky and A. Pakonen, “Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions”, IEEE Access, vol. 7, 162139–162156, 2019. doi: 10.1109/ACCESS.2019.2951938.

28. I. Buzhinsky and A. Pakonen, “Symmetry Breaking in Model Checking of Fault-Tolerant Nuclear Instrumentation and Control Systems”, IEEE Access, vol. 8, 197684–197694, 2020. doi:10.1109/ACCESS.2020.3034799.

29. E. M. Clarke and E. A. Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic”, in 25 Years of Model Checking: History, Achievements, Perspectives, ser. LNCS, vol. 5000, 2008, pp. 196–215, isbn: 978-3-540-69849-4. doi: 10.1007/978-3-540-69850-0_12.

30. D. Park, “Concurrency and Automata on Infinite Sequences”, in Theoretical Computer Science: 5th GI-Conference Karlsruhe, vol. 104, 1981, pp. 167–183. doi: 10.1007/BFb0017309.

31. G. J. Holzmann and R. Joshi, “Model-Driven Software Verification”, in International SPIN Workshop on Model Checking of Software, Springer, vol. 2989, 2004, pp. 76–91. doi: 10.1007/978-3-540-24732-6_6.

32. V. M. Glushkov, The Synthesis of Digital Automata. Moscow: PhisMathGis, 1962, p. 476, in Russian.

33. M. V. Neyzov and E. V. Kuzmin, “LTL-Specification for Development and Verification of Logical Control Programs in Feedback Systems”, Modeling and Analysis of Information Systems, vol. 31, no. 3, pp. 240–279, 2024. doi: 10.18255/1818-1015-2024-3-240-279.

34. G. Holzmann, SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley, 2003, p. 608, isbn: 0-321-22862-6.