Susmit Kumar Jha and Sumit Gulwani and Sanjit A. Seshia and Ashish Tiwari

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2010-28

March 10, 2010

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-28.pdf

Cyber-physical systems (CPS) can be usefully modeled as hybrid automata combining the physical dynamics within modes with discrete switching behavior between modes. CPS designs must satisfy safety and performance requirements. While the dynamics within each mode is usually defined by 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 fixpoint computation, numerical simulation, and machine learning. 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 performed using numerical simulation and machine learning. 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.

---

BibTeX citation:

@techreport{Jha:EECS-2010-28,
    Author= {Jha, Susmit Kumar and Gulwani, Sumit and Seshia, Sanjit A. and Tiwari, Ashish},
    Title= {Synthesizing Switching Logic for Safety and Dwell-Time Requirements},
    Year= {2010},
    Month= {Mar},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-28.html},
    Number= {UCB/EECS-2010-28},
    Abstract= {Cyber-physical systems (CPS) can be usefully modeled as hybrid automata combining the physical dynamics within modes with discrete switching behavior between modes. 
CPS designs must satisfy safety and performance requirements. While the dynamics within each mode is usually defined by 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 fixpoint computation, numerical simulation, and machine learning. 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 performed using numerical simulation and machine learning. 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.},
}

EndNote citation:

%0 Report
%A Jha, Susmit Kumar 
%A Gulwani, Sumit 
%A Seshia, Sanjit A. 
%A Tiwari, Ashish 
%T Synthesizing Switching Logic for Safety and Dwell-Time Requirements
%I EECS Department, University of California, Berkeley
%D 2010
%8 March 10
%@ UCB/EECS-2010-28
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-28.html
%F Jha:EECS-2010-28