Biomedical Engineering Reference
In-Depth Information
In this section, the heart model is presented as abstract as possible to capture all
possible scenarios of the heart, which is completely based on the conduction speed
and conduction time. Whenever these two parameters change or lie out of the range,
then the ECG signal deforms and we cannot obtain the desired ECG signal, which
represents an abnormal heart state. Moreover, we have introduced heart blocking be-
haviour using stepwise refinement. Rather than considering any particular behaviour
of the heart, we have formalised the heart abstractly. For instance, we have not done
any special treatment in our model to capture the retrograde conduction (travel back-
ward). We have considered the perfect heart condition (see HeartOK, we have only
forward conduction network). The retrograde conduction results in many symptoms,
primarily those symptoms result from the delayed, non-physiologic timing of atrial
contraction in relation to ventricular contraction. According to our model, if the
retrograde conduction affects the timing cycle or conduction speed, then the heart
presents an abnormal state. Normal state of the closed-loop model is presented ac-
cording to the timing and speed of the conduction requirements. In case of abnormal
state of the heart, the cardiac pacemaker does pacing and sensing according to the
patient needs. In this closed-loop system, the cardiac pacemaker can take effect
when the heart presents an abnormal state, which helps to maintain the patient heart
rhythm. We have considered heart state (
OK
or
KO
) for each cycle. If the cycle has
any abnormality, heart will be in abnormal state and pacemaker takes over to main-
tain heart rhythm. However, this closed-loop model helps to identify the pacemaker
requirements according to the heart behaviour.
9.11.4 To Discover Essential Safety Properties
The closed-loop model provides higher insurance for safety and security. The num-
ber of POs of the closed-loop model of the cardiac pacemaker are higher than the
simple model of the cardiac pacemaker model (see Tables
9.3
and
9.4
). In the closed-
loop model invariants are stronger than the plain model. The closed model generates
more than 70 % extra POs.
9.12 Real-Time Animation Using Pacemaker Case Study
This section shows an applicability of the real-time animator [
42
] through anima-
tion of formal models of the pacemaker using real-time data sets. Figure
9.11
repre-
sents an implementation of the given architecture for the formal model of a cardiac
pacemaker case study. We have mainly used this case study to experiment on our
proposed architecture, which enables the animation of a proved specification with
real-time data set without generating the source code in any programming language.
According to the proposed architecture (see Fig.
9.11
) for this experiment, we have
not used any data-acquisition device to collect the ECG (electrocardiogram) signal.
Search WWH ::
Custom Search