Christoph Lembeck (Universitaet Muenster)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Constraint Solving for Generating Glass-Box Test Cases
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Abstract
~~~~~~~~
Glass-box testing tries to cover paths through the tested code, based
on a given criterion such as def-use chain coverage. When generating
glass-box test cases manually, the user is likely to overlook some
def-use chains. Moreover it is difficult to find suitable test cases
which cause certain def-use chains to be passed. We have developed a
tool which automatically generates a system of test cases for a piece
of Java byte code, which ensures that all def-use chains are
covered. The tool consists of a symbolic Java virtual machine (SJVM)
and a system of dedicated constraint solvers. The SJVM uses the
constraint solvers in order to determine which branches the symbolic
execution needs to consider. A backtracking mechanism is applied in
case that several branches remain feasible. Thus we have applied
implementation techniques known from functional logic and constraint
programming to handle the considered applications problems.
As already mentioned, the main difficulty of the approach above is
checking, whether the collected constraints remain solvable, or if
they are already contradicting each other. For this purpose we have
implemented a dedicated constraint solver, which is integrated into
our SJVM and is connected to the symbolic execution engine by a
special constraint solver manager that administrates the gathering of
new constraints and facilitates an incremental growth and solving of
the constraints. The SJVM will be presented by Roger Müller and will
not be explained in detail here. We will rather focus on the system of
constraint solvers and the constraint solver manager, which acts as an
interface between the symbolic execution engine of the SJVM and the
different constraint solvers we have implemented to handle different
kinds of constraints. Since the constraints produced by the execution
engine arrive incrementally at the CSM, it has to store each of them
for further calculations. As the backtracking mechanism of our tool
also guarantees that the latest constraints added to the system are
the first that will be removed again, the CSM needs a constraint stack
to maintain them.
Moreover, the constraint solver manager analyzes the constraints and
transforms them to some kind of normal form. Additionally, it selects
the most appropriate constraint solver for each system of constraints
and distributes each constraint to the corresponding constraint
solver, in case that the overall system of constraints consisted of
several independent subsystems. Therefor it is Necessary to normalize
the incomming constraints by removing fractions, modulo operations and
the Java specific typecasts with the goal of getting easier manageable
polynomial constraints.
As a result of the calculations of the constraint solvers the SJVM
will be able to present the user a set of test cases consiting of both
constraints and numerical values that lead to the specified test paths
and the symbolical and numerical results representing the results of
the program as they will be generated using a real virtual machine.