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

practitioners and patient decisions about appropriate health care for specific circum-
stances” [ 11 , 36 ]. Based on updated empirical evidence; the medical protocols to
provide clinicians with health-care testimonial and facilitate the spreading of high-
standard practices. In fact, this way represents that adherence to protocol may reduce
thecostsofcareupto25%[ 36 ]. In order to reach their potential benefits, protocols
must fulfil strong quality requirements. Medical bodies worldwide have made ef-
forts in this direction, e.g. elaborating appraisal documents that take into account a
variety of aspects, of both protocols and their development process. However, these
initiatives are not sufficient since they rely on informal methods and notations. The
informal methods and notations have not any mathematical foundation.
We are concerned with a different approach, namely the quality improvement of
medical protocols through formal methods. In this chapter, we report on our experi-
ences in the formalisation and verification of a medical protocol for diagnosis of the
Electrocardiogram (ECG) [ 21 , 22 ]. The ECG signals are too complex for diagnosis.
All kinds of diseases related to the heart are predictable using 12-lead ECG signals.
A high number of medical guidelines for the ECG interpretation has been published
in the literature and on the Internet, making them more accessible. Currently, proto-
cols are described using a combination of different formats, e.g. text, flow diagrams
and tables. These approaches are used in form of informal processes and notations
for analysing the medical protocols, which are not sufficient for medical practices.
As a result, the ECG interpretation guidelines and protocols 1 still contain ambigu-

ous, incomplete or even inconsistent elements.
The idea of our work is translating the informal descriptions of the ECG inter-
pretation into a more formal language, with the aim of analysing a set of properties
of the ECG protocol. In addition to the advantages of such a kind of formal verifica-
tion, making these descriptions more formal can serve to expose problematic parts
in the protocols.
Formal methods have well structured representation language with clear and
well-defined semantics, which can be used for taxonomy verification of clinical the
guidelines and medical protocols. The representation language represents guidelines
and protocols explicitly and in a non-ambiguous way. The process of verification
using formal semantic representation of guidelines and protocols to allow the deter-
mination of consistency and correctness.
Formal modelling and verification of medical protocol to have been carried out
as a case study to assess the feasibility of this approach. Throughout our case study,
we have shown formal specification and verification of medical protocols. The ECG
interpretation protocol is very complex, ambiguous, incomplete and inconsistent.
The contribution of this chapter is to give a complete idea of formal develop-
ment of the ECG interpretation protocol, and we have discovered a hierarchical
structure for the ECG interpretation efficiently using incremental refinement ap-
proach [ 21 , 22 ]. Same approach can be also applied for developing a formal model
of the protocol of any other disease. Our approach is based on the Event-B [ 1 , 7 ]

1 Guideline and protocol are different terms. The term protocol is used to represent a specialised
version of a guideline. In this chapter, we use them indistinctively.