Statistical Model Checking based Validation


Origin: Mathieu Barbier / INRIA, Jean Quilbeuf / INRIA, Alessandro Renzaglia / INRIA, Christian Laugier / INRI

Written: April 2019

Purpose: Application of the statistical model checking to validate probabilistic decision making and perception algorithms.

Context/Pre-Conditions: availability of
– KPI definition, Scenario definition
– Working simulation platform

To consider: The boundary for the analysis must be set by experts.


Participants and Important Artefacts

Simulation engineer: In charge of the setup of the simulation platform and the generation of traces.

Validation engineer: In charge of defining BLTL statement.

System expert: In charge of defining relevant KPI for the SUT.

Simulation traces: Executions of the system generated according to the probabilities in the model.

Probability of bounded occurrences: The final result is given in terms of probability to meet a certain property expressed as a BLTL formula.


(1) KPI definition task:

(1.a) The first step is to look at criteria that could be used to judge performances of the ACPS.

(1.b) Then, given the scenario, some KPI must be defined to validate the behavior of the ACPS in the scenario.

(2) Scenario definition:

(2.a) The first task is to defined dynamic and static elements that the ACPS will have to interact with.

(2.b) For each element included in the scenario, find what variability is required for each characteristics of an element (e.g. initial velocity of a vehicle).

(2.c) Then, find criteria that will be used to determine whether the test was successful or not.

(3) BLTL creation: Transform success criteria and KPI into BLTL expressions that can be used by the SMC to estimate the probability of remaining within certain bounds.

(4) Simulation execution: Selected scenarios are simulated using CARLA simulator and Robot Operating System (ROS), relying on a random generation of parameters such as: the non-ego vehicle class (cars or motorcycles), initial positions and initial speeds of ego and non-ego vehicle, etc.

(5) SMC: Statistical Model Checking, which represents an intermediate between test and exhaustive verification by relying on statistics, provides an estimation of the probability to meet a certain property based on the analysis of the simulation traces.

Application Example

ENABLE-S3 Use Case 2 “Intersection Crossing”: We applied this approach to the decision making system and the perception system of an autonomous vehicle in road intersection crossing scenarios.


Relations to other Patterns

Pattern Name Relation*
KPI Model-based validation That pattern describes how the first activity can be realized
Abstract Scenarios Mining That pattern supports the second activity
Requirements Formalization Both patterns use similar approaches

* “this pattern” denotes the pattern described here, “that pattern” denotes the related pattern