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
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
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.
The model source files are available via the following link: models.zip.
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.
[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