View article

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 …