Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time

TL;DR

This paper presents a modular verification approach for autonomous vehicle platooning, enabling separate analysis of decision-making, real-time, and spatial properties to improve system safety assurance.

Contribution

It introduces a modular verification framework that combines algorithmic and deductive techniques for analyzing different aspects of autonomous vehicle systems.

Findings

Successful verification of decision-making components

Effective analysis of real-time properties

Spatial verification of vehicle platooning

Abstract

The spread of autonomous systems into safety-critical areas has increased the demand for their formal verification, not only due to stronger certification requirements but also to public uncertainty over these new technologies. However, the complex nature of such systems, for example, the intricate combination of discrete and continuous aspects, ensures that whole system verification is often infeasible. This motivates the need for novel analysis approaches that modularise the problem, allowing us to restrict our analysis to one particular aspect of the system while abstracting away from others. For instance, while verifying the real-time properties of an autonomous system we might hide the details of the internal decision-making components. In this paper we describe verification of a range of properties across distinct dimesnions on a practical hybrid agent architecture. This allows us to verify the autonomous decision-making, real-time aspects, and spatial aspects of an autonomous vehicle platooning system. This modular approach also illustrates how both algorithmic and deductive verification techniques can be applied for the analysis of different system subcomponents.