Exercise 2 --- ELG 7187C --- Winter 2007

(February 2, 2007, due date February 13)

We consider the protocol defined by the following diagram which contains two state machines that communicate with one another. You may think of telephone call establishment. On the left is the telephone (and the user) and the right represents the central office of the telephone company. R means ready, C means connected, Req means call request, Inc means incoming call notification, and Term means termination of the call.

Part A: In this exercise, we propose to interpret these two diagrams in three different manners:

  1. As two LTS that communicate by rendezvous for the three interactions Req, Int and Term (that means, we ignore the + and - signs): Please consider the composition of these two machines and indicate its behavior (in the form of a single LTS), that means, do a reachability analysis (do you detect any design error ? ). If you find a problem with the design, please suggest a modification of the defined behavior for the machines in order to resolve the identified problem. Please explain !
  2. As two IOA that communicate by direct coupling for the three interactions Req, Int and Term (the - means output and + means input): Please consider the composition of these two machines and indicate its behavior (in the form of a single state machine), that means, do a reachability analysis (do you detect any design error ? ). If you find a problem with the design, please suggest a modification of the defined behavior for the machines in order to resolve the identified problem. Please explain !
  3. As two communicating finite state machines that communicate by message passing with queuing: Please consider the composition of these two machines and indicate its behavior (in the form of a single transition diagram), that means, do a reachability analysis (do you detect any design error ? ) . If you find a problem with the design, please suggest a modification of the defined behavior for the machines in order to resolve the identified problem. If the reachable queue length is not bounded you will not be able to perform a complete reachability analysis.  Please explain !
Part B:  Now we assume that the specification of the left machine has been changed and an additional "- Term" transition from state C back to state C is introduced (Note: This modified component is non-deterministic). Do again the three tasks above.