Test input generation with java PathFinder

ABSTRACT

We show how model checking and symbolic execution can be used to generate test inputs to achieve structural coverage of code that manipulates complex data structures. We focus on obtaining branch-coverage during unit testing of some of the core methods of the red-black tree implementation in the Java TreeMap library, using the Java PathFinder model checker. Three different test generation techniques will be introduced and compared, namely, straight model checking of the code, model checking used in a black-box fashion to generate all inputs up to a fixed size, and lastly, model checking used during white-box test input generation. The main contribution of this work is to show how efficient white-box test input generation can be done for code manipulating complex data, taking into account complex method preconditions.

REFERENCES

• 1: The economic impacts of inadequate infrastructure for software testing. National Institute of Standards and Technology, Planning report 02-3, May 2002.
• 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: Paul Ammann , Paul E. Black, A Specification-Based Coverage Metric to Evaluate Test Sets, The 4th IEEE International Symposium on High-Assurance Systems Engineering, p.239-248, November 17-19, 1999
• 4: Paul E. Ammann , Paul E. Black , William Majurski, Using Model Checking to Generate Tests from Specifications, Proceedings of the Second IEEE International Conference on Formal Engineering Methods, p.46, December 09-11, 1998
• 5: C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu, and W. Visser. Experiments with test case generation and runtime analysis. In Proceedings of the 10th International Workshop on Abstract State Machines, Taormina, Italy, March 2003.
• 6: T. Ball. Abstraction-guided test generation: A case study, 2003. Microsoft Research Technical Report MSR-TR-2003-86.
• 7: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 8: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 9: Boris Beizer, Software Testing Techniques, John Wiley & Sons, Inc., New York, NY, 1990
• 10: 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
• 11: G. Brat, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, W. Visser, and R. Washington. Experimental evaluation of verification and validation tools on martian rover software. In Proceedings of the SEI/CM Software Model Checking Workshop, Pittsburgh, March 2003. To Appear in Formal Methods in System Design Journal.
• 12: Juei Chang , Debra J. Richardson, Structural specification-based testing: automated support and experimental evaluation, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.285-302, September 06-10, 1999, Toulouse, France
• 13: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 14: L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering, Sept. 1976.
• 15: 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]
• 16: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 17: Claudio DeMartini , Radu Iosif , Riccardo Sisto, A deadlock detection tool for concurrent Java programs, Software—Practice & Experience, v.29 n.7, p.577-603, June 1999 [doi>10.1002/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V]
• 18: Michael R. Donat, Automating Formal Specification-Based Testing, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.833-847, April 14-18, 1997
• 19: Roong-Ko Doong , Phyllis G. Frankl, The ASTOOT approach to testing object-oriented programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.2, p.101-130, April 1994 [doi>10.1145/192218.192221]
• 20: Foundations of Software Engineering, Microsoft Research. The AsmL test generator tool. http://research.microsoft.com/fse/asml/doc/AsmLTester.html.
• 21: Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.146-162, September 06-10, 1999, Toulouse, France
• 22: 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]
• 23: John B. Goodenough , Susan L. Gerhart, Toward a theory of test data selection, ACM SIGPLAN Notices, v.10 n.6, p.493-510, June 1975
• 24: Arnaud Gotlieb , Bernard Botella , Michel Rueher, Automatic test data generation using constraint solving techniques, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.53-62, March 02-04, 1998, Clearwater Beach, Florida, United States
• 25: Wolfgang Grieskamp , Yuri Gurevich , Wolfram Schulte , Margus Veanes, Generating finite state machines from abstract state machines, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 26: M. P. E. Heimdahl, S. Rayadurgam, W. Visser, D. George, and J. Gao. Auto-generating test sequences using model checkers: A case study. In Proc. 3rd International Workshop on Formal Approaches to Testing of Software (FATES), Montreal, Canada, Oct. 2003.
• 27: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with blast. In Proceedings of the Tenth International SPIN Workshop on Model Checking of Software, volume 2648 of LNCS, 2003.
• 28: Hyoung Seok Hong , Insup Lee , Oleg Sokolsky , Hasan Ural, A Temporal Logic Based Theory of Test Coverage and Generation, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.327-341, April 08-12, 2002
• 29: J. C. Huang, An Approach to Program Testing, ACM Computing Surveys (CSUR), v.7 n.3, p.113-128, Sept. 1975 [doi>10.1145/356651.356652]
• 30: S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Warsaw, Poland, April 2003.
• 31: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 32: B. Korel. Automated test data generation for programs with procedures. San Diego, CA, 1996.
• 33: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 34: D. Marinov. Testing Using a Solver for Imperative Constraints. PhD thesis, Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 2004. (to appear).
• 35: Darko Marinov , Sarfraz Khurshid, TestEra: A Novel Framework for Automated Testing of Java Programs, Proceedings of the 16th IEEE international conference on Automated software engineering, p.22, November 26-29, 2001
• 36: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 37: J. Offutt and A. Abdurazik. Generating tests from UML specifications. In Proc. Second International Conference on the Unified Modeling Language, Oct. 1999.
• 38: C. Pasareanu and W. Visser. Verification of java programs using symbolic execution and invariant generation. In Proceedings of the 11th International SPIN Workshop on Model Checking of Software, volume 2989 of LNCS. Springer-Verlag, 2004.
• 39: John Penix , Willem Visser , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verification of time partitioning in the DEOS scheduler kernel, Proceedings of the 22nd international conference on Software engineering, p.488-497, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337364]
• 40: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 41: C. V. Ramamoorthy, S.-B. F. Ho, and W. T. Chen. On the automated generation of program test data. IEEE Transactions on Software Engineering, 2(4), 1976.
• 42: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 43: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 44: G. Yorsh, T. W. Reps, and S. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In Proceedings of the 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Barcelona, Spain, April 2004.

INDEX TERMS

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

General Terms:
Algorithms, Verification

Keywords:
coverage, model checking, red-black trees, symbolic execution, testing object-oriented programs