Online Verification of Automated Road Vehicles Using Reachability Analysis

Althoff, Matthias; Dolan, John M. · 2014 · OpenAlex-citations

DOI: 10.1109/tro.2014.2312453

archive: archived pipeline: cataloged verified

Get this paper ↗ (DOI — opens at the source; we link to it, we don't host it)

Summary

This paper proposes a formal method for the online verification of automated road vehicles to guarantee safety during operation. The authors address the challenge that every traffic situation is unique, making offline verification insufficient. They argue that traditional simulation techniques cannot guarantee safety due to the infinite number of possible future scenarios and the exponential computational cost required to cover all cases. Instead, the paper introduces a reachability analysis approach that predicts the set of all possible occupancies for both the automated vehicle (ego vehicle) and surrounding traffic participants. Safety is formally guaranteed if the occupancy sets of the ego vehicle and other participants do not intersect for all times, considering bounded uncertainties in sensor noise, disturbances, and initial states. The methodology relies on dynamic models and set-based computations. The ego vehicle is modeled using a bicycle model that captures lateral and longitudinal dynamics, including slip angle, heading, yaw rate, and velocity, with additive disturbances to account for real-world imperfections. A tracking controller is integrated into this model to simulate the vehicle's response to planned trajectories. For other traffic participants, a simpler point-mass model is used, constrained by traffic rules such as speed limits, acceleration bounds, and lane boundaries. The core of the verification process involves computing the reachable sets of the ego vehicle and the occupancy of other agents. If a planned trajectory is verified as safe, it is executed; if unsafe, the vehicle remains on a previous safe trajectory or executes a braking maneuver to a safe stop. The approach assumes that sensors detect all relevant participants and that uncertainties are bounded sufficiently to capture all real-world behaviors, either deterministically or with a defined probability bound. The applicability of the approach is demonstrated through test drives using a Cadillac SRX research vehicle from Carnegie Mellon University. The vehicle model was validated against real-world data from double-lane-change maneuvers, showing high conformity in yaw angle and position, with minor deviations in yaw rate and steering angle attributed to unmodeled actuator dynamics. These mismatches were handled by incorporating uncertainty bounds into the model. The experiments confirmed that the reachability analysis could be performed online, allowing the vehicle to verify planned maneuvers in real-time. The system successfully accounted for the interaction between the maneuver planner and the verification module, adapting to the specific control interface of the test vehicle. The significance of this work lies in its ability to provide formal safety guarantees for automated vehicles in dynamic, uncertain environments, a critical requirement for certification. By using reachability analysis, the method avoids the conservatism of fixed deviation buffers and the incompleteness of simulation-based approaches. It enables the verification of complex maneuvers, such as intersection crossings and evasive actions, by explicitly modeling the vehicle's dynamic response to uncertainties. This approach bridges the gap between theoretical formal methods and practical automotive applications, offering a rigorous framework for ensuring that automated vehicles do not cause avoidable crashes.

Provenance

The full processing record for this entry. Every stage of this paper's journey through the pipeline is logged — what ran, with which tool and model, how many attempts it took, and when it last completed.

Summary generated by qwen3.6-27b-prismaquant on 2026-06-26; verification: verified.

Topics

Ranked by relevance to this paper. Hover a topic for its definition.

• situational awareness