Getting Your Hands Dirty
Event-B Examples
Fuel Level
Introduction
This example demonstrates how to specify a software and to implement it by using a modular architecture.
Natural Language Description
Measuring fuel level in a tank
We are considering to estimate the remaining amount of fuel in a tank. This information is critical for a plane, for example, because an error in the estimation might lead to a crash.
So we would like to develop a piece of software that would make the pilot aware of the situation (fuel level below a given capacity). This is in fact the main property of our software, independently from the way the fuel level is estimated.
As the sensors are likely to provide inaccurate / erroneous measures, the architecture of the system includes redundancy (2 ultrasonic level sensors, 3 flowmeters) and the estimation of the fuel left in the tank is performed in two steps:
- initial level in the tank is estimated with the 2 ultrasonic level sensors (minimum value of the two measures)
- each cycle, current level is estimated by substracting the maximum value given by the 3 flowmeters)
When the estimated level is less or equal to a given value, an alarm is raised.
With the B modelling, the objective is:
- estimating the remaining amount of fuel
- making the pilot aware of any fuel shortage
Formal specification
The resulting modelling contains 7 files:
- fuel0 is the top level specification of our software.
- fuel_i is its implementation, that requires services from measure and utils
- measure is a basic machine, in charge of acquiring data from sensors. This component is implemented manually.
- utils is a stateless machine offering 2 services: minimum of 2 NATURAL numbers, maximum of 3 NATURAL numbers.
- utils_i is its implementation
- ctx contains the definition of constants
- ctx_i is its implementation. The values of the constants are provided, in order to be checked against their properties. Constants are then demonstrated to be implementable.
The machine fuel0 contains two operations:
- compute_initial_level: initial estimation of the amount of fuel in the tank
- compute_remaining_fuel: called repeatidly to estimate consumption and remaining fuel
The main property of this component is: (estimated_level <= WARNING_CAPACITY => status = LOW_LEVEL)
The variable status is used to raise an alarm.
1
MACHINE fuel0
2
SEES
3
ctx
4
VARIABLES
5
estimated_level,
6
estimated_consumption,
7
status
8
INVARIANT
9
/* Typing */
10
estimated_level : 0..TANK_CAPACITY &
11
estimated_consumption : 0 ..MAX_CONSUMPTION &
12
status : tSTATUS &
13
/* Security property */
14
(estimated_level <= WARNING_CAPACITY => status = LOW_LEVEL)
15
INITIALISATION
16
estimated_level := 0 ||
17
estimated_consumption := 0 ||
18
status := LOW_LEVEL
19
OPERATIONS
20
compute_initial_level =
21
BEGIN
22
estimated_level, status :(
23
estimated_level: 0..TANK_CAPACITY &
24
status : tSTATUS &
25
(estimated_level <= WARNING_CAPACITY => status = LOW_LEVEL))
26
END
27
;
28
compute_remaining_fuel =
29
BEGIN
30
estimated_level, estimated_consumption, status :(
31
estimated_level: 0..TANK_CAPACITY &
32
estimated_consumption : 0..MAX_CONSUMPTION &
33
status : tSTATUS &
34
(estimated_level <= estimated_level$0) &
35
(estimated_level <= WARNING_CAPACITY => status = LOW_LEVEL))
36
END
37
END
Copied!
This implementation fuel_i implements the two operations defined in fuel0, and imports services from measure and utils.
1
IMPLEMENTATION fuel_i
2
REFINES fuel0
3
SEES ctx
4
IMPORTS
5
measure,
6
utils
7
8
CONCRETE_VARIABLES
9
estimated_level ,
10
estimated_consumption ,
11
status
12
13
INITIALISATION
14
estimated_level := 0 ;
15
estimated_consumption := 0 ;
16
status := LOW_LEVEL
17
18
OPERATIONS
19
compute_initial_level =
20
VAR m1, m2 IN
21
m1, m2 <-- measure_level;
22
estimated_level <-- minimum(m1, m2);
23
IF estimated_level <= WARNING_CAPACITY
24
THEN
25
status := LOW_LEVEL
26
ELSE
27
status := NOMINAL
28
END
29
END
30
;
31
compute_remaining_fuel =
32
VAR m1, m2, m3 IN
33
m1, m2, m3 <-- measure_consumption;
34
estimated_consumption <-- maximum(m1,m2,m3);
35
IF estimated_consumption >= estimated_level
36
THEN
37
estimated_level := 0
38
ELSE
39
estimated_level := estimated_level - estimated_consumption
40
END;
41
IF estimated_level <= WARNING_CAPACITY
42
THEN
43
status := LOW_LEVEL
44
END
45
END
46
END
Copied!
The component measure provides two services: measure_level and measure_consumption. These two operations have to be developped manually.
1
MACHINE measure
2
SEES ctx
3
4
OPERATIONS
5
m1, m2 <-- measure_level =
6
BEGIN
7
m1 :: 0..TANK_CAPACITY ||
8
m2 :: 0..TANK_CAPACITY
9
END;
10
11
m1, m2, m3 <-- measure_consumption =
12
BEGIN
13
m1 :: 0..MAX_CONSUMPTION ||
14
m2 :: 0..MAX_CONSUMPTION ||
15
m3 :: 0..MAX_CONSUMPTION
16
END
17
END
Copied!
The component utils provides two services: minimum and maximum.
1
MACHINE utils
2
3
OPERATIONS
4
rr <-- minimum(aa, bb) =
5
PRE
6
aa: NAT &
7
bb: NAT
8
THEN
9
rr := min({aa, bb})
10
END;
11
12
rr <-- maximum(aa, bb, cc) =
13
PRE
14
aa: NAT &
15
bb: NAT &
16
cc: NAT
17
THEN
18
rr := max({aa, bb, cc})
19
END
20
END
Copied!
The component utils_i implements the two services defined in utils
1
IMPLEMENTATION utils_i
2
3
REFINES utils
4
5
OPERATIONS
6
rr <-- minimum ( aa , bb) =
7
BEGIN
8
IF aa >= bb
9
THEN
10
rr := bb
11
ELSE
12
rr := aa
13
END
14
END
15
;
16
rr <-- maximum ( aa , bb , cc ) =
17
BEGIN
18
IF aa >= bb
19
THEN
20
IF aa >= cc THEN
21
rr := aa
22
ELSE
23
rr := cc
24
END
25
ELSIF bb >= cc THEN
26
rr := bb
27
ELSE
28
rr := cc
29
END
30
END
31
END
Copied!
The component ctx contains the constants of the software.
1
MACHINE ctx
2
3
SETS
4
tSTATUS = {NOMINAL, LOW_LEVEL}
5
6
CONSTANTS
7
TANK_CAPACITY, /* max quantity of fuel in the tank */
8
MAX_CONSUMPTION, /* max quantity of fuel consumed in a cycle */
9
WARNING_CAPACITY /* low fuel level */
10
11
PROPERTIES
12
TANK_CAPACITY : NAT1 &
13
MAX_CONSUMPTION : NAT1 &
14
WARNING_CAPACITY : NAT1 &
15
MAX_CONSUMPTION < TANK_CAPACITY &
16
WARNING_CAPACITY < TANK_CAPACITY
17
END
Copied!
The component ctx_i contains the values of the constants.
1
IMPLEMENTATION ctx_i
2
REFINES ctx
3
4
VALUES
5
TANK_CAPACITY = 1000;
6
MAX_CONSUMPTION = 10;
7
WARNING_CAPACITY = 100
8
END
Copied!
Populating the Project
Once the project is created (software development), add the various machines starting with ctx, utild, measure, then fuel0. Then create the implementations. Each time, create the component empty then copy-paste the contents from this page.
Once all the components are in the project:
- generate the proof obligations (button Po on the toolbar)
- execute the proof in force 0 (button F0 on the toolbar)
- execute the proof in force 1 (button F1 on the toolbar)
You should obtain the following status below from the Top-Bottom graphical view. The color green indicates that the components are fully proven.
Project structure: the lines are decomposition links (fuel_i imports measure and utils components)
Generating code
When everything is proved:
- generate C code for the implementations fuel_i, Utils_i, and Ctx_i,
- Generate C code for the machine Measure: you obtain a skeleton for your C file. Complete measure.c manually, using for example a random number generator to simulate fuel consumption.
- Create main.c such as
void main(void ) { fuel0__compute_initial_level(); while(fuel0__estimated_level>0) { fuel0__compute_remaining_fuel(); printf("Consumption = %d, Level = %d, status = %d\n", fuel0__estimated_consumption, fuel0__estimated_level, fuel0__status); }}- Compile main.c fuel0.cpp utils.c measure.c
- Execute the resulting software
Last modified 2mo ago