Incremental state-space exploration for programs with dynamically allocated data

ABSTRACT

We present a novel technique that speeds up state-space exploration (SSE) for evolving programs with dynamically allocated data. SSE is the essence of explicit-state model checking and an increasingly popular method for automating test generation. Traditional, non-incremental SSE takes one version of a program and systematically explores the states reachable during the program's executions to find property violations. Incremental SSE considers several versions that arise during program evolution: reusing the results of SSE for one version can speed up SSE for the next version, since state spaces of consecutive program versions can have significant similarities. We have implemented our technique in two model checkers: Java PathFinder and the J-Sim state-space explorer. The experimental results on 24 program evolutions and exploration changes show that for non-initial runs our technique speeds up SSE in 22 cases from 6.43% to 68.62% (with median of 42.29%) and slows down SSE in only two cases for -4.71% and -4.81%.

REFERENCES

• 1: T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In CAV 2004.
• 2: Taweesup Apiwattanapong , Alessandro Orso , Mary Jean Harrold, Efficient and precise dynamic impact analysis using execute-after sequences, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062534]
• 3: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 4: E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS 2004.
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: C. L. Conway, K. S. Namjoshi, D. Dams, and S. A. Edwards. Incremental algorithms for inter-procedural analysis of safety properties. In CAV 2005.
• 7: Christoph Csallner , Yannis Smaragdakis, JCrasher: an automatic robustness tester for Java, Software—Practice & Experience, v.34 n.11, p.1025-1050, September 2004 [doi>10.1002/spe.602]
• 8: Marcelo d'Amorim , Steven Lauterburg , Darko Marinov, Delta execution for efficient state-space exploration of object-oriented programs, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273472]
• 9: M. d'Amorim, A. Sobeih, and D. Marinov. Optimized execution of deterministic blocks in Java PathFinder. In ICFEM 2006.
• 10: Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of data structure properties, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 11: Hyunsook Do , Sebastian Elbaum , Gregg Rothermel, Supporting Controlled Experimentation with Testing Techniques: An Infrastructure and its Potential Impact, Empirical Software Engineering, v.10 n.4, p.405-435, October 2005 [doi>10.1007/s10664-005-3861-2]
• 12: FSM-Based Incremental Conformance Testing Methods, IEEE Transactions on Software Engineering, v.30 n.7, p.425-436, July 2004 [doi>10.1109/TSE.2004.31]
• 13: Sebastian Elbaum , Hui Nee Chin , Matthew B. Dwyer , Jonathan Dokulil, Carving differential unit test cases from system test cases, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181806]
• 14: Sebastian Elbaum , Alexey G. Malishevsky , Gregg Rothermel, Test Case Prioritization: A Family of Empirical Studies, IEEE Transactions on Software Engineering, v.28 n.2, p.159-182, February 2002 [doi>10.1109/32.988497]
• 15: Todd L. Graves , Mary Jean Harrold , Jung-Min Kim , Adam Porter , Gregg Rothermel, An empirical study of regression test selection techniques, ACM Transactions on Software Engineering and Methodology (TOSEM), v.10 n.2, p.184-208, April 2001 [doi>10.1145/367008.367020]
• 16: Mary Jean Harrold , James A. Jones , Tongyu Li , Donglin Liang , Alessandro Orso , Maikel Pennings , Saurabh Sinha , S. Alexander Spoon , Ashish Gujarathi, Regression test selection for Java software, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.312-326, October 14-18, 2001, Tampa Bay, FL, USA
• 17: Klaus Havelund , Grigore Roşu, An Overview of the Runtime Verification Tool Java PathExplorer, Formal Methods in System Design, v.24 n.2, p.189-215, March 2004 [doi>10.1023/B:FORM.0000017721.39909.4b]
• 18: T. A. Henzinger, R. Jhala, R. Majumdar, and M. A. A. Sanvido. Extreme model checking. In International Symposium on Verification: Theory and Practice, 2003.
• 19: Chalermek Intanagonwiwat , Ramesh Govindan , Deborah Estrin, Directed diffusion: a scalable and robust communication paradigm for sensor networks, Proceedings of the 6th annual international conference on Mobile computing and networking, p.56-67, August 06-11, 2000, Boston, Massachusetts, United States [doi>10.1145/345910.345920]
• 20: Radu Iosif, Exploiting Heap Symmetries in Explicit-State Model Checking of Software, Proceedings of the 16th IEEE international conference on Automated software engineering, p.254, November 26-29, 2001
• 21: S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS 2003.
• 22: James Law , Gregg Rothermel, Whole program Path-Based dynamic impact analysis, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 23: Zheng Li , Mark Harman , Robert M. Hierons, Search Algorithms for Regression Test Case Prioritization, IEEE Transactions on Software Engineering, v.33 n.4, p.225-237, April 2007 [doi>10.1109/TSE.2007.38]
• 24: Johann A. Makowsky , Elena V. Ravve, Incremental Model Checking for Decomposable Structures (Extended Abstract), Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science, p.540-551, August 28-September 01, 1995

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Performance, Verification

Keywords:
incremental computation, j-sim, java pathfinder, jpf, model checking, state-space exploration