Seminars & Meetings | Abstracts

Wednesday, March 16, 2011

Sayan Mitra
Department of Electrical Engineering
University of Illinois at Urbana-Champaign

Abstraction refinement for verification of hybrid systems

Abstract:
The hybrid automaton framework is an expressive mathematical formalism for modeling a wide variety of cyber-physical systems. While automatic tools for verifying subclasses of hybrid automata, e.g., rectangular initialized automata are available, general hybrid automata are known to be intractable. As a result, creation of tractable abstractions for hybrid models has received a fair bit of attention. In this talk, I will discuss two recent results in this theme. First, I will discuss a counterexample guided abstraction refinement algorithm for safety verification that relies on rectangular-initialized abstractions. This algorithm has been implemented in a new tool and I will present some of the experimental results. Next, I will present an algorithm for stability verification which relies on slow switching, transition invariants, and approximations for hybrid-steps that combine discrete transitions and continuous flows. I will briefly discuss the completeness of both these algorithms for rectangular initialized automata.

 

Bio:

Sayan Mitra is an Assistant Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign since 2008. His research interests are in verification of cyber-physical systems, distributed algorithms, and application of formal methods in automotive and aerospace. Prior to joining Illinois, he was a post-doctoral fellow at the Center for Mathematics of Information of California Institute of Technology for a year. He earned a Ph.D. from MIT in 2007 and received National Science Foundation's Faculty Early Career Development award in 2011.