Reachability analysis

It is used to determine which global states can be reached by a distributed system which consists of a certain number of local entities that communicated by the exchange of messages.

In the simplest case, the medium between two entities is modeled by two FIFO queues in opposite directions, which contain the messages in transit (that are sent, but not yet consumed).

The question whether the number of messages remains bounded in the case of finite state entities is in general not decidable.

The following are design flaws: As an example, we consider the system of two protocol entities that exchange the messages ma, mb, mc and md with one another, as shown in the first diagram.

The third diagram shows the result of the reachability analysis for this protocol in the form of a global state machine.

One sees that this example has a bounded global state space - the maximum number of messages that may be in transit at the same time is two.

Protocols using the Internet IP service should also deal with the possibility of out-of-order delivery.

Higher-level protocols normally use a session-oriented Transport service which means that the medium provides reliable FIFO transmission of messages between any pair of entities.

The basic models are the following: The original paper identifying the problem of unspecified receptions,[6] and much of the subsequent work, assumed a single input queue.

[7] Sometimes, unspecified receptions are introduced by a race condition, which means that two messages are received and their order is not defined (which is often the case if they come from different partners).

[8] With the systematic use of reception pools, reachability analysis should check for partial deadlocks and messages remaining forever in the pool (without being consumed by the entity) [9] Most of the work on protocol modeling use finite-state machines (FSM) to model the behavior of the distributed entities (see also Communicating finite-state machines).

Therefore often so-called extended FSM models are used, such as supported by languages like SDL or UML state machines.

We mention only two examples: The SPIN model checker and a toolbox for the construction and analysis of distributed processes.

The diagram shows two protocol entities and the messages exchanged between them.
The diagram shows two finite state machines that define the dynamic behavior of the respective protocol entities.
This diagram shows a state machine model of the global system consisting of the two protocol entities and two FIFO channels used for the exchange of messages between them.