The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - Sept.-Oct. (2008 vol.34)
pp: 597-613
Marcelo d'Amorim , University of Illinois at Urbana-Champaign, Urbana
Steven Lauterburg , University of Illinois at Urbana-Champaign, Urbana
Darko Marinov , University of Illinois at Urbana-Champaign, Urbana
ABSTRACT
We present Delta Execution, a technique that speeds up state-space exploration of object-oriented programs. 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. We exploit the fact that many execution paths in state-space exploration partially overlap. Delta Execution simultaneously operates on several states/heaps and shares the common parts across the executions, separately executing only the "deltas" where the executions differ. We implemented Delta Execution in two model checkers: JPF, a popular general-purpose model checker for Java programs, and BOX, a specialized model checker that we developed for efficient exploration of sequential Java programs. The results for bounded-exhaustive exploration of ten basic subject programs and one larger case study show that Delta Execution reduces exploration time from 1.06x to 126.80x (with median 5.60x) in JPF and from 0.58x to 4.16x (with median 2.23x) in BOX. The results for a non-exhaustive exploration in JPF show that Delta Execution reduces exploration time from 0.92x to 6.28x (with median 4.52x).
INDEX TERMS
Software/Program Verification, Model checking, Testing and Debugging
CITATION
Marcelo d'Amorim, Steven Lauterburg, Darko Marinov, "Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs", IEEE Transactions on Software Engineering, vol.34, no. 5, pp. 597-613, Sept.-Oct. 2008, doi:10.1109/TSE.2008.37
REFERENCES
[1] JPF Webpage, http:/javapathfinder.sourceforge.net, 2008.
[2] S. Anand, C.S. Pasareanu, and W. Visser, “JPF-SE: A Symbolic Execution Extension to Java PathFinder,” Proc. Int'l Conf. Tools and Algorithms for Construction and Analysis of Systems, pp. 134-138, 2007.
[3] T. Andrews, S. Qadeer, S.K. Rajamani, J. Rehof, and Y. Xie, “Zing: A Model Checker for Concurrent Software,” Proc. Int'l Conf. Computer Aided Verification, pp. 484-487, 2004.
[4] C. Artho, V. Schuppan, A. Biere, P. Eugster, M. Baur, and B. Zweimüller, “JNuke: Efficient Dynamic Analysis for Java,” Proc. Int'l Conf. Computer Aided Verification, pp. 462-465, 2004.
[5] T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani, “Automatic Predicate Abstraction of C Programs,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 203-213, 2001.
[6] T. Ball and S.K. Rajamani, “Bebop: A Symbolic Model Checker for Boolean Programs,” Proc. Int'l SPIN Workshop Model Checking of Software, pp. 113-130, 2000.
[7] C. Boyapati, S. Khurshid, and D. Marinov, “Korat: Automated Testing Based on Java Predicates,” Proc. Int'l Symp. Software Testing and Analysis, pp. 123-133, 2002.
[8] R.E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,” ACM Computing Surveys, vol. 24, no. 3, pp. 293-318, 1992.
[9] C. Cadar, V. Ganesh, P.M. Pawlowski, D.L. Dill, and D.R. Engler, “EXE: Automatically Generating Inputs of Death,” Proc. ACM Conf. Computer and Comm. Security, pp. 322-335, 2006.
[10] E. Clarke, D. Kroening, and F. Lerda, “A Tool for Checking ANSI-C Programs,” Proc. Tools and Algorithms for the Construction and Analysis of Systems, pp. 168-176, 2004.
[11] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. The MIT Press, 1999.
[12] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng, “Bandera: Extracting Finite-State Models from Java Source Code,” Proc. Int'l Conf. Software Eng., pp. 439-448, 2000.
[13] C. Csallner and Y. Smaragdakis, “JCrasher: An Automatic Robustness Tester for Java,” Software—Practice and Experience, vol. 34, pp. 1025-1050, 2004.
[14] M. d'Amorim, “Efficient Explicit-State Model Checking of Programs with Dynamically Allocated Data,” PhD thesis, Univ. of Illinois at Urbana-Champaign, Oct. 2007.
[15] M. d'Amorim, S. Lauterburg, and D. Marinov, “Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs,” Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 50-60, 2007.
[16] M. d'Amorim, C. Pacheco, T. Xie, D. Marinov, and M.D. Ernst, “An Empirical Comparison of Automated Generation and Classification Techniques for Object-Oriented Unit Testing,” Proc.IEEE Int'l Conf. Automated Software Eng., pp. 59-68, 2006.
[17] M. d'Amorim, A. Sobeih, and D. Marinov, “Optimized Execution of Deterministic Blocks in Java PathFinder,” Proc. Int'l Conf. FormalMethods and Software Eng., vol. 4260, pp. 549-567, 2006.
[18] P.T. Darga and C. Boyapati, “Efficient Software Model Checking of Data Structure Properties,” Proc. ACM SIGPLAN Conf. Object-Oriented Programming Systems, Languages, and Applications, pp. 363-382, 2006.
[19] C. DeMartini, R. Iosif, and R. Sisto, “A Deadlock Detection Tool for Concurrent Java Programs,” Software—Practice and Experience, vol. 29, no. 7, pp. 577-603, 1999.
[20] P. Godefroid, “Model Checking for Programming Languages Using Verisoft,” Proc. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp. 174-186, 1997.
[21] P. Godefroid, N. Klarlund, and K. Sen, “DART: Directed Automated Random Testing,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, vol. 40, pp. 213-223, 2005.
[22] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[23] R. Iosif, “Exploiting Heap Symmetries in Explicit-State Model Checking of Software,” Proc. IEEE Int'l Conf. Automated Software Eng., p. 254, 2001.
[24] J-Sim, http:/www.j-sim.org/, 2008.
[25] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, “Symbolic Model Checking: $10^{20}$ States and Beyond,” Proc. IEEE Symp. Logic in Computer Science, pp. 1-33, 1990.
[26] S. Khurshid, C.S. Pasareanu, and W. Visser, “Generalized Symbolic Execution for Model Checking and Testing,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 553-568, Apr. 2003.
[27] V. Kuncak, P. Lam, and M. Rinard, “Role Analysis,” Proc. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.17-32, 2002.
[28] F. Lerda and W. Visser, “Addressing Dynamic Issues of Program Model Checking,” Proc. Int'l SPIN Workshop Model Checking of Software, pp. 80-102, 2001.
[29] O. Lhotak and L. Hendren, “Jedd: A BDD-Based Relational Extension of Java,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 158-169, 2004.
[30] M. Musuvathi and D.L. Dill, “An Incremental Heap Canonicalization Algorithm,” Proc. Int'l SPIN Workshop Model Checking of Software, pp. 28-42, 2005.
[31] M. Musuvathi, D. Park, A. Chou, D.R. Engler, and D.L. Dill, “CMC: A Pragmatic Approach to Model Checking Real Code,” Proc. Symp. Operating Systems Design and Implementation, pp. 75-88, Dec. 2002.
[32] M. Musuvathi and S. Qadeer, “Iterative Context Bounding for Systematic Testing of Multithreaded Programs,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 446-455, 2007.
[33] A.J. Offutt, Z. Jin, and J. Pan, “The Dynamic Domain Reduction Procedure for Test Data Generation,” Software—Practice and Experience, vol. 29, no. 2, pp. 167-193, 1999.
[34] C. Pacheco and M.D. Ernst, “Eclat: Automatic Generation and Classification of Test Inputs,” Proc. European Conf. Object-Oriented Programming, pp. 504-527, July 2005.
[35] C.E. Perkins and E.M. Royer, “Ad-Hoc On-Demand Distance Vector Routing,” Proc. IEEE Workshop Mobile Computing Systems and Applications, pp. 90-100, 1999.
[36] S. Qadeer, “Daisy File System,” Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software, 2004.
[37] Robby, M.B. Dwyer, and J. Hatcliff, “Bogor: An Extensible and Highly-Modular Software Model Checking Framework,” Proc. European Software Eng. Conf. and SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 267-276, 2003.
[38] R. Rugina, “Shape Analysis Quantitative Shape Analysis,” Proc. Static Analysis Symp., pp. 228-245, 2004.
[39] K. Sen, D. Marinov, and G. Agha, “CUTE: A Concolic Unit Testing Engine for C,” Proc. European Software Eng. Conf. and the Int'l Symp. Foundations of Software Eng., pp. 263-272, Sept. 2005.
[40] A. Sobeih, M. Viswanathan, D. Marinov, and J.C. Hou, “Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics,” Proc. Int'l Conf. Formal Eng. Methods, pp. 235-250, 2005.
[41] D. Stotts, M. Lindsey, and A. Antley, “An Informal Formal Method for Systematic JUnit Test Case Generation,” Proc. XP/Agile Universe Conf., pp. 131-143, 2002.
[42] Sun Microsystems, jstat: Java Virtual Machine Statistics Monitoring Tool, http://java.sun.com/j2se/1.5.0/docs/tooldocs/ sharejstat.html, 2008.
[43] M. Veanes, C. Campbell, W. Schulte, and N. Tillmann, “Online Testing with Model Programs,” Proc. European Software Eng. Conf. and the ACM SIGSOFT Symp. the Foundations of Software Eng, pp.273-282, 2005.
[44] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, “Model Checking Programs,” Automated Software Eng., vol. 10, no. 2, pp.203-232, Apr. 2003.
[45] W. Visser, C.S. Pasareanu, and S. Khurshid, “Test Input Generation with Java PathFinder,” Proc. Int'l Symp. Software Testing and Analysis, pp. 97-107, 2004.
[46] W. Visser, C.S. Pasareanu, and R. Pelanek, “Test Input Generation for Java Containers Using State Matching,” Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 37-48, 2006.
[47] J. Whaley and M.S. Lam, “Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 131-144, 2004.
[48] T. Xie, D. Marinov, and D. Notkin, “Rostra: A Framework for Detecting Redundant Object-Oriented Unit Tests,” Proc. IEEE/ACM Int'l Conf. Automated Software Eng., pp. 196-205, Sept. 2004.
[49] T. Xie, D. Marinov, W. Schulte, and D. Notkin, “Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution,” Proc. Int'l Conf. Tools and Algorithms for Construction and Analysis of Systems, pp. 365-381, Apr. 2005.
[50] G. Yorsh, T.W. Reps, and S. Sagiv, “Symbolically Computing Most-Precise Abstract Operations for Shape Analysis,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 530-545, 2004.
[51] Y. Zhou, D. Marinov, W. Sanders, C. Zilles, M. d'Amorim, S. Lauterburg, R.M. Lefever, and J. Tucek, “Delta Execution for Software Reliability,” Proc. Workshop Hot Topics in System Dependability, June 2007.
20 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool