Check 'n' crash: combining static checking and testing

ABSTRACT

We present an automatic error-detection approach that combines static checking and concrete test-case generation. Our approach consists of taking the abstract error conditions inferred using theorem proving techniques by a static checker (ESC/Java), deriving specific error conditions using a constraint solver, and producing concrete test cases (with the JCrasher tool) that are executed to determine whether an error truly exists. The combined technique has advantages over both static checking and automatic testing individually. Compared to ESC/Java, we eliminate spurious warnings and improve the ease-of-comprehension of error reports through the production of Java counterexamples. Compared to JCrasher, we eliminate the blind search of the input space, thus reducing the testing time and increasing the test quality.

REFERENCES

• 1: K. Beck and E. Gamma. Test infected: Programmers love writing tests. Java Report, 3(7):37--50, July 1998.
• 2: Dirk Beyer , Adam J. Chlipala , Rupak Majumdar, Generating Tests from Counterexamples, Proceedings of the 26th International Conference on Software Engineering, p.326-335, May 23-28, 2004
• 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: D. R. Cok and J. R. Kiniry. ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2. Technical Report NIII-R0413, Nijmegen Institute for Computing and Information Science, May 2004.
• 5: 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]
• 6: D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, Hewlett-Packard Systems Research Center, July 2003.
• 7: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically discovering likely program invariants to support program evolution, Proceedings of the 21st international conference on Software engineering, p.213-224, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302467]
• 8: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 9: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 10: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 11: M. Hapner, R. Burridge, R. Sharma, and J. Fialli. Java message service: Version 1.1. Sun Microsystems, Inc., Apr. 2002.
• 12: Erik Hatcher , Steve Loughran, JAVA development with Ant, Manning Publications Co., Greenwich, CT, 2003
• 13: David Hovemeyer , William Pugh, Finding bugs is easy, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028717]
• 14: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 15: T. Kremenek and D. Engler. Z-ranking: Using statistical analysis to counter the impact of static analysis approximations. In R. Cousot, editor, Static Analysis: 10th Annual International Static Analysis Symposium, pages 295--315. Springer, June 2003.
• 16: D. Kroening, A. Groce, and E. M. Clarke. Counterexample guided abstraction refinement via program execution. In J. Davies, W. Schulte, and M. Barnett, editors, Formal Methods and Software Engineering: 6th International Conference on Formal Engineering Methods, pages 224--238. Springer, Nov. 2004.
• 17: G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR98-06y, Department of Computer Science, Iowa State University, June 1998.
• 18: K. R. M. Leino. Efficient weakest preconditions. Technical Report MSR-TR-2004-34, Microsoft Research, Apr. 2004.
• 19: K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC/Java user's manual. Technical Report 2000-002, Compaq Computer Corporation Systems Research Center, Oct. 2000.
• 20: M. Musuvathi and D. Engler. Some lessons from using static analysis and software model checking for bug finding. In B. Cook, S. Stoller, and W. Visser, editors, SoftMC 2003: Workshop on Software Model Checking. Elsevier, July 2003.
• 21: Nick Rutar , Christian B. Almazan , Jeffrey S. Foster, A Comparison of Bug Finding Tools for Java, Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE'04), p.245-256, November 02-05, 2004 [doi>10.1109/ISSRE.2004.1]
• 22: H. Schlenker and G. Ringwelski. POOC: A platform for object-oriented constraint programming. In B. O'Sullivan, editor, Recent Advances in Constraints: Joint ERCIM/CologNet International Workshop on Constraint Solving and Constraint Logic Programming, pages 159--170. Springer, June 2002.
• 23: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 24: 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
• 25: M. Vaziri and D. Jackson. Checking properties of heap-manipulating procedures with a constraint solver. In H. Garavel and J. Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems: 9th International Conference, pages 505--520. Springer, Apr. 2003.
• 26: T. Xie and D. Notkin. Tool-assisted unit test selection based on operational violations. In Proceedings of the 18th Annual International Conference on Automated Software Engineering (ASE 2003), pages 40--48. IEEE Computer Society Press, Oct. 2003.
• 27: Y. Xie and D. Engler. Using redundancies to find errors. IEEE Transactions on Software Engineering, 29(10):915--928, Oct. 2003.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

  H. Information Systems
  H.5 INFORMATION INTERFACES AND PRESENTATION (I.7)
      H.5.2 User Interfaces (D.2.2, H.1.2, I.3.6)
          Subjects: Ergonomics; User-centered design

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program verification

General Terms:
Human Factors, Reliability, Verification

Keywords:
automatic testing, dynamic analysis, extended static checking, static analysis, test case generation, usability