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

9.7.3 Second Refinement: Hysteresis

Hysteresis is a programmed feature whereby the pacemaker paces at a faster rate
than the sensing rate. For example, pacing at 80 pulses a minute with a hysteresis
rate of 55 means that the pacemaker will be inhibited at all rates down to 55 beats
per minute, having been activated at a rate below 55, the pacemaker then switches on
and paces at 80 pulses a minute [ 22 , 39 ]. The application of the hysteresis interval
provides consistent pacing of the atrial or ventricle, or prevents constant pacing
of the atrial or ventricle. The main purpose of hysteresis is to allow the patient to
have his or her own underlying rhythm as much as possible. Two new variables
( Hyt_Pace_Int_flag , HYT_State ) are introduced to define the functional properties
of the hysteresis operating modes. Both variables are defined as a boolean type.
The hysteresis state HYT_State is used to set the hysteresis functional parameter as
TRUE or FALSE, to apply the hysteresis operating modes.

inv 1 : Hyt _ Pace _ Int _ flag ∈ BOOL
inv 2 : HYT _ State ∈ BOOL

A new event Hyt_Pace_Updating is introduced to implement the functional prop-
erties of the hysteresis operating modes. In the hysteresis operating modes, the pace-
maker tries to maintain own heart rhythm as much as possible. Hence, this event
can change the pacing interval and set a pacing length longer than existing, which
changes the pacing length of the cardiac pacemaker. This event is only used for up-
dating the pacing interval ( Pace_Int ). Guards of this event state that the pace chang-
ing flag ( Pace_Int_flag ) is TRUE, the hysteresis pacing flag ( Hyt_Pace_Int_flag )is
TRUE and the hysteresis pace interval ( Hyt_Pace_Int ) should be within the range
of the pace interval ( Pace_Int ) and lower rate interval ( LRI ). Actions of this event
state that a new hysteresis pace interval ( Hyt_Pace_Int ) updates the pace interval
Pace_Int , the hysteresis pacing flag ( Hyt_Pace_Int_flag ) sets to FALSE and the hys-
teresis state ( HYT_State ) becomes TRUE.

EVENT Hyt_Pace_Updating Refines Change _ Pace _ Int
ANY
Hyt _ Pace _ Int
WHERE
grd1 : Pace _ Int _ flag = TRUE

grd2 : Hyt _ Pace _ Int _ flag = TRUE

grd3 : Hyt _ Pace _ Int ∈ Pace _ Int ..LRI

THEN

act1 : Pace _ Int := Hyt _ Pace _ Int

act2 : Hyt _ Pace _ Int _ flag := FA L S E

act3 : HYT _ State := TRUE

END