Provably Safe Controller Synthesis Using Safety Proofs as Building Blocks

We describe an approach to developing a verified controller using hybrid system safety predicates. It selects from a dictionary of sequences of control actions, interleaving them and under model assumptions guaranteeing their continuing safety in unbounded time. The controller can adapt to changing priorities and objectives during operation. It can confer safety guarantees on a primary controller, identifying, intervening, and remediating actions that might lead to unsafe conditions in the future. Remediation is delayed until the latest time at which a safety-preserving intervention is available. When the assumptions of the safety proofs are violated, the controller provides altered but quantifiable safety guarantees. We apply this approach to synthesize a controller for aircraft collision avoidance, and report on the performance of this controller as a stand-alone collision avoidance system, and as a safety controller for the FAA’s next-generation aircraft collision avoidance system ACAS X.