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 receiver-object 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 defines 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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)
Ball, T.: A theory of predicate-complete test coverage and generation. Technical Report MSR-TR-2004-28, Microsoft Research, Redmond, WA (April 2004)
Ball, T., Larus, J.R.: Using paths to measure, explain, and enhance program behavior. IEEE Computer 33(7), 57–65 (2000)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pp. 203–213 (2001)
Beck, K.: Extreme programming explained. Addison-Wesley, Reading (2000)
Beizer, B.: Software Testing Techniques. International Thomson Computer Press (1990)
Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proc. 26th International Conference on Software Engineering, pp. 326–335 (2004)
Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: Proc. International Symposium on Software Testing and Analysis, pp. 123–133 (2002)
Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Softw. Pract. Exper. 30(7), 775–802 (2000)
Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. In: Proc. 16th European Conference Object-Oriented Programming, pp. 231–255 (June 2002)
Clark, S.B., Barrett, W.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Csallner, C., Smaragdakis, Y.: JCrasher: an automatic robustness tester for Java. Software: Practice and Experience 34, 1025–1050 (2004)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Technical Report HPL-2003-148, HP Laboratories, Palo Alto, CA (2003)
Foundations of Software Engineering, Microsoft Research. The AsmL test generator tool, http://research.microsoft.com/fse/asml/doc/AsmLTester.html
Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: Proc. International Symposium on Software Testing and Analysis, pp. 112–122 (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Proc. 10th SPIN Workshop on Software Model Checking, pp. 235–239 (2003)
JUnit (2003), http://www.junit.org
Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proc. 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 553–568 (April 2003)
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University (June 1998)
Legeard, B., Peureux, F., Utting, M.: A comparison of the LIFC/B and TTF/Z test-generation methods. In: Proc. 2nd International Z and B Conference, pp. 309–329 (January 2002)
Liskov, B., Guttag, J.: Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, Reading (2000)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Microsoft Visual Studio Developer Center (2004), http://msdn.microsoft.com/vstudio/
Pacheco, C., Ernst, M.D.: Eclat documents. Online manual (Oct. 2004), http://people.csail.mit.edu/people/cpacheco/eclat/
Parasoft. Jtest manuals version 5.1. Online manual (July 2004), http://www.parasoft.com/
Pugh, W.: A practical algorithm for exact array dependence analysis. Commun. ACM 35(8), 102–114 (1992)
Robby, Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: Proc. 9th ESEC/FSE, pp. 267–276 (2003)
Robby, Dwyer, M.B., Hatcliff, J., Iosif, R.: Space-reduction strategies for model checking dynamic systems. In: Proc. 2003 Workshop on Software Model Checking (July 2003)
Schlenker, H., Ringwelski, G.: POOC: A platform for object-oriented constraint programming. In: Proc. 2002 International Workshop on Constraint Solving and Constraint Logic Programming, pp. 159–170 (June 2002)
Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proc. 15th IEEE International Conference on Automated Software Engineering, pp. 3–12 (2000)
Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with Java PathFinder. In: Proc. 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 97–107 (2004)
Xie, T., Marinov, D., Notkin, D.: Rostra: A framework for detecting redundant object-oriented unit tests. In: Proc. 19th IEEE International Conference on Automated Software Engineering, pp. 196–205 (September 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xie, T., Marinov, D., Schulte, W., Notkin, D. (2005). Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)