Title :
Statistical Model Checking for Steady State Dependability Verification
Author :
Rabih, Diana El ; Pekergin, Nihal
Author_Institution :
LACL, Univ. of Paris-Est (Paris 12), Creteil, France
Abstract :
We propose to apply the perfect simulation to perform statistical model checking of large Markov chains. Perfect simulation is an extension of Monte Carlo Markov Chain (MCMC) methods, it allows us to obtain exact steady-state samples of the underlying chain thus it avoids the burn-in time problem to detect the steady-state. The statistical model checking by MCMC methods has been already proposed in the last years. However the steady-state formulas can not be checked by this approach because of the problem of detecting steady-state. Thus we propose to do statistical model checking by combining perfect simulation and statistical hypothesis testing in order to verify steady state formulas. We apply our proposed method to verify the saturation and availability properties at long run for a multistage interconnection queueing network illustrating its efficiency when considering very large models.
Keywords :
Markov processes; Monte Carlo methods; formal verification; statistical analysis; Monte carlo Markov chain method; multistage interconnection queueing network; statistical model checking; steady state dependability verification; steady-state sample; Discrete event simulation; Formal verification; Monte Carlo methods; Performance evaluation; Probabilistic logic; Steady-state; Stochastic processes; Stochastic systems; Testing; Time measurement; CSL; Statistical model checking; dependability verification; perfect simulation;
Conference_Titel :
Dependability, 2009. DEPEND '09. Second International Conference on
Conference_Location :
Athens, Glyfada
Print_ISBN :
978-0-7695-3666-8
DOI :
10.1109/DEPEND.2009.32