SIMULATION-BASED TO VERIFICATION OF TEMPORAL PRECEDENCE
Sayan Mitra, University of Illinois, Urbana-Champaign
January 9, 2014,10:00 am, NASA Langley, Bldg 1220, Rm 212
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, Dr. Mitra will present recent developments in this area on sound and relatively complete simulation-based verification algorithms for nonlinear and switched systems. The approach introduces the new type of model annotations which are used to verify bounded time temporal precedence properties of moderately high dimensional systems. Dr Mitra will discuss results of applying these technique to an alerting system for a SAPA/ALAS-inspired parallel landing protocol.
Biography:
http://users.crhc.illinois.edu/mitras
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, and IEEE-HKN C. Holmes MacDonald Outstanding
Teaching Award 2013.