By the same authors

Towards Formal Verification of Control Algorithms for Autonomous Marine Vehicles

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Full text download(s)

Links

Author(s)

Department/unit(s)

Publication details

Title of host publicationProceeding of the 25th International Conference on Engineering of Complex Computer Systems (ICECCS 2020)
DateAccepted/In press - 2 Aug 2020
Number of pages6
PublisherIEEE
Original languageEnglish

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.

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations