Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System

Benjamin Martin
(LIX, Ecole Polytechnique, CNRS, Université Paris-Saclay)
Khalil Ghorbal
Eric Goubault
(LIX, Ecole Polytechnique, CNRS, Université Paris-Saclay)
Sylvie Putot
(LIX, Ecole Polytechnique, CNRS, Université Paris-Saclay)

We formally verify a hybrid control law designed to perform a station keeping maneuver for a planar vehicle. Such maneuver requires that the vehicle reaches a neighborhood of its station in finite time and remains in it while waiting for further instructions. We model the dynamics as well as the control law as a hybrid program and formally verify both the reachability and safety properties involved. We highlight in particular the automated generation of invariant regions which turns out to be crucial in performing such verification. We use the theorem prover Keymaera X to discharge some of the generated proof obligations.

In Lukas Bulwahn, Maryam Kamali and Sven Linker: Proceedings First Workshop on Formal Verification of Autonomous Vehicles (FVAV 2017), Turin, Italy, 19th September 2017, Electronic Proceedings in Theoretical Computer Science 257, pp. 91–104.
Published: 7th September 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: