Seminars

From Simulation to Verification of Hybrid and Distributed Systems PDF
Sayan Mitra, Dept. of ECE, University of Illinois at Urbana-Champaign

5/10/2013, 3:30pm, GHC 8102

Abstract

Design defects in embedded systems can be elusive and expensive. The simulation to verification research program aims to exploit finite data generated from 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 from our research: (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 from their data logs. 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.

Biography

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, Samsung GRO Award 2012.

http://users.crhc.illinois.edu/mitras/