Results and sources for the paper titled “A Review Of Statistical Model Checking Pitfalls on Real-Time Stochastic Models”, submitted for review to ISoLA 2014

Hardware

The hardware used to analyze the models consists of:

·         CPU: Intel(R) Core(TM) i7-2640M CPU @ 2.80GHz

·         Memory: 16GB Ram

·         Operating system:  Arch Linux and Windows 7

UPPAAL

The UPPAAL tool can be retrieved from http://www.uppaal.org/ . The version used for the experiments as presented in the paper is 4.1.15. UPPAAL was executed under Arch Linux by directly running the provided shell script.

The following parameters were used for the statistical analysis:

Probability of uncertainty: 0.01
Alpha: 0.01
Beta: 0.01

Modes

The modes tool is part of the Modest toolset, which can be retrieved from http://www.modestchecker.net/ . The version used for the experiments as presented in the paper is 2.0 Beta 3. Modes was executed under Windows 7 via command line as follows:

modes.exe -R Uniform -S ASAP -N 26492 [modelfile]

The number of traces was calculated via the Chernoff-Hoeffding bound[1], with a confidence of 0.01 and error bound of 0.01.

Source files

The model source files are available via the following link: models.zip.

Application output

The outputs of UPPAAL and models were collected in the following file: model_results.txt. Note: due to the stochastic nature of statistical model checking, the exact same results may not be reproducible.

References

[1] Hérault, T., & Lassaigne, R. (2004). Approximate probabilistic model checking. Retrieved from http://link.springer.com/chapter/10.1007/978-3-540-24622-0_8