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.
