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.
- R. Alur, T. A. Henzinger, O. Kupferman, and M. Vardi. Alternating refinement relations. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR '98), volume 1466 of LNCS, pages 163--178, 1998. Google ScholarDigital Library
- C. Artho, H. Barringer, A. Goldberg, K. Havelund, S. Khurshid, M. Lowry, C. Pasareanu, G. Rosu, K. Sen, W. Visser, and R. Washington. Combining test case generation and runtime verification. Theor. Comput. Sci., 336(2--3):209--234, 2005. Google ScholarDigital Library
- 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.Google Scholar
- K. Beck. Extreme Programming Explained: Embrace Change. Addison-Wesley, 2001. Google ScholarDigital Library
- K. Beck. Test-Driven Development: By Example. Addison-Wesley, 2002. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- L. de Alfaro and T. A. Henzinger. Interface automata. In Proceedings of the 8th European Software Engineering Conference and the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 109--120. ACM, 2001. Google ScholarDigital Library
- E. Gamma and K. Beck. JUnit: A regression testing framework, 2001. http://www.junit.org.Google Scholar
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI'05), pages 213--223, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- W. Grieskamp, Y. Gurevich, W. Schulte, and M. Veanes. Generating finite state machines from abstract state machines. In ISSTA'02, volume 27 of Software Engineering Notes, pages 112--122. ACM, 2002. Google ScholarDigital Library
- W. Grieskamp and N. Kicillof. A schema language for coordinating construction and composition of partial behavior descriptions. In J. Whittle, L. Geiger, and M. Meisinger, editors, SCESM, pages 59--66. ACM, 2006. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385--394, 1976. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- 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). Google ScholarDigital Library
- 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. Google ScholarDigital Library
- N. Tillmann and W. Schulte. Unit tests reloaded: Parameterized unit testing with symbolic execution. IEEE software, 23:38--47, 2006. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- J. Tretmans and A. Belinfante. Automatic testing with formal methods. In EuroSTAR'99: 7th European Int. Conference on Software Testing, Analysis & Review, Barcelona, Spain, November 8--12, 1999. EuroStar Conferences, Galway, Ireland.Google Scholar
- M. Utting and B. Legeard. Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2006. Google ScholarDigital Library
- G. Venolia, R. DeLine, and T. LaToza. Software development at microsoft observed. Technical Report MSR-TR-2005-140, Microsoft Research, October 2005.Google Scholar
- W. Visser, C. S. Pasareanu, and R. Pelánek. Test input generation for red-black trees using abstraction. In D. F. Redmiles, T. Ellman, and A. Zisman, editors, ASE, pages 414--417. ACM, 2005. Google ScholarDigital Library
Index Terms
- Achieving both model and code coverage with automated gray-box testing
Recommendations
Grey-box concolic testing on binary code
ICSE '19: Proceedings of the 41st International Conference on Software EngineeringWe present grey-box concolic testing, a novel path-based test case generation method that combines the best of both white-box and grey-box fuzzing. At a high level, our technique systematically explores execution paths of a program under test as in ...
Parameterized unit testing: theory and practice
ICSE '10: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2Unit testing has been widely recognized as an important and valuable means of improving software reliability, as it exposes bugs early in the software development life cycle. However, manual unit testing is often tedious and insufficient. Testing tools ...
Automatically performing weak mutation with the aid of symbolic execution, concolic testing and search-based testing
Automating software testing activities can increase the quality and drastically decrease the cost of software development. Toward this direction, various automated test data generation tools have been developed. The majority of existing tools aim at ...
Comments