Comments on solutions for Exercise 3

Task 1

An initial service specification could be the following:

• PROC Main = invite^A ; accept^B ; ack^A ; Talk END
• PROC Talk = ( t^A ||| t^B ) ; (Talk [] (term^A ; a-term^B) ) END

Task 2

We have to check the restrictions R1 and R2 which should be satisfied (otherwise the protocol derivation algorithm described in the paper of Khendek et al. may not give a correct protocol specification).

The service specification is simple enough; we do not need to construct the derivation trees for the procedures of the specification; we can determine the sets SP (starting places) and EP (ending places) intuitively.

We find that R1 is not satisfied for the choice operator: SP(Talk) = {A, B} but should consist of a single place. As far as EP of the two alternatives are concerned, there appears to be no problem, because the only way Talk can terminate is through the second alternative: so both alternative end on place B only.

Since R1 is not satisfied we should find a different service specification which satisfies R1 and R2 and which is still close to the original problem defined in the text of the execise. One possibility is to argue that a telephone conversation does not really mean that both parties talk at the same time; a reasonable conversion should have alternative talkers. Then we may rewrite the Talk procedure as follows:

• PROC Talk =  t^A ; t^B ; (Talk [] (term^A ; a-term^B) ) END

This definition satisfies R1 and R2.

Task 3

In order to apply the formula given in the paper, we have to determine also the sets preceding places and following places for each occurence of the ";" operator. This is quite easy. Concerning the numbers that are sent as content of the messages, it is not necessary that they are obtained from a numbering through the derivation trees. The requirement is that they are all different (so you may use different choices). Here is the protocol specification obtained from the above revised service specification (I hope I do not make too many errors):

• For place A
  • PROC Main = invite^A ; s2(3) ; r2(6) ;  ack^A ; s1(2) ; r1(2) ; Talk END
  • PROC Talk =  t^A ; s2(8) ;  r2(9) ; (Talk [] (term^A ; s2(10) ) END
• For place B
  • PROC Main = r1(3) ; accept^B ; s1(6) ; Talk END
  • PROC Talk =  r1(8) ; t^B ; s1(9) ; r1(8) ; (Talk [] (r1(10) ; a-term^B) ) END

The sending and receiving from/to the same place (shown in blue above) can be dropped (optimization).

Task 4

Modifying the original service specification for Main, we obtain the following

• PROC Main = invite^A ; ( (accept^B ; ack^A ; Talk) []  see-busy^A ) END

However, the choice operator does not satisfy R1 here. It may be reasonable to introduce an action at place B, called busy, which means that the system component at B indicates that the user is busy. Then we get the modified Main that satisfies R1 (but not R2; however this does not matter since nothing follows after one of the alternatives has been executed).

• PROC Main = invite^A ; ( (accept^B ; ack^A ; Talk) []  (busy^B ; see-busy^A ) END

Derived protool specification (the Talk part does not change);

• For place A
  • PROC Main = invite^A ; s2(3) ; ( ( r2(6) ;  ack^A ; s1(2) ; r1(2) ; Talk ) [] (r2(12) ; see-busy^{A ) )} END
• For place B
  • PROC Main = r1(3) ; ( ( accept^B ; s1(6) ; Talk ) [] ( busy^B ; s1(12)) ) END

Task 5

One may write down initially the following specification for Main:

• PROC Main = invite^A ; ( (accept^B ; ack^A ; Talk) []  (busy^B ; see-busy^A ) [] no-answer^A ) END

Again, R1 is not satisfied. For justifying the following revised specification, we may argue as follows: (a) no-answer is better left with place B, and (b) they way place A find out that there is no answer, is by a time-out. Revised specification:

• PROC Main = invite^A ; ( (accept^B ; ack^A ; Talk) []  (busy^B ; see-busy^A ) [] no-answer^B ; time-out^A ) END

This leads to the protocol specification:

• For place A
  • PROC Main = invite^A ; s2(3) ; ( ( r2(6) ;  ack^A ; s1(2) ; r1(2) ; Talk ) [] (r2(12) ; see-busy^A ) [] (r2(13) ; time-out^A ) END
• For place B
  • PROC Main = r1(3) ; ( ( accept^B ; s1(6) ; Talk ) [] ( busy^B ; s1(12)) ) [] ( no-answer^B ; s1(13)) ) END

This protocol can be optimized to make it more realistic: The part shown in brown may be dropped, since the time-out in place A will be used to detect the occurrence of this alternative (and it is not necessary to send a message).

Task 6

If we take the original form of the service specification for Talk and modify it in a straightforward manner, we obtain the following:

• PROC Talk = ( t^A ||| t^B ) ; (Talk [] (term^A ; a-term^B) [] (term^B ; a-term^A) ) END

Considering only the second choice operator, we have a choice distributed over places A and B, actually both sides may start the disconnect at the same time. We may have to introduce a distributed choice protocol, or we have to constrain the possibility of choices made available to the difrerent parties. If we inspire us from the revised service specification given for Task 2, we may impose that only the side that is allowed to talk my choose to terminate the call. Then we get the specification:

• PROC Talk =  ( t^A ; TalkB ) [] (term^A ; a-term^B)     END
• PROC TalkB = ( t^B ; Talk ) [] (term^B ; a-term^A)     END

The two choice operators satisfy R1 (but not R2, however, this is OK since no action follows when on of the alternatives terminates). The derivation of the protocol is straightforward.