Issue No. 04 - April (2013 vol. 39)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.44
Masahiro Jibiki , National Institute of Information and Communication Technology, Koganei
Satoshi Ikeda , NEC Corporation, Kawasaki
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.
Estimation, Reliability, Probabilistic logic, Accuracy, Mathematical model, Space exploration, Equations, bitstate hashing, Coverage estimation, model checking
Masahiro Jibiki, Satoshi Ikeda, Yasushi Kuno, "Coverage Estimation in Model Checking with Bitstate Hashing", IEEE Transactions on Software Engineering, vol. 39, no. , pp. 477-486, April 2013, doi:10.1109/TSE.2012.44