Formal Verification of Autonomous Vehicle Platooning

TL;DR

This paper presents a combined formal verification approach to ensure the safety of autonomous vehicle platooning systems by verifying both the agent code and the overall system model.

Contribution

It introduces a hybrid verification method that integrates local and global techniques to certify autonomous vehicle behaviors in platoons.

Findings

Successfully verified safety requirements of autonomous vehicle agents.

Demonstrated scalability of the combined verification approach.

Validated safety properties on actual agent code.

Abstract

The coordination of multiple autonomous vehicles into convoys or platoons is expected on our highways in the near future. However, before such platoons can be deployed, the new autonomous behaviors of the vehicles in these platoons must be certified. An appropriate representation for vehicle platooning is as a multi-agent system in which each agent captures the "autonomous decisions" carried out by each vehicle. In order to ensure that these autonomous decision-making agents in vehicle platoons never violate safety requirements, we use formal verification. However, as the formal verification technique used to verify the agent code does not scale to the full system and as the global verification technique does not capture the essential verification of autonomous behavior, we use a combination of the two approaches. This mixed strategy allows us to verify safety requirements not only of a model of the system, but of the actual agent code used to program the autonomous vehicles.