Database of Case Studies Achieved Using CADP

Probabilistic Collision Risk Estimation for Autonomous Driving

Organisation: CHROMA and CONVECS project-teams, Inria Grenoble - Rhône-Alpes, CITI, and LIG

Method: XTL

Tools used: CARLA
CADP (Construction and Analysis of Distributed Processes)

Domain: Autonomous Vehicles.

Period: 2019

Size: 800 traces

Description: Autonomous vehicles are complex cyber-physical systems that must satisfy critical correctness requirements to increase the safety of road traffic. The validation of autonomous driving is a challenging field because of the complexity of its key components (perception of the environment, scene interpretation, decision making and undertaking of actions) and the intertwinning of physical and software components. Since intelligent vehicles are supposed to be driven on existing roads, along with other vehicles with human drivers, a high level of uncertainties need to be taken into account, requiring the use of probabilistic approaches for perception and prediction.

We propose a methodology to validate perception systems based on a combination of simulation, formal verification, and statistical analysis. The simulation framework, based on the CARLA simulator, comprises a realistic description of the dynamic physical environment (e.g., urban landscape and vehicles), the perception system under study, and a set of relevant scenarios (e.g., leading to collisions). We considered the CMCDOT (Conditional Monte Carlo Dense Occupancy Tracker) perception system, in particular its collision risk estimation functionality. Simulating a large number of realistic intersection crossing scenarios with two vehicles yields traces of events containing the suitable data for validation (timestamp, estimated probabilities of collision, position and velocities of the vehicles, etc.). On each such trace, a number of typical temporal properties (invariants, safety, liveness) are verified using the XTL model checker of CADP, producing quantitative verdicts (sets of events violating the properties, with their diagnostic information). Finally, a statistical analysis of the verdicts is carried out using RStudio, by defining an appropriate KPI (Key Performance Indicator) for each property, using it to compute a grade for each trace, and aggregating the results in analysis reports.

Conclusions: The proposed methodology was applied to validate the collision risk prediction feature of CMCDOT for a set of relevant scenarios involving collisions between vehicles, but also corner cases (near misses or bare touches). This allowed to assess the accurate behaviour of CMCDOT w.r.t. collision risk prediction.

Publications: [Ledent-Paigwar-Renzaglia-et-al-19] Philippe Ledent, Anshul Paigwar, Alessandro Renzaglia, Radu Mateescu, and Christian Laugier. Formal Validation of Probabilistic Collision Risk Estimation for Autonomous Driving. Proceedings of the 9th IEEE International Conference on Cybernetics and Intelligent Systems, Robotics, Automation and Mechatronics CIS-RAM'2019 (Bangkok, Thailand), November 18-20, 2019.
Available on-line at:
or from the CADP Web site in PDF or PostScript

Radu Mateescu
655, avenue de l'Europe
CS 90051
38334 Montbonnot

Further remarks: This case-study, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:22:04 2021.

Back to the CADP case studies page