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

((

∃ l 1 ,k 1 · l 1 ∈{ V 1 ,V 2 ,V 3 ,V 4 ,V 5 ,V 6 }∧ k 1 ∈{ V 1 ,V 2 ,V 3 ,V 4 ,V 5 ,V 6 }∧

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

(ST _ seg _ ele(l 1 )

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

∧ l 1 = k 1

(
(l 1 = V 1 ∧ k 1 = V 2 ) ∨
(l 1 = V 2 ∧ k 1 = V 3 ) ∨
(l 1 = V 3 ∧ k 1 = V 4 ) ∨
(l 1 = V 4 ∧ k 1 = V 5 ) ∨
(l 1 = V 5 ∧ k 1 = V 6 )
)
))

: Disease _ step 4 ∈{ Acute _ inferior _ MI, Acute _ anterior _ MI }

grd3

THEN
act1 : Disease _ step 4 := STEMI

END

The event ST_seg_elevation_NOTCKMB_Yes is used to trace the symptoms of
the Non-ST Elevation Myocardial Infarction (Non-STMEI). A set of guard predi-
cates characterised the heart state and shows that the sinus rhythm is Ye s ,STele-
vation is TRUE and the length of ST segment elevation is greater than or equal to
1000 µm in anyone lead (II, III, aVF), or the ST elevation is FALSE and the length
of ST segment elevation is less than 1000 µm in all leads (II, III, aVF), the ST de-
pression is greater than or equal to 1000 µm in two or more leads (LEADS), and
disease must be Troponin, CK-MB.

EVENT ST_seg_elevation_NOTCKMB_Yes Refines ST _ seg _ elevation _ NO
WHEN
grd1 : Sinus = Ye s

grd2 : ( ∃ l,k · l ∈{ II, III, aVF }∧ k ∈{ II, III, aVF }∧

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

(ST _ seg _ ele(l)

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

∧ l = k)

(

∀ l 1 · l 1 ∈{ II, III, aVF }⇒

(ST _ elevation(l 1 ) = FA L S E ∧ ST _ seg _ ele(l 1 )< 1000 ))

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

(ST _ depression(l) ≥ 1000 ∧ ST _ depression(k) ≥ 1000 )

∧ l = k

grd4 : Disease _ step 4 ∈{ Troponin, CK _ MB }

THEN
act1 : Disease _ step 4 := Non _ STEMI

END

The event ST_seg_elevation_NO_TCKMB_No captures the essential conditions
to determine the ischemia. A set of guards of this event describes that the sinus