Skip to main content

From Simulation to Verification of Hybrid and Distributed Systems

Sayan Mitra

Design defects in embedded systems can be elusive and expensive. Effective formal verification of such systems has been a challenge problem for several years. The simulation to verification research program aims to exploit finite data generated from validated simulation tools or from system's executions to provide formal guarantees about uncountable sets of executions. In this talk, I will present two recent developments in this area: (1) a sound and relatively complete simulation-based verification algorithm for nonlinear and switched systems and and (2) an algorithm for checking bounded time safety properties of distributed systems for executions that are consistent with recorded data. The first approach introduces the idea of model annotations, in the spirit of loop invariants, which are used effectively verify bounded time properties of moderately high dimensional systems. The second approach combines static analysis of the system model with dynamically generated data and can be applied to distributed systems with imperfectly synchronized clocks. Along the way, I will mention some of the case studies we have performed.

Speaker bio

Sayan Mitra is an Assistant Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign. His research aims to develop mathematical, algorithmic and software tools for design and analysis of distributed and cyber-physical systems. Sayan graduated from MIT in 2007 and spent one year as a post-doctoral researcher at the Center for Mathematics of Information of CalTech. His research group has received several awards; most recently, the National Science Foundation's CAREER award in 2011, AFOSR Young Investigator Research Program Award in 2012, Best paper award at FORTE/FMOODS 2012, and the Samsung GRO Award 2012.

Share this: