Biomedical Engineering Reference
In-Depth Information
teresis and rate modulation) under the real-time constraints. In order to guarantee the
correctness of these functional behaviours, we have established various invariants in
the stepwise refinements. As it can be seen, the abstract model in one electrode re-
quired by far the largest number of proofs: it is due to the large number of invariants
(57), together with the number of events (26) which shows a size of the model. Sim-
ilarly, large numbers of proofs are in the abstract model and the first refinement of
two electrodes, where a large number of invariants (36 (abstract), 30 (refinement 1)),
together with the number of events (41 (abstract), 43 (refinement 1)). It should be
noted that the manual proofs were not difficult. Proofs are quite simple, and have
been achieved with the help of do case operation. Guards of some events are very
complex, so for proving invariants and theorems; we simplify guards using do case .
The stepwise refinement of the pacemaker system helps to achieve a high degree of
automatic proofs.
9.10 Closed-Loop Model of Heart and Cardiac Pacemaker
A detailed description of the heart model based on electrocardiography analy-
sis [ 5 , 21 , 33 ] and cellular automata is given in Chap. 8 . The heart model is based
on logico-mathematical theory. The logico-mathematical based heart model is de-
veloped using refinement approach in Event-B modelling language [ 1 , 56 ]. In this
investigation, we present a methodology for modelling a heart model, to extract a
set of biological nodes (i.e. SA node, AV node, etc.), impulse propagation speed
between nodes, impulse propagation time between nodes and cellular automata for
propagating impulses at the cellular level. A main key feature of this heart model
is a representation of all the possible morphological states of the electrocardiogram
(ECG) [ 2 , 5 ]. The morphological states represent the normal and abnormal states of
the electrocardiogram (ECG). The morphological representation generates any kind
of heart model (patients model or normal heart model using ECG). This model can
observe a failure of the impulse generation and a failure of the impulse propagation.
This model is also verified through electro-physiologist and cardiac experts.
Formal specification of the cardiac pacemaker is expressed in this chapter. But
this cardiac pacemaker is modelled without any biological environment like the
heart system. This section describes a closed-loop formal model of a cardiac pace-
maker and the heart system, where the cardiac pacemaker responses according to the
functional behaviour of the heart [ 49 , 50 , 52 ]. The main objective of this model is
to verify the complex properties of the cardiac pacemaker under the virtual environ-
ment. Figure 9.9 represents a block diagram of the cardiac pacemaker and the heart
system, where the cardiac pacemaker responses when it senses intrinsic activities
from the heart. In this system specification, the heart model simulates the functional
behaviour of the normal and abnormal heart. The heart model activities are always
monitored by the cardiac pacemaker and it responses according to the user needs.
This section presents a closed-loop model of the cardiac pacemaker, where the
heart is used as an environment. For developing this closed-loop model [ 50 ], we
Search WWH ::




Custom Search