Modularisation Plug-in Tutorial

Modularisation Plug-in Tutorial

The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstrates some basic principles of introducing modules during the development process.

Sluice Control Example

The example is a sluice with two doors connecting areas with dramatically different pressures. The pressure difference makes it unsafe to open a door unless the pressure is leveled between the areas connected by the door. The purpose of the system is to adjust the pressure in the sluice area and control the door locks to allow a user to get safely inside to outside. Such system can be deployed, for example, on a submarine to allow divers to get out while submerged.

The system parts are two doors that can be operated independently of each other and a pressure controller that allows the change of pressure in the sluice area. The following is a schematic depiction of the system.

The system is summarised with the following set of requirements:

1. the system allows a user to get inside or outside by leveling pressure between room and a destination
2. the system has three locations - outside, sluice and inside
3. the system has two doors - door1, connecting outside and sluice, and door2, connecting sluice and inside;
4. there is a device to change pressure in sluice;
5. a door may be opened only if the pressures in the locations it connects is equalised;
6. at most one door is open at any moment;
7. the pressure can only be switched on when the doors are closed.