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 to build 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 cyber-physical systems. Exact verification is undecidable, but we will see that some pragmatism in the form of bounded-time analysis, access to numerical simulation data, 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, a system involving a pacemaker, a power train control system, and a neurological network.
Sayan Mitra is an Associate Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign. His research develops algorithms and tools for design and verification of computing systems and applies those to automotive, medical, and aerospace systems. Sayan got his PhD from MIT in 2007 and spent one year as a postdoctoral researcher at Caltech. He has held visiting positions at Oxford University and the Air Force Research Laboratory, NM. He has received the National Science Foundation’s CAREER Award (2011), an AFOSR Young Investigator Research Program Award (2012), the IEEE-HKN C. Holmes MacDonald Outstanding Teaching Award (2013), and a Samsung Global Research Outreach Award, and his group has received several best paper awards.