Modularisation Plug-in Tutorial

Go to the plug-in description page.

TODO: This tutorial document is under construction

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.

Requirements 1-4 characterise the system by stating its goal and its major parts. The last three characterise the system behaviour. More precisely, they are the safety properties of the system.

The following diagram shows the stages of the system operation that let a user to get outside starting in the inside area.

The shaded rectagles denote a pressure level, high pressure area corresponds to a higher rectangle. The "u" label marks the current position of a system user. Initially, a user is inside and the sluice pressure is levelled with the outside pressure. Before the door connecting to the sluice is opened, the pressure is decreased to level it with the inside pressure. Once the door is open, the user moves in, the door is sealed again. Finally, the sluice pressure is set to match the outside pressure and the door leading may be safely opened.

Initial Model

The initial model contains three variables, one for each major system part.

variables door1 door2 pressure error

The typing is as follows:

invariants
 @inv1 door1 ∈ BOOL
 @inv2 door2 ∈ BOOL
 @inv3 pressure ∈ {0,1}
 @inv7 error ∈ BOOL 	

The requirement 6 that at most one door may be open at any given moment translates into the following model invariant

@inv4 error = FALSE ∧ door1 = door2 ⇒ door1 = FALSE

We also formally state the when it is safe to open a door

@inv5 error = FALSE ∧ door1 = TRUE ⇒ pressure = 0
@inv6 error = FALSE ∧ door2 = TRUE ⇒ pressure = 1

The two invariants above correspond to the 5th requirement.

The following is complete characterisation of the model events.

 event INITIALISATION
   then
     @act1 door1 ≔ FALSE
     @act2 door2 ≔ FALSE
     @act3 pressure ≔ 0
     @act4 error ≔ FALSE
 end
 event open1
   where
     @grd1 pressure = 0
     @grd2 door1 = FALSE
     @grd3 error = FALSE
   then
     @act1 door1 ≔ TRUE
     @act2 error :∈ BOOL
 end
 event close1
   where
     @grd1 door1 = TRUE
     @grd2 error = FALSE
   then
     @act1 door1 ≔ FALSE
     @act2 error :∈ BOOL
 end
 event open2
   where
     @grd1 pressure = 1
     @grd2 door2 = FALSE
     @grd3 error = FALSE
   then
     @act1 door2 ≔ TRUE
     @act2 error :∈ BOOL
 end
 event close2
   where
     @grd1 door2 = TRUE
     @grd2 error = FALSE
   then
     @act1 door2 ≔ FALSE
     @act2 error :∈ BOOL
 end
 event pressure_low
   where
     @grd1 door1 = FALSE
     @grd2 door2 = FALSE
     @grd3 error = FALSE
   then
     @act1 pressure ≔ 0
     @act2 error :∈ BOOL
 end
 event pressure_high
   where
     @grd1 door1 = FALSE
     @grd2 door2 = FALSE
     @grd3 error = FALSE
   then
     @act1 pressure ≔ 1
     @act2 error :∈ BOOL
 end

Preparing to the first Refinement

Since the purpose of the tutorial is to demonstrate the use of modules in a development, a link to a module appears very early - in the first refinement step. The strategy here is to decompose a model in such manner that the functionality of all the major components is encapsulated in independent modules while the main development does high-level management of components.

The first module is door controller. Its interface mirrors the modelling of door behaviour in the abstract model.

INTERFACE DoorController
VARIABLES door error
INVARIANTS
	@inv1 door ∈ BOOL
	@inv2 error ∈ BOOL	   
OPERATIONS

operation for opening a door

open   ≙       PRE
			@pre1: door = FALSE
			@pre2: error = FALSE
		RETURN error_status
		POST
			@post1: door' = TRUE
			@post2: error' ∈ BOOL
			@post3: error_status' = error'
		END

operation for closing a door

close   ≙      PRE
			@pre1: door = TRUE
			@pre1: error = FALSE
		RETURN error_status
		POST
			@post1: door' = FALSE
			@post2: error' ∈ BOOL
			@post3: error_status' = error'
		END
END

According to the interface above, a door is characterised by its current state door that correspond to door being shut or open, and error flag denoting whether the door controller has experienced a failure.

First Refinement

In the first refinement we remove the modelling of doors from the main model and start relying on the module which interface we have just described (with an assumption the interface would be implemented later).

As there are two doors in the system, the door controller module is imported twice. To distinguish between the variables, constants and operations of the two modules, a user provides a module prefix.

uses @d1 DoorController
uses @d2 DoorController

This refinement step removes abstract variables door1 and door2 by replacing them with corresponding variables of imported modules.

variables pressure error 

invariants
 	@inv1 door1 = d1_door
 	@inv2 door2 = d2_door
 	@inv4 d1_error = TRUE ∨ d2_error = TRUE ⇒ error = TRUE

This is how door-related events are refined.

event open1 refines open1 
   where
     @grd1 pressure = 0
     @grd2 d1_door = FALSE
     @grd3 error = FALSE ∧ d1_error = FALSE
   then
     @act1 error ≔ d1_open
 end

In error ≔ d1_open, d1_open is an operation call modelling the opening of the first door. The case of closing a door is similar.

 event close1 refines close1 
   where
     @grd1 d1_door = TRUE
     @grd2 error = FALSE ∧ d1_error = FALSE
   then
     @act1 error ≔ d1_close
 end

Let us see what it means to call d1_open in event open1. Similar to the VDM approach, 'd1_open is merely a reference standing for the conjunction of post-conditions of operation open from module d1. Expanding d1_open using the interface definition, we get the following event:

event open1 refines open1 
   where
     @grd1 pressure = 0
     @grd2 d1_door = FALSE
     @grd3 error = FALSE ∧ d1_error = FALSE
   then
     @act1 error :∈ BOOL
     @act2 d1_door ≔ TRUE 
 end

There is, however, also a additional proof obligation that requires to demonstrate that a call to d1_open was done in a state satisfying the operation preconditions. This is the reason we are required to add d1_error = FALSE into the event guard.