The Community for Technology Leaders
RSS Icon
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
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
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
[1] E.M. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[2] G.J. Holzmann, The Spin Model Checker: Primer and Reference Manual. Addison Wesley, 2003.
[3] D.L. Dill, A.J. Drexler, A.J. Hu, and C.H. Yang, "Protocol Verification as a Hardware Design Aid," Proc. IEEE Int'l Conf. Computer Design on VLSI in Computer and Processors, pp. 522-525, 1992.
[4] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, "Model Checking Programs," Automated Software Eng., vol. 10, no. 2, pp. 203-232, 2003.
[5] P. Wolper and D. Leroy, "Reliable Hashing without Collision Detection," Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 59-70, 1993.
[6] G.J. Holzmann, "An Analysis of Bitstate Hashing," Formal Methods in System Design, vol. 13, no. 3, pp. 289-307, 1998.
[7] U. Stern and D.L. Dill, "A New Scheme for Memory-Efficient Probabilistic Verification," Proc. IFIP TC6/WG6.1 Joint Int'l Conf. Formal Description Technique for Distributed Systems and Comm. Protocols, and Protocol Specification, Testing, and Verification, pp. 333-348, 1996.
[8] B.H. Bloom, "Space/Time Trade-Offs in Hash Coding with Allowable Errors," Comm. ACM, vol. 13, no. 7, pp. 422-426, 1970.
[9] J. Eckerle and T. Lais, "New Methods for Sequential Hashing with Supertrace," 1998.
[10] G. Holzmann, R. Joshi, and A. Groce, "Swarm Verification Techniques," IEEE Trans. Software Eng., vol. 37, no. 6, pp. 845-857, Nov./Dec. 2011.
[11] P.C. Dillinger and P. Manolios, "Bloom Filters in Probabilistic Verification," Formal Methods in Computer-Aided Design, pp. 367-381, Springer, 2004.
[12] D. Owen and T. Menzies, "Lurch: A Lightweight Alternative to Model Checking," Proc. Int'l Conf. Software Eng. and Knowledge Eng., pp. 158-165, 2003.
[13] R. Pelánek, T. Hanžl, I. Černá, and L. Brim, "Enhancing Random Walk State Space Exploration," Proc. 10th Int'l Workshop Formal Methods for Industrial Critical Systems, pp. 98-105, 2005.
[14] R. Grosu and S.A. Smolka, "Monte Carlo Model Checking," Tools and Algorithms for Construction and Analysis of Systems, vol. 3440, pp. 271-286, 2005.
[15] E. Tronci, G.D. Penna, B. Intrigila, and M.V. Zilli, "A Probabilistic Approach to Automatic Verification of Concurrent Systems," Proc. Asia-Pacific Software Eng. Conf., pp. 317-324, 2001.
[16] T. Menzies, D. Owen, and B. Cukic, "Saturation Effects in Testing of Formal Models," Proc. 13th Int'l Symp. Software Reliability Eng., pp. 15-26, 2002.
[17] P. Flajolet, P.J. Grabner, P. Kirschenhofer, and H. Prodinger, "On Ramanujan's Q-Function," J. Computational and Applied Math., vol. 58, no. 1, pp. 103-116, 1995.
[18] R. Pelánek, "Typical Structural Properties of State Spaces," Model Checking Software, S. Graf and L. Mounier, eds., pp. 5-22, Springer, 2004.
[19] M.B. Dwyer, S. Elbaum, S. Person, and R. Purandare, "Parallel Randomized State-Space Search," Proc. 29th Int'l Conf. Software Eng., pp. 3-12, 2007.
28 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool