An example of reachability analysis (taken from [Braek])

Note: This was included in the course notes of 2010. The notation for global states is slightly different than in the course notes of 2011. - Page with diagrams only

The idea is to explore all possible execution paths that may occur with different input sequences and different interleaving of internal transitions due to concurrency. This is called reachability analysis (one analyses the specification of the system to find all global states that are reachable from the initial state). A global system state consists of a particular state for each concurrent process participating in the system and the set of messages in transit (or in the case of SDL systems, the content of the input queues of all processes).

An example is given in the book by Braek: Figue 12.1 shows two SDL processes, and Figure 12.2 shows corresponding transition charts that include intermediate states (which represent the state of a process during a transition - after the acceptance of a new input, and before the generation of the output produced by that transition).

Figure 12.3 (below) shows a reachability analysis (incomplete, since certain branches have not been explored). Each transition in the reachability diagram corresponds to an input accepted by a process or an output produced by a process (or the environment). The state at the bottom represents a deadlock: there is no transition that could be executed in this state. Notation: A global state, represented as an oval, is identified "x1, s1 / x2, s2z" where si (i = 1 or 2) is the state of the left or right state machine (respectively) and xi is the content of its input queue. Notes:

• State (2) - and others - shown in Figure 12.2 are intermediate states. According to the SDL semantics, the process cannot accept any message from the input queue within such an intermediate state.
• The transition annotated "!Ra", "!Rb", "!Ea" and "!Eb" are due to the environment that generates an Ra or Rb message, respectively.
  • Open System: Here nothing is assumed about the environment of the two processes A and B. That means the inputs from the environment may occur at any time in any order.
  • A more sensible assumption may be to construct a Closed System: adding the specification of the behavior of the environment. In the case of our example, one may assume that there are two additional processes Ua and Ub that communicate with the processes A and B, respectively. They could have the following behavior: (1) send an Rx signal, (2) wait for an Ax signal, (3) then send a Ex signal and then start again at point (1). Note: A Closed System has no interactions with its environment.
• Figure 12.3 contains two states that are labelled with two lines. Each line, in fact, represents a different global state. It would have been more correct to draw two states in each of these cases. For instance, the transition labelled "!Rb" leads to the state "-3/Sb.Rb,1" (on the left side of the diagram) which will lead to the transition "?Sb" (Sb is consumed from the input queue of process B - we note that "-3/Sb.Rb,1" means that the left process, process A is in state 3 and its input queue is empty, and process B is in state 1 and its input queue contains the messages Sb followed by Rb). However, Sb is not specified as a possible input for process B in state 1, therefore this is a situation of "unspecified reception", which in SDL semantics means that the received message will be dropped, however, it may also means that the two processes are not compatible with one another and this is a design error.
• The part of the diagram that is shown in yellow represents the reachability analysis at a more abstract level where the intermediate states of Figure 12.2 are not explicitely shown. In such an analysis, each SDL transition is considered to be executed completely in mutual exclusion with other transitions of other processes within the system. Such an analysis generates less global states, but the hypothesis that transitions are executed in mutual exclusion may not be realistic; one has to be careful with this approach.
• As mentioned above, the global state "-,3 / -,3" is a deadlock. It is reached after the messages Sa and Sb, generated from global state "-,2 / -,2", have been lost because they represented an "unspecified reception" in the receiving states 3 of the two state machines. After having analysed the behavior of the system for the case that a single message Ra or Rb has been received from the environment (both machines come back to their initial state), one may be surprised to find this deadlock. Question: How can such a deadlock be avoided ? - How should we revise the design of this distributed system in order to obtain a design without problems ? - There is no general answer to this question. However, in many cases where situations of unspecified reception are encountered, one can add transitions to the original specification for consuming the unspecified input; but what action should follow when such a message is received ? - In many cases, such problems are due to "competing initiatives" (as in our example, where the two sides have taken contradicting initiatives). In his paper from 1984, Gouda proposed to give priority to one of the sides. If in our example we give priority to the right side, the right side may ignore the message Sb in state 3, while the left side, when it receives message Sa in state 3 should follow the "priority proposal" from the right side and do what is foreseen for the reception of this message, that is, send Ga and go into state 8.