EAPSI: Formal Verification of Autonomous Driving Scenarios

O'Kelly Matthew E, Philadelphia PA

Investigators

Abstract

Reliable and provably safe autonomous systems remain a grand challenge of engineering because of their potential ability to perform hazardous jobs, increase task efficiency, and prevent accidents attributable to human error. Despite these promises, such systems cannot be put into general service because, there is a lack of plan verification and validation methods for safety and performance that prevents all but relatively low levels of autonomy from being certified for use (US Air Force Research Laboratory). Thus, ensuring the safety of scenarios involving autonomous systems will require a decision control framework for plan verification and execution that interfaces tightly with sensing, online estimation, vehicle control and human intervention. Because autonomous systems are primarily implemented as software, we approach this problem through the development of rigorous software modeling and design techniques. This research effort will afford an opportunity to test recent theoretical advances in autonomous driving scenario verification on a state-of-the-art autonomous vehicle. The work will be carried out in collaboration with Dr. Shinpei Kato, an expert in parallel and distributed computing and autonomous vehicles at Nagoya University, Japan. Given this motivation, the work is centered on the development of the modeling and verification foundations for plan execution of autonomous and semi-autonomous systems, which operate in real-time and in conjunction with human decision makers. A secondary goal is to make such formal modeling and verification available and accessible by the larger engineering community through the development of easy to use tools for describing scenarios, establishing safety and translating verified properties models to verified code. To address the above challenges a framework for Autonomous System Plan verification and Execution (APEX) has been developed. Underlying this tool is a domain specific language for describing autonomous driving scenarios (agents, dynamics, topology, traffic rules, safety and efficacy properties). The tool is built around a theory of scenario composition as well as an automated abstraction chain, which together, map a graphical mission sketch to formal descriptions such as timed automata, probabilistic automata and hybrid automata. These descriptions may then be verified against safety, liveness, and efficacy requirements. The work at Nagoya University will attempt to demonstrate such formal modeling within urban driving (lane merging), highway maneuvers (overtaking and lane switching) and intersection arbitration scenarios. This NSF EAPSI award is funded in collaboration with the Japan Society for the Promotion of Science (JSPS).