*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Atlanta, GA | Posted: October 12, 2018
Summary Sentence:
Scalable Formal Verification of Cyber-Physical Systems
Full Summary:
Scalable Formal Verification of Cyber-Physical Systems
Parasara DuggiralaAbstract:
The integration of embedded sensors, computation, and communication have enabled the development of sophisticated control strategies for Cyber-Physical Systems (CPS). Such control strategies are being deployed in ubiquitous systems such as air-traffic control systems, autonomous vehicles, medical devices, smart grids, etc. Given the safety critical nature of these systems, it is necessary that they should satisfy the safety specification. Violation of such safety specification can lead to loss of property or life. One of the widely used technique for ensuring that a CPS satisfies it safety requirements is to apply formal verification techniques. The interaction between the discrete components (described as state machines) and continuous components (described by differential equations) of these systems makes the verification problem challenging.
In this talk, I will present recent developments in the field of dynamic analysis technique for verification of CPS. In dynamic analysis, rigorous safety guarantees for CPS are provided by only analyzing a few sample behaviors. I will first describe a procedure for analyzing CPS where differential equations are nonlinear and then proceed to systems where differential equations are linear. For CPS with linear differential equations, I will describe a method where verification of an an n-dimensional system requires using a mere n+1 sample behaviors. I will also describe several enhancements such as constraint propagation, dynamic (de)aggregation, counterexample generation, and adapting it to model uncertainities. I will demonstrate the scalability of verification by presenting verification results for systems with 10 - 10,000 dimensions.
Bio:
Parasara Sridhar Duggirala is an Assistant Professor in the Department of Computer Science and Engineering at University of Connecticut (UConn). His main research interests are in Cyber-Physical Systems, Formal Methods, and Control Theory. His paper on Safety Verification of Linear Control Systems won the best paper award at the International Conference on Embedded Software (conducted as part of ESWeek) 2013. His work on "Verification of Powertrain Control Systems" and his paper on "Direct Verification of Linear Systems with over 10000 Dimensions" has won the best paper awards at ARCH workshop conducted as part of CPSWeek 2015 and 2017 respectively. He was a research intern at NEC Labs America in the summer of 2011 and SRI International in the summer of 2012. He has received his PhD (in 2015) from University of Illinois at Urbana Champaign (UIUC) and his B.Tech (in 2009) from Indian Institute of Technology Guwahati.
