Formal Verification of Platoon Control Strategies

TL;DR

This paper formalizes and verifies the stability of various platoon control strategies using higher-order logic, enabling both static and runtime safety checks aligned with industrial standards.

Contribution

It introduces a formal framework in HOL Light for verifying stability constraints of platoon controllers, combining static and dynamic verification methods.

Findings

Formalization of platoon control strategies in higher-order logic

Verification of stability constraints using HOL Light

Development of runtime monitors for stability violations

Abstract

Recent developments in autonomous driving, vehicle-to-vehicle communication and smart traffic controllers have provided a hope to realize platoon formation of vehicles. The main benefits of vehicle platooning include improved safety, enhanced highway utility, efficient fuel consumption and reduced highway accidents. One of the central components of reliable and efficient platoon formation is the underlying control strategies, e.g., constant spacing, variable spacing and dynamic headway. In this paper, we provide a generic formalization of platoon control strategies in higher-order logic. In particular, we formally verify the stability constraints of various strategies using the libraries of multivariate calculus and Laplace transform within the sound core of HOL Light proof assistant. We also illustrate the use of verified stability theorems to develop runtime monitors for each controller, which can be used to automatically detect the violation of stability constraints in a runtime execution or a logged trace of the platoon controller. Our proposed formalization has two main advantages: 1) it provides a framework to combine both static (theorem proving) and dynamic (runtime) verification approaches for platoon controllers, and 2) it is inline with the industrial standards, which explicitly recommend the use of formal methods for functional safety, e.g., automotive ISO 26262.