The Cardiac Pacemaker - Using Event-B for Critical Device Software Systems - page 195

measured value ( acler_sensed ) from the accelerometer sensor goes higher or lower
than the activity threshold acc_thr .

EVENT Increase_Interval Refines Change _ Pace _ Int
WHEN
grd1 : Pace _ Int _ flag = TRUE
grd1 : acler _ sensed ≥ threshold
grd1 : HYT _ State = FA L S E

THEN

act1 : Pace _ Int := 60000 /MSR
act1 : acler _ sensed _ flag := TRUE

END

EVENT Decrease_Interval Refines Change _ Pace _ Int
WHEN
grd1 : Pace _ Int _ flag = TRUE
grd1 : acler _ sensed < threshold
grd1 : HYT _ State = FA L S E

THEN

act1 : Pace _ Int := 60000 /LRL
act1 : acler _ sensed _ flag := TRUE

END

A new event ( Acler_sensed ) is defined as to simulate the behaviour of accelerom-
eter sensor. This event senses continue the motion of the body to increase or decrease
the length of the pace interval ( Pace_Int ). In this event, the guards state that the ac-
celerometer sensor flag is TRUE and the hysteresis state is FALSE. A new variable
acl_sen is used to store the current sensing value. Actions of this event state that
a local variable acl_sen updates accelerometer sensor ( acler_sensed ) and the ac-
celerometer sensor flag ( acler_sensed_flag ) becomes FALSE.

EVENT Acler_sensed
ANY
acl _ sen
WHERE
grd1

: acl _ sen ∈ N

grd1 : acler _ sensed _ flag = TRUE

grd1 : HYT _ State = FA L S E

THEN

act1 : acler _ sensed := acl _ sen

act1 : acler _ sensed _ flag := FA L S E

END

In the next section, we explore the formal model of the two-electrode pacemaker
system using incremental refinements.