• The original specification of this example has a four-way rendezvous for the interactions dMR and dMS. Each execution of one of these interactions involves all four parties: I, R, MIR and MRI. This is clearly not realistic, because it means when I initiates a disconnect request (dMS interaction) then R must do the same at the same time. Such synchrony is not realistic in a distributed environment.

The questions:

1. Analyzing a communication protocol with LTSA. Study the specification of the simplified TCP model ( CommProtocol.lts ) by comparing the LTS model with the SDL model given in the course notes (see at the end of this page). Do you note any differences ? - You may use the LTSA tool to perform a simulated execution of the model, or use the CHECK facilities to find problems with the model. Notes:

   • There are two LTS-machines representing the communication medium (the underlying IP network) in the two direction of message transfer. They are written in such a way that in each direction, there can be at most one message in transit; but there may be two messges in transit, one in each direction.
   • The situation where in the SDL model discussed in the course notes, there is a message to be received for which the behavior definition of the receiving component has nothing mentioned for this case (called non-specified reception) will normally lead to a deadlock in the corresponding LTS model (because in the LTS model the different components communicate by rendezvous and a message which is not foreseen by the receiving component cannot be received - there is no possible rendezvous - the system gets blocked.
   • Identify the reason why the behavior of this model may lead to a deadlock. Find a solution to this problem by suggesting some changes to the model about how the disconnection is handled. (Suggestion: instead of having a single message signalling disconnection, introduce a disconnect confirmation message which must be received before a telephone can go back to the initial state). Verify that the modified model does not have any deadlock.
   • Your report should include: (1) explanation of the reason for deadlock, (2) revised system specification, (3) explanation of the verification results obtained from LTSA for the revised specification.



2. The figure above shows the behavior of two LTSs A and B that communicate with one another by rendezvous for the interactions a, b, c, while x and y are interactions with the environment, as indicated in the architecture diagram (a) below: Please consider the composition of these twa 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 !

• (a) Please solve this problem by hand.
• (b) Please use the LTSA tool to solve this problem. See pointers about LTSA. A number of examples can be found here (mainly for course SEG-2106); you may look at the example CoffeeMachine (which was also explained in the course notes of ELG-7187C). A short introduction to using the tool is given in Lab2 for course SEG-2106.
• (c) In the global behavior of this system, are the number of executions of the interactions x related to the number of executions of the interactions y ? - Explain!
• 
3. Now we assume that the transition diagrams shown above define the behavior of two IOAs A, and B where the interactions now are inputs or outputs as indicated in the architecture diagram (b). Please consider the composition of these two machines and indicate their joint 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 !
• (a) Please solve this problem by hand. - Do you make any assumptions about the environment of the two IOAs ? - Explain!
• (b) Please, look at the LTSA example "IOA example". It shows how one can use the LTSA tool (which was built for analysing LTS systems) to analyse IOA compositions. Use this approach to do a reachability analysis with LTSA, and report on the kind of information you can get from LTSA about the behavior of the global system.
• (c) Assume that the environment at the right interface of the architecture contains a component that receives the y interactions. Suppose that this component has two states: ready and busy. In the ready state it has a transition for receiving a y interaction, but not in state busy. We assume that there is a spontaneous transition going from the busy state to the ready state. With the behavior specified for component B, there may be a non-specified reception of y in the busy state of the component in the environment. Please modify the behavior of B and revise the behavior of the environment component in such a way that a non-specified reception is avoided (but keeping the busy state in which no y can be received). Explain your design.
4. Now consider the machines A, and B with inputs and outputs (as under point (2)), but assume that they communicate asynchronously, that is an output is first put into a queue before it is received by the other side (that is, assume that we have communicating finite state machines with FIFO queuing). Please consider the composition of these two machines and indicate their 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 may not be able to perform a complete reachability analysis.  Please explain ! - What happens if you assume that in the case of non-specified reception the received message is dropped (as in the case of the SDL language) ? - You may use LTSA to do your analysis.