Proving Autonomous Vehicle & Advanced Driver Assistance Systems Safety

Source Organization:
University:Carnegie Mellon University
Principal Investigator:André Platzer
PI Contact
Project Manager:
Funding Source(s) and Amounts Provided (by each agency or organization):
Total Dollars:
Agency ID/Contract/Grant Number:
Start and End Dates:
Project Status:Complete
Subject Categories:
Abstract:Smart transportation systems hold tremendous potential to make future transportation both safer and more efficient. As a consequence, we increasingly put control decisions into the hands of computers. Widely deployed examples in modern cars include adaptive cruise control, lane departure warning systems, and emergency braking systems or electronic traction control systems. Even fully autonomous cars are becoming increasingly possible. Safety of the interaction of autonomous cars with their environment is of prime importance. Examples of such safety features include obstacle and pedestrian avoidance, lane assistance, and safe lane change maneuvers. Without sufficiently strong guarantees about certain minimal baseline safety behavior, it is getting increasingly impossible to advance computer-assisted car safety technology in reliable ways. Such guarantees are crucial pieces of evidence for authorities and stakeholders to accept novel designs that are, for good reasons, getting further away from the historic safety arguments. This project studies the use of formal verification techniques with differential dynamic logic in the KeYmaera theorem prover and the modeling tool Sphinx to develop provably safe controls for car traffic situations that can be helpful for both driver assistance technology and autonomous driving.
Describe Implementation of Research Outcomes (or why not implemented):
Impacts/Benefits of Implementation (actual, not anticipated):
Project URL: