Formal Verification of Swerving Maneuvers for Car Collision Avoidance

Many road vehicle accidents are the result of collisions with foreign objects, and automatic collision avoidance is of critical interest to car manufacturers and their customers. Previous work on formally verifying collision avoidance maneuvers typically assumes point-shaped or circular-shaped vehicles for simplicity. In this paper, we formulate and formally verify sufficient conditions for the safety of a representative collision avoidance system for cars with a realistic geometrical shape. The collision avoidance system discussed here is designed to issue swerving advisories. We model the vehicle kinematics and control advisory as a hybrid program, allowing to model both discrete decisions of the system and continuous dynamics of the car. We formally verify the collision avoidance system by providing rigorous, computer-checked mathematical proofs of collision avoidance under well-defined, explicit sufficient conditions on vehicle kinematics and parameters. This formal verification provides a mathematical guarantee that the collision avoidance system can prevent the vehicle from collision under all possible scenarios as long as certain conditions hold true. We model the system using differential dynamic logic dL and use the automated theorem prover KeYmaera X for formal verification. This work employs a purely symbolic model, and can thus be extended to verify other types of collision avoidance systems exhibiting richer behavior.