Download class16_symstra.pdf

Contents : Symstra: A Framework for Generating Object-Oriented Unit Tests using Symbolic Execution Tao Xie1 Darko Marinov2 Wolfram Schulte3 David Notkin1 1 2 Dept. of Computer Science & Engineering Univ. of Washington Seattle WA 98195 USA Department of Computer Science University of Illinois Urbana-Champaign IL 61801 USA 3 Microsoft Research One Microsoft Way Redmond WA 98052 USA taoxie notkin @cs.washington.edu marinov@cs.uiuc.edu schulte@microsoft.com Abstract. Object-oriented unit tests consist of sequences of method invocations. Behavior of an invocation depends on the method s arguments and the state of the receiver at the beginning of the invocation. Correspondingly generating unit tests involves two tasks: generating method sequences that build relevant receiverobject states and generating relevant method arguments. This paper proposes Symstra a framework that achieves both test generation tasks using symbolic execution of method sequences with symbolic arguments. The paper de nes symbolic states of object-oriented programs and novel comparisons of states. Given a set of methods from the class under test and a bound on the length of sequences Symstra systematically explores the object-state space of the class and prunes this exploration based on the state comparisons. Experimental results show that Symstra generates unit tests that achieve higher branch coverage faster than the existing test-generation techniques based on concrete method arguments. 1 Introduction Object-oriented unit tests are programs that test classes. Each test case consists of a xed sequence of method invocations with xed arguments that explores a particular aspect of the behavior of the class under test. Unit tests are becoming an important component of software development. The Extreme Programming discipline 5 for instance leverages unit tests to permit continuous and controlled code changes. Unlike in traditional testing it is developers (not testers) who write tests for every aspect of the classes they develop. However manual test generation is time consuming and so typical unit test suites cover only some aspects of the class. Since unit tests are gaining importance many companies now provide tools frameworks and services around unit tests. Tools range from specialized test frameworks such as JUnit 18 or Visual Studio s new team server 25 to automatic unit-test generation such as Parasoft s Jtest 27 . However existing test-generation tools typically do not provide guarantees about the generated unit-test suites. In particular the suites rarely satisfy the branch-coverage test criterion 6 let alone a stronger criterion such as the bounded intra-method path coverage 3 of the class under test. We present an approach that uses symbolic execution to exhaustively explore bounded method sequences of the class under test and to generate tests that achieve high branch and intra-method path coverage for complex data structures such as container implementations. 1.1 Background Generating test sequences involves two tasks: generating method sequences that build relevant receiver-object state and generating relevant method arguments. Researchers have addressed this problem several times. Most tools generate test sequences using concrete representations. A popular approach is to use (smart) random generation this approach is embodied in tools such as Jtest 27 (a commercial tool for Java) or JCrasher 13 and Eclat 26 (two research prototypes for Java). Random tests generated by these tools often execute the same sequences 34 and are not covering (do not cover all sequences). The AsmLT model-based testing tool 15 16 uses concrete-state space-exploration techniques 12 to generate covering method sequences. But AsmLT requires the user to carefully choose suf ciently large concrete domains for method arguments and the right abstraction functions to guarantee the covering. Tools such as Korat 8 are able to generate non-isomorphic object graphs that can be used for testing but they do not generate covering test sequences. King proposed in the 70 s to use symbolic execution for testing and veri cation 20 . Because of the advances in constraint solvers this technique recently regained the attention for test generation. For example the BZ-TT tool uses constraint solving to derive method sequences from B speci cations 22 . However the B speci cations are not object-oriented. Khurshid et al. 19 33 proposed an approach for generating tests for Java classes based on symbolic execution. They show that their generation based on symbolic execution generates tests faster than their model checking of method sequences with concrete arguments. This is expected: symbolic representations describe not only single states but sets of states and when applicable symbolic representations can yield large improvements witnessed for example by symbolic model checking 24 . The

INFO HASH : 3b99ed6f49e7d2837f9f2cba0c7f11d7fa9316c3

Download now

File Size: 129.6 kb