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

EVENT R _ Q _ Assessment _ R _ Abnormal _ V56
WHEN
grd1 : Q _ Wa v e _ State(V 5 ) = TRUE ∧

Q _ Wa v e _ State(V 6 ) = TRUE

grd3 : Heart _ State = KO

THEN
act1 : Disease _ step 5 :∈ { lateral _ MI, Hypertrophic _ cardiomyopathy }

END

10.5.6 Fifth Refinement: P-wave

This refinement level introduces a criterion to assess the P-wave for abnormali-
ties, including the atrial hypertrophy in the ECG signal [ 16 ]. A new variable Dis-
ease_step6 is introduced in this refinement to introduce a set of diseases related
to the P-wave. Some new variables are also introduced to assess the P-wave from
12-leads ECG signals, which are represented by inv 2- inv 4. The first two invariants
introduce new variables in form of total functions mapping from leads (LEADS)
to

. These functions return height and broadness of the P-waves. The next invari-
ant ( inv 4) represents total function mapping leads (LEADS) to BOOL . It returns
diphasic state in a boolean type. A set of invariants ( inv 5- inv 7) are representing the
confirmation of an abnormal state of the heart ( KO ). These invariants state that if
the sinus rhythm is Ye s and a new disease is found, then the heart will be in an ab-
normal state. The invariant ( inv 5) is checking for existence of multiple diseases dur-
ing the P-wave diagnosis. Five new events P_Wave_assessment_Peaked_Broad_No ,
P_Wave_assessment_Peaked_Yes , P_Wave_assessment_Peaked_Yes_Check_RAE ,
P_Wave_assessment_Broad_Yes and P_Wave_assessment_Broad_Yes_Check_LAE
are introduced to assess the P-wave.

N

inv 1 : Disease _ step 6 ∈ Disease _ Codes _ Step 6

inv 2 : P _ Wa v e _ Peak ∈ LEADS → N

inv 3 : P _ Wa v e _ Broad ∈ LEADS → N

inv 4 : Diphasic ∈ LEADS → BOOL

inv 5 : Sinus = Ye s ∧ Disease _ step 6 ∈

{ RVH, RV _ strain, pulmonary _ embolism,

RAE, mitral _ stenosis, mitral _ regurgitation, LV _ failure,
LAE, dilated _ cardiomyopathy, LVH _ cause }

Heart _ State

= KO

inv 6 : Sinus = Ye s ∧ Disease _ step 6 = LAE ⇒ Heart _ State = KO

inv 7 : Sinus = Ye s ∧ Disease _ step 6 = RAE ⇒ Heart _ State = KO

The textual representation of formal notation of the P-wave assessment is given
in [ 16 ]. We have formalised all the textual guidelines.
The event P_Wave_assessment_Peaked_Broad_No shows that there is not any
particular condition related to the heart disease under the specified guards. The
guard of this event state that the peak of P-wave is less than 3000 µm in leads II