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

and the hysteresis pace interval ( Hyt_Pace_Int ) should be lied between the pace in-
terval ( Pace_Int ) and lower rate interval ( LRI ). The 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 FALSE and hysteresis state
( HYT_State )setsTRUE.

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

9.8.4 Third Refinement: Rate Modulation

Rate modulation is the final refinement of the two-electrode pacemaker. Rate mod-
ulation refers to the ability of the pacemaker to increase the rate of pacing on its
own. The manner that the pacemaker does this is by having its own special sensor's
measure such as things as vibration or minute ventilation (volume of air moved in
1 minute's time). The pacemaker uses these measurements as a determination of at
least how fast heart rate should be. This rate is termed the “sensor indicated rate.”
Rate modulation is typically used when a patient's heart does not appropriately
increase its own rate with exertion or stress. This intrinsic inability to increase heart
rate is called “chronotropic incompetence.” Use of rate modulation also demands to
set an upper limit on how fast the heart may be paced.
This refinement is similar to the one-electrode pacemaker and pacing rate con-
trol both chambers according to the required physiologic need. Here, we intro-
duce the rate modulation function and found some new operating modes (DDDR,
DVIR, AAIR, DDIR, VDDR and DOOR) of the two-electrode pacemaker system.
For modelling the rate modulation, we introduce some new constants maximum
sensor rate MSR as MSR ∈ N 1 using axioms

( axm 1 , axm 2). The maximum sensor rate ( MSR ) is the maximum pacing rate al-
lowed as a result of sensor control, and it must be between 50 and 175 pulse per
minute (ppm). The constant acc_thr represents the activity threshold. Axiom ( axm 3)
represents a static property for the rate modulation operating modes.

∈ 50 .. 175 and acc _ thr as acc _ thr