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.