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

10.6 Lesson Learnt
The task of modelling of the ECG interpretation protocol in the Event-B has required
a significant effort. It is a typical knowledge engineering task, where the knowledge
is the original document, is transformed into the Event-B formal notation, which
provides a significant hierarchical structure for analysing the ECG interpretation
protocol and to diagnose different kinds of heart diseases. As the result, the Event-B
ECG interpretation protocol specification is much more lengthy than the original
text: the original ECG interpretation protocol. The complete formal specification of
the ECG interpretation protocol in the Event-B is more than 200 pages.
We consider that logic-based modelling approach is very difficult to model a
complex medical protocol. This approach has required a good understanding of
logic as well as knowledge of the medical protocol. We have spent lots of time with
medical experts to understand the structure of the medical protocols for formalising
purpose. For modelling the ECG protocol, we have consulted with cardiologist and
medical experts. The formal model of ECG protocol is based on original protocol
and checked by medical experts [ 21 , 22 ].
We cannot strictly say that the formal representation of the ECG interpretation
protocol in the Event-B modelling language has contributed to the improvement
of the original protocol. Most important contribution is refinements-based formal
development of the ECG interpretation protocol and to generate a new optimal way
of the ECG interpretation protocol for diagnosing the ECG signal. The developed
formal model is proved and verified according to the given protocol properties as
discussed in the formal development. Furthermore, the Event-B formalisation has
served to disambiguate unclarities in the original document that resulted from the
modelling stage: a number of ambiguity and repetition diagnosis problems with
original document are uncovered and resolved by refining the formal specification
of the ECG interpretation protocol in the Event-B. The formal model can help to
restructure the original document of guidelines and protocols.
The verification attempts have served to clarify any remaining problems in the
original ECG interpretation protocol document. More importantly, we have shown
that it is possible in practice to systematically analyse whether a protocol formalised
in the Event-B complies with certain medically relevant properties. Various proper-
ties of the ECG interpretation protocol have been the object of formal verification
using the Event-B system, with different type of results. Mostly, the given properties
of the ECG interpretation protocol have been confirmed by the formal representa-
tion of the ECG interpretation protocol. However, in other cases, verification is not
simple and lots of ambiguous informations, i.e. it is not possible to complete the
proof or further development of the model due to ambiguity. We have introduced
some additional assumptions with the help of cardiologist experts for describing the
conditions needed to make the property true and added more conditions to remove
the ambiguity. These assumptions are missing piece of information in the medical
protocol, which helps to improve the medical protocol. We have applied a pragmatic
approach to collect lots of information through literature survey and medical experts
advises for finding the exact facts to introduce new assumptions and conditions for
discharging all the generated proof obligations.