  We present a new method for the automated synthesis of safe and robust
Proportional-Integral-Derivative (PID) controllers for stochastic hybrid
systems. Despite their widespread use in industry, no automated method
currently exists for deriving a PID controller (or any other type of
controller, for that matter) with safety and performance guarantees for such a
general class of systems. In particular, we consider hybrid systems with
nonlinear dynamics (Lipschitz-continuous ordinary differential equations) and
random parameters, and we synthesize PID controllers such that the resulting
closed-loop systems satisfy safety and performance constraints given as
probabilistic bounded reachability properties. Our technique leverages SMT
solvers over the reals and nonlinear differential equations to provide formal
guarantees that the synthesized controllers satisfy such properties. These
controllers are also robust by design since they minimize the probability of
reaching an unsafe state in the presence of random disturbances. We apply our
approach to the problem of insulin regulation for type 1 diabetes, synthesizing
controllers with robust responses to large random meal disturbances, thereby
enabling them to maintain blood glucose levels within healthy, safe ranges.
