[Colloq] Reminder: Colloquium on industrial-scale control systems design

[Thomas Wahl]

The colloquium below has been scheduled to take place right after the 
Academic Review on Thursday. I am aware of the inconvenience of this 
time slot. The speaker is visiting several local universities this week 
(which was all scheduled many weeks ago), so the only alternative to 
this time slot would be to cancel the talk.

If you are interested and absolutely cannot make it Thursday afternoon, 
here is a pointer to an alternative venue + time:

http://www.bu.edu/systems/december-6-2013-jyotirmoy-deshmukh-toyota/

-------- Original Message --------
Subject: [professors] [Colloq] Colloquium
Date: Wed, 27 Nov 2013 14:29:02 -0500 (EST)
From: Francoise Niang <fniang at ccs.neu.edu>
To: colloq <colloq at lists.ccs.neu.edu>


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.