Exercise 2 --- ELG 7187C --- Winter 2008

(January 302, 2008, 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 this system of two communicating components performs the following task: When the left component is in state I (idle), a user may push a button. This button-push is associated with the transition !a which, in turn, is associated with the transition ?a in the right component. When in the state A (active) the two components perform some task. When they have completed their task, they perform the transition back to the idle state (or as soon as they get the information that the other machine has completed its task the return to the idle state - there are different interpretations, depending on whether the two components communication by rendezvous or by input/output interactions).

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 a, b and c (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 a, b and c (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 "!a" transition from state I back to state I is introduced (Note: This modified component is non-deterministic - it means that sometimes a button-push does not get the left component into the A state). Do again the three tasks above.