Synthesizing Switching Logic for Safety and Dwell-Time Requirements
Cyber-physical systems (CPS) can be usefully modeled as hybrid automata
combining the physical dynamics within each mode with
discretized switching behavior between modes.
Designers of CPS need to create models that
satisfy safety and performance requirements.
While the physical dynamics within each mode is usually defined
by the parameters of the physical plant, the tricky design problem
often involves getting the switching logic right.
In this paper, we present a new approach to assist designers by
synthesizing the switching logic, given a partial system model,
using a combination of numerical simulation and fixpoint computation.
Our technique begins with an over-approximation of the guards on transitions
between modes. In successive iterations, the over-approximations are refined
by eliminating points that will cause the system to reach unsafe states,
and such refinement is guided by numerical simulation.
In addition to safety requirements, we synthesize models to satisfy
dwell-time constraints, which impose upper and/or lower bounds on the
amount of time spent within a mode. We demonstrate using case studies that
our technique quickly generates intuitive system models and that dwell-time constraints
can help to tune the performance of a design.