Events Calendar

Center for Cyber-Physical Systems and Internet of Things and Ming Hsieh Institute for Electrical Engineering Joint Seminar Series on Cyber-Physical Systems

Speaker: Jyotirmoy V. Deshmukh, Principal Research Engineer , Toyota Technical Center

Talk Title: Formal Reasoning for the Cyber-Physical Systems of Tomorrow

Abstract: As cyberphysical systems (CPS) researchers, we are in the process of shaping human societies of tomorrow. Smart transportation infrastructures, autonomous driving cars, medical devices, avionics systems, unmanned aerial vehicles, smart agriculture are just a few examples of technologies that will have a major impact on how we will lead our lives. CPS is not just a buzzword: it truly represents a convergence of a number of separate streams of science and engineering. Today, building a smart CPS requires a deep understanding of the physical aspects of the system being controlled in addition to being able to program intelligence into the controlling software. Increasingly, such software combines sophisticated algorithms from control theory with machine learning and AI algorithms. Often, system designers also have to model the underlying communication between the physical and the cyber worlds. The result is that even the simplest closed-loop model of a CPS is very complex and typically not amenable to reasoning in a formal sense. The burning question is: how do we increase our confidence in the correctness of system-designs with such complexities when even their models are not amenable to rigorous mathematical reasoning? This talk gives some directions to tackle this problem in the setting of model-based development of CPS designs.
Correctness of engineered systems is typically judged in an application-specific and manual fashion; a key step before we can formally reason about system correctness is to have a formalism to express correctness of the CPS being designed. We will discuss the use of logical formalisms based on real-time temporal logics as a possible requirement language for the CPS domain. The other main challenge is to automate the process of testing and finding undesirable behavior with respect to a given set of requirements. We will look at how the use of logical formalisms can greatly aid test automation and in some specific cases give formal guarantees. We will conclude by considering the data deluge problem for CPS; we will suggest techniques to learn logical patterns from time-series data to aid our understanding of the system under study.


Biography: Jyotirmoy Deshmukh is a Principal Research Engineer at Toyota Technical Center in Gardena, California. His research interests are in requirement engineering, temporal logic, formal testing, verification, automatic synthesis and repair of systems, with special focus on cyberphysical system models. Previously, Jyotirmoy got his Ph.D. from the University of Texas at Austin, on the topic of verification of sequential and concurrent software libraries using techniques such as the theory of tree automata and static program analysis. After his Ph.D., he worked as a post-doctoral researcher as part of the Computing Innovation Fellows program at the University of Pennsylvania. His current research interest is in techniques for improving reliability of embedded control software used in cyber-physical systems.

Host: Paul Bogdan

Location: Hughes Aircraft Electrical Engineering Center (EEB) - 248

Audiences: Everyone Is Invited

Contact: Estela Lopez