Biomedical Engineering Reference
In-Depth Information
Our models are superior to the sequential model of H.D. Macedo et al. [
38
] and
Gomes et al. [
19
]. We have added the
threshold
,
hysteresis
and
rate adaptive
brady-
cardia operating modes in our formal specification. We have developed the para-
metric and functional incremental development of bradycardia operating modes.
Incremental development is based on refinement approach and at every level of the
development, we have proved all the required safety properties (
refinement
and
con-
sistency checking
). Other specifications [
19
,
38
] of the pacemaker developed as a
one-shot model, means those are not based on the refinement and the correctness
of a model is not checked by any model checker, for safely desired behaviour of
the pacemaker system. We use the formal verification for consistency checking,
and a model checker tool ProB is used to check the desired behaviour of the car-
diac pacemaker. ProB animator helps to validate system behaviour according to the
medical experts at each refinement level of the formal development. In this chapter,
we present a complete system development of a cardiac pacemaker [
48
] from re-
quirement analysis to source code generation in Event-B modelling language with
several other techniques [
13
,
41
,
46
,
47
].
9.1.3 Structure of This Chapter
The outline of the remaining chapter is as follows. We give a brief outline of the
pacemaker and the heart system in Sect.
9.2
. Section
9.3
presents patterns for mod-
elling the cardiac pacemaker. Refinement structure of the cardiac pacemaker is given
in Sect.
9.4
. Section
9.5
presents development of the cardiac pacemaker using re-
finement charts, and the control requirements of a cardiac pacemaker is given in
Sect.
9.6
. Sections
9.7
and
9.8
explore stepwise formal development of the one- and
two-electrode cardiac pacemakers. Section
9.9
presents model validation using the
ProB model checker. Section
9.10
presents a closed-loop formal model for the heart
and cardiac pacemaker. Section
9.11
explores the requirements of the closed-loop
modelling. Section
9.12
presents use of the real-time animator for validating the
pacemaker models according to the domain experts. Section
9.13
presents code gen-
eration process from formal specifications of the cardiac pacemaker using EB2ALL
tool, and finally, Sects.
9.14
and
9.15
summarise this chapter with some discussions.
9.2 Basic Overview of Pacemaker System
The conventional pacemakers serve two major functions, namely
pacing
and
sensing
. The pacemaker actuator is pacing by the delivery of a short, intense elec-
trical pulse into the heart. However, the pacemaker sensor uses the same electrode
to detect the intrinsic activity of the heart. So, the pacemaker function of pacing
and sensing activities are dependent on the behaviour of the heart. The sensing and
pacing functions regulate the heart rhythm.
Search WWH ::
Custom Search