ELG 7187C --- Winter 2013 --- Assignment 2 --- Reachability Analysis

(February 4, 2013, due date: February 25)

  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:

  2. behaviors

  3. 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 !
  1. 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 !
  2. 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.