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

modelling language which is supported by the Rodin platform integrating tools for
proving models and refinements of the models. Here, we present an incremental
proof-based development to model and verify such interdisciplinary requirements
in the Event-B [ 1 , 7 ]. The ECG interpretation models must be validated to ensure
that they meet requirements of the ECG protocols. Hence, validation must be carried
out by both formal modelling and medical domain experts.
We have used a general formal modelling tool like Event-B [ 1 ] for modelling
a complex medical protocol related to diagnoses of the ECG signal. To apply a
refinement based technique to model a medical protocol is our main objective. The
Event-B supports refinement technique. The refinement supported by the Rodin [ 29 ]
platform guarantees the preservation of safety properties. The safety properties are
detection of an actual disease under the certain conditions. The behaviour of the
final system is preserved by an abstract model as well as in the correctly refined
models. This technique is used to model a medical protocol more rigorously based
on formal mathematics, which helps to find the anomalies and provide the consis-
tency and correctness of the medical protocol. The current work intends to explore
those problems related to the modelling of the ECG protocols. The formalisation
of the ECG protocol is based on the original protocol, and all the safety properties
and related assumptions are verified with the medical experts. Moreover, an incre-
mental development of the ECG interpretation protocol model helps to discover the
ambiguous, incomplete or even inconsistent elements in current the ECG interpre-
tation protocol.
10.1.1 Structure of This Chapter
The outline of the remaining chapter is as follows. Section 10.2 contains related
work. Section 10.3 presents selection of medical protocol for formalisation. We give
a brief outline of the ECG in Sect. 10.4 . In Sect. 10.5 , we explore the incremental
proof-based formal development of the ECG interpretation protocol. The verifica-
tion results are discussed in Sect. 10.6 . Finally, Sect. 10.7 summarises the chapter.
10.2 Related Work
Section 10.2 currently presents ongoing research work related to computer-based
medical guidelines and protocols for clinical purposes. From past few years many
languages have been developed for representing medical guidelines and protocols
using various levels of formality based on expert's requirements. Although we have
used the Event-B modelling language for guidelines and protocol representation in
our case study. Various kinds of protocol representation languages like Asbru [ 33 ,
36 ], EON [ 26 ], PROforma [ 12 ] and others [ 27 , 38 ] are used to represent a formal
semantics of guidelines and medical protocols.