Industrial-scale control systems are more and more developed in the model-based design paradigm. This typically involves capturing a plant model that describes the dynamical characteristics of the physical processes within the system, and a controller model, which is a block-diagram-based representation of the software used to regulate the plant behavior. In practice, plant models and controller models are highly complex as they can contain nonlinear hybrid dynamics, look-up tables storing pre-computed values, several levels of design-hierarchy, design-blocks that operate at different frequencies, and so on. Moreover, the biggest challenge is that system requirements are often imprecise, non-modular, evolving, or even simply unknown. As a result, formal techniques have been unable to digest the scale and format of industrial-scale control systems.
On the other hand, the Simulink modeling language -- a popular language for describing such models -- is widely used as a high-fidelity simulation tool in the industry, and is routinely used by control designers to experimentally validate their controller designs. This raises the question: "What can we accomplish if all we have is a very complex Simulink model of a control system?"
In this talk, we give an example of a simulation-guided formal technique that can help characterize temporal properties of the system, or guide the search for design behaviors that do not conform to "good behavior". Specifically, we present a way to algorithmically mine temporal assertions from a Simulink model. The input to our algorithm is a requirement template expressed in Parametric Signal Temporal Logic -- a formalism to express temporal formulas in which concrete signal or time values are replaced by parameters. Our algorithm is an instance of counterexample-guided inductive synthesis: an intermediate candidate requirement is synthesized from simulation traces of the system, which is refined using counterexamples to the candidate obtained with the help of a falsification tool. The algorithm terminates when no counterexample is found. Mining has many usage scenarios: mined requirements can be used to validate future modifications of the model, they can be used to enhance understanding of legacy models, and can also guide the process of bug-finding through simulations. (Joint work with X. Jin, J. Deshmuck and S. Seshia).
Alexandre Donzé is a post-doctoral faculty at the department of Electrical Engineering and Computer Science of UC Berkeley, working under the supervision of Sanjit Seshia. He holds a PhD of Mathematics and Computer Science from the University of Joseph Fourier at Grenoble. From 2008 to 2009, he was also a postdoc at the university of Carnegie Mellon, working with Edmund Clarke and Bruce Krogh. The main goal of his research is to develop mathematical and computational tools for the analysis and the design of dynamical systems arising from different domains, in particular embedded systems (or software interacting with a physical environment), analog and mixed signal circuits and biological systems. He developed Breach, a toolbox that is today getting the attention of large groups in the automative industry such as Toyata and Bosh, and (modestly) contributed to Spaceex, the current leading model-checking tool for hybrid systems.