Database of Case Studies Achieved Using CADP

Generation of Scenarios for Autonomous Vehicles

Organisation: INRIA Grenoble - CHROMA and CONVECS teams (FRANCE)

Method: LNT

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

Domain: Autonomous Vehicles.

Period: 2022-2023

Size: about 1000 lines of LNT

Description: AV (Autonomous Vehicles) are complex and safety critical systems, whose components (sensors, decision making, control, etc.) need to be thoroughly tested to ensure they handle critical situations even better than human drivers. A common practice is to reproduce these critical situations in a simulator, such as CARLA. The scenarios to drive a simulator can be specified randomly or manually, both approaches having difficulties in ensuring a satisfactory coverage of all possible situations.

Formal methods provide a rigorous approach to automatically generate scenarios, which are guaranteed to be relevant for testing AV’s behaviour in a particular situation (e.g., collision, near miss, etc). This work applies the conformance testing tool TESTOR to generate scenarios from a formal model and a test purpose characterizing the desired situation. The formal model, built using the LNT language of the CADP toolbox, describes a configuration including a scene map and several actors (AV and static/mobile obstacles) with their initial positions and constraints on their trajectories. Precise trajectories of the actors are automatically induced by the generated scenarios. In general, each test purpose yields several scenarios, with guarantees to cover all relevant variations of the behavior related to the test purpose. These scenarios are then automatically translated into behaviour trees, which are used to drive the CARLA simulator.

This approach was evaluated on ten configurations, involving three scene maps (T-crossing, highway, and X-crossing) and various actors, for which a large number of scenarios were generated, featuring collisions of the AV with other actors, near-misses of such collisions, and arrivals of the AV at its destination.

Conclusions: The proposed approach makes possible the formalization (as test purposes) of safety requirements defined in standards, such as ISO 26262, and the generation of test cases, which can be used both for producing simulation scenarios and for assessing the correct functioning of AVs in their environment.

Publications: [Horel-Laugier-Marsso-et-al-22] Jean-Baptiste Horel, Christian Laugier, Lina Marsso, Radu Mateescu, Lucie Muller, Anshul Paigwar, Alessandro Renzaglia, and Wendelin Serwe. Using Formal Conformance Testing to Generate Scenarios for Autonomous Vehicles. Proceedings of Design, Automation and Test in Europe - Autonomous Systems Design (DATE/ASD'2022), Antwerp, Belgium, March 14-18, 2022.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Marsso-Mateescu-Muller-Serwe-22] Lina Marsso, Radu Mateescu, Lucie Muller, and Wendelin Serwe. Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing. Proceedings of the 5th Workshop on Models for Formal Analysis of Real Systems (MARS'2022), Munich, Germany, April 2, 2022.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Horel-Ledent-Marsso-et-al-23] Jean-Baptiste Horel, Philippe Ledent, Lina Marsso, Lucie Muller, Christian Laugier, Radu Mateescu, Anshul Paigwar, Alessandro Renzaglia, and Wendelin Serwe. Verifying Collision Risk Estimation using Autonomous Driving Scenarios Derived from a Formal Model. Journal of Intelligent & Robotic Systems 107, 59, 2023.
Available on-line at:
or from the CADP Web site in PDF or PostScript

Radu Mateescu
Inria centre at the University Grenoble Alpes
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin

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

Last modified: Fri Feb 9 11:14:37 2024.

Back to the CADP case studies page