Diana El Rabih , Nihal Pekergin , Gaël Gorgo , Jean-Marc Vincent
July 2010
Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010) (VECOS)
Verification and Evaluation of Computer and Communication Systems (VECoS 2010)
1-2 July 2010
Model Checking, Probabilistic Verification, Continuous Stochastic Logic (CSL), Perfect Simulation
Model checking of probabilistic models can be done either by numerical analysis or by simulation and statistical methods. In this paper, we compare the efficiency and the scalability of different model checking approaches when they are applied to the verification of steady-state properties of large models. We provide an experimental comparison study between the statistical model checking using perfect sampling implemented in Ψ 2 [15] and proposed in [11, 10] and the numerical method implemented in PRISM [6], for the verification of CSL [2] steady-state properties. We show that the proposed statistical approach lets us to consider very large models.
This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/