Human-in-the-Loop Embedded Systems: Specification, Design, and Verification

Human interaction is central to many computing systems that require a high level of assurance. Examples of such systems include aircraft control systems (interacting with a pilot), automobiles with self-driving features (interacting with a driver), and medical devices (interacting with a doctor or patient). The correctness of such systems depends not only on the autonomous controller, but also on the actions of the human controller, and, critically, on the interaction between the two.

In this talk, I will present a formalism for human-in-the-loop embedded systems. I will then discuss the problem of synthesizing a semi-autonomous controller from high-level specifications that expect occasional human intervention for correct operation. We present an algorithm for this problem, and demonstrate its operation on problems related to driver assistance in automobiles. Finally, I will present a data-driven approach to probabilistic modeling and verification of human driver behavior. Since probabilistic models learned from data can suffer from estimation errors, we have designed and applied a new approach for model checking probabilistic models with uncertainties. The talk will conclude with a broad survey of research challenges in this area.

Bio: Sanjit A. Seshia is an Associate Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in dependable computing and computational logic, with a current focus on applying automated formal methods to problems in embedded systems, electronic design automation, computer security, and program analysis. His Ph.D. thesis work on the UCLID verifier and decision procedure helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based verification. He is co-author of a widely-used textbook on embedded systems. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE) from the White House, an Alfred P. Sloan Research Fellowship, the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University, and the inaugural Prof. R. Narasimhan Lecture Award from TIFR.