Formal Logic Based Heart-Model - Using Event-B for Critical Device Software Systems - page 145

Fig. 8.3 A typical one-cycle ECG tracing

tricular depolarisation, the latter waveform (i.e., the QRS-complex) is of much
greater amplitude, and atrial repolarisation is therefore not seen on the ECG.

• QT-interval: The time between the onset of ventricular depolarisation and the end

of ventricular repolarisation. Clinical studies have demonstrated that the QT in-
terval increases linearly as the RR-interval increases. A prolonged QT-interval
may be associated with delayed ventricular repolarisation, which may cause ven-
tricular tachyarrhythmias leading to sudden cardiac death.

• ST-interval: The time between the end of the S-wave and the beginning of the

T-wave. Significantly elevated or depressed amplitudes away from the baseline
are often associated with cardiac illness.

• T-wave: Ventricular repolarisation, whereby the cardiac muscle is prepared for

the next cycle of the ECG.

8.4 Proposed Idea

Our proposed method exploits a heart model based on logico-mathematics to help
the formal methods community to verify the correctness of a developed model of
medical devices such as cardiac pacemakers. The heart model is based mainly on
the impulse propagation time and conduction speed at a cellular level [ 33 - 35 ]. This
method uses the advanced capabilities of a combined approach of formal verification