Roger A. Mueller (Universitaet Muenster) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Issues in the Implementation of a Symbolic Java Virtual Machine for Test Case Generation ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Abstract ~~~~~~~~ Software testing is considered to be a more and more important part of the software development process. As manual testing is rather time-consuming, costly and most likely imprecise, developers increasingly rely on software testing tools. Software testing is commonly split into black- and glass-box testing. Black-box testing derives test cases from the specification of the user requirements, whereas glass-box testing is based solely on the code. The test utility market has traditionally been dominated by tools that either manage test cases (i.e. regression test suites) or check existing test cases against a pre-defined coverage criterion, both glass- or black-box. If a coverage criterion is not met, it is usually up to the user to figure out which new test cases are required to gain a better coverage. Our test tool generates test cases for glass-box testing automatically. Up to now, three ways to implement test case generation for structural criteria have been discovered. The first and simplest is the random generation of test cases. Obviously this technique is naive but easy to implement. The main drawback is that despite the high costs (every generated example has to be checked for validity and relevance) this method cannot guarantee the quality of its results. The dynamic approach actually executes the software. Test cases are discovered on the fly usually by local or global search (please refer to the related work section for more details). The static approach usually uses symbolic execution, which we will describe in a modified version in this paper. Based on a user defined criterion a symbolic execution of the Java byte code is performed. Symbolic essentially means that the value of a variable is an expression depending on some input parameters (e.g. the parameters of the considered method) rather than a number. As a byproduct of the symbolic execution a system of equations is built, which describes the relation of the variables at the current instruction. If the symbolic execution reaches a branching instruction like ifgt, where a new constraint has to be added, a constraint solver is used in order to determine which branch to take. If two (or more) alternatives are still possible, the symbolic Java virtual machine (SJVM) tries them one by one using a backtracking mechanism similar to that of the implementation of logic and functional-logic languages like the Babel Abstract Machine (LBAM) or the Warren Abstract Machine (WAM). At the end of the symbolic computation, one particular solution of the generated system of constraints will be determined. This solution represents a test case in the sense that the considered byte code has to produce the computed result, if executed with the appropriate values for the input parameter. Due to backtracking, alternative computation paths and the corresponding test cases will also be determined. If the symbolic computation would closely follow the actual concrete computation, this would be too expensive and unnecessarily precise. Thus, in our approach the symbolic computation is guided by a user-specified coverage criterion. In the present work, we will focus on the well-known def-use-chain criterion If the symbolic execution is performed for a given procedure or method the generated system of equations should be solvable for suitable input parameters. The solutions represent the input(s) required for a set of test cases that satisfy the given test criterion.