This is an exercise in relation with protocol derivation from service specification. The process algebra notation of Khendek's paper is suggested for describing the service. The service is a simple telephone conversation. Note that the verbs written in italics in the following represent local service primitives at the side of user A or user B.

Service specification: User A invites user B for a telephone conversation. Then user B accepts the call. Then this fact is acknowledged by A, and both users start talking concurrently. Talking is a sequence of talk operations. Talking is interrupted when user A terminates the call. Then user B will accept-termination.

Tasks

1. Formalize the service description using the notation used in the paper by Khendek.
2. Verify that all assumptions made in the paper by Khendek are satisfied.
3. If so, use the approach described in Khendek's paper to derive a protocol specification, that is, a specification of the two user agents for user A and user B, respectively. If some assumption is not satisfied, explain the issue and try to find a modification of the service specification that would satisfy the assumption. Then derive the corresponding protocol.
4. Consider the following addition to the service specification: After inviting B, A may see-busy-signal. Do the three steps 1 through 3 again.
5. Consider (4) plus the possibility that user B does not answer (does not do the accept operation). Do the three steps 1 through 3 again.
6. Consider the original service specification with the following extension: User B may also take the initiative to terminate the call. Do the three steps 1 through 3 again.