: Industrial-scale control systems are often developed in the model-based design paradigm. This typically involves capturing a ‘plant model’ that describes the dynamical characteristics of 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 highly nonlinear and hybrid dynamics, look-up tables storing pre-computed values, several levels of design-hierarchy, design-blocks that operate at different frequencies, and so on. A big challenge is that local requirements amenable to use with verification tools are typically not available and have to be inferred from global, high-level requirements. Design validation in the industry often takes the form of extensive testing on various platforms such in-vehicle testing, hardware-in-the-loop simulations, software-in-the-loop simulations, and so on. In the model-based design paradigm, the Simulink modeling framework (from the Mathworks) has become the de facto standard across industry for describing closed-loop plant + controller systems. The key feature of this framework is a high-fidelity simulation tool, now routinely used by control designers to experimentally validate their controller designs. In effect, we have a situation where designers have access to a wide range of methods that can perform extensive (but not exhaustive) simulations of a system. On the other end of the spectrum, the hybrid systems community has been developing a number of formal verification techniques that provide sound (but conservative and hence inaccurate) results. These techniques, at the present time, are largely applicable to simplified models such as continuous dynamical systems, and piecewise-affine systems. There is a wide chasm between the models that are amenable to formal analysis and the scale and format of industrial-scale control systems. This raises the question: ‘What can we “formally” accomplish if all we have is the ability to simulate a system?’ We present an overview of some our recent work that is our first foray into this problem space.
Jyotirmoy V. Deshmukh is a senior engineer and researcher at Toyota Technical Center in Gardena (Los Angeles) California. His research interests are in the broad area of formal verification, automatic synthesis and repair of systems, and temporal logic. His current focus is in the area of cyber-physical systems, in particular, automotive control systems modeled as hybrid automata and nonlinear dynamical systems. Previously, Jyotirmoy got his Ph.D. in the area of formal verification for software libraries under the supervision of E. Allen Emerson at the University of Texas at Austin. Jyotirmoy was a 2010 Computing Innovation fellow, which supported his post-doctoral work with Rajeev Alur at the University of Pennsylvania from 2010-2012.