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

Benjamin Martin (1) , Khalil Ghorbal (2) , Eric Goubault (1) , Sylvie Putot (1)

1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques

In this case study paper, we investigate the formal verification of 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 commands. We model the dynamics as well as the control law as a hybrid program and formally verify 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 hybrid system theorem prover KeymaeraX to formally check the parts of the proof that can be automatized in the current state of the tool.

Domaines: Théorie et langage formel [cs.FL]

Benjamin Martin, Khalil Ghorbal, Eric Goubault, Sylvie Putot. Formal Verification of Station Keeping Maneuvers for a Planar Autonomous Hybrid System. FVAV 2017 - 1st Formal Verification of Autonomous Vehicles Workshop, Sep 2017, Turin, Italy. pp.91--104, ⟨10.4204/EPTCS.257.9⟩. ⟨hal-01657848⟩