An Adaptive, Provable Correct Simplex Architecture

Simplex architectures optimize performance and safety by switching between an advanced controller and a base controller.
We propose an approach to synthesize the switching logic and extensions of the base controller in the Simplex architectures
to achieve high performance and provable correctness for a rich class of temporal specifications by maximizing the time the
advanced controller is active. We achieve provable correctness by performing static verification of the baseline controller.
The result of this verification is a set of states that is proven to be safe, called the recoverable region. We employ proofs
on demand to ensure that the base controller is safe in those states that are visited during runtime, which depends on the
advanced controller. Verification of hybrid systems is often overly conservative, resulting in smaller recoverable regions that
cause unnecessary switches to the baseline controller. To avoid these switches, we invoke targeted reachability queries to
extend the recoverable region at runtime. In case the recoverable region cannot be extended using the baseline controller, we
employ a repair procedure. This tries to synthesize a patch for the baseline controller and can further extend the recoverable
region. Our offline and online verification relies upon reachability analysis since it allows observation-based extension of
the known recoverable region. We implemented our methodology on top of the state-of-the-art tool HyPro which allowed us
to automatically synthesize verified and performant Simplex architectures for advanced case studies, like safe autonomous
driving on a race track.