Statistical model checking for steady state dependability verification

被引:0
作者
El Rabih, Diana [1 ]
Pekergin, Nihal [1 ]
机构
[1] Univ Paris 12, LACL, F-94010 Creteil, France
来源
DEPEND: 2009 SECOND INTERNATIONAL CONFERENCE ON DEPENDABILITY | 2009年
关键词
Statistical model checking; perfect simulation; CSL; dependability verification;
D O I
暂无
中图分类号
TM [电工技术]; TN [电子技术、通信技术];
学科分类号
0808 ; 0809 ;
摘要
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.
引用
收藏
页码:166 / 169
页数:4
相关论文
共 11 条
  • [1] [Anonymous], 1997, An engineering approach to computer networking: ATM net- works, the Internet, and the telephone network
  • [2] [Anonymous], 2000, ACM Trans. Comput. Logic, DOI DOI 10.1145/343369.343402
  • [3] Hansson H., 1994, Formal Aspects of Computing, V6, P512, DOI 10.1007/BF01211866
  • [4] Propp JG, 1996, RANDOM STRUCT ALGOR, V9, P223, DOI 10.1002/(SICI)1098-2418(199608/09)9:1/2<223::AID-RSA14>3.0.CO
  • [5] 2-O
  • [6] Sen Koushik, 2005, LNCS, V3576
  • [7] On the exact simulation of functionals of stationary Markov chains
    Vincent, JM
    Marchand, C
    [J]. LINEAR ALGEBRA AND ITS APPLICATIONS, 2004, 386 : 285 - 310
  • [8] VINCENT JM, 2007, QEST
  • [9] Younes H. L. S., 2002, Computer Aided Verification. 14th International Conference, CAV 2002. Proceedings (Lecture Notes in Computer Science Vol.2404), P223
  • [10] Statistical probabilistic model checking with a focus on time-bounded properties
    Younes, Hakan L. S.
    Simmons, Reid G.
    [J]. INFORMATION AND COMPUTATION, 2006, 204 (09) : 1368 - 1409