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

inv 1 : Delta _ Wa v e ∈ N

inv 2 : Disease _ step 3 ∈ Disease _ Codes _ Step 3

inv 3 : ST _ elevation ∈ LEADS → BOOL

inv 4 : Epsilon _ Wa v e ∈ LEADS → BOOL

inv 5 : Sinus = Ye s ∧ Disease _ step 3 = WPW _ Syndrome

Heart _ State

KO
inv 6 : Sinus = Ye s ∧ Disease _ step 3 = Brugada _ Syndrome
Heart _ State = KO
inv 7 : Sinus = Ye s ∧ Disease _ step 3 = RV _ Dysplasia
Heart _ State = KO
inv 8 : Sinus = Ye s ∧ Disease _ step 3 = IVCD
Heart _ State = KO

=

We have introduced four events QRS_Test_Atypical_RLBBB_WPW_Syndrome ,
QRS_Test_Atypical_RBBB_Brugada_Syndrome , QRS_Test_Atypical_RBBB_RV_
Dysplasia and QRS_Test_Atypical_RBBB_IVCD to interpret atypical right bundle
branch block using QRS interval. The basic rules for assessing the ECG signal in
this refinement are given as follows:

• If the QRS duration is prolonged 110 ms and bundle branch block appears to

be present but is atypical, consider WPW syndrome, particularly if there is a tall
R-wave in leads V1 and V2.

≥

• Assess for a short PR interval ≤ 120 ms and for a delta wave.

The event QRS_Test_Atypical_RLBBB_WPW_Syndrome is used to identify a dis-
ease WPM Syndrome, where a set of required conditions for diagnosis purpose is
given in form of guard predicates. The guards of this event state that the QRS in-
terval is greater than or equal to 110 ms, already symptoms of RBBB or LBBB is
identified, summation of delta wave and PR interval is less than or equal to 120 ms,
and the heart is in abnormal state ( KO ).

EVENT QRS _ Te s t _ Atypical _ RLBBB _ WPW _ Syndrome
ANY sympt,d _ wave
WHERE
grd1 : QRS _ Int ≥ 110

grd2 : sympt = A _ RBBB ∨ sympt = A _ LBBB

grd3 : d _ wave ∈ N

grd4 : d _ wave + PR _ Int) ≤ 120

grd5 : Heart _ State = KO

THEN
act1 : Delta _ Wa v e := d _ wave

act2 : Disease _ step 3 := WPW _ Syndrome

END