Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2020
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913745928716288 |
|---|---|
| author | Foster, Simon Gleirscher, Mario Calinescu, Radu |
| author_facet | Foster, Simon Gleirscher, Mario Calinescu, Radu |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2006_09233 |
| institution | arXiv |
| publishDate | 2020 |
| record_format | arxiv |
| spellingShingle | Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles Foster, Simon Gleirscher, Mario Calinescu, Radu Software Engineering Systems and Control 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. |
| title | Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles |
| topic | Software Engineering Systems and Control |
| url | https://arxiv.org/abs/2006.09233 |