Biomedical Engineering Reference
In-Depth Information
•
In our formal verification process of the ECG interpretation, we have obtained a
list of anomalies.
•
Verification proofs for the ECG interpretation protocol, and properties have
proved using the Rodin proof tool. Generated proof obligations and proofs show
that formal verification of the ECG interpretation protocols is feasible.
•
Original protocol of the ECG is also based on some hierarchy, but in that hier-
archy, some diagnosis is repeating in multiple branches (see in [
16
]). We have
also discovered an optimised hierarchical structure for the ECG interpretation ef-
ficiently using incremental refinement approach, which can help to diagnose more
efficiently then old techniques, and this obtained hierarchical structure is verified
through medical experts.
The ECG interpretation protocol [
21
,
22
] is very complex, and it interprets vari-
ous kinds of heart diseases. Improving quality of medical protocol using the formal
verification tools like highly mathematical based modelling languages; Event-B, is
the main contribution of our work. We have also discovered a hierarchical struc-
ture for the ECG interpretation efficiently that helps to discover a set of conditions
that can be very helpful to diagnose particular disease an early stage of the diagnosis
without using multiple diagnosis. Our hierarchical tree structure provides more con-
crete solutions for the ECG interpretation protocol and helps to improve the original
ECG interpretation protocol. Our objective behind this work is that if any medical
protocol is developed under particular circumstances to handle a set of specific prop-
erties according to the medical experts, formal verification can also meet whether
the protocol actually complies with them. This has been the first attempt ever in
verifying medical protocols with mathematical rigour with the generalised formal
modelling tool Event-B. The main objective of this approach to test correctness and
consistency of the medical protocol using refinement based incremental develop-
ment. This approach is not only for diagnosis purpose, but it may be applicable to
covering a large group of other categories (i.e. treatment, management, prevention,
counselling, evaluation, etc.)
3
related to the medical protocols.
References
1. Abrial, J.-R. (2010).
Modeling in Event-B: System and software engineering
(1st ed.). New
York: Cambridge University Press.
2. Advani, A., Goldstein, M., Shahar, Y., & Musen, M. A. (2003). Developing quality indicators
and auditing protocols from formal guideline models: Knowledge representation and transfor-
mations. In
AMIA annual symposium proceedings
(pp. 11-15).
3. Balser, M., Reif, W., Schellhorn, G., & Stenzel, K. (1999). KIV 3.0 for provably correct sys-
tems. In D. Hutter, W. Stephan, P. Traverso, & M. Ullmann (Eds.),
Lecture notes in computer
science: Vol. 1641
.
Applied formal methods—FM-trends 98
(pp. 330-337). Berlin: Springer.
4. 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