From Simulations to Verification of Cyberphsical Systems and Applications

Traditional approaches for testing and certification are beginning to be stretched at the seams for systems that involve complex software implementation of controllers. Software design bugs caused 24% of all medical device recalls in 2011 and millions of vehicle recalls cost billions of dollars every year. In the most recent standard for airborne software certification (DO-178C), model-based design and formal methods are put forward as alternatives to testing as a way for building high assurance systems; other industries are following this lead. In this context, I will present our recent results on verification of hybrid automata models that capture a wide variety of cyberphysical systems. Exact verification is undecidable but we will see that some pragmatism in the form of bounded-time analysis, access to numerical simulators, and robustness, can make the problem decidable. I will discuss these ideas and present several case studies including a NASA-developed alerting protocol for parallel landing of aircraft and a system involving a pacemaker and a network of cardiac cells.

Sayan Mitra is an Associate Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign. His research develops algorithms & tools cyberphysical systems. Sayan graduated from MIT in 2007 and spent one year as a post-doctoral researcher at CalTech. He received the National Science Foundation's CAREER Award in 2011, AFOSR Young Investigator Research Program Award in 2012, IEEE-HKN C. Holmes MacDonald Outstanding Teaching Award (2013), Samsung Global Research Outreach Award, and his group has received several best paper awards.