Presentation / Exposé :
On-the-fly model-checking techniques to generate
test cases in conformance testing
Invited conference.
CIRM Workshop on verification and proofs,
December 1998, Marseille, France.
Slides
Claude Jard Pampa/IRISA/CNRS.
The first part of the talk presents the main principles of TGV, a prototype
tool developed by IRISA Rennes and Verimag Grenoble. Its aim is to
automatically generate test cases from formal specifications in the context of
conformance testing of protocols. TGV is based on testing theories which
consider models of transitions systems with a distinction between inputs and
outputs and a conformance relation relating implementations to specifications.
In TGV, test selection is achieved by a test purpose specified by an abstract
automaton. TGV is based on on-the-fly verification techniques which allow to
produce a test case in a lazy way by the construction of parts of the state
graph of the specification.
The on-the-fly generation induces a particular tool architecture composed of a
stack of modules each of them providing an API for the construction of parts of
intermediate state graphs. TGV can be connected to the API of the SDL simulator
ObjectGéode and the API of the LOTOS simulator of the CADP tool-box. Using this
API, the different modules perform a synchronous product of the specification
test graph and the test purpose, hiding and renaming, tau^*-reduction and
determinization, and finally test generation.
The second part of the talk presents this test generation algorithm.
The algorithm is adapted from the Tarjan's algorithm which computes maximal
strongly connected components.
The principle here is to build a subgraph of sequences leading to acceptor
states of the test purpose. It is quite similar with the model-checking
algorithm for reachability properties with adaptations for subgraph synthesis
and elimination of controllability conflicts.
This algorithm produces correct test cases having loops and minimal
INCONCLUSIVE verdicts.
We conclude with a small example which additionally advocates for the use of
static analysis on source specifications in order to avoid unnecessary
unfoldings and improve test generation.