Guaranteed safe controller synthesis for switched systems using analytical solutions

In this paper we present a method for synthesizing safe controllers for continuous-time sampled switched systems, where the analytical solution for the state trajectories is available. The method creates integer-valued lower and upper bounds on the evolution of the system, so that the tool Uppaal Tiga can be used to synthesize a guaranteed safe controller for the continuous system. We compare our method to the Euler method, which our method is based upon, using two case studies covering cruise control and management of storm water detention ponds. The cruise control example shows that the proposed method can obtain tighter bounds, allowing the controller to be less conservative. The industrial case study on storm water detention ponds shows that we can obtain reasonable bounds in situations where the Euler method fails to obtain them.