Formally Verified Guardians for Enhanced Driving: Emergency Braking, Swerving, and Combined Maneuvers

Project Abstract/Statement of Work:

Our research focuses on formal verification of cyber-physical systems, typically systems where software interacts with the physical world and its continuous dynamics. The objective of formal verification is to establish strong mathematical properties of a system, and to provide rigorous formal proofs of those properties. Furthermore, the formal proofs of those properties are not only proved by hand, but the proofs are checked by computer software, giving us the utmost level of assurance.

This project would like to establish and formally prove safety conditions for emergency braking, emergency swerving, and combined emergency braking-emergency swerving maneuvers. Emergency braking and adaptive cruise control have already received significant attention, but other maneuvers less so. It is also important to take into account combined maneuvers, for which turning capabilities of the vehicle may be reduced under heavy braking or accelerating.

Our work will start with emergency braking and emergency swerving, the two simplest maneuvers. For those maneuvers, we will study the relevant parameters and establish some candidate safety conditions. After establishing such conditions, as well as a formal model of the system, we will formally prove our safety conditions safe in the KeYmaera hybrid systems theorem prover. We will then extend our work to simultaneous braking (or accelerating) and swerving, and follow the same process: first establish some safety conditions and a model of the system, then prove the conditions safe in the KeYmaera theorem prover. Our proofs typically need significant computing resources, for which we will have access to the Conflux computer cluster.