Subscribe

Issue No.04 - April (2013 vol.39)

pp: 477-486

Satoshi Ikeda , NEC Corporation, Kawasaki

Masahiro Jibiki , National Institute of Information and Communication Technology, Koganei

Yasushi Kuno , University of Tsukuba, Bunkyo

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.44

ABSTRACT

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.44REFERENCES