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

and VI, or the broad of P-wave is less than 110 ms in leads II and VI, or the diphasic
is FALSE in lead (II or VI).

EVENT P _ Wave _ assessment _ Peaked _ Broad _ No
WHEN
grd1 : (P _ Wa v e _ Peak (II)< 3000 ∧

P _ Wa v e _ Peak (V 1 )< 3000 )
(P _ Wa v e _ Broad(II)< 110

∧ P _ Wa v e _ Broad(V 1 )< 110 ) ∨

Diphasic(II) = FA L S E ∨

Diphasic(V 1 ) = FA L S E

THEN
act1 : Disease _ step 6 := NDS 6

END

The event P_Wave_assessment_Peaked_Yes is used to assess the heart condition
using ECG signal. The guards of this events state that the peak of P-wave is greater
than or equal to 3000 µm in lead II and VI and the heart is in abnormal state.

EVENT P _ Wave _ assessment _ Peaked _ Ye s
WHEN
grd1 : P _ Wa v e _ Peak (II) ≥ 3000
grd2 : P _ Wa v e _ Peak (V 1 ) ≥ 3000
grd3 : Heart _ State = KO
THEN
act1

: Disease _ step 6 := RAE

END

The event P_Wave_assessment_Peaked_Yes_Check_RAE is used to identify sev-
eral diseases related to the RVH, RV strain, and pulmonary. The guards of this event
are very simple that formalise basic assessment process to discover the disease from
the ECG signal. The guards of this event state that the peak of P-wave is greater than
or equal to 3000 µm in lead II and VI, the heart is in abnormal state and the heart
condition must be equivalent by RAE.

EVENT P_Wave_assessment_Peaked_Yes_Check_RAE
Refines P_Wave_assessment_Peaked_Yes
WHEN
grd1 : P _ Wa v e _ Peak (II) ≥ 3000

grd2 : P _ Wa v e _ Peak (V 1 ) ≥ 3000

grd3 : Heart _ State = KO

grd4 : Disease _ step 6 = RAE

THEN
act1 : Disease _ step 6 :∈ { RVH, RV _ strain, pulmonary _ embolism }

END