On the random walk method for protocol testing

Abstract

An important method for testing large and complex protocols repeatedly generates and tests a part of the reachable state space by following a random walk; the main advantage of this method is that it has minimal memory requirements. We use the coupling technique from Markov chain theory to show that short trajectories of the random walk sample accurately the reachable state space of a nontrivial family of protocols, namely, the symmetric dyadic flip-flops. This is the first evidence that the random walk method is amenable to rigorous treatment. Following West’s original reasoning, efficient sampling of the reachable state space by random walk suffices to ensure effectiveness of testing. Is, however, efficient sampling of the random walk necessary for the effectiveness of the random walk method? In the context of Markov chain theory, “small cover time” can be thought of as a simpler justification for the effectiveness of testing by random walk; all symmetric (reversible) protocols possess the small cover time property. Thus the conclusions of our work are that (i)the random walk method can be understood in the context of known Markov chain theory, and (ii)symmetry (reversibility) is a general protocol style that supports testing by random simulation.