Using Symmetry in Programming and Verification of a Resource Arbiter

The large states pace of programs makes their direct verification by model checking difficult or impossible. The presence of symmetry in a program often allows simplifying the model and reducing its state space, leading to significant decrease of verification time. The classical approach consists in detecting a symmetry group and constructing a quotient model based on it — a simplified model for verification purposes. However, not all tools provide support for symmetry, and those that do may still struggle because finding an appropriate symmetry group is computationally complex problem.

This work proposes an approach to program development based on explicit symmetry exploitation, which is an alternative to the classical one. In the program, a core is extracted — a coordination center working under consideration of symmetry and responsible for ensuring temporal properties. The core coordinates computations outside itself — those placed in the wrapper surrounding the core. As a result, the core has a small state space, replace the quotient model and allows verification using a model checker without symmetry support. The wrapper cannot interfere in the operation of the verified core and violate its properties. The approach is demonstrated by the example of the development and verification of the Mars rover resource arbiter. The arbiter coordinates access of n processes to m resources where both n and m are natural numbers. Programming languages C/C++ and the Spin model checker tool are used. The behavioral model of the core is automatically extracted by the Spin tool from the C code. Temporal properties expressed via Linear Temporal Logic (LTL) are subject to verification.

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.