Warning!<\/strong><\/p>Prerequisite<\/strong> The experiment panel<\/strong> is made of 3 different areas which are<\/p>\n In order to verify our property we choose the Monte-Carlo method<\/strong> with a Total samples<\/em> 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.<\/p>\n Configuration of a Monte-Carlo experiment<\/p><\/div>\n Finally we click on the start button<\/strong> at the bottom of the interface. Once the 1000 simulations have been computed, results show up in the result panel<\/strong>.<\/p>\n Results of the Monte-Carlo experiment<\/p><\/div>\n We can then select the plot panel<\/strong> to have a better understanding of our results by drawing plots.<\/p>\n Once here we can return to our project panel and modify our properties and models or make a new experiment with a different method.<\/p>\n We could also run a bigger experiment in distributed mode<\/strong>. This is the next step<\/a><\/strong> of our tutorial.<\/p>\n 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<\/strong><\/a>.<\/p>\n 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:<\/strong><\/p>\n Chernoff method also computes an estimation of the probability, but it determines the number of simulations to run based two parameters:<\/p>\n More details on the Chernoff method can be found in the Statistical Model Checking section (Quantitative question)<\/em><\/strong><\/a>.<\/p>\n 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 :<\/p>\n <\/strong>More details on the Sequential method can be found in the Statistical Model Checking section (Qualitative question)<\/strong><\/em><\/a>.<\/p>\n 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\u2026<\/p>\n
\nFor 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<\/a>.<\/div><\/p>\n\n
\n
![\"\"](\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_images\/plasma_expe_montecarlo.png\")
<\/a>![\"\"](\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_images\/plasma_results_montecarlo.png\")
<\/a>
\nExperimentation methods<\/h3>\n
Monte-Carlo<\/h5>\n
\n
Chernoff<\/h5>\n
\n
Sequential<\/h5>\n
\n
\n
\n<\/strong><\/em><\/p>","protected":false},"excerpt":{"rendered":"