A simplex architecture for hybrid systems using barrier certificates

This paper shows how to use Barrier Certificates (BaCs) to design Simplex Architectures for hybrid systems. The Simplex architecture entails switching control of a plant over to a provably safe Baseline Controller when a safety violation is imminent under the control of an unverified Advanced Controller. A key step of determining the switching condition is identifying a recoverable region, where the Baseline Controller guarantees recovery and keeps the plant invariably safe. BaCs, which are Lyapunov-like proofs of safety, are used to identify a recoverable region. At each time step, the switching logic samples the state of the plant and uses bounded-time reachability analysis to conservatively check whether any states outside the zero-level set of the BaCs, which therefore might be non-recoverable, are reachable in one decision period under control of the Advanced Controller. If so, failover is initiated. Our approach of using BaCs to identify recoverable states is computationally cheaper and potentially more accurate (less conservative) than existing approaches based on state-space exploration. We apply our technique to two hybrid systems: a water tank pump and a stop-sign-obeying controller for a car.