We use the MIO Workbench for verification of service implementations and service protocols. This page offers two examples for download.
Flight Booking
The flight booking service allows a client to book a flight including seat reservation.
Our simplified version of the flight booking scenario serves well for instructional purposes. Extract the file into your Eclipse workspace. You’ll find five MIOs:
- The protocol of the service itself
- The protocol of the service client
- Two implementations of the service; each of which is different with regard to internal actions.
It is interesting to check the protocol against the implementations using various notions of refinement, and checking compatibility of the partner protocol against the protocol of the service and its implementations.
eUniversity
The eUniversity example shows the applicability of strict-observational refinement and compatibility to the domain of services and service orchestrations. The example includes 8 MIOs.
- There are two orchestrations – one which is correct, and one which is incorrect
- Three protocols are given which the orchestration refines – two provided, one required
- Another three protocols are given which must be compatible to the other three protocols.
Again, it is interesting to check the protocol against the implementations using various notions of refinement, and checking compatibility of the partner protocol against the protocol of the service and its implementations.