Abstract:

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 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.

Bio:

Sayan is an Associate Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign. His research develops algorithms & tools for design and verification of computing systems and applied those to automotive, medical, and aerospace systems. Sayan got his PhD from  MIT in 2007 and spent one year as a post-doctoral researcher at CalTech. He has held visiting positions at Oxford University and the Air Force Research Laboratory, NM. 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.

Host:

Dr. Sandeep Kulkarni