Exploiting symmetry in protocol testing

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 behavior of specification and implementation may substantially reduce the amount of tests. We present a framework for describing and exploiting symmetries in black box test derivation methods based on finite state machines (FSMs). An algorithm is presented that, for a given symmetry relation on the traces of an FSM, computes a subautomaton that characterizes the FSM up to symmetry. This machinery is applied to the classical W-method [Ch78,Vas73] for test derivation. Finally, we focus on symmetries defined in terms of repeating patterns.