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

inv 11 : Sinus = Ye s ∧ Disease _ step 8 = posterior _ MI ⇒ Heart _ State = KO

inv 12 : Sinus Definite _ ischemia,

Probable _ ischemia, Digitalis _ effect

= Ye s ∧ Disease _ step 8 ∈{

}

Heart _ State

= KO

inv 13 : Sinus = Ye s ∧ Disease _ step 8 = Definite _ ischemia ⇒ Heart _ State = KO

inv 14 KO

inv 15 : Sinus = Ye s ∧ Disease _ step 8_ B ∈{ Cardiomyopathy, other _ nonspecific }
Heart _ State = KO

: Sinus = Ye s ∧ Disease _ step 8 = Probable _ ischemia ⇒ Heart _ State =

The event T_Wave_Assessment_Peaked_V123456 presents basic symptoms for
assessing the hyperkalaemia. The guards of this event state that the heart is in ab-
normal state, and the state of T-wave is peaked in leads from V1 to V6.

EVENT T _ Wave _ Assessment _ Peaked _ V123456
WHEN
grd1 : Heart _ State = KO

grd2 :∀ l · l ∈{ V 1 ,V 2 ,V 3 ,V 4 ,V 5 ,V 6 }⇒ T _ Wa v e _ State(l) = Peaked

THEN
act1 : Disease _ step 8 := Hyperkalemia

END

The event T_Wave_Assessment_Peaked_V12 is used to assess normal variant in
the ECG signal. A list of conditions for assessing the normal variant is given in the
guards. The guards of this event state that the normal status of the R-wave is FALSE,
the state of T-wave is peaked in leads V1 and V2, 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, inversion in T-wave is less than 5000 µm in all leads, and
the status of T-wave is FALSE.

EVENT T _ Wave _ Assessment _ Peaked _ V12
WHEN
grd1 : R _ Normal _ Status = FA L S E
grd2 : T _ Wa v e _ State(V 1 ) = Peaked ∧
T _ Wa v e _ State(V 2 ) = Peaked

grd3 : (( ∃ 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)
∨