A Case Study in Formal Testing and an Algorithm for Automatic Test Case Generation with Symbolic Transition Systems
Floor Sietsma

Abstract:
We present a case study of two black-box testing techniques. We
compare constraint logic programming with symbolic transition
systems. Both techniques generate automatically test cases out of the
specification of an algorithm. After our case study we decided to
design an algorithm to improve the technique using symbolic transition
systems with a way to generate test cases automatically based on a
coverage criterion. Because we do black-box testing and we have no
access to the implementation of the algorithm, we apply this coverage
criterion to the specification. Our algorithm attempts to cover all
states of the symbolic transition system that models the specification
of the algorithm. This task is complicated due to non-determinism and
symbolic constraints in the model. We use an external constraint
solver to solve these constraints. We try to simplify them as much as
possible because constraint solvers only have limited power and often
use a great amount of computational resources.