Title
Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
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.
Year
DOI
Venue
2020
10.1109/ICECCS51672.2020.00020
2020 25th International Conference on Engineering of Complex Computer Systems (ICECCS)
Keywords
DocType
ISBN
theorem proving,dynamical systems,autonomous vehicles,control systems,assurance cases
Conference
978-1-7281-8559-0
Citations 
PageRank 
References 
0
0.34
0
Authors
3
Name
Order
Citations
PageRank
Foster Simon100.34
Mario Gleirscher25711.88
Radu Calinescu390563.01