Autonomous Vehicle Safety Verification

This project investigates safety verification of autonomous driving behaviors. Our work to date uses reachability analysis to compute the set of all possible behaviors of an autonomous vehicle. A reachable set is the set of states a system can possibly reach for a given set of initial states, disturbances, and sensor noise values. We consider autonomous vehicles which plan trajectories for a certain lookahead horizon which are followed using feedback control. While a perfectly followed trajectory might not violate specified safety properties (e.g. lane departures or vehicle collisions), there might exist a violating deviation from the planned trajectory. Given the mathematical model of the controlled vehicle and bounds on uncertainty, our approach detects any possible violation. In addition, the approach provides results faster than real time such that maneuvers of vehicles can be checked before they are fully executed.