Recent advances in autonomous driving technologies have raised the problem of safety to the forefront. For this project, we are developing a novel safety standard for driving controllers with full or shared autonomy.
The standard defines clear model assumptions and safety guarantees in the form of a safety verification framework built on compositional and contract-based ideas to overcome scalability and computational issues. Instead of verifying car controllers over entire road networks, the approach first builds a library of local and verified road models, such as intersections and road segments, that are composed together to certify safety over networks.
Composition is achieved using assume-guarantee contracts that are synthesized concurrently during verification. Thus, we can reuse local models within and across networks, add additional models to cover local road geometries without re-verifying the entire library, and the computation can be performed in a parallel and distributed way.
This allows for efficient use of computational resources over the entire life cycle of the standard: initial development, usage, and extension. Furthermore, we employ controller contracts such that any controller satisfying them can be certified safe. Therefore, expanding the scope of the verified library.
The proposed verification framework has the potential to impact companies as a safety standard, road administrators and mapping businesses as road safety certificates, and legislators and policymakers as a tool to asses and certify the safety of autonomous driving technologies.
