Formalisation of Electrocardiogram (ECG) - Using Event-B for Critical Device Software Systems - page 238

Chapter 10
Formalisation of Electrocardiogram (ECG)
Abstract Today, an evidence-based medicine has given number of medical prac-
tice clinical guidelines and protocols. Clinical guidelines systematically assist prac-
titioners with providing appropriate health care for specific clinical circumstances.
However, a significant number of guidelines and protocols are lacking in quality. In-
deed, ambiguity and incompleteness are more likely anomalies in medical practices.
From last few years, many researchers have tried to address the problem of protocol
improvement in clinical guidelines, but results are not sufficient since they believe
on informal processes and notations. Our objective is to find anomalies and to im-
prove the quality of medical protocols using well known formal techniques, such
as Event-B. In this chapter; we use a modelling language to capture the guidelines
for their validation. We have established a classification of the possible properties
to be verified in a guideline. Our approach is illustrated with a guideline which pub-
lished by the National Guideline Clearing House (NGC) and AHA/ACC Society.
Our main contribution is to evaluate the real-life medical protocols using refinement
based formal methods for improving quality of the protocols. Refinement based
formalisation is very easy to handle any complex medical protocols. For this eval-
uation, we have selected a real-life reference protocol (ECG Interpretation), which
covers a wide variety of protocol characteristics related to the several heart diseases.
We formalise the given reference protocol, verify a set of interesting properties of
the protocol and finally determine anomalies. Our main results are: to formalise an
ECG interpretation protocol for diagnosing the ECG signal in an optimal way; to
discover a hierarchical structure for the ECG interpretation efficiently using incre-
mental refinement approach; a set of properties which should be satisfied by the
medical protocol; verification proofs for the protocol and properties according to
the medical experts; and perspectives of the potentials of this approach. Finally, we
have shown the feasibility of our approach for analysing the medical protocols.
10.1 Introduction
A promising and challenging application area for the application of formal meth-
ods is a clinical decision making, as it is vital that the clinical decisions are
sound. In fact, ensuring safety is the primary preoccupation of medical regula-
tory agencies. Medical guidelines are “systematically developed statements to assist