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

TL;DR

This paper presents a formal verification method for a hybrid control law enabling a planar vehicle to achieve and maintain station keeping, ensuring safety and reachability through automated invariant generation and theorem proving.

Contribution

It introduces a formal verification framework for hybrid control laws, emphasizing automated invariant generation and the use of Keymaera X for proof obligations.

Findings

Successful verification of reachability and safety properties

Automated generation of invariant regions is effective

The approach enhances reliability of station keeping maneuvers

Abstract

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.