Biomedical Engineering Reference
In-Depth Information
ical advances have enabled the production of a high-quality cellular model of an
entire heart.
K.R. Jun et al. [
37
] have produced a CA model of the activation process in ven-
tricular muscle tissue. They presented a two-dimensional (2D) CA model that ac-
counts for the local orientation of the myocardial fibres and their distributed ve-
locity and refractory period. A three-dimensional (3D) finite-volume-based com-
puter mesh model of human atrial activation and current flow has been presented
by Harrild et al. [
15
]. This cellular-level-based model included both the left and
right atria and the major muscle bundles of the atria. The results of using this model
demonstrate a normal sinus rhythm and can extract the patterns of the septum's
activation. Because of memory and time complexity in the computation of a 3D
model, an empirical approach is used in modelling the whole heart. The empirical
approach implies a simpler representation of the complex process at a cellular level.
In this new approach, researchers have adopted some approximations in modelling
the whole heart without compromising the actual behaviour of the heart. Berenfeld
et al. [
8
] have developed a model that can give insight into the local and global
complex dynamics of the heart in the transition from normal to abnormal myocar-
dial activity, which helps to estimate myocardial properties. Adam [
2
] has analysed
wave activities during depolarisation in his cardiac model, which is represented by
a simplification of the heart tissue.
Recently, a real-time Virtual Heart Model (VHM) has been developed by Jiang
et al. [
22
] to model the electro-physiological operation of proper functioning and
malfunctioning. They used a time-automaton model to define the timing properties
of the heart. Simulink Design Verifier
1
was used as the main tool for designing the
VHM. A heart model based on Uppaal Model checker [
7
] is developed by Jee et
al. [
19
] for developing the cardiac pacemaker model. This is a very simple heart
model, which provides an environment to simulate and verify the pacemaker soft-
ware in modelling phase.
Our approach is based purely on formal techniques for modelling the heart using
electrocardiography analysis. To model the heart for a cardiac pacemaker or ICD, we
propose a method based on logico-mathematical theory, which can be implemented
using any formal-methods-based tools (Z, TLA
+
, VDM, etc.). In this chapter, the
model is developed using a maximal refinement approach at the cellular level. The
incremental refinement approach helps both to introduce several properties in an
incremental way and to verify the correctness of the heart model [
33
-
35
]. The key
feature of this heart model is the representation of all possible morphological states
of the ECG, which is used to represent both normal and abnormal states through ob-
servation of the failure of impulse generation and the failure of impulse propagation
in the heart [
3
,
6
,
24
,
30
].
Search WWH ::
Custom Search