Protocol validation using a pumping-based approach

Two pumping theorems are derived for a network N of CFSMs (communicating finite state machines). 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. The authors 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, they develop a pumping-based approach for detecting deadlocks and unspecified receptions in a network of CFSMs. The experimental results of applying this new approach to validate several communication protocols are shown