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.
Formal Verification of Intersection Safety for Automated Driving
2023-09-24
687157 byte
Conference paper
Electronic Resource
English
Safety verification of automated driving systems
Online Contents | 2013
|Testing and verification of active safety systems with coordinated automated driving
Automotive engineering | 2009
|Formal verification method for safety diagnosis software
Automotive engineering | 2015
|Formal Verification Method for Safety Diagnosis Software
British Library Conference Proceedings | 2015
|