Using verified control envelopes for safe controller design

This paper concerns the use of formal methods to design controllers for dynamic systems such that the closed-loop system satisfies given safety specifications. The usual approach to using formal methods for control applications is to verify safety for an abstraction of the closed-loop system using a candidate controller. We propose an alternative approach. The formal method is applied first to verify the safety of an entire class of possible controllers characterized by a nondeterministic input-output mapping call a control envelope. Safety of candidate controllers can then be verified by showing they are a refinement of the control envelope over an invariant set, rather than verifying the entire closed-loop system. Alternatively, the control envelope can be incorporated as an additional set of constraints directly in the controller synthesis procedure. Furthermore, this approach allows the designer to evaluate parameter trade-offs. Checking that the control envelope is satisfied is a static check on the input-output relation of the controller, rather than a dynamic check of closed-loop properties. The method is developed using differential dynamic logic (dL) and the associated theorem prover KeYMaera as the formal method and illustrated for an example of designing a safe strategy for an automotive cooperative intersection collision avoidance system for stop-sign assist (CICAS-SSA).