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

Fig. 9.8 The required DDDR pacing cycle

•

Scenario D—represents the case where both pacing activities are inhibited due to
a sensing of intrinsic activities in both chambers.

Figure 9.8 gives a flow chart for the basic required operations of the DDD mode.
This gives an informal description of the requirements for the pacemaker operat-
ing in the DDDR mode. If a ventricle pulse has just been delivered, the pacemaker
watches the atrial channel for a spontaneous P wave (intrinsic activity in the atrium).
If the VAI times out, the pacer delivers a pacing pulse to the atrium; otherwise,
the atrial output is inhibited. The pacemaker now watches the ventricle for a spon-
taneous QRS complex wave (indicating intrinsic activity in the ventricle). If it is
detected, the ventricular pace is inhibited, otherwise the pacemaker delivers a pac-
ing pulse. If the accelerometer detects a change in the patient's activity level, it
changes the VAI timeout to compensate—thus speeding up or slowing down the
heart beat [ 57 ].

9.7 Formal Development of the One-Electrode Cardiac
Pacemaker

9.7.1 Context and Initial Model

Abstraction of AOO and VOO Modes

We begin by defining the Event-B context. The context uses sets and constants to
define axioms and theorems. Axioms and theorems represent the logical theory of
a system. The logical theory is the static properties and properties of the system.
In the context, we define constants LRL and URL that relate to the lower rate limit
(minimum number of pace pulses delivered per minute by pacemaker) and upper
rate limit (how fast the pacemaker will allow the heart to be paced). These constants
are extracted from the pacemaker specification document [ 7 ]. The lower rate limit
(LRL) must be between 30 and 175 pulse per minute (ppm) and upper rate limit
(URL) must be between 50 and 175 pulse per minute (ppm).
The two new constants URI and LRI represent the corresponding upper rate in-
terval and lower rate interval, respectively. The pacemaker (or pacing) rate is pro-
grammed in milliseconds. To convert a heart rate from beats per minute (bpm) to
milliseconds, 60,000 is divided by the heart rate. For example, a heart rate of 70 bpm