Perform statistical model checking

Description

This solution method allows the designer to evaluate the likelihood that a system satisfies a set of goals and contracts, by exploring the space of system behaviours through simulation of a UPDM model, extended with stochastic information, against a specification written in GCSL. The tool is based on statistical approaches: it estimates the probability that the given specification, i.e. some GCSL requirements are satisfied by the model.

Initial Situation

Before performing statistical model checking, the system must have been modelled in UPDM, including the stochastic information provided by the DANSE profile, and exported to the simulator as an FMU. This implicitly means that the system has to be fully implemented to be model-checked: the initial situation is similar to the joint simulation for the model. The goals and contracts that need to be verified must be modelled in GCSL. In DANSE, since there is no support for the simulation of the dynamical characteristics of a mode, the GCSL requirements about dynamicity cannot be verified by the tool chain. The GCSL requirements are not model-checked directly by the tool PLASMA. Its input language is a more powerful and low-level language into which all the GCSL requirements have to be translated. These models must be made available through the Tool-Net. The user must configure the analysis tools: PLASMA needs some input parameters that establish the confidence of the final result.

Expected Result

The solution method provides a measure of the likelihood that the system under test satisfies each of the goals and contracts specified in the analysis configuration. For each given GCSL requirement, PLASMA returns an estimation of the probability (between 0 and 1) to satisfy this requirement according to the confidence level given by the experiment parameters. Example from the CAE: the GCSL requirement "The mean city area under fire shall be less than 0.01%". PLASMA answered the probability of satisfaction was in the interval [0.913, 0.933] with a probability of 0.9. The estimation is given as an interval with a confidence level (0.9) that is the probability that the probability to satisfy the requirement belongs to the returned interval.

The SoS designer has to consider several options when he interprets the results. If the estimation is precise enough to deduce that the system satisfies the requirement then the result gives a formal guaranty of the model against the specification. If it fails, the designer has to deduce using co-jointly the tools to identify the cause of the failure and modify the system in consequence. He can thus iterate the Statistical Model Checking to evaluate the modification validity. Finally, the estimation is not enough precise to conclude anything, e.g. he expected to have a probability greater than 91.5 but the estimation is given in the interval [0.913, 0.933]. The designer must start a new analysis with an increased accuracy in order to reduce the interval size.

Required Tools

·         Rhapsody UPDM

·         DANSE Profile Extension for Rhapsody (D6.5.1)

·         GCSL language (D6.3.2)

·         GCSL editor

·         DESYRE (“Joint simulation”) / PLASMA ( “Statistical Model Checking”) requires:

o    FMU/FMI exporter

o    FMUs of CS behaviours

Figure 52: Tool Flow: Perform Statistical Model Checking

Activities

The very first activities of the Statistical Model-Checking are similar to the Simulation activities.  Statistical Model Checking requires an executable SoS model to perform the analysis.  Figure 53 shows the flow of activities.

Figure 53: Activity Diagram, Statistical Model Checking

Model SoS

This is the solution method Model SoS described in section 5.1.  The model of the SoS must specify how the Constituent Systems are interconnected and what information they exchanged in order to properly interact. This activity can be carried out using UPDM in Rhapsody, by developing an Internal Block Diagram that connects the Constituent Systems through a set of ports.

Abstract Constituent System Models

This is the solution method Abstract CS Models described in section 5.2.  The constituent systems can be modelled for instance in UPDM in Rhapsody, by taking advantage of the statecharts view, which provides an executable specification.

Perform joint simulation

This is the solution method Perform Joint Simulation described in section 5.6.  The joint simulation uses the capabilities of DESYRE to combine the executable elements of the SoS and CS models into a single simulation environment.  Part of this activity is to define the simulation configuration and trace configuration that creates the information needed for statistical model checking.

The simulation configuration file in the DESYRE workspace specifies the SoS model to be simulated, simulation time, number of independent simulation runs, fault injection, and so on. These parameters are essential for the correct execution of the simulation, and allow the designer to customise the simulation infrastructure according to the objective of the analysis.

The trace configuration file specifies which elements of the SoS model shall be traced by the simulator (by default, all CS input/outputs are traced). The designer must specify the signals of interest in the SoS, whose evolution must be recorded and then displayed by the simulator.

Import GCSL goals and contracts

The SoS Goals and Contracts edited in Rhapsody using the GCSL Editor can also be retrieved from the Tool-Net thanks to the mediation. Translate the GCSL goals to B-LTL properties that is the specification input format of PLASMA. They can go through to the tool-net and are collected by DESYRE.

Run statistical model checking (SMC) simulations

At this point the model is ready for the simulation and for the Statistical Model Checking also.

From DESYRE, PLASMA is activated as an Statistical Model Checking extension.

Initialise SMC engine and perform the simulations for the Statistical Model-Checking.

Evaluate the results. At the end PLASMA/DESYRE returns the estimation of the probability of satisfaction for each given SoS goals. At his point, the SoS designer can consider two options: either the system satisfies the SoS contracts as expected and the result can be considered as formal proof .verification step, or the designer has to take in account the results, return at the modelling step, modify the SoS modelling and perform the SMC analysis again.

Limitations

The method does not exhaustively verify the system behaviour, but is based on a statistical sampling of the behaviour space. The measure may therefore be affected by an error, and specific corner cases could be missed. The risk can be controlled by reducing the width of the estimation interval and increasing the confidence level, but the analysis time may increase too much. There is a trade-off that must be fixed by the SoS architect between the scalability of the analysis and the strength of the estimation. It has to be studied in accordance with the importance of each evaluated requirement. The results also depend on the quality of the contracts, and therefore on the expressive power of the GCSL constructs.

Follow-up Solution Methods

Statistical model checking provides information on the correctness of the design, and is therefore logically followed by the Evaluate Goals and Contracts solution method. It is an essential element of iterative refinement and the study of the system dynamic evolution. It can also be followed by an analysis of emergent behaviour, when emergence is specified using GCSL. It may be used to gather information regarding alternative architectural solutions.
Home About Technical Approach Perform statistical model checking