Exploiting Symmetry in Protocol Testing

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 finite-state 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:	[Romijn-Springintveld-98] 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 CSI-R9821, Computing Science Institute, University of Nijmegen, September 1998. Available on-line 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 E-mail: [email protected]
Further remarks:	This application, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page