Organisation: 
Department of Software Technology  CWI Amsterdam and
Computing Science Institute, University of Nijmegen (The Netherlands)


Functionality: 
Test generation for Finite State Machines (FSMs) using symmetry

Tools used: 
OPEN/CAESAR

Period: 
1998.

Description: 
Test generation and execution are often hampered by the large state
spaces of the systems involved. In automata (or transition system)
based test algorithms, taking advantage of symmetry in the behaviour
of specification and implementation may substantially reduce the amount
of tests. This work presents a framework for describing and exploiting
symmetries in black box test derivation methods based on finitestate
machines (FSMs). In particular, an algorithm is presented that, for a
given symmetry relation on the traces of an FSM, computes a
subautomaton characterizing the FSM up to symmetry.
A prototype of the algorithm (called kernel) has been implemented using the OPEN/CAESAR and BCG environments for transition system manipulation available in the CADP toolset. The kernel algorithm has been experimented (by instantiating it to the framework of symmetries defined by repeating patterns) on an example describing a chatbox, i.e. a system that allows to talk with users connected to it. After one joins (connects to) the chatbox, one can talk with all other connected users, until one leaves (disconnects). The kernel algorithm has been experimented on chatboxes with up to 4 users (having up to 4096 reachable state), leading to a significantly smaller kernel for each of the models, provided a suitable symmetry is given. 
Conclusion: 
A general, FSM based, framework for exploiting symmetry in
specifications and implementations in order to reduce the amount of
tests has been proposed and illustrated experimentally. It appears
that the OPEN/CAESAR environment is suitable for describing transition
system exploration algorithms such as kernel. Moreover, since the
kernel algorithm uses two finite state machines, the OPEN/CAESAR
environment had to be generalized such as it allows now to
simultaneously explore several transition systems.

Publications: 
[RomijnSpringintveld98]
Judi Romijn and Jan Springintveld.
"Exploiting Symmetry in Protocol Testing".
In: Proceedings of the IFIP Joint International Conference on
Formal Description Techniques and Protocol Specification, Testing,
and Verification FORTE/PSTV'98 (Paris, France), November 1998.
Full version available as Technical Report CSIR9821,
Computing Science Institute, University of Nijmegen, September 1998.
Available online at: http://www.cs.kun.nl/~judi/papers/symmetry_full.ps.gz or also from the CADP Web site in PDF or PostScript 
Contact:  Judi Romijn Computing Science Institute University of Nijmegen Toernooiveld 1 (Room A5025) 6525 ED Nijmegen P.O. Box 9010 6500 GL Nijmegen The Netherlands Tel: +31 (0)24 36 52599 Fax: +31 (0)24 36 53137 Email: judi@cs.kun.nl 
Further remarks:  This application, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software 