Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
Simon Foster, Mario Gleirscher, Radu Calinescu
TL;DR
The paper tackles safety guarantees for autonomous marine vehicles by bridging simulation-based validation with formal deductive verification. It presents a pipeline that translates an Octave-based hybrid AMV model into Isabelle/HOL via $\textsf{d}\mathcal{H}$, extending the framework to support matrices and discrete state for modular proofs. A case study on the AMV C-Worker 5 demonstrates verification of obstacle-avoidance properties, including invariants such as collinearity of $\bm{a}$ and $\bm{v}$, using a differential Hoare-style approach and automated tactics like $dInduct$. The work illustrates that Isabelle provides a flexible, library-rich environment capable of integrating numerical computations with rigorous hybrid-system proofs, offering a path toward stronger safety guarantees for autonomous marine systems.
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.