Delta execution for efficient state-space exploration of object-oriented programs

ABSTRACT

State-space exploration is the essence of model checking and an increasingly popular approach for automating test generation. A key issue in exploration of object-oriented programs is handling the program state, in particular the heap. Previous research has focused on standard program execution that operates on one state/heap. We present Delta Execution, a technique that simultaneously operates on several states/heaps. It exploits the fact that many execution paths in state-space exploration partially overlap and speeds up the exploration by sharing the common parts across the executions and separately executing only the "deltas" where the executions differ.

We have implemented Delta Execution in JPF, a popular general-purpose model checker for Java programs, and in BOX, a specialized model checker that we have developed for efficient exploration of sequential Java programs. We have evaluated Delta Execution for (bounded) exhaustive exploration of ten basic subject programs without errors. The experimental results show that on average Delta Execution improves the exploration time 10.97x (over an order of magnitude) in JPF and 2.07x in BOX. We have also evaluated Delta Execution for one larger case study with errors, where the exploration time improved up to 1.43x.

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: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 3: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 4: 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
• 5: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 6: Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180405.1180445]
• 7: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 8: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 9: 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]
• 10: Daisy File System. Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software.
• 11: M. d'Amorim, S. Lauterburg, and D. Marinov. Delta execution for efficient state-space exploration of object-oriented programs. Technical Report UIUCDCS-R-2007-2844, University of Illinois, Urbana, IL, April 2007.
• 12: Marcelo d'Amorim , Carlos Pacheco , Tao Xie , Darko Marinov , Michael D. Ernst, An Empirical Comparison of Automated Generation and Classification Techniques for Object-Oriented Unit Testing, Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, p.59-68, September 18-22, 2006 [doi>10.1109/ASE.2006.13]
• 13: M. d'Amorim, A. Sobeih, and D. Marinov. Optimized execution of deterministic blocks in Java PathFinder. In ICFEM, 2006.
• 14: 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
• 15: Eclipse foundation. http://www.eclipse.org/.
• 16: Foundations of Software Engineering at Microsoft Research. The AsmL test generator tool. http://research.microsoft.com/fse/AsmL.
• 17: Daniel P. Friedman , Christopher T. Haynes , Mitchell Wand, Essentials of programming languages (2nd ed.), Massachusetts Institute of Technology, Cambridge, MA, 2001
• 18: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 19: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 20: K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4), 2000.
• 21: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 22: 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
• 23: J-Sim. http://www.j-sim.org/.
• 24: J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 10²⁰ States and Beyond. In LICS, 1990.
• 25: S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS, April 2003.
• 26: Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.17-32, January 16-18, 2002, Portland, Oregon
• 27: Flavio Lerda , Willem Visser, Addressing dynamic issues of program model checking, Proceedings of the 8th international SPIN workshop on Model checking of software, p.80-102, May 2001, Toronto, Ontario, Canada
• 28: Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 29: P. C. Mehlitz, W. Visser, and J. Penix. The JPF runtime verification system. http://javapathfinder.sourceforge.net/JPF.pdf.
• 30: M. Musuvathi and D. L. Dill. An incremental heap canonicalization algorithm. In SPIN, 2005.
• 31: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 32: A. Jefferson Offutt , Zhenyi Jin , Jie Pan, The dynamic domain reduction procedure for test data generation, Software—Practice & Experience, v.29 n.2, p.167-193, Feb. 1999 [doi>10.1002/(SICI)1097-024X(199902)29:2<167::AID-SPE225>3.3.CO;2-M]
• 33: C. Pacheco and M. D. Ernst. Eclat: Automatic generation and classification of test inputs. In ECOOP, 2005.
• 34: Charles E. Perkins , Elizabeth M. Royer, Ad-hoc On-Demand Distance Vector Routing, Proceedings of the Second IEEE Workshop on Mobile Computer Systems and Applications, p.90, February 25-26, 1999
• 35: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 36: R. Rugina. Quantitative shape analysis. In 11th International Static Analysis Symposium (SAS'04), Aug. 2004.
• 37: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 38: A. Sobeih, M. Viswanathan, D. Marinov, and J. C. Hou. Finding bugs in network protocols using simulation code and protocol-specific heuristics. In ICFEM, volume 3785 of LNCS, 2005.
• 39: P. David Stotts , Mark Lindsey , Angus Antley, An Informal Formal Method for Systematic JUnit Test Case Generation, Proceedings of the Second XP Universe and First Agile Universe Conference on Extreme Programming and Agile Methods - XP/Agile Universe 2002, p.131-143, August 04-07, 2002
• 40: Willem Visser , Corina S. Pǎsǎreanu , Sarfraz Khurshid, Test input generation with java PathFinder, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 41: Willem Visser , Corina S. Păsăreanu , Radek Pelánek, Test input generation for red-black trees using abstraction, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101983]
• 42: Willem Visser , Corina S. Pǎsǎreanu , Radek Pelánek, Test input generation for java containers using state matching, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146243]
• 43: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 44: Tao Xie , Darko Marinov , David Notkin, Rostra: A Framework for Detecting Redundant Object-Oriented Unit Tests, Proceedings of the 19th IEEE international conference on Automated software engineering, p.196-205, September 20-24, 2004 [doi>10.1109/ASE.2004.61]
• 45: T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In TACAS, 2005.
• 46: G. Yorsh, T. W. Reps, and S. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In TACAS, 2004.
• 47: Y. Zhou, D. Marinov, W. Sanders, C. Zilles, M. d'Amorim, S. Lauterburg, R. M. Lefever, and J. Tucek. Delta execution for software reliability. To appear in HotDep, 2007.

INDEX TERMS

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

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

General Terms:
Performance, Verification

Keywords:
delta execution, model checking