1 Introduction

Over the past few decades, much research has been done in the area of medical domain to address the growing challenges in the field of biomedical informatics, life sciences, pharmacology, neuroscience and clinical research. There are several databases to manage different kinds of biological information. However, these databases face new challenges in terms of increasing amount of data due to the growing number of users. These new challenges are: data are voluminous, unstructured and collected from a variety of incompatible sources; difficult to use and understand the available data, information and knowledge; needs of better techniques and tools to manage the databases; needs of semantical description of biological domain and medical systems; and needs of some sound techniques to meet regulators and certification standards [37].

Mostly, the system development process does not consider the domain knowledge explicitly. However, such knowledge is provided implicitly during the system development by making some assumptions on an environment and some of the past experiences. It is very common that such implicit domain knowledge often shows some contradictory results, which may lead to a system failure state. Integrating domain knowledge into a system model explicitly may improve the quality of the development process. Note that one of the main reasons for not integrating domain knowledge into the system development is the lack of modelling languages. Most of the languages are unable to express environment requirements related to a system [5].

Medical guidelines are “systematically developed statements to assist practitioners and patients to determine appropriate health care for specific circumstances” [27, 45]. Medical protocols provide healthcare testimonials and facilitate high standard practices. For developing high-quality protocols, we need regular amendments. Medical bodies worldwide have made efforts for improving existing protocols and their development process. However, these initiatives are not sufficient since they rely on informal methods and they do not apply domain knowledge during the development of protocols [28].

We are concerned with a different approach, namely the quality improvement of medical protocols using formal methods. In order to find anomalies and to improve the quality of medical protocols, this paper presents a stepwise formal development of a medical protocol. The whole development is composed of two different models: domain model and system model. The domain model contains domain concepts based on ontologies [15] and the system model contains the required functional behaviour of a given medical protocol. Note that an annotation mechanism is used to integrate these two models for developing and verifying the medical protocol. Combining these two models allows us to verify some new properties related to the domain knowledge within the enriched design medical protocol. In this work, we use the Event-B language for modelling the domain model and the system protocol model. Our main contributions are:

  • to use domain-specific knowledge in a system model explicitly;

  • to link a domain model and a system model using an annotation mechanism;

  • to use a proof-based formal approach to evaluate a medical protocol;

  • to find ambiguity, incompleteness and inconsistency in a medical protocol.

The main goal of this work is to translate an informal description of a medical protocol into a formal language, with the aim of analysing a set of properties. Such kinds of formal verification allow us to expose problematic parts in the protocol by analysing the formal description of the protocol. The current work intends to explore those problems related to the modelling of medical protocols. Moreover, an incremental development of the medical protocol model helps to discover the ambiguous, incomplete or even inconsistent elements in the medical protocol under the explicit domain knowledge. The electrocardiogram (ECG) protocol covers a wide variety of characteristics related to different heart conditions. Formal modelling and verification of the ECG clinical protocols have been carried out as a case study to assess the feasibility of this approach.

The outline of the remainder of the paper is as follows: Section 2 describes the ontology concepts and the modelling framework is presented in Sect. 3. Section 4 presents a modelling methodology. In Sect. 5, we explore the incremental proof-based formal development of the ECG protocol, including domain model. Related work is presented in Sects. 6 and 7 concludes the paper.

2 Ontology

Ontology—“science of being”—is originated in philosophy, which is defined as “hierarchical structuring of knowledge about concepts by sub-classing them according to their properties and qualities” [19]. It can also be defined as “a declarative model of a domain that defines and represents the concepts existing in that domain, their attributes and the relationships between them” [19, 20]. Ontology provides a description of concepts along with desired relations. The concept plays a very important role in data sharing and knowledge representation. Nowadays ontologies are adopted by almost every area of science and engineering for a common understanding between different user groups. In general, ontologies are classified as (i) Upper ontologies, (ii) General Ontologies (iii) Domain Ontologies and (iv) Application ontologies. All these classes are provided according to a detailed conceptual knowledge. Upper ontologies or top-level ontologies provide a very generic knowledge applicable to various domains. They mainly contain basic notions of objects, relations, events and processes. General ontologies are not dedicated to any specific domain or field. These ontologies represent general knowledge of a large field at an intermediate level without addressing low-level details. Domain ontologies are only applicable to a domain with a specific viewpoint that represent knowledge about a particular field or area of the world. Application ontologies are the specialisation of domain ontologies that are designed for specific tasks.

The prime use of defining or developing ontology is to share knowledge or information with groups, who work in the same domain. The main reasons for developing ontologies are [33, 46]: (1) to share knowledge in the same domain; (2) to reuse existing developed ontologies; (3) to provide an explicit list of domain assumptions; (4) to separate domain knowledge from operational knowledge; and (5) to perform domain-specific methodical analyses.

2.1 Ontology in Medical Domain

Medicine is a branch of science dealing with the maintenance of health, and the prevention and treatment of diseases. It offers a solid foundation in the core biomedical subjects, such as anatomy, physiology, pharmacology, neuroscience, etc. A medical domain is characterised by abundant knowledge of medical science collected from various sources. It is constantly growing due to new discoveries provided by medical experts and researchers. Most of the existing data are distributed into heterogeneous databases and architecture. They have different implementations and are not compatible with each other. Integrating heterogeneous databases can be a solution to provide a centralised and reliable database, but it is a very costly operation and requires huge resources [37]. Note that most of the individual databases are developed by different research groups for their own purpose that do not follow standard approaches. Data collected from different sources are mainly inconsistent and hard to understand. Therefore, an approach is required to systematically represent medical knowledge that could be used for analysis, clinical practices and supporting the different healthcare activities [12]. Ontology has played a significant role in representing medical knowledge systematically in an independent format to share and reuse across the other biomedical domains. The medical ontology framework provides a common medical concepts, relationships, properties, and axioms related to biomedical, disease, diagnosis, treatment, anatomy, pharmacology, clinical procedure and so on. There are several medical ontologies, such as GALAN [14], OpenCyc [13], WordNet [30], UMLS [12], SNOMED-CT [26], FMA [36] and Gene Ontology [6] developed by researchers, industries and medical centres. In our work, we adopt these ontologies to define the domain concepts related to the selected medical protocol.

3 The Modelling Framework: Event-B

This section describes the essential components of modelling framework. In particular, we will use the Event-B modelling language [3] for modelling a complex system in a progressive way. There are two main components in Event-B: context and machine. A context is a formal static structure that is composed of several other components, such as carrier sets, constants, axioms and theorems. A machine is a formal dynamic structure that is composed of variables, invariants, theorems, variants and events. A machine and a context can be connected with sees relationships.

An Event-B model is characterised by a list of state variables possibly modified by a list of events. Events play an important role in modelling the functional behaviour of a system. An event is a state transition that contains two main components: guard and action. A guard is a predicate based on the state variables that define a necessary condition for enabling the event. An action is also a predicate that allows modifying the state variables when the given guard becomes true. A set of invariants defines required safety properties that must be satisfied by all the defined state variables. There are several proof obligations, such as invariant preservation, nondeterministic action feasibility, guard strengthening in refinements, simulation, variant, well-definedness, that must be checked during the modelling and verification process.

The Event-B modelling language allows us modelling a complex system gradually using refinement. Refinement enables us to introduce more detailed behaviour and the required safety properties by transforming an abstract model to a concrete version. At each refinement step, the events can be refined by (1) keeping the event as it is; (2) splitting an event into several events; or (3) refining by introducing another event to maintain state variables. Note that the refinement always preserves a relation between an abstract model and its corresponding concrete model. The newly generated proof obligations related to refinement ensures that the given abstract model is correctly refined by its concrete version. Note that the refined version of the model always reduces the degree of nondeterminism by strengthening the guards and/or predicates. The modelling framework has a very powerful tool support (Rodin [35]) for project management, model development, conducting proofs, model checking and animation and automatic code generation. There are numerous publications and books available for an introduction to Event-B and its related refinement strategies [3].

4 Modelling Methodology

In this section, we present a modelling methodology, which is described in [5]. Figure 1 depicts a stepwise modelling methodology, which contains the different modelling steps: domain modelling, system modelling, model annotation and model verification. These modelling steps are described as follows:

  1. 1.

    Domain Modelling. Domain knowledge plays an important role in making assumptions for a given system. Mostly, the required information related to a domain may be considered hypothetically based on previous experiences and the available domain knowledge. Note that an ontology modelling language can be used to characterise and formally specify a domain knowledge in the form of domain ontology through the definition of concepts, entities, relationships, constraints and rules. In this work for modelling a domain model, we choose the Event-B modelling language [3] to formalise the required domain concepts derived from the domain ontology, which can be described in Event-B context using sets, constants, axioms and theorems.

  2. 2.

    System Modelling. For developing a safe system considering all the required functionalities is a challenging problem. In order to design a safe system, we can use any formal modelling language to describe a desired behaviour under the given specification. The selected modelling language and associated verification approach allows us to check the required behaviour. In this work for modelling a system model, we also choose the Event-B modelling language [3], which allows us the progressive development of the system behaviour satisfying the required safety properties using machines and contexts.

    In many cases, we should develop a domain model before developing a system model so that we can use the domain model during the system model development. If we do not have any domain model before developing a system model then we need to introduce the domain-specific information implicitly to design a correct system model and to check the system model independently. Note that during the annotation for combining the system model and domain model, we need to remove the implicit domain-specific concepts.

  3. 3.

    Model Annotation. Model annotation is a mechanism that allows us to establish a relationship between the domain model and the system model by describing the design model entities and ontology concepts. The annotation mechanism can be defined independently and can be used to annotate both the system and domain models. These models can be developed using the same formal notations or different formal notations. An independent annotation mechanism, like a plugin, can be used to bind the domain model and the system model together. Developing a new annotation mechanism is beyond the scope of this paper. Note that in our current work, we have not used any specific annotation mechanism to apply our approach. In fact, we have used the same modelling language (Event-B [3]) to design the two models. Thus we have got a free implicit annotation mechanism (i.e. see context relationship) for our purpose used to integrate the domain and system models together. In order to integrate the domain model and system model in Event-B, we use the domain model as a set of contexts during the development of the system model for describing the desired properties and functional behaviour.

  4. 4.

    Model Verification. This is the last step of the modelling methodology, which can be performed when a system model is annotated with a domain model. The annotated design model is enriched by the domain properties expressed in the ontology. For verifying the annotated model, we should apply the verification in two steps. The first verification must be conducted on the designed system model before annotation (may be no longer correct after annotation) to check the consistency and then the second verification must be conducted on the designed system model after annotation to check the overall consistency considering the domain knowledge. Note that in the second step, the verification also allows us for checking the new emerging properties due to the integration of domain model and system model using annotation mechanism.

Fig. 1
figure 1

Four steps modelling methodology

Full size image

5 Case Study: ECG Protocol

An electrocardiogram (EKG or ECG) [10, 24, 44] reflects an electrical activity of the heart that shows depolarization and repolarization of the atria and ventricles. The typical one-cycle ECG is shown in Fig. 2, which is a sequence of different segments and intervals to represent the time evolution of electrical activity in the heart. These sequences are denoted as P-QRS-T-U to show different functionalities of the heart. These sequences are described as follows:

Fig. 2
figure 2

ECG Deflections

Full size image

  • P-wave: It is a small deflection caused by the atrial depolarization before contraction to show an electrical wave propagation from the SA (sinus) node through the atria;

  • PR interval—It is an interval between the beginning of the P-wave to the beginning of the Q-wave;

  • PR segment—It is a flat segment between the end of the P-wave and the start of the QRS interval;

  • QRS interval: It is an interval between the P-wave and T-wave with greater amplitude to show the depolarization of the ventricles;

  • ST interval: It is an interval between the end of S-wave and the beginning of T-wave;

  • ST-segment—It is a flat segment starts at the end of the S-wave and finishes at the start of the T-wave;

  • T-wave: It is a small deflection caused by the ventricular repolarization, whereby the cardiac muscle is prepared for the next cycle of ECG;

  • U-wave: It is a small deflection immediately following the T-wave due to repolarization of the Purkinje fibres;

For analysing the different heart conditions and possible behaviour, Electrocardiogram (ECG) plays a key role in clinical trials. Medical practitioners heavily depend on the result of ECG interpretation. A series of deflections and wave of the ECG has different characteristics to show the different clinical conditions, which can be used for diagnosis purpose. To our knowledge, there are several databases and ontologies to represent the ECG. In our work, we use the existing ontological definition [25] to define the domain. The domain knowledge encapsulates all the required knowledge in ontology relationship. For describing the conceptual knowledge of the biological process, we use the OBO (Open Biomedical Ontologies) Process Ontology [11], which can be automated using the first-order reasoning. The main OBO relations are classified as the foundational relation, spatial relation, temporal relation and participation relation [11].

5.1 Domain Modelling

According to our four steps modelling methodology, we develop a domain model derived from the ontology of ECG. In this work, we define the OBO relations using the Event-B [3] modelling language then we use these formalised relations to describe the ECG ontology to develop a domain model for capturing the required domain knowledge. In the current work, we use the foundational relations as follows:

figure a

The first relation states that every instance of class A is an instance of class B and the second relation states that A part_of B holds if and only if: for every individual x, if x instantiates A then there is some individual y such that y instantiates B and x is a part of y. The instance_of is a relation between a class instance and a class which it instantiates and the PartOf_Inst is a relation between two class instances. The foundational relations, is_a and part_of, are defined in Event-B context using axioms (axm1–axm5). axm2 and axm3 define is_a relation and part_of relation, respectively. Other axioms (axm1, axm4 and axm5) are used to support the formal definition of the defined relations. Note that these defined OBO relations are used further to define the required domain knowledge for formalising the ECG protocol.

figure b

In our work, we adopt the existing available work [1, 2, 17, 18, 24] for designing and developing the domain model of ECG. Note that the developed ECG domain model based on existing ontologies contains a very abstract information related to the heart and ECG by hiding the main complexities. It is important to include complex details to consider every aspect of the domain knowledge. For the sake of simplicity, the produced domain model is used only for realising the case study of ECG protocol.

In order to define an ECG domain model, we define several small models based on sub-ontologies. These sub-ontologies are human heart, blood circulation, bioelectric phenomena and ECG, which are depicted in Fig. 3. All these sub-ontologies are connected to each other using dependency relationships. For instance, the sub-ontology of the human heart depends on the other sub-ontologies ECG, bioelectric phenomena and blood circulation.

Fig. 3
figure 3

Overview of a domain model based on ontology

Full size image

Human Heart. It is a domain model based on sub-ontology depicted in Fig. 4 to describe a very high-level abstraction of the heart. The heart consists of four chambers: left atrium, right atrium, left ventricle and right ventricle. There is the part_of relationships between the heart and four chambers. These relationships indicate that the heart has an only single chamber of each type. For instance, only one left atrium. There is also the is_a relationship between the Chamber and four heart chambers. Similarly, there is the is_a relationship between Muscle and four heart chambers.

Fig. 4
figure 4

Human heart domain model based on human heart sub-ontology

Full size image

The human heart domain model is formalised in the Event-B modelling language using a context. This context is an extension of our previous context, which contains the formal description of OBO relations. In this extended context, we use the is_a and part_of relationships to describe the relational properties between different biological entities according to the Fig. 4. All the possible relationships are defined using axioms (axm1–axm6). The next axiom (axm7) is declared as an enumerated set to define a set of physical units, which can be associated with variables and constants to maintain the physical unit consistency between variables during a calculation. For example, in our case, we define the beat per minute (bpm), centimetre (cm), millimetre (mm), micrometre (mu_m). axm8 defines a function to map between physical units and integer numbers that can be associated with any class to describe the class attributes. The next two axioms (axm9 and axm10) are used to define the heart rate considering the physical unit bpm. In a similar way, the next two axioms (axm11 and axm12) are used to define the normal heart rate associating with the same unit. The last axiom (axm13) defines the abnormal heart rate using the previous definitions of the heart rate and normal heart rate.

figure c
Fig. 5
figure 5

ECG domain model based on ECG sub-ontology

Full size image

ECG. It is a domain model based on sub-ontology depicted in Fig. 5 to describe a very high-level abstraction of the ECG. As we have previously described that the ECG is a sequence of deflections. All these elementary deflections can be described in different types of waves and segments, which form a typical ECG cycle. All these elementary entities, such as waves, segments and cycle, of ECG are organised using the is_a and part_of relationships to show the conceptual knowledge. Elementary entities are divided into two different types: Wave and Segment. There is the part_of relationship between the elementary entity and the wave and segment entities. In a typical ECG cycle, there are two kinds of segments, PQ Segment and ST-segment. The is_a relationships are used to denote the relations between Segment, and ST-segment and PQ segment. Similarly, the Wave entity is also divided into the different types of waves: P- wave, QRS wave, T-wave and U-wave. These waves are also related to the Wave entity using the is_a relationship. There is the part_of relationships between the QRS Wave and Q-wave, R-wave and S-wave. In a similar way, the Cycle entity and different waves (P-wave, Q-wave, R-wave, S-wave, T-wave and U-wave) entities and segments (PQ segment and ST-segment) are connected with the part_of relationship.

figure d

The ECG sub-ontology is formalised in the Event-B modelling language using the OBO relationships (is_a and part_of) according to the Fig. 5. All the possible relationships are defined in axioms (axm1–axm13). The next axiom (axm14) defines a set of leads (12-leads) as an enumerated set that represents the heart’s electrical activity recorded from electrodes on the body surface. The next five axioms (axm15–axm19) are defined as functions to characterise the ECG signal. These functions are RR_Int_equidistant to show the boolean state of the equidistant of RR interval; PP_Int_equidistant to show the boolean state of the equidistant of PP interval; P_Positive to show the positive visualisation of the P-wave, PP_Interval to represent the PP interval; and RR_Interval to represent the RR interval.

5.2 System Modelling

This section describes the second step of our modelling methodology. To design a system model (ECG protocol) using the domain knowledge, we revisit our developed case study of the ECG interpretation protocol [28, 42]. In this case study, our main objective is to utilise the domain knowledge explicitly in the development of ECG protocol. The ECG protocol is formalised to detect possible anomalies in the existing ECG protocol. In this development, we use the Event-B [3] modelling language that allows us to develop the whole complex ECG protocol using a correct by construction approach to introduce the detailed clinical properties of the ECG protocol. Figure 7 depicts an incremental formal development of the ECG interpretation protocol. Every refinement level introduces a diagnosis criteria for different components of the ECG signal, and each new criterion helps to analyse a particular set of diseases. The whole development of the ECG protocol is summarised below.

Fig. 6
figure 6

Basic diagram of assessing rhythm and rate [24]

Full size image
Fig. 7
figure 7

Refinements of ECG protocol

Full size image

5.2.1 Abstract Model (Assessing Rhythm and Rate)

Figure 6 depicts a standard clinical procedure for analysing the ECG protocol abstractly that is taken from [24]. This is a basic procedure that is used by most of the medical practitioners at the initial stage of clinical procedure for analysing the different heart conditions. In this basic procedure, the ECG protocol assesses the rhythm and heart rate to distinguish between the normal and abnormal heart conditions. We have used this clinical step for modelling the abstract model and the other clinical steps will be introduced progressively in the next refinement levels that are also adopted from [24].

In order to define the static properties, we define State and YesNoState as enumerated sets in axioms (axm1 and axm2). These two axioms are further used to define the normal and abnormal states of the heart in axm3 and the sinus states of the heart in axm4.

figure e

In our development, we define the clinical steps for analysing the ECG protocol. The first clinical step CS1 is defined as a function ClinicalProp1. This function has two input parameters Cycle and \(P\_Wave\), which are used to assess the ECG signal by the following clinical strategy: there exists equivalent in the PP interval, equivalent in the RR interval, the RR interval and PP interval are equal in leads (II, V1 and V2) and the positive visualisation of P-wave in lead II is TRUE. In order to satisfy this property the function ClinicalProp1 results as TRUE. In a similar way, we define the second clinical step CS2 defined as a function ClinicalProp2. This function has also two input parameters Cycle and \(P\_Wave\), which are used to assess the ECG signal by the following clinical strategy: the PP interval and RR interval are not equidistant, the RR intervals and PP intervals are not equivalent in all leads (II, V1 and V2), or the positive visualisation of P-wave in lead II is FALSE. In order to satisfy this property the function ClinicalProp2 results as TRUE. Note that these clinical properties are defined explicitly to build the domain knowledge of the ECG protocol.

figure f

To define the initial clinical procedure for assessing the rhythm and heart rate, we define three variables (inv1–inv3): Sinus to represent the sinus state of the heart; Heart_Rate to represent the heart rate limit; and Heart_State to show the normal or abnormal state of the heart. In the abstract model, we provide a list of safety properties using invariants (saf1–saf6) to verify the required conditions for the ECG interpretation protocol based on analysis of the signal features.

All these invariants are generated from the ECG protocol and extracted from the required documents with the help of medical experts. The first safety property (saf1) states that if the positive visualisation of P-wave in lead II is FALSE, then there is no sinus rhythm. The next safety property (saf2) states that if the sinus is yes then the clinical property ClinicalProp1 must be TRUE. This clinical property is defined in the context. Similarly, the next safety property (saf3) states that if the clinical property ClinicalProp2 is TRUE then there is no sinus rhythm. The next two safety properties (saf4 and saf5) state that if the heart rate belongs to the range of the normal heart rate and sinus rhythm is yes then the heart state is OK, and if the heart rate belongs to the abnormal heart rate and the sinus rhythm is yes then the heart state is KO. The last safety property (saf6) states that if the heart rate belongs to the range of the normal heart rate and the sinus rhythm is no then the heart state is KO.

In this abstract model, we define three events Rhythm_test_TRUE, Rhythm_test_-FALSE and Rhythm_test_TRUE_abRate. The guards of the first event state that the clinical property ClinicalProp1 is TRUE in the selected Cycle and \(P\_Wave\), and the heart rate belongs to the normal heart rate. The action of this event shows that the sinus rhythm is yes, the current heart rate is assigned and the heart state is OK.

figure g

In a similar way, the second event is used to assess the ECG to determine that the sinus rhythm is no, the current heart rate is assigned and the heart state is KO. The guards of this event state that the clinical property ClinicalProp2 is TRUE in the selected Cycle and \(P\_Wave\), and the heart rate belongs to the heart rate.

figure h

The last event also represents the ECG assessment for determining the sinus rhythm is Yes and the heart state is KO in the case of an abnormal heart rate. The guards of this event state that the clinical property ClinicalProp1 is TRUE in the selected Cycle and \(P\_Wave\), and the heart rate belongs to the abnormal heart rate.

figure i

5.2.2 An Overview of Refinement

This section describes an overview of the progressive development of the ECG protocol by defining new properties and introducing new recommended clinical practices to identify the possible heart diseases. Note that all the refinement steps correspond to the standard analyses steps of the ECG protocol [24]. Due to limited space, we present only a summary of each refinement development to understand the overall development process. A detailed formal development of the ECG protocol is available in the technical report [29].

  • First Refinement (Intervals and blocks). To classify different types of heart diseases, this refinement introduces a set of intervals and blocks. In particular, the PR interval and QRS interval are introduced to characterise the ECG signal. These intervals play an important role to assess the RBBB (Right Bundle Branch Block) and LBBB (Left Bundle Branch Block). In this development, we introduce new events for assessing the RBBB and LBBB through carefully analysing the QRS complex signal, and assessing the first degree AV block using the PR interval.

  • Second Refinement (Nonspecific intraventricular conduction delay and Wolff–Parkinson–White syndrome). The second refinement step is used to introduce the clinical analysis steps for the nonspecific intraventricular conduction delay (IVCD) and Wolff–Parkinson–White (WPW) syndrome. The WPW syndrome may mimic as an inferior MI, which is further analysed in the next refinements. According to the standard clinical process if the WPW syndrome, RBBB or LBBB is not detected during the clinical process then it indicates the presence of the nonspecific intraventricular conduction delay (IVCD).

  • Third Refinement (ST-segment elevation or depression). In this refinement, we introduce the ST-segment to analyse the ST-segments elevation or depression by defining the textual criteria, which is given in [24]. According to the clinical analysis step, it is necessary to assess the ST-segment before assessing the T-waves, QT-interval, electrical axis and hypertrophy because the diagnosis of acute MI or ischemia is vital and depends on the careful assessment of the ST-segment. A list of events is introduced to assess the ST-segment elevation, detection of troponin or CK-MB and acute inferior or anterior MI.

  • Fourth Refinement (Q-wave). This refinement is used to introduce the Q-wave for assessing the ECG signal. The introduction of Q-wave allows us to characterise the different clinical conditions, such as normal Q-wave assessment, abnormal Q-wave assessment for inferior MI (IMI) and anterolateral MI (AMI). In addition, we also introduce the R-wave to analyse the normal and abnormal pathological conditions of the R-wave together with the Q-wave.

  • Fifth Refinement (P-wave). This refinement introduces clinical assessment steps for analysing the P-wave to detect possible diseases due to an abnormality in the P-wave and atrial hypertrophy in ECG.

  • Sixth Refinement (Left and right ventricular hypertrophy). In this refinement, we introduce the clinical step for assessing the Left Ventricular Hypertrophy (LVH) and Right Ventricular Hypertrophy (RVH). According to the clinical step, the LVH and RVH do not require to determine if any bundle branch block (RBBB or LBBB) is present. Thus, it is necessary to exclude the possible clinical assessment for the LBBB and RBBB, which are described in the refinement 2 and refinement 3.

  • Seventh Refinement (T-wave). In this refinement, we introduce the T-wave to analyse the changing pattern of T-wave in ECG signal collected from 12-leads. The T-wave changes are usually nonspecific, but the T-wave inversion associated with other ST-segments indicates the myocardial ischemia, posterior MI, Hyperkalemia and pulmonary embolism.

  • Eighth Refinement (Electrical Axis). During the clinical assessment of the ECG, the electrical axis plays an important role to determine the different and correct positions of leads for detecting a desired quality of the ECG signal. According to the ECG protocol, there are two main criteria. First, if the leads I and aVF are upright then the axis is normal. Second, the axis is perpendicular to the lead with the most equiphasic or smallest QRS deflection. The left-axis deviation and commonly associated left anterior fascicular block are always visible in the ECG.

  • Ninth Refinement (Miscellaneous conditions). After several steps of clinical analysis, there are still several diseases which group together. To distinguish each disease at this level is very difficult due to the ambiguous nature of the clinical protocol and the associated properties. In this refinement level, we introduce the QT-interval and the required clinical steps for assessing the QT-interval. Moreover, this refinement also determines that if the electronic pacing is required using a pacemaker then there is no need to further assess the ECG signal. Otherwise, this refinement allows grouping of multiple miscellaneous conditions of the ECG for further clinical analysis.

  • Tenth Refinement (Arrhythmias). This is the last refinement of the ECG interpretation protocol, in which we introduce different types of tachyarrhythmias. In particular, we introduce clinical steps for determining the narrow complex tachycardia and the wide complex tachycardia to assess the different kinds of heart diseases.

5.3 Model Annotation

In our selected case study, we have developed the domain model and the ECG protocol as the system model. Both these models are formalised in Event-B. The domain model is described according to the ontology descriptions (see Sect. 5.1) and the ECG protocol is developed using the refinement approach by describing the intended clinical steps and the required properties. The domain model and system model are linked together with the annotation mechanism (i.e. see context relationship). In fact, this step is performed by using the ECG domain model, defined in context, in the ECG interoperation protocol for describing the stepwise clinical protocol. This annotation mechanism provides a specific relationship between the ECG protocol and ECG ontology concepts. For example, in the abstract model of the medical protocol, a variable \(Heart\_Rate\) is defined as the type of \(HEART\_RATE\), which is described in the domain model of the heart. Similarly, the two clinical assessment properties (CS1 and CS2) are defined as the functions ClinicalProp1 and ClinicalProp2 in the context C0 to use in the process of assessment of the ECG protocol.

Figure 8 depicts annotation relations between the domain model and ECG protocol. Note that the different arrow lines are used to show the use of ontology concepts of the ECG domain knowledge in the ECG interpretation protocol. Each arrow is linked with a specific refinement level, which uses required domain knowledge defined in the ECG domain model. Note that this annotation mechanism allows us to link the domain model and the system model explicitly.

Fig. 8
figure 8

Annotation between domain model (ECG) and system model (ECG interpretation protocol)

Full size image

5.4 Model Verification

This section describes the proof statistics of the generated proof obligations of the developed ECG interpretation protocol using stepwise refinement by considering the domain knowledge in the form of ontology and ECG protocol as a system model. In this development, we use the Event-B modelling language, which supports the consistency checking and refinement checking. The consistency checking guarantees that all the events of the model preserve all the given invariants. The refinement checking allows checking the correct refinement relation between progressively developed models. Table 1 shows the proof statistics of the revisited formal development of the ECG protocol. To guarantee the correctness of the system behaviour, we provide a list of safety properties in the incremental refinements. This development results in 592 (100%) POs, in which 401 (68%) POs are proved automatically, and the remaining 191 (32%) POs are proved interactively using the Rodin prover and SMT solver. These interactive proof obligations are mainly related to the refinement and complex mathematical expressions, which are simplified through interaction, providing additional information for assisting the Rodin prover. Some of the proofs are quite simple that is achieved by simplifying the predicates. According to the Table 1 in this new development, the proof efforts have been decreased significantly compared with the previous development of the ECG protocol [28, 42]. The proposed modelling approach restructures the system model by integrating the domain model explicitly. Note that the domain model has been developed progressively by analysing the domain-specific ontology and previously developed the system model. For instance, in the development of ECG interpretation protocol, we use the existing model and the ECG ontology to design the domain model. Note that several elements, such as constants, axioms, variables, invariants and functions, are removed/redefined in the system model and domain model. The modelling and integration of system model and domain model reduce the overall system complexity, proof efforts and improves the model consistency. For example, the clinical properties (CS1 and CS2) are defined once in the context model using the domain concepts. These properties have been used later in the ECG system model to define safety properties (see saf2 and saf3) and guards (grd1 in all three events). Once these properties are proved (CS1 and CS2) then these are used automatically in the process of proof automation for discharging the other POs. This indicates that the new development applying domain knowledge explicitly in the system development has improved the modelling processes and proof strategies.

Table 1 Proof statistics
Full size table

5.5 Anomalies

In this work, we have discovered several anomalies in the ECG interpretation protocol that are categorised into three main groups: ambiguity, inconsistency and incompleteness. Ambiguity is a well known anomaly that can represent more than one possible meaning of a fact, which causes possible confusion in a decision. For example, in our work, we encountered a problem to determine whether the terms “ST-depression” and “ST-elevation” have the same meaning or not. Inconsistency anomaly always leads to a conflicting result or different decision for similar data/input. For instance, in our work we found an inconsistency in form of applicable conditions, which state that the given conditions are applicable for both “male” and “female” subjects, however, elsewhere in the protocol it is advised that the given conditions are not applicable for “female”. Incompleteness anomaly is related to either missing piece of information or insufficient information in the original document. For instance, the original protocol contains “normal variant” factors to be considered for assessing T-wave. However, the meaning of “normal variant” is not defined in the protocol. Note that we have not listed all anomalies. In our work, we have identified these anomalies which may help for improving the quality of medical protocols.

6 Related Work

The use of ontology in software engineering for designing a complex system has great interest by several researchers to consider the domain knowledge explicitly. In [4, 5, 43], authors proposed a new approach for handling domain knowledge in design models. In this work, the domain models are developed using ontologies that can be used further during the system development applying the annotation mechanism. Hacid et al. [21, 22] have used the similar approach to develop a domain model based on ontologies for developing a system model using stepwise development. In [31], authors proposed a generic approach for integrating domain descriptions formalised by ontologies into an Event-B development process.

From the last decade, several pioneering works have been done to develop and analyse the medical guidelines and protocols based on expert’s requirements. Protocol representation languages, such as Asbru [39, 45], EON [32], PROforma [16] and others [34, 47] are used to represent a formal semantics of guidelines and medical protocols. The main objective of all these languages is to provide some standardisation and to improve the clinical practices by modifying the existing or outdated medical protocols. A detailed survey of different techniques and tools related to the clinical guidelines is described in [23]. The simplification and verification of the clinical guidelines using decision-table are presented in [40, 41] to guarantee the properties of completeness and consistency.

Jonathan et al. [38] proposed interactive formal verification for finding a bug and to improve the quality of medical protocols or guidelines. Simon et al. [9] used the Asbru modelling language and temporal logic to represent the medical protocols and then model checking approach was used for checking consistency and error detection. A European project, Protocure [7], developed the techniques and tools for improving the medical protocols by identifying anomalies like ambiguity and incompleteness in medical guidelines and protocols by using formal methods. This project used the Asbru [45] modelling language for describing the medical protocols and KIV interactive theorem prover [8] was used for formal proof of the medical protocol. Méry et al. [28, 29, 42] proposed a new approach for developing a complex medical protocol using a correct by construction approach in Event-B. Note that this case study is revisited in this work by developing the domain model and system model separately, and then these models are linked through an annotation approach (see context relationship) according to the four steps modelling methodology [5].

7 Conclusion

We have presented an approach to the development of medical protocols or guidelines using a correct by construction method that explicitly represents domain knowledge. Considering domain knowledge in the system development can be an excellent way for determining the confidence we have that a system model is safe, secure and effective by respecting all the required domain properties, used physical units and possible relations. In this work, we have presented a stepwise formal development of the medical protocol. The development model contains two different models: domain model and system model. The domain model describes the domain concepts based on ontologies [15] and the system model describes the functional behaviour of the medical protocol. The domain knowledge has been described in Event-B context using ontology relations to capture the functional behaviour of the medical protocols. The medical protocol is developed as a system model to assess the clinical protocol. Note that both the domain model and system model are linked through annotations, in which the system model uses all axioms and theorems defined in the domain ontology model. The main objective of this work is to check the consistency of a clinical medical protocol using a refinement based development that integrates domain knowledge explicitly. Moreover, the same approach can be used for developing any other medical protocols. In this work, we have used an ECG medical protocol and conducted a systematical analysis to verify that the formalisation complies with certain medically relevant protocol properties. This approach allows us to identify possible anomalies and improve the quality of medical protocols.