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) RStudio |
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: https://hal.inria.fr/hal-02355551/en or from the CADP Web site in PDF or PostScript |
Contact: | Radu Mateescu Inria - LIG / CONVECS 655, avenue de l'Europe CS 90051 38334 Montbonnot FRANCE Email: Radu.Mateescu@inria.fr |
Further remarks: | This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |