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

The event T_Wave_Assessment_B_DI refines T_Wave_Assessment_Inverted_Yes .
This event is used to discover the symptoms for definite ischemia from the ECG sig-
nal. A set of guards is used that specifies underlined conditions for definite ischemia.
The guards of this event state that the ST elevation is TRUE in all leads or the normal
status of Q-wave is FALSE, the normal status of T-wave is FALSE, the ST elevation
is TRUE and the ST segment elevation is greater than or equal to 1000 µm, or the
abnormal shape of ST segment is TRUE in any two leads.

EVENT T_Wave_Assessment_B_DI Refines T _ Wave _ Assessment _ Inverted _ Ye s
WHEN
grd2 :∀ l · l ∈ LEADS ⇒ ST _ elevation(l) = TRUE

Q _ Normal _ Status

= FA L S E

grd3 : T _ Normal _ Status = FA L S E

grd4 :∃ l,k · l ∈ LEADS ∧ k ∈ LEADS ∧

((ST _ seg _ ele(l) ≥ 1000 ∧ ST _ seg _ ele(k) ≥ 1000 ) ∨

(ST _ elevation(l) = TRUE ∧ ST _ elevation(k) = TRUE)

(Abnormal _ Shaped _ ST(l)

= TRUE ∧ Abnormal _ Shaped _ ST(k) = TRUE))

l

= k

THEN
act1 : Disease _ step 8 := Definite _ ischemia
END

The event T_Inversion_Likely_Ischemia refines T_Wave_Assessment_Inverted_
Ye s . This event is used to trace the symptoms for probable ischemia from the ECG
signal. A set of guards is used that specifies the required conditions for the proba-
ble ischemia. The guards of this event state that the state of T-wave is inverted in
all leads, the ST elevation is TRUE in all leads or the normal status of Q-wave is
FALSE, the inversion in T-wave is greater than 5000 µm in all leads, the ST eleva-
tion is TRUE and the ST segment elevation is greater than or equal to 1000 µm, or
the abnormal shape of ST segment is TRUE in anyone lead, or the ST elevation is
FALSE or the ST segment elevation is less than 1000 µm, and the abnormal shape
of ST segment is FALSE in any two leads, the inversion in T-wave is localised in
leads II, III, aVF, and V2 to V5, and the normal state of T-wave is FALSE.

EVENT T_Inversion_Likely_Ischemia Refines T _ Wave _ Assessment _ Inverted _ Ye s
WHEN
grd1 :∀ l · l ∈ LEADS ⇒ T _ Wa v e _ State(l) = Inverted

grd2 :∀ l · l ∈ LEADS ⇒ ST _ elevation(l) = TRUE

Q _ Normal _ Status

= FA L S E

grd3 :∀ l · l ∈ LEADS ⇒ T _ inversion(l) > 5000