Reverse Reachability Analysis a New Technique for Deadlock Detection on Communicating Finite State Machines.
Journal
Softw., Pract. Exper.
Journal Volume
23
Journal Issue
9
Pages
965-979
Date Issued
1993
Author(s)
Hung, Yung-Chen
Abstract
Abstract 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 of X.25 call establishment/clear protocol and Bartlet's alternating bit protocol.
Type
journal article