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

teresis mode is represented by transitions Hysteresis Mode TRUE and Hysteresis
Mode FALSE . The main objective of hysteresis is to allow the patient to have his or
her own underlying rhythm as much as possible. The hysteresis operating mode is
available in AAI, AAT, VVI, VVT and DDD modes.
According to the last refinement step (Figs. 9.5 (D), 9.6 (D)), it introduces the
rate adapting pacing technique in the bradycardia operating modes of the pace-
maker. The rate modulation mode is represented by transitions Accel. ON and Accel.
OFF . The rate modulation operating modes are available in all pacemaker operating
modes which are given under multiple refinements. The pacemaker uses the ac-
celerometer sensors to sense the physiologic need of the heart and increase and de-
crease the pacing 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 pacing rate down to the lower rate.
The next section presents only selected parts of our formalisation and omit proof
details. For instance, we have omitted the specification of refinement of every event
from all operating modes. Only newly introduced event specifications are given in
all refinements. To find more detailed information see the published papers and
research reports [ 40 , 43 , 48 ].
9.6 Cardiac Pacemaker Control Requirements
There are several operating modes in the cardiac pacemaker, and DDD operating
mode is one of the complex operating mode that contains the features of other op-
erating modes. The data flow and pacing algorithm of DDD cover the functionality
of the other operating modes. Therefore, this section presents only the control re-
quirement of the DDD operating mode. As explained above, the DDD operating
mode of the pacemaker is used, where the sensors sense intrinsic activities from
both chambers and the actuators discharge electrical pulse in both chambers.
Figure 9.7 depicts the scenarios for sensing and pacing activities [ 4 ]. In Fig. 9.7 ,
time goes left to right, and a flat line indicates no heart activity. A spike above the
lines indicates intrinsic activity and a spike below the line indicates activity as a
result of the action of the pacemaker. A rounded spike indicates activity in the atrial
and a sharp spike indicates activity in the ventricle. The Ventriculoatrial Interval
(VAI) is the maximum time the pacemaker should wait after sensing ventricle activ-
ity (either intrinsic or paced) for some indication of intrinsic activity in the atrium.
If none is present, the pacemaker should pace in the atrial chamber. The Atrioven-
tricular Interval (AVI) is the maximum time the pacemaker should wait after sens-
ing atrial activity (either intrinsic or paced) for some indication of intrinsic activity
in the ventricles. If none is present then the pacemaker should pace in the ventricle
chamber. After every pace in the ventricle, there is some sensed activity in the atrial,
but this is not true intrinsic heart activity and should be ignored. The Postventricu-
lar atrial refractory period (PVARP) indicates the length of time that such activity