Experimentation mode

The experiment panel is made of 3 different area which are

• A data selection panel

And also

• A distributed settings panel
• A results panel

In order to verify our property we choose the montecarlo method with a samplecount 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 property or contract that we want to check.

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.

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 propriety on each of these traces. These experiments method change the way that the number of simulation to run is fixed.

Montecarlo

Montecarlo method lets you set a fixed number of simulation to run. The name of the parameter is

• samplecount the number of simulations to run.

Chernoff

Chernoff method compute the number of simulation to run given 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

Sequential method sets four parameters :

• alpha the false positives probability.
• beta the false negatives probability.
• delta the indifference region around prob.
• proba the probability.

More details on the Sequential method can be found in the Statistical Model Checking section (Qualitative question).