Document Open Access Logo

Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL

Authors Fang Yan , Benoît Ballenghien , Simon Foster , Ana Cavalcanti , James Baxter , Burkhart Wolff

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.10.pdf
  • Filesize: 0.89 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • process algebra
  • Isabelle/HOL
  • automated proof methods
  • deadlock freedom

Metrics

Abstract

We present a theorem-proving-based technique for verifying deadlock freedom of CSP-style concurrent models in Isabelle/HOL. The approach addresses challenges that are difficult to handle using model checking alone, including infinite state spaces, compositional reasoning in the presence of shared variables, and the need for mechanised proofs. Our main contribution is a coinductive characterisation of deadlock freedom that is equivalent to the standard CSP refinement-based definition, but is more amenable to automated reasoning in an interactive theorem prover. To support reasoning about shared variables, we introduce an assume–guarantee strategy that enforces invariants within transition semantics. The technique is generally applicable to CSP specifications that model shared variables using standard CSP constructs. In particular, we consider the semantics of RoboChart, a domain-specific modelling language for robotic control software, which we mechanise in Isabelle via a shallow embedding in HOL-CSP, and implement automated proof methods. The approach is evaluated on three case studies, including two RoboChart models of industrial robotic systems.

Cite As Get BibTex

Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter, and Burkhart Wolff. Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.10

Author Details

Fang Yan
  • University of York, UK
Benoît Ballenghien
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, France
Simon Foster
  • University of York, UK
Ana Cavalcanti
  • University of York, UK
James Baxter
  • University of York, UK
Burkhart Wolff
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, France

Funding

The work is partially funded by the UK EPSRC Grants EP/R025479/1 and EP/V026801/2, by the Royal Academy of Engineering Grants No CiET1719/45 and IF2122$$1183 and by the RoboSAPIENS project funded by the European Commission’s Horizon Europe programme under grant agreement number 101133807.

Supplementary Materials

References

  1. Jean-Raymond Abrial. The B-book. Assigning Programs to Meaning, to be published, 1996. Google Scholar
  2. Étienne André, Shuang Liu, Yang Liu, Christine Choppy, Jun Sun, and Jin Song Dong. Formalizing UML state machines for automated verification-A survey. ACM Computing Surveys, 55(13s):1-47, 2023. URL: https://doi.org/10.1145/3579821.
  3. Pedro Antonino, Augusto Sampaio, and Jim Woodcock. A refinement based strategy for local deadlock analysis of networks of csp processes. In International Symposium on Formal Methods, pages 62-77. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06410-9_5.
  4. Benoît Ballenghien, Safouan Taha, and Burkhart Wolff. HOL-CSPM - Architectural operators for HOL-CSP. Archive of Formal Proofs, December 2023. , Formal proof development. URL: https://isa-afp.org/entries/HOL-CSPM.html.
  5. Benoît Ballenghien, Safouan Taha, Burkhart Wolff, and Lina Ye. HOL-CSP Version 2.0. Archive of Formal Proofs, April 2019. , Formal proof development. URL: https://isa-afp.org/entries/HOL-CSP.html.
  6. Michael Balser, Simon Bäumler, Alexander Knapp, Wolfgang Reif, and Andreas Thums. Interactive verification of UML state machines. In International Conference on Formal Engineering Methods, pages 434-448. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30482-1_36.
  7. Michael Balser, Wolfgang Reif, Gerhard Schellhorn, and Kurt Stenzel. KIV 3.0 for provably correct systems. In International Workshop on Current Trends in Applied Formal Methods, pages 330-337. Springer, 1998. URL: https://doi.org/10.1007/3-540-48257-1_23.
  8. James Baxter, Bert Van Acker, Morten Kristensen, Thomas Wright, Ana Cavalcanti, and Cláudio Gomes. Formal architectural patterns for adaptive robotic software. In International Conference on Fundamental Approaches to Software Engineering, pages 145-165. Springer Nature Switzerland Cham, 2025. Google Scholar
  9. Ana Cavalcanti, Madiel Conserva Filho, Pedro Ribeiro, and Augusto Sampaio. Laws of timed state machines. The Computer Journal, 67(6):2066-2107, 2024. URL: https://doi.org/10.1093/COMJNL/BXAD124.
  10. P. Crisafulli, S. Taha, and B. Wolff. Modeling and analysing cyber-physical systems in HOL-CSP. Robotics and Autonomous Systems, 170, 2023. Google Scholar
  11. F. Falcao, L. Lima, A. Sampaio, and P. Antonino. A formal component model for UML based on CSP aiming at compositional verification. Software and Systems Modeling, 2024. Google Scholar
  12. Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff. Isabelle/circus: A process specification and verification environment. In International Conference on Verified Software: Tools, Theories, Experiments, pages 243-260. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-27705-4_20.
  13. Simon Foster, James Baxter, Ana Cavalcanti, Alvaro Miyazawa, and Jim Woodcock. Automating verification of state machines with reactive designs and Isabelle/UTP. In International Conference on Formal Aspects of Component Software, pages 137-155. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02146-7_7.
  14. Simon Foster, Chung-Kil Hur, and Jim Woodcock. Formally verified simulations of state-rich processes using interaction trees in Isabelle/HOL. arXiv preprint arXiv:2105.05133, 2021. URL: https://arxiv.org/abs/2105.05133.
  15. Simon Foster, Yakoub Nemouchi, Colin O'Halloran, Karen Stephenson, and Nick Tudor. Formal model-based assurance cases in Isabelle/SACM: An autonomous underwater vehicle case study. In Proceedings of the 8th International Conference on Formal Methods in Software Engineering, pages 11-21, 2020. URL: https://doi.org/10.1145/3372020.3391559.
  16. T. Gibson-Robinson, P. Armstrong, A. Boulgakov, and A. W. Roscoe. FDR3 - A Modern Refinement Checker for CSP. In Tools and Algorithms for the Construction and Analysis of Systems, pages 187-201, 2014. Google Scholar
  17. Steffen Helke and Florian Kammuller. Verification of statecharts using data abstraction. International Journal of Advanced Computer Science and Applications, 7(1), 2016. Google Scholar
  18. Yoshinao Isobe and Markus Roggenbach. CSP-Prover—A proof tool for the verification of scalable concurrent systems. Information and Media Technologies, 5(1):32-39, 2010. URL: https://doi.org/10.11185/IMT.5.32.
  19. Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 5(4):596-619, 1983. URL: https://doi.org/10.1145/69575.69577.
  20. Jeffrey O Kephart and David M Chess. The vision of autonomic computing. Computer, 36(1):41-50, 2003. URL: https://doi.org/10.1109/MC.2003.1160055.
  21. Dimitrios S Kolovos, Richard F Paige, and Fiona AC Polack. The epsilon object language (EOL). In European conference on model driven architecture-foundations and applications, pages 128-142. Springer, 2006. Google Scholar
  22. Kevin Lano, David Clark, and Kelly Androutsopoulos. UML to B: Formal verification of object-oriented models. In International Conference on Integrated Formal Methods, pages 187-206. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24756-2_11.
  23. Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, and Jon Timmis. Automatic property checking of robotic applications. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 3869-3876, 2017. URL: https://doi.org/10.1109/IROS.2017.8206238.
  24. Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, Jon Timmis, and Jim Woodcock. RoboChart: modelling and verification of the functional behaviour of robotic applications. Software and Systems Modeling, 18(5):3097-3149, 2019. URL: https://doi.org/10.1007/s10270-018-00710-z.
  25. Alvaro Miyazawa, Pedro Ribeiro, Kangfeng Ye, Ana Cavalcanti, Wei Li, Jim Woodcock, and Jon Timmis. Robochart reference manual, 2021. URL: https://robostar.cs.york.ac.uk/publications/techreports/reports/robochart-reference.pdf.
  26. Karla Morris, Colin Snook, Thai Son Hoang, Geoffrey Hulette, Robert Armstrong, and Michael Butler. Formal verification and validation of run-to-completion style state charts using Event-B. Innovations in Systems and Software Engineering, 18(4):523-541, 2022. URL: https://doi.org/10.1007/S11334-021-00416-4.
  27. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  28. M. V. M. Oliveira, P. Antonino, R. Ramos, A. Sampaio, A. Mota, and A. W. Roscoe. Rigorous development of component-based systems using component metadata and patterns. Formal Aspects of Computing, 2016. Google Scholar
  29. Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. A UTP semantics for Circus. Formal Aspects of Computing, 21(1):3-32, 2009. URL: https://doi.org/10.1007/S00165-007-0052-5.
  30. Sam Owre, John M Rushby, and Natarajan Shankar. PVS: A prototype verification system. In International Conference on Automated Deduction, pages 748-752. Springer, 1992. URL: https://doi.org/10.1007/3-540-55602-8_217.
  31. A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, 1998. Google Scholar
  32. Louis M Rose, Richard F Paige, Dimitrios S Kolovos, and Fiona AC Polack. The Epsilon Generation Language. In European conference on model driven architecture-foundations and applications, pages 1-16. Springer, 2008. Google Scholar
  33. Colin Snook, Vitaly Savicks, and Michael Butler. Verification of uml models by translation to uml-b. In International Symposium on Formal Methods for Components and Objects, pages 251-266. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-25271-6_13.
  34. J Michael Spivey and Jean-Raymond Abrial. The Z notation, volume 29. Prentice Hall Hemel Hempstead, 1992. Google Scholar
  35. S. Taha, B. Wolff, and L. Ye. Philosophers may dine - definitively! In Proc. 16th Intl. Conf. on Integrated Formal Methods, LNCS. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-63461-2_23.
  36. Jim Woodcock, Ana Cavalcanti, Simon Foster, Marcel Oliveira, Augusto Sampaio, and Frank Zeyda. Utp, circus, and isabelle. In Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, pages 19-51. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-40436-8_2.
  37. Jim Woodcock and Jim Davies. Using Z: specification, refinement, and proof. Prentice-Hall, Inc., 1996. Google Scholar
  38. Fang Yan, Simon Foster, and Ibrahim Habli. Automated compositional verification for robotic state machines using Isabelle/HOL. In 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS), pages 167-176. IEEE, 2023. URL: https://doi.org/10.1109/ICECCS59891.2023.00029.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact