ELG 7187C --- Winter 2009 --- Exercise 2 --- Reachability Analysis
(January 31, 2009, due date February 11)
- The figure above shows two LTSs A and B that communicate with one another by rendezvous for the interactions
a, b, c and d , while x and e are independent: 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 !
- (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 Lab1 for course SEG-2106 (see second part).
- The figure above shows two IOAs C and D where alll the interactions
a, b, c, d and e are with one another (the ! indicates output and ? indicates 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 !
- (a) Please solve this problem by hand.
- (b) What happens if machine D is modified and the two lower states are combined into a single state sending e and d interactions intermixed ?
- (c) 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. You may use this approach to deal with point (b).
- Now consider again the machines C and D, 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 these are two communicating finite state machines: 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 !