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

9.7.4 Third Refinement: Rate Modulation

Rate modulation term is used to describe the capacity of a pacing system to respond
to physiologic needs by increasing and decreasing pacing rate. The rate modulation
mode of the pacemaker can progressively pace faster than the lower rate, but no
more than the upper sensor rate limit, when it determines that heart rate needs to
increase. This typically occurs with exercise in patients who cannot increase their
own heart rate. The amount of rate increases is determined by the pacemaker based
on maximum exertion is performed by the patient. This increased pacing rate is
sometimes referred to as the “sensor indicated rate”. When exertion has stopped the
pacemaker will progressively decrease the paced rate down to the lower rate.
In this last refinement, we introduce the rate modulation function and found some
new operating modes (AOOR, VOOR, AAIR, VVIR, AATR and VVTR) of the
pacemaker system. For modelling the rate modulation, we introduce some new con-
stants maximum sensor rate MSR as MSR ∈ N 1

using axioms ( axm 1 , axm 2). The maximum sensor rate ( MSR ) is the maximum pac-
ing rate allowed 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. Ax-
iom ( axm 3) represents a static property for the rate modulation operating modes.

∈ 50 .. 175 and acc_thr as acc _ thr

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
a measured value from the accelerometer and boolean type of the accelerometer
sensor. Boolean type 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 new 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
Decrease_Interval , which are the refinement of 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