Formal Methods for Design and Verification of Embedded Control Systems
The design of reliable embedded control systems inherits the difficulties involved in designing both control systems and distributed (concurrent) computing systems. Design bugs in these systems may arise from the unforeseen interactions among the computing, communication and control subsystems. Motivated by the difficulties of finding this type of design bugs, this project focuses on developing mathematical frameworks, based on formal methods, to facilitate the design and analysis of such embedded systems. This work incorporates methodology from computer science and control, including model checking, theorem proving, synthesis of digital designs, reachability analysis, Lyapunov-type methods and receding horizon control. Various applications have been considered, including autonomy, vehicle management and multi-target tracking.
My research focuses on formal methods, motion planning, situational reasoning, hybrid systems, and distributed control systems.
- DARPA Urban Challenge 2007
- Planning with Conflicting Specifications
- Formal Specifications of Autonomous Systems
- Sharing the World with Autonomous Systems: What Goes Wrong and How to Fix It (NSF)
- CAREER: Establishing Correctness of Learning-Enabled Autonomous Systems with Conflicting Requirements (NSF)