December 6, 2013, Jyotirmoy Deshmukh, Toyota

Friday, December 6, 2013 at 3:00 PM to 4:00 PM
8 St. Mary’s Street, Room 211

Refreshments served at 2:45.

DeshmukhJyotirmoy Deshmukh
Toyota

How Can We Formally Reason About Industrial-Scale Control Systems?

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 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 highly 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 local requirements amenable to use with verification tools are not typically available and have to be inferred from global, high-level requirements. 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 the ability to simulate a closed-loop system?” In this talk, we present a broad overview of some of the simulation-based formal techniques that we have been developing.

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 PhD in the area of formal verification for software libraries under the supervision of E. Allen Emerson at the University of Texas at Austin. He also worked a post-doctoral researcher with Rajeev Alur at the University of Pennsylvania on topics such as computer-aided program synthesis and automata-theoretic models for streaming computations.

Hosting Professor: Calin Belta
Student Host: Sepideh Pourazarm