Source-linked AI summary
Formal Verification of Autonomous Vehicle Platooning
Maryam Kamali, Louise A. Dennis, Owen McAree, Michael Fisher, Sandor M. Veres
TL;DR
Autonomous vehicle platoons require safety certification of complex agent decisions, while agent-level and whole-system verification have different scope and scalability constraints. The paper combines AJPF verification of actual agent code with Uppaal verification of an abstract agent automaton, supporting safety verification of both autonomous behavior and platoon requirements. The verified code controls vehicles in simulation and the developing real vehicle, subject to correct environmental abstractions.
Problem
Vehicle platoons need formal safety certification, but autonomous agent behavior and full hybrid-system verification present complementary verification challenges.
Method
The paper combines AJPF model checking of agent code with Uppaal verification of an abstract agent automaton derived from the BDI code.
Results
The verified agent code is the code controlling vehicles in TORCS simulation and the developing real vehicle, provided the environmental abstractions are correct.
Takeaways & Limitations
The mixed strategy verifies platoon safety requirements while retaining verification of the autonomous decisions implemented in vehicle agents.
Takeaways & Limitations
AJPF cannot realistically verify the whole system and lacks real-time capabilities, while vehicular control systems are left to standard control-systems techniques.
Abstract
from arXiv · showhide
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.
1 Introduction
Vehicle platoons increase autonomy and coordination demands, making safety certification challenging. The paper separates high-level agent decisions from continuous control and verifies the resulting rational-agent behavior.
- 1 Introduction: Vehicle platoons use autonomous following and V2V communication to coordinate vehicle spacing and operations.Communication supports both continuous position control and higher-level joining, leaving, and dissolution commands.
- 1 Introduction: Hybrid automata make discrete decision-making and continuous control difficult to separate as platoon behaviors become more complex.The paper also notes that high-level decision representations can become unnecessarily complex.
- 1 Introduction: The proposed hybrid autonomous-systems architecture separates discrete decisions from continuous control and represents the discrete behavior in greater detail.The architecture uses the agent paradigm for implementation, analysis, and verification.
- 1 Introduction: Rational agents expose reasons for their choices, enabling formal reasoning about both autonomous actions and the decisions behind them.This addresses the opacity that can remain when the agent concept is used alone.
- 1 Introduction: The paper applies model checking to show that rational agents follow platoon requirements and do not deliberately choose unsafe options.The verification targets agent decisions in combination with other vehicles.
2 Automotive Platoons
Automotive platoons combine a manually driven leader with autonomously controlled follower vehicles using predefined spacing and agent-level coordination. Joining and leaving procedures impose authorization, spacing, and controller-transition requirements.
- 2 Automotive Platoons: A platoon is led manually while follower vehicles autonomously control speed and steering and maintain predefined gaps.V2V communication connects vehicles at both control and agent levels, with the leader coordinating platoon operations.
- 2 Automotive Platoons: Joining requires a vehicle to request authorization, receive agreement, change lane manually, approach the preceding vehicle, and enable automatic controllers in sequence.The leader may first create additional spacing, then restore normal spacing after successful joining.
- 2 Automotive Platoons: A joining vehicle must receive leader confirmation before changing lane and must approach the preceding vehicle before autonomous control is enabled.Automatic steering is enabled only after the vehicle is sufficiently close and in the correct lane.
- 2 Automotive Platoons: Leaving requires leader authorization, increased spacing, manual control restoration, lane changing, and acknowledgement to the leader.The vehicle switches speed and steering control to manual only after maximum spacing is achieved.
- 2 Automotive Platoons: Except in emergencies, vehicles must not leave without authorization, and autonomous control must remain active until maximum allowable spacing is reached.
3 Agent-based Development of Automotive Platoon
Each vehicle combines physical feedback control with abstraction and rational decision-making agents. GWENDOLEN expresses joining behavior through goals, beliefs, and plans that sequence controller and communication actions.
- 3 Agent-based Development of Automotive Platoon: The hybrid architecture links a MATLAB feedback-controlled Physical Engine to Abstraction and Decision-Making Agents.The Abstraction Agent converts continuous sensory data into discrete information, while the Decision-Making Agent sends interpreted instructions back toward vehicle control.
- 3 Agent-based Development of Automotive Platoon: TORCS supplies the simulation environment, MATLAB implements the Physical Engine, and GWENDOLEN implements the abstraction and decision-making agents.An interface connects TORCS with MATLAB/Simulink for vehicle control.
- 3 Agent-based Development of Automotive Platoon: GWENDOLEN represents goals, beliefs, and plans, selecting plans according to the follower agent’s current goals and beliefs.The joining procedure is implemented as an achievement goal with plans conditioned on beliefs such as leader agreement and lane status.
- 3 Agent-based Development of Automotive Platoon: The joining goal is achieved when the follower believes the prescribed joining steps are complete, represented by the platoon-ok belief.This belief captures successful lane placement, enabled automatic controllers, and leader acknowledgement.
4 Verification
The verification strategy separates autonomous-agent reasoning from timed system behavior, checking actual agent programs with AJPF and whole-platoon timing with Uppaal abstractions. This combination verifies safety and liveness properties for joining, leaving, controller activation, spacing, and lane changes.
- Verification Methodology: The twin strategy verifies individual agent properties with AJPF and whole-system timing properties with Uppaal using an abstract agent automaton.AJPF checks agent programs in untimed environments, while Uppaal checks timing after replacing internal BDI reasoning with input-output automata.
- Verification Methodology: The approach verifies actual autonomous-agent code while abstracting unavailable communications, vehicle-control, and environmental implementations.AJPF is used for the agent program, whereas the other components are represented by abstract formal models.
- Verification Methodology: AJPF cannot realistically verify the whole system because it is slow and lacks real-time capabilities, motivating separation of agent and timing verification.The BDI layer makes AJPF at least an order of magnitude slower than JPF, and timing verification within AJPF is difficult.
- Verification Methodology: The decomposition is justified because agent beliefs and intentions are local, while timed and BDI formulae remain separate in the requirements.This permits local agent-property checking and separate whole-system timing verification.
- Verified Properties: Verified properties ensure that vehicles do not initiate joining, autonomous speed control, or autonomous steering without the required confirmations, lane changes, or distances.The properties cover confirmation before joining, changed-lane belief before speed control, confirmation before speed control, and sufficient distance before steering control.
- Verified Properties: The verification also covers liveness and platoon safety, including eventual joining initiation, changing-lane spacing, and eventual increases in spacing after joining requests.The reported properties include a leads-to condition connecting a joining request with an increase-space command and action.
5 Concluding Remarks
The paper addresses the scale and coverage limits of formal verification for hybrid autonomous platoons through a twin strategy combining agent-level and whole-system verification. This approach verifies actual agent-code decisions while checking global timed safety properties, subject to environmental abstractions and AJPF limitations.
- 5 Concluding Remarks: The strategy addresses the need to verify hybrid systems, implementation code, BDI-agent properties, and timed interactions without relying on one verification technique alone.AJPF cannot practically verify whole-system platooning properties, while global timed verification does not replace agent-code verification.
- 5 Concluding Remarks: The twin strategy uses AJPF for individual agent properties and Uppaal for platoon-wide safety and timed requirements.The agent code is abstracted into a timed automaton for global verification.
- 5 Concluding Remarks: The approach verifies the actual code controlling vehicles in simulation and development vehicles, provided the environmental abstractions are correct.This links verified autonomous decisions to the implementation used in TORCS and physical rover vehicles.
- 5 Concluding Remarks: Two latency-recovery procedures remain outside the verified agent code because adding them makes AJPF unable to verify any property.The authors are investigating abstraction at the level of goals, beliefs, and intentions to handle more complex agents.
- 5 Concluding Remarks: Future work includes improving AJPF efficiency, extracting more formal properties from official requirements, and testing the architecture on real vehicles.The paper also reports ongoing efforts to move beyond simulation into physical testing.
- 5 Concluding Remarks: Manually generated Uppaal models were linked to agent-code execution by extracting temporal formulae and checking them against the agent code.The authors identify automation of automaton construction from AJPF explorations as future work to improve completeness and efficiency.