Warning!
PrerequisiteFor this tutorial we assume that you have a opened a model and a property. If you don’t know how to do that please refer to step 1.
The experiment panel is made of 3 different areas which are
- A file selection panel
- An execution settings panel
- An experimentation results panel
In order to verify our property we choose the Monte-Carlo method with a Total samples parameter of 1000 simulations to run. Then we check that we have selected the right project and model in the project selection panel. After that we select one or more properties or contracts that we want to check.
Configuration of a Monte-Carlo experiment
Finally we click on the start button at the bottom of the interface. Once the 1000 simulations have been computed, results show up in the result panel.
Results of the Monte-Carlo experiment
We can then select the plot panel to have a better understanding of our results by drawing plots.
Once here we can return to our project panel and modify our properties and models or make a new experiment with a different method.
We could also run a bigger experiment in distributed mode. This is the next step of our tutorial.
Experimentation methods
To summarize, Statistical Model Checkers generate a large amount of execution traces and check the validity of a set of properties on each of these traces. Several algorithms can be used to determine the number of traces that are executed and how the resutls are computed. The basic algorithms are presented below. PLASMA Lab also implements some more specific algorithms described here.
Monte-Carlo
Monte-Carlo method lets you set a fixed number of simulation to run. It computes an estimation of the probability to satisfy the property. The name of the parameter is:
- Total samples the number of simulations to run.
Chernoff
Chernoff method also computes an estimation of the probability, but it determines the number of simulations to run based two parameters:
- Epsilon the error margin.
- Delta the confidence bound.
More details on the Chernoff method can be found in the Statistical Model Checking section (Quantitative question).
Sequential
The Sequential Probability Ratio Test (SPRT) is used check if the probability to satisfy a property is above or below to a given threshold. It needs four parameters :
- Alpha the false positives probability.
- Beta the false negatives probability.
- Delta the indifference region around proba.
- Proba the probability.
More details on the Sequential method can be found in the Statistical Model Checking section (Qualitative question).
