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

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

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

((ST _ seg _ ele(l)

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

(Abnormal _ Shaped _ ST(l)

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

∧ k)

( ∀ l 1 ,k 1 · l 1 ∈ LEADS ∧ k 1 ∈ LEADS ∧
((ST _ elevation(l 1 ) = FA L S E ∨ ST _ elevation(k 1 ) = FA L S E )
((ST _ seg _ ele(l 1 )< 1000 ∨ ST _ seg _ ele(k 1 )< 1000 )
(Abnormal _ Shaped _ ST(l 1 ) = FA L S E ∨
Abnormal _ Shaped _ ST(k 1 ) = FA L S E )))
⇒ l 1

l =

= k 1 ))

grd5 : T _ inversion _ l _ d(V 2 ) = Localized ∧

T _ inversion _ l _ d(V 3 ) = Localized ∧

T _ inversion _ l _ d(V 4 ) = Localized ∧

T _ inversion _ l _ d(V 5 ) = Localized

grd6 : T _ inversion _ l _ d(II) = Localized ∧

T _ inversion _ l _ d(III) = Localized ∧

T _ inversion _ l _ d(aVF) = Localized

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

THEN
act1 : Disease _ step 8 := Probable _ ischemia

END

The event T_Inversion_Diffuse_B is used to diagnose the symptoms for car-
diomyopathy, other nonspecific from the ECG signal. A set of guards is used that
specifies the required conditions that state that 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 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 greater than 5000 µm in all leads, the T
inversion is diffuse, and the normal state of T-wave is FALSE.

T _ Inversion _ Diffuse _ B
WHEN
grd1 : (( ∃ l,k · l ∈ LEADS ∧ k ∈ LEADS ∧

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

((ST _ seg _ ele(l) ≥

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

(Abnormal _ Shaped _ ST(l) =

TRUE ∧

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

∧ l = k)