Biomedical Engineering Reference
In-Depth Information
Fig. 8.1
Cardiac pacemaker and heart interaction
at the cellular level. This model is developed through incremental refinement, which
introduces several properties in an incremental way and verifies the correctness of
the heart model. A key feature of this heart model is the representation of all possible
morphological states of the (ECG) [
3
,
6
]. These morphological states represent both
the normal and the abnormal states of the ECG. The morphological representation
can generate any kind of heart model (a patient's model or a normal heart model)
using the ECG. This model can observe both the failure of impulse generation and
the failure of impulse propagation. The mathematical heart model, based on logico-
mathematical theory, is verified using the RODIN [
38
] proof tool and the model
checker ProB [
26
]. The model is also verified by electro-physiology and cardiac ex-
perts. The main objective of this heart model is to provide a biological environment
(the heart) for formalising a closed-loop system (a combined model of a cardiac
pacemaker and the heart).
8.1.2 Structure of This Chapter
The outline of the remaining chapter is as follows. Section
8.2
presents related work.
A brief outline of the heart system is introduced in Sect.
8.3
. Section
8.4
explains the
proposed approach. Section
8.5
gives an outline of the formal development of the
heart model. Section
8.6
discusses the results of lessons learnt from this experience,
and Sect.
8.7
summarises the chapter.
8.2 Related Work
Heart modelling is a challenging problem in the area of real-time simulation for
clinical purposes. It is handled by the research community using a variety of differ-
ent methods. The ECG is an important diagnostic method for measuring the heart's
electrical activities, and was invented by Willem Einthoven in 1903 [
36
]. In this
study, the ECG is used in modelling the heart [
36
]. At the present time, technolog-
Search WWH ::
Custom Search