Erroneous state detection in piecewise FIFO system

Distributed systems normally use concurrent systems which communicate via unbounded FIFO channels. Despite well-known difficulties in analyzing such systems, they are of significant interest as they can describe a wide range of communication protocols. In this paper, we have studied the problem of computing the set of reachable states of a FIFO system composed of piecewise components. This problem is closely related to computing the set of all possible channel contents. For each control location which can be realized by the sequence diagrams produced by the SPIN. We present a model checking approach to find set of reachable states of FIFO channels via different paths in which some of the paths end in an erroneous state.