Achieving both model and code coverage with automated gray-box testing

ABSTRACT

We have devised a novel technique to automatically generate test cases for a software system, combining black-box model-based testing with white-box parameterized unit testing. The former provides general guidance for the structure of the tests in the form of test sequences, as well as the oracle to check for conformance of an application under test with respect to a behavioral model. The latter finds a set of concrete parameter values that maximize code coverage using symbolic analysis. By applying these techniques together, we can produce test definitions (expressed as code to be run in a test management framework) that exercise all selected paths in the model, while also covering code branches specific to the implementation. These results cannot be obtained from any of the individual approaches alone, as the model cannot predict what values are significant to a particular implementation, while parameterized unit testing requires manually written test sequences and correctness validations. We provide tool support, integrated into our model-based testing tool.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman , Moshe Y. Vardi, Alternating Refinement Relations, Proceedings of the 9th International Conference on Concurrency Theory, p.163-178, September 08-11, 1998
• 2: Cyrille Artho , Howard Barringer , Allen Goldberg , Klaus Havelund , Sarfraz Khurshid , Mike Lowry , Corina Pasareanu , Grigore Rosu , Koushik Sen , Willem Visser , Rich Washington, Combining test case generation and runtime verification, Theoretical Computer Science, v.336 n.2-3, p.209-234, 26 May 2005 [doi>10.1016/j.tcs.2004.11.007]
• 3: M. Barnett, W. Grieskamp, L. Nachmanson, W. Schulte, N. Tillmann, and M. Veanes. Towards a tool environment for model-based testing with AsmL. In Petrenko and Ulrich, editors, Formal Approaches to Software Testing, FATES 2003, volume 2931 of LNCS, pages 264--280. Springer, 2003.
• 4: Kent Beck , Cynthia Andres, Extreme Programming Explained: Embrace Change (2nd Edition), Addison-Wesley Professional, 2004
• 5: Beck, Test Driven Development: By Example, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 6: C. Campbell, W. Grieskamp, L. Nachmanson, W. Schulte, N. Tillmann, and M. Veanes. Testing concurrent object-oriented systems with spec explorer. In J. Fitzgerald, I. J. Hayes, and A. Tarlecki, editors, FM 2005: Formal Methods, International Symposium of Formal Methods Europe, volume 3582 of Lecture Notes in Computer Science, pages 542--547. Springer, 2005.
• 7: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 8: E. Gamma and K. Beck. JUnit: A regression testing framework, 2001. http://www.junit.org.
• 9: 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
• 10: W. Grieskamp. Multi-paradigmatic model-based testing. In K. Havelund, M. Núñez, G. Rosu, and B. Wolff, editors, FATES/RV 2006: Formal Approaches to Testing and Runtime Verification, volume 4262 of Lecture Notes in Computer Science, pages 1--19. Springer, 2006. invited contribution.
• 11: 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
• 12: Wolfgang Grieskamp , Nicolas Kicillof, A schema language for coordinating construction and composition of partial behavior descriptions, Proceedings of the 2006 international workshop on Scenarios and state machines: models, algorithms, and tools, May 27-27, 2006, Shanghai, China [doi>10.1145/1138953.1138966]
• 13: W. Grieskamp, N. Kicillof, and N. Tillmann. Action machines: a framework for encoding and composing partial behaviors. International Journal of Software Engineering and Knowledge Engineering, 16(5):705--726, 2006.
• 14: R. Grosu and S. A. Smolka. Monte carlo model checking. In N. Halbwachs and L. D. Zuck, editors, TACAS, volume 3440 of Lecture Notes in Computer Science, pages 271--286. Springer, 2005.
• 15: 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]
• 16: Z. Li, L. Tan, X. Wang, S. Lu, Y. Zhou, and C. Zhai. Have things changed now? -- An empirical study of bug characteristics in modern open source software. In ICSE: Proceedings 29th International Conference on Software Engineering, 2007.
• 17: H. Robinson. Finite state model-based testing on a shoestring. In Proceedings of the International Conference on Software Testing Analysis and Review (STARWEST 1999), Software Quality Engineering, San Jose, CA, USA, October 1999.
• 18: K. Sen and G. Agha. Cute and jCUTE: Concolic unit testing and explicit path model-checking tools. In 18th International Conference on Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 419--423. Springer, 2006. (Tool Paper).
• 19: K. Stobie. Model based testing in practice at microsoft. In Proceedings of the Workshop on Model Based Testing (MBT 2004), volume 111 of Electronic Notes in Theoretical Computer Science. Elsevier, 2004.
• 20: Nikolai Tillmann , Wolfram Schulte, Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution, IEEE Software, v.23 n.4, p.38-47, July 2006 [doi>10.1109/MS.2006.117]
• 21: O. Tkachuk, M. B. Dwyer, and C. S. Pasareanu. Automated environment generation for software model checking. In ASE, pages 116--129. IEEE Computer Society, 2003.
• 22: J. Tretmans and A. Belinfante. Automatic testing with formal methods. In EuroSTAR'99: 7^th European Int. Conference on Software Testing, Analysis & Review, Barcelona, Spain, November 8--12, 1999. EuroStar Conferences, Galway, Ireland.
• 23: Mark Utting , Bruno Legeard, Practical Model-Based Testing: A Tools Approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2006
• 24: G. Venolia, R. DeLine, and T. LaToza. Software development at microsoft observed. Technical Report MSR-TR-2005-140, Microsoft Research, October 2005.
• 25: 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]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing); Symbolic execution

General Terms:
Algorithms, Design, Verification

Keywords:
concolic execution, model-based testing, parameterized unit testing, symbolic execution, test-case generation