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

axm 1 : MSR ∈ 50 .. 175

axm 2 : acc _ thr ∈ N 1

axm 3 : MSR = URL

Two new variables acler_sensed and acler_sensed_flag are defined as to store
the measured value from the accelerometer and boolean stats of the accelerometer
sensor. Boolean state of the accelerometer sensor is used to synchronise with other
functionalities of the system. The accelerometer is used to measure the physical
activities of the body in the pacemaker system. Two invariants ( inv 3, inv 4) provide
the safety margin and state that the heart rate never falls below the lower rate limit
(LRL) and never exceeds the maximum sensor rate (MSR) limit.

inv 1 : acler _ sensed ∈ N

inv 2 : acler _ sensed _ flag ∈ BOOL

inv 3 : HYT _ State = FA L S E ∧ acler _ sensed < acc _ thr ∧

acler _ sensed _ flag = TRUE ⇒ Pace _ Int = 60000 /LRL

inv 4 : HYT _ State = FA L S E ∧ acler _ sensed =≥ acc _ thr ∧

acler _ sensed _ flag = TRUE ⇒ Pace _ Int = 60000 /MSR

In this final refinement, we introduce two new events Increase_Interval and De-
crease_Interval , which are the refinements of the event Change_Pace_Int . These
new events are used to control the pacing rate of the one-electrode pacemaker in
the rate modulating operating modes. The new events Increase_Interval and De-
crease_Interval control the value of the pace interval variable Pace_Int , whenever a
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