Test Case Generation for Reactive Systems with Constraint Logic Programming

discrepancies between the actual and intended behaviors of a
system, or at increasing confidence that the two behaviors
conform. If specification documents exist, the description of
the intended behavior often is imprecise and incomplete.
Model-Based Testing is based on the idea to encode it in
explicit and executable behavior models. These may serve as
specification, or as grounds to automatically generate test
sequences: After suitable transformations, traces of the model
can be used to test an implementation.

We show how test case generation for concurrent reactive
systems specified in a time-synchronous graphical language is
performed. To this end, the model is translated into a
Constraint Logic Programming Language. The program is executed.
This yields symbolic traces of the model: traces of sets of I/O
signals. Test case generation often boils down to finding
elements in the model's state space. In order to alleviate the
state space explosion problem, directed search and strategies
for storing sets of states (and checking inclusion or computing
differences) are deployed. We discuss the relationship with
model checking and tabled resolution.