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:
- 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 !
- 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 !
- 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.