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 Simon | 1 | 0 | 0.34 |
Mario Gleirscher | 2 | 57 | 11.88 |
Radu Calinescu | 3 | 905 | 63.01 |