Biomedical Engineering Reference
In-Depth Information
heart system, we have used the Event-B modelling language [ 1 , 38 ] to develop the
proof-based formal model. Our approach involves formalising and reasoning about
impulse propagation in the whole heart system through the conduction network (see
Fig. 8.4 (a)). More precisely, we would like to stress the original contribution of our
work. We have proposed a method for modelling a human heart based on logico-
mathematical theory. The main objectives of this proposed idea are as follows:
To obtain a certification procedure for providing a higher safety integrity level.
To verify the system in a patient model (in a formal representation).
To analyse the biological environment (the heart) in a mathematical way.
To analyse the interaction between the heart model and a cardiac pacemaker or
ICD.
In summary, we have formalised the known characteristics and physiological be-
haviour of the heart. The formalisation highlights various aspects of the problem,
making different assumptions about impulse propagation and establishing different
properties related to the CA. We have outlined how an incremental refinement ap-
proach to the heart system enables a high degree of automatic proof using the Rodin
tool. Our various developments reflect not only many facets of the problem, but also
the learning process involved in understanding the problem and its ultimate possible
solutions.
The consistency of our specification has been checked through reasoning, and
validation experiments were performed using the ProB model checker with respect
to safety conditions. As part of our reasoning, we have proved that the initialisa-
tion of the system is valid, and we have calculated the preconditions for operations.
These have been executed to guarantee that our intention to have total operations has
been fulfilled. At each stage of the refinement, we have introduced a new behaviour
for the system and proved its consistency and refinement checking .Wehaveintro-
duced more general invariants at the refinement level, showing that the initialisation
of the whole system is valid. Finally, we have validated the heart system using the
ProB model checker as a validation tool and have verified the correctness of the
exact behaviour of our heart system with the help of physiology and cardiology
experts.
References
1. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.
2. Adam, D. R. (1991). Propagation of depolarization and repolarization processes in the
myocardium—an anisotropic model. IEEE Transactions on Biomedical Engineering , 38 (2),
133-141.
3. Artigou, J. Y., & Monsuez, J. J. (2007). Cardiologie et maladies vasculaires . Paris: Elsevier
Masson.
4. Back, R. J. R. (1981). On correct refinement of programs. Journal of Computer and System
Sciences , 23 (1), 49-68.
5. Barold, S. S., Stroobandt, R. X., & Sinnaeve, A. F. (2004). Cardiac pacemakers step by step .
London: Futura. ISBN 1-4051-1647-1.
Search WWH ::




Custom Search