This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Coverage Estimation in Model Checking with Bitstate Hashing
April 2013 (vol. 39 no. 4)
pp. 477-486
Satoshi Ikeda, NEC Corporation, Kawasaki
Masahiro Jibiki, National Institute of Information and Communication Technology, Koganei
Yasushi Kuno, University of Tsukuba, Bunkyo
Explicit-state model checking which is conducted by state space search has difficulty in exploring satisfactory state space because of its memory requirements. Though bitstate hashing achieves memory efficiency, it cannot guarantee complete verification. Thus, it is desirable to provide a reliability indicator such as a coverage estimate. However, the existing approaches for coverage estimation are not very accurate when a verification run covers a small portion of state space. This mainly stems from the lack of information that reflects characteristics of models. Therefore, we propose coverage estimation methods using a growth curve that approximates an increase in reached states by enlarging a bloom filter. Our approaches improve estimation accuracy by leveraging the statistics from multiple verification runs. Coverage is estimated by fitting the growth curve to these statistics. Experimental results confirm the validity of the proposed growth curve and the applicability of our approaches to practical models. In fact, for practical models, our approaches outperformed the conventional ones when the actual coverage is relatively low.
Index Terms:
Estimation,Reliability,Probabilistic logic,Accuracy,Mathematical model,Space exploration,Equations,bitstate hashing,Coverage estimation,model checking
Citation:
Satoshi Ikeda, Masahiro Jibiki, Yasushi Kuno, "Coverage Estimation in Model Checking with Bitstate Hashing," IEEE Transactions on Software Engineering, vol. 39, no. 4, pp. 477-486, April 2013, doi:10.1109/TSE.2012.44
Usage of this product signifies your acceptance of the Terms of Use.