Protocol validation using a pumping-based approach

Although the pumping theorem for a finite state machine is well-known, it is interesting to us whether the pumping phenomenon exists for a network of Communicating Finite State Machines (CFSM's). In this paper we derive two pumping theorems for a network N of CFSM's. Each pumping theorem describes a set of conditions under which a feasible event sequence of N can be "pumped" to produce an infinite set of feasible event sequences of N. We show that if a feasible event sequence E satisfying the conditions in one pumping theorem does not result in a deadlock or unspecified reception, neither does any event sequence derived by "pumping" E. Based on these results, we develop a pumping-based approach for detecting deadlocks and unspecified receptions in a network of CFSM's. We also show the experimental results of applying this new approach to validate several communication protocols.