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

rhythm is Ye s , the ST elevation 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), ST depression 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_NO_TCKMB_No 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 := Ischemia

END

The event Acute_IA_MI presents a diagnoses process for the Acute inferior MI
and Acute anterior MI. A set of guard predicates characterised the heart state and
shows that the sinus rhythm is Ye s , the ST elevation is TRUE and the length of ST
segment elevation is greater than or equal to 1000 µm in two or more leads (II, III,
aVF), or the ST elevation is TRUE and the length of ST segment elevation is greater
than or equal to 1000 µm in two or more contiguous pre-cordial leads V1 to V6.

EVENT Acute _ IA _ MI
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) ≥

∧ ST _ seg _ ele(k) ≥

1000 1000 )

∧ l = k)
(( ∃ 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

∧