Test input generation for java containers using state matching

ABSTRACT

The popularity of object-oriented programming has led to the wide use of container libraries. It is important for the reliability of these containers that they are tested adequately. We describe techniques for automated test input generation of Java container classes. Test inputs are sequences of method calls from the container interface. The techniques rely on state matching to avoid generation of redundant tests. Exhaustive techniques use model checking with explicit or symbolic execution to explore all the possible test sequences up to predefined input sizes. Lossy techniques rely on abstraction mappings to compute and store abstract versions of the concrete states; they explore underapproximations of all the possible test sequences.We have implemented the techniques on top of the Java PathFinder model checker and we evaluate them using four Java container classes. We compare state matching based techniques and random selection for generating test inputs, in terms of testing coverage. We consider basic block coverage and a form of predicate coverage - that measures whether all combinations of a predetermined set of predicates are covered at each basic block. The exhaustive techniques can easily obtain basic block coverage, but cannot obtain good predicate coverage before running out of memory. On the other hand, abstract matching turns out to be a powerful approach for generating test inputs to obtain high predicate coverage. Random selection performed well except on the examples that contained complex input spaces, where the lossy abstraction techniques performed better.

REFERENCES

• 1: 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
• 2: S. Anand, C. S. Pǎsǎreanu, and W. Visser. Symbolic execution with abstract subsumption checking. In Proc. 13th International SPIN Workshop, 2006.
• 3: T. Ball. A theory of predicate-complete test coverage and generation, 2004. Microsoft Research Technical Report MSR-TR-2004--28.
• 4: T. Ball, D. Hoffman, F. Ruskey, R. Webber, and L. J. White. State generation and automated class testing. Softw. Test., Verif. Reliab., 10(3):149--170, 2000.
• 5: André Baresel , David Binkley , Mark Harman , Bogdan Korel, Evolutionary testing in the presence of loop-assigned flags: a testability transformation approach, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 6: 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
• 7: 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
• 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: 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]
• 10: 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
• 11: 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]
• 12: 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
• 13: A. Groce and W. Visser. Heuristics for model checking Java programs. STTT Journal, 6(4), December 2004.
• 14: Walter J. Gutjahr, Partition Testing vs. Random Testing: The Influence of Uncertainty, IEEE Transactions on Software Engineering, v.25 n.5, p.661-674, September 1999 [doi>10.1109/32.815325]
• 15: 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.
• 16: G. J. Holzmann and R. Joshi. Model-driven software verification. In Proc. 11th International SPIN Workshop, 2004.
• 17: 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
• 18: 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
• 19: Java PathFinder. http://javapathfinder.sourceforge.net.
• 20: JTest. http://www.parasoft.com/jsp/home.jsp.
• 21: S. Khurshid, C. S. Pǎsǎreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2003.
• 22: 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]
• 23: 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
• 24: C. S. Pǎsǎreanu, R. Pelanek, and W. Visser. Concrete model checking with abstract matching. In Proc. 17th International Conference on Computer Aided Verification (CAV), 2005.
• 25: 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]
• 26: 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]
• 27: Paolo Tonella, Evolutionary testing of classes, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 28: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 29: 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]
• 30: 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
• 31: Elaine J. Weyuker , Bingchiang Jeng, Analyzing Partition Testing Strategies, IEEE Transactions on Software Engineering, v.17 n.7, p.703-711, July 1991 [doi>10.1109/32.83906]
• 32: 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]
• 33: T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Proc. 11th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2005.

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:
Experimentation, Reliability, Verification