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

9.11 Closed-Loop Modelling Requirements
This section presents a set of requirements for modelling the closed-loop system to
guarantee the safety properties [ 29 ]. These requirements are useful for verifying the
closed-loop system.
9.11.1 Patient Safety in Closed-Loop
The closed-loop system must hold a set of requirements related to the physiological
needs. Few properties are constant and others are conditional. The heart indicates the
patient condition, which presents conditional properties. In the closed-loop system
the heart states are connected to the heart model parameters, which are not affected
by pacemaker therapy. The integration of the heart model and pacemaker model
allow us to evaluate whether the pacemaker provides an appropriate therapy for any
arrhythmias.
9.11.2 Behavioural Requirements
The closed-loop system exposes several conditions for normal and abnormal heart,
which are represented through node automata (Fig. 9.10 (b)) using ranges of impulse
propagation speed and impulse propagation time. Condition is a boolean value for
whether the heart state is true. The cardiac pacemaker presents pacing and sens-
ing activities under specified conditions. Some behaviour requirements are given as
follows: (1) Atria and ventricular pace should not occur during atrial and ventricle
refractory period, respectively. This requirement is an important safety properties,
which is verified in the closed-loop model. Any pacing during the refractory period
creates derangements in timing for the atria and ventricle. (2) Intrinsic activities of
the atrial and ventricles should be sensed by different leads. The intrinsic activities
are essential input for the pacemaker. The pacemaker should ensure that the intrinsic
activities are sensed accurately. (3) Natural pacing in the atria and ventricle, and ar-
tificial pacing and sensing activities of the pacemaker must be coordinated to ensure
efficient pumping for maintaining the heart rhythm.
9.11.3 Clinical Requirements with Closed-Loop
Clinical requirements are depended on the patient needs such as normal sinus
rhythm, bradycardia, heart block and tachycardia. These requirements are common
critical conditions, which can vary for each patient because of different physiologi-
cal needs.