A Driver’s License Test for Driverless Vehicles

This article elaborates the approaches that can be used to verify an autonomous vehicle (AV) before giving it a driver’s license. Formal methods applied to the problem of AV verification include theorem proving, reachability analysis, synthesis, and maneuver design. Theorem proving is an interactive technique in which the computer is largely responsible for demonstrating that the model satisfies the specification, with occasional help from the user. The latter provides lemmas and axioms that the tool leverages to advance the proof towards its conclusion. Reachability analysis is used to verify the operation of the AV during navigation. This provides an extension of onboard diagnostics to whole-AV operation, where the diagnosis does not concern one component’s requirements, but the safety of the entire AV. Another approach is to design correct-by-construction controllers from preverified maneuvers. The basic idea is that one builds a library of maneuvers, such as Left-Turn and Right-Turn, and verifies that the car can perform these maneuvers from any initial state.