Information Technology Reference
In-Depth Information
Z specification into Perfect Developer. Finally, in Section 6 we discuss the re-
sults presented in this paper, followed by conclusions and future directions in
Section 7.
2ThePemar
A pacemaker is a small electronic device that is capable of dealing with some of
the human heart's deficiencies. It is implanted into the human chest by surgery
and connected to the heart via one or two thin leads [7]. Such leads are capable
of pacing and sensing pulses from the heart and may be connected to the atrial
chamber, to the ventricular chamber or to both chambers, depending on the
heart's needs. The pacemaker system [13] works basically in two modes:
perma-
nent mode
running the main operation,
bradycardia therapy
, sensing and pacing
pulses, and in
temporary mode
testing the pacemaker functionalities and emitting
reports. During the
bradycardia therapy
, the pacemaker will be able to deliver
pulses according to a set of parameters programmed by the cardiologist during
the implant [22]. These parameters are related to the frequency of paced pulses,
their voltages, and the type of response to sensed beats from the heart.
Among such parameters, the
bradycardia operation mode
, mentioned in our
formalisation as
bo mode
, is the parameter that describes how the therapy will
behave regarding: (1) the chambers (atrium or ventricle) in which the pacemaker
will sense pulses (chambers sensed); (2) the chambers to which the pacemaker
will deliver pulses (chambers paced); (3) how the pacemaker will react to pres-
ence or absence of intrinsic pulses from the heart (response to sensing); and (4)
whether or not, the pacemaker makes use of an accelerometer to increase the
frequency of delivered pulses according to the intensity of body motion.
Fig. 1.
VOO mode
As an example, the VOO mode, illustrated in Figure 1, is the
bradycardia
operation mode
in which pulses are paced to the ventricle chamber (represented
by the character 'V'), pulses are not sensed by the pacemaker (represented by
the first character 'O'), and there is no response to sensing events (represented
by the last character 'O'). In such mode, the pacemaker will deliver pulses to
Search WWH ::
Custom Search