Speaker: Dr. Wenchao Li
Affiliation: SRI International
Abstract: Dependability is becoming a first-order concern for robotic systems as they are being increasingly used for safety-critical tasks such as performing surgery and assisting in driving. Each of these tasks requires the software commanding the robots to meet an interlaced set of logical, temporal and real-time constraints. An autonomous vehicle, for example, needs to determine how to navigate around obstacles, while the controller performing the actual maneuver relies on the underlying middleware providing timely communication. In this talk, I will present my research on enabling and ensuring these Robot software systems to compute reliably with provable guarantees.
In the first part of my talk, I will present a systematic framework for designing and verifying multi-rate distributed systems. The framework takes its inspiration from the Robot Operating System (ROS), but redefines the publish-and-subscribe architecture in a formal model of computation. The framework centers around a declarative language called the Robot Architecture Definition Language (RADL) that is used to capture the system architecture and drive code generation and system integration. On the verification side, I will present a suite of techniques and tools for formally verifying these real-time multi-rate systems using a combination of contract, model translation, automata encoding and specification reduction techniques. The RADL paradigm was key to the design of a high-assurance ground robot in a recent DARPA demonstration. In the second part of the talk, I will highlight results in automatically synthesizing robot motion planners in underspecified environment. The technique is based on temporal logic synthesis but tackles the prevalent problem of incomplete specification. I will show that this technique is also applicable to a semi-autonomous driving setting where the delay in car-to-driver handoff has to be properly accommodated. I will conclude the talk by presenting my current research and future vision on dependable robot software.
Biography: Dr. Wenchao Li is currently a Computer Scientist at SRI International. He received his Ph.D. in Electrical Engineering and Computer Sciences from UC Berkeley in 2013. His research focuses on developing theory and tools for the construction of provably dependable systems. His research has been recognized with the ACM Outstanding Ph.D. Dissertation Award in Electronic Design Automation and the Leon O. Chua Award for outstanding achievement in nonlinear science.
Date(s) - Apr 04, 2016
11:00 am - 12:15 pm
EE-IV Shannon Room #54-134
420 Westwood Plaza - 5th Flr., Los Angeles CA 90095