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

prediction are also encountered lots of diagnosis to find the various kinds of heart
diseases.
This section describes the abstract model of the ECG interpretation protocol.
Every level of refinement introduces new context file for adding static properties of
the system and list of heart diseases after introducing certain protocol of the ECG
interpretation. Every refinement level is used to introduce a new set of diagnosis
criteria to test the ECG signals. The following sections presents a sufficient detail
information of the remaining refinement stages helping a reader to understand the
rational of each refinement stage for formalising the ECG interpretation protocol.

10.5.2 First Refinement: Assess Intervals and Blocks

In an abnormal ECG signal, all the ECG features are varying according to the symp-
toms of heart diseases. We formalise the ECG interpretation protocol using an incre-
mental approach, where we determine all features of the ECG signal. This level of
refinement determines the PR- and QRS-intervals for the ECG interpretation. These
intervals classify different kinds of the heart diseases.
Invariants ( inv 1- inv 3) represent a set of new introduced variables in the refine-
ment for expressing formalisation of the ECG interpretation protocol. These vari-
ables are PR_Int , Disease_step2 , QRS_Int . Other variables ( M_Shape_Complex ,
Slurred_S , Notched_R , Small_R_QS and Slurred_S_duration ) are introduced as
total functions in invariants ( inv 4- inv 8) where total functions are mapping from
leads (LEADS) to BOOL and

N 1 , respectively. The function M_Shape_Complex
returns existence of M-shape complex from the ECG signals in form of TRUE or
FALSE . The function Slurred_S represents Slurred S-wave, the function Notched_R
represents notched R-wave and the function Small_R_QS represents small R- or
QS-waves, in boolean type. The function Slurred_S_duration is used to calculate
Slurred-S duration.
A set of invariants ( inv 9- inv 14) presents safety properties to validate formal rep-
resentation of the ECG interpretation protocol. All these properties are derived from
the original protocol to verify the correctness and consistency of the system. These
properties are formulated through logic experts as well as cardiologist experts ac-
cording to the original protocol. The main advantage of this technique is that if
any property does not hold by the model, then it helps to find anomalies or to find
missing parts of the model such as required conditions and parameters.
Invariants ( inv 9- inv 13) represent an abnormal state of the heart ( KO ) to identify
any disease and unsatisfying condition for features of the ECG signal, in the formal
diagnosis process. While the last invariant ( inv 14) presents all the required proper-
ties for a normal heart. It states that if the heart rate is in between 60 to 100 bpm,
the sinus rhythm is Ye s , the PR interval is less than or equal to 200 ms and the QRS
interval is less than 120 ms, then the heart state is OK .