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

grd6 : LVH _ specificity = 90

sensitivity < 40

grd7 : Disease _ step 6 = LAE ⇒ LVH _ specificity < 98

grd8 : Heart _ State = KO

THEN
act1 : Disease _ step 6 := LVH _ cause

END

The event RVH_Assessment refines P_Wave_assessment_Broad_Yes_Check_
RAE . This event is used to identify the Right Ventricular Hypertrophy RVH. A list
of guards presents the required conditions for the symptoms of RVH. The guards
of this event state that the peak of P-wave is greater than or equal to 3000 µm in
leads II and V1, using previous assessment of the disease indicates the symptoms
of RAE, the depth of R-wave is greater than or equal to 7000 µm and age is greater
than 30 years, the depth of S-wave is greater than or equal to 7000 µm in leads V5
or V6, the ratio of R- and S-wave is greater than or equal to 1 in lead V1, the ratio
of R-wave and S-wave is less than or equal to 1 in lead V5 or V6, angular axis is
greater than or equal to 110 degree, the previous assessment of the disease does not
indicate the symptoms of LBBB or RBBB, QRS interval is less than 120 ms, and
heart state is in abnormal state.

EVENT RVH_Assessment Refines P _ Wave _ assessment _ Peaked _ Ye s _ Check _ RAE
ANY age, aixs
WHERE
grd1 : P _ Wa v e _ Peak (II) ≥ 3000
grd2 : P _ Wa v e _ Peak (V 1 ) ≥ 3000
grd3 : Disease _ step 6 = RAE
grd4 : R _ Depth(V 1 ) ≥ 7000 ∧ age > 30
grd5 : S _ Depth(V 5 ) ≥ 7000 ∨
S _ Depth(V 6 ) ≥ 7000
grd6 : R _ S _ Ratio(V 1 ) ≥ 1
grd7

: R _ S _ Ratio(V 5 ) ≤

1
R _ S _ Ratio(V 6 ) ≤

1

grd8 : aixs ∈ 0 .. 360 ∧ aixs ≥ 110

grd9 : Disease _ step 2 ∈{ LBBB, RBBB }

grd10 : QRS _ Int < 120

grd11 : Heart _ State = KO

THEN
act1 : Disease _ step 6 := RVH

END