REVERSE REACHABILITY ANALYSIS - A NEW TECHNIQUE FOR DEADLOCK DETECTION ON COMMUNICATING FINITE-STATE MACHINES

The communicating finite state machines can exchange messages over bounded FIFO channels. In this paper, a new technique, called reverse reachability analysis, is proposed to detect deadlocks on the communication between the communicating finite state machines. The technique is based on finding reverse reachable paths starting from possible deadlock states. If a reverse reachable path can reach the initial global state, then deadlock occurs. Otherwise the communication is deadlock-free. The effectiveness of the technique has been verified by some real protocols such as a specification ot X.25 call establishment/clear protocol and Bartlet's alternating bit protocol.