Robotics and Integrated Formal Methods: Necessity meets Opportunity
Marie Farrell, Matt Luckcuck, and Michael Fisher

TL;DR
This paper argues that integrating diverse formal methods is essential for developing, verifying, and certifying complex robotic systems, and highlights robotics as a catalyst for advancing formal methods research.
Contribution
It advocates for the integration of multiple formal techniques tailored to robotic system complexities and positions robotics as a key driver for formal methods innovation.
Findings
Diverse formal techniques are necessary for complex robotic systems
Robotics can accelerate the development of integrated formal methods
Formal methods can improve verification and certification processes in robotics
Abstract
Robotic systems are multi-dimensional entities, combining both hardware and software, that are heavily dependent on, and influenced by, interactions with the real world. They can be variously categorised as embedded, cyberphysical, real-time, hybrid, adaptive and even autonomous systems, with a typical robotic system being likely to contain all of these aspects. The techniques for developing and verifying each of these system varieties are often quite distinct. This, together with the sheer complexity of robotic systems, leads us to argue that diverse formal techniques must be integrated in order to develop, verify, and provide certification evidence for, robotic systems. Furthermore, we propose the fast evolving field of robotics as an ideal catalyst for the advancement of integrated formal methods research, helping to drive the field in new and exciting directions and shedding light…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
