Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
arXiv:2006.09233 · doi:10.1109/ICECCS51672.2020.00020
Abstract
The use of autonomous vehicles in real-world applications is often precluded by the difficulty of providing safety guarantees for their complex controllers. The simulation-based testing of these controllers cannot deliver sufficient safety guarantees, and the use of formal verification is very challenging due to the hybrid nature of the autonomous vehicles. Our work-in-progress paper introduces a formal verification approach that addresses this challenge by integrating the numerical computation of such a system (in GNU/Octave) with its hybrid system verification by means of a proof assistant (Isabelle). To show the effectiveness of our approach, we use it to verify differential invariants of an Autonomous Marine Vehicle with a controller switching between multiple modes.
References in corpus (5)
- Formal Verification of Obstacle Avoidance and Navigation of Ground Robots
- Robotics and Integrated Formal Methods: Necessity meets Opportunity
- New Opportunities for Integrated Formal Methods
- Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP
- Deeply Integrating C11 Code Support into Isabelle/PIDE