The traveler first logs on to a flight server by sending his/her user name and password (login!). Then, (s)he can look for a flight (searchFlight!), and then receive either a flight identifier and price (reply?) according to the wished destination and departure and return dates, or an expiration of his/her connexion. Once the request is replied, depending on his/her preferences (internal choice specified with tau transitions), the user can either start a new flight request or end up on a final state.

The flight server service starts by receiving a user name and password (login?). Next, this service can receive and reply several flight requests or terminate in its final state after a time-out.

The Compatibility Matrix:

Analysis:

Considering the unspecified-receptions compatibility notion, the protocols are not compatible because they can deadlock even though they seem to be compatible from an observable point of view. The deadlcok may occur when the traveler internally decides to evolve into state t5 while the flight server terminates in state f5 after a time-out. At these states, neither internal evolution nor synchronisation can be executed and the traveler deadlocks.

The global compatibility for the flight server and traveler protocols is equal to 0.89 (t=0.7).