Formal Verification of Intersection Safety for Automated Driving

TL;DR

This paper introduces a formal framework for mathematically verifying the safety of control strategies in intersection scenarios for automated driving, extending existing logic and automating safety condition discovery.

Contribution

It extends the program logic dFHL and introduces hybrid control flow graphs to automatically find responsibility-sensitive safety conditions for intersections.

Findings

The safety conditions are proven to ensure safety.

The discovered safety conditions are safe and not overly conservative.

Experimental evaluation confirms the effectiveness of the approach.

Abstract

We build on our recent work on formalization of responsibility-sensitive safety (RSS) and present the first formal framework that enables mathematical proofs of the safety of control strategies in intersection scenarios. Intersection scenarios are challenging due to the complex interaction between vehicles; to cope with it, we extend the program logic dFHL in the previous work and introduce a novel formalism of hybrid control flow graphs on which our algorithm can automatically discover an RSS condition that ensures safety. An RSS condition thus discovered is experimentally evaluated; we observe that it is safe (as our safety proof says) and is not overly conservative.