[Colloq] Colloquium

[Francoise Niang]

Colloquium announcement

Title: Bridging the gap between industrial-scale control systems and 
formal methods

Speaker: Jyotirmoy V. Deshmukh, senior engineer and researcher at Toyota 
Technical Center in Gardena (Los Angeles) California

Date and time: Thursday, Dec 5, 4pm, in 366 WVH

Abstract: 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.

Bio: 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.