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

EVENT T _ Wave _ Assessment _ Inverted _ Ye s _ PM
WHEN
grd1 : P _ Wa v e _ Peak (II) ≥ 3000

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

grd3 : Disease _ step 6 = RAE

grd4 : (( ∀ p · p ∈ LEADS ⇒ T _ Wa v e _ State(p) = Inverted) ∧

( ∀ t · t ∈ LEADS ⇒ ST _ elevation(t) = TRUE

Q _ Normal _ Status = FA L S E ))
grd5 : (( ∃ 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) = FA L S E ∧
Abnormal _ Shaped _ ST(k) = FA L S E ))
⇒ l = 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 = k 1 ))

grd6 : Asy _ T _ Inversion _ strain(V 1 ) = TRUE ∧

Asy _ T _ Inversion _ strain(V 2 ) = TRUE ∧

Asy _ T _ Inversion _ strain(V 3 ) = TRUE

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

THEN
act1 : Disease _ step 6 := pulmonary _ embolism

END

The event T_Wave_Assessment_B is used to identify the status of the T-wave.
Moreover, this event assess the pattern of T-wave changes. The guards of this event
state that the state of T-wave is upright in leads I, II, and V3 to V6, the state of
T-wave is inverted in lead aVL, and the state of T-wave is variable in leads III, aVL,
aVF, V1 and V2.

EVENT T _ Wave _ Assessment _ B
WHEN
grd1 :∀ l · l ∈{ I,II,V 3 ,V 4 ,V 5 ,V 6 }⇒ T _ Wa v e _ State _ B(l) = Upright

grd2 : T _ Wa v e _ State _ B(aVL) = Inverted _ B

grd3 :∀ l · l ∈{ III, aVL, aVF,V 1 ,V 2 }⇒ T _ Wa v e _ State _ B(l) = Variable

THEN
act1 : T _ Normal _ Status := TRUE

END