Instructions - ac6g12/SCsystems GitHub Wiki

Lecturer: Michael Butler

Due: 4pm Tuesday 18th December 2012

Hand in to: C-BASS

This coursework will contribute 30% towards the total for the unit. It is intended to re-enforce your ability to write Event-B models, and also to get you used to working as a group. The coursework is to be done in groups of three students. Only one person from each group should submit the solution for that group.

System Requirements

The coursework involves developing a formal specification of an ambulance dispatch system using the Event-B language. The dispatch system is responsible for allocating ambulances to emergency incidents and monitoring the progress of the response to each incident. The dispatch system is required to process each incident in the following way:

  1. An emergency call is received by a control assistant.

  2. The control assistant logs the details of the incident including the location, the emergency level (on a scale of 1 to 5) and the medical capabilities required.

  3. After the incident is logged, an ambulance is allocated to the incident. The ambulance allocated to an incident should have sufficient medical capabilities to deal with the incident.

  4. The ambulance is selected from a pool of available ambulances. Ambulances are distributed across several base stations. The ambulance allocated to an incident should be as close as possible to the location of the incident.

  5. When allocating ambulances, an incident with a higher emergency level gets priority over an incident with a lower emergency level.

  6. If there is no ambulance with sufficient capabilities available, then an ambulance with fewer capabilities can be allocated and this is treated as a reduced response. When the ambulance allocated to an incident has sufficient capabilities, then this is treated as a full response.

  7. While the ambulance is on its way to the incident, the control assistant allocates a hospital to the incident. It should try to allocate a hospital that is close to the incident.

  8. So that the dispatch system may track the progress of an incident, an ambulance informs the system when it has arrived at the incident. After that it informs the dispatch system that it has arrived at a hospital. Finally an ambulance will return to its base so that it is available for allocation to another incident.

  9. If the number of incidents with reduced response goes above a threshold, then a warning is given to the dispatch manager.

  10. If the number of incidents with no allocated ambulances reaches a threshold, then a warning is given to the dispatch manger.

Tasks

  • Model the ambulance dispatch system using Event-B. Start by drawing a class diagram for your model. You are advised to use extension refinement to layer the specification as follows: start with an Event-B model that does not deal with locations, then refine this model to include locations. Make sure to
  1. Identify appropriate Event-B sets and constants
  2. Identify appropriate Event-B variables and invariants
  3. Identify appropriate Event-B events

  • Analyse your Event-B models using the Rodin tool including the ProB plug-in.

  • For each of the requirements 1..10 above, provide a few sentences explaining whether and how that requirement is addressed in your models.

Hints

To model closeness of locations, use the concept of distance between locations. To model the distance between locations, you could introduce a constant function distance of the following type:

distance ∈ (LOCATION × LOCATION) → ℕ

where distance(l1↦l2) represents the distance between locations l1 and l2. You do not have to specify distance any further. With this function, we can say that l1 is closer to l2 than to l3 if distance(l1,l2) < distance(l1,l3).

If you have more than two sets that need to be disjoint, it can be convenient to use the Event-B partition operator:

partition(A,B1,B2,B3,…,Bn)

This is equivalent to saying that each Bi is a subset of A and that all the B’s are disjoint from each other:

Bi ∩ Bj = ∅

The partition operator can also be used to specify an enumerated type:

context C constants north south east west sets COMPASS axioms @axm1 partition(COMPASS, {north}, {south}, {east}, {west}) end

Instructions

Each group should submit a written report (PDF format, one report per group) giving your answer to each of the tasks above (Class diagram, Event-B models and all supporting text). Make sure your Event-B models are appropriately commented. You should also include an archive of your project from the Rodin tool containing your models. You should use the automated hand-in facilities found on the student Web pages at:

https://handin.ecs.soton.ac.uk/

The group allocations are available on the course web page.

If you feel there are any ambiguities in the requirements feel free to make your own interpretation, but make sure any interpretations you make are clearly indicated in the report. Make sure your group's number and names are provided on the front of your report. You should work together as a group to accomplish these tasks. It is the responsibility of each group to arrange their own group meetings. You should avoid discussing your solutions with other groups.