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

The communicating finite state machines can exchange messages over bou nded FIFO channels. In this paper, a new technique, called reverse rea chability analysis, is proposed to detect deadlocks on the communicati on between the communicating finite state machines. The technique is b ased on finding reverse reachable paths starting from possible deadloc k states. If a reverse reachable path can reach the initial global sta te, then deadlock occurs. Otherwise the communication is deadlock-free . The effectiveness of the technique has been verified by some real pr otocols such as a specification ot X.25 call establishment/clear proto col and Bartlet's alternating bit protocol.