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

EVENT Q _ Assessment _ Normal
WHEN
grd1 : Q _ Width(II)< 40 ∧ Q _ Depth(II) ≤ 3000 ∧

Q _ Width(aVF)< 40 ∧ Q _ Depth(aVF) ≤ 3000 ∧

Q _ Width(aVL)< 40

grd2 : Q _ Width(III) ≤ 40 ∧ Q _ Depth(III) ≤ 7000 ∧ Q _ Depth(aVL) ≤ 7000

grd3 : Q _ Depth(I ) < 40 ∧ Q _ Depth(I ) ≤ 1500

THEN
act1 : Q _ Normal _ Status := TRUE
END

The event Q_Assessment_Abnormal_AMI is used to identify the Acute_anterior_
MI symptoms of the heart using ECG signal. A list of guards are defined to cover
the conditions of the diagnosis process. These guards express that the sinus rhythm
is Ye s , 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, the width of Q-wave is greater than
or equal to 40 ms and the depth of Q-wave is greater than or equal to 3000 µm in
leads V5 and V6, the width of Q-wave is greater than or equal to 40 ms and depth
of Q-wave is greater to 7000 µm in lead aVL, the width of Q-wave is greater than
or equal to 40 ms and the depth of Q-wave is greater to 1500 µm in lead I, and the
normal state of the Q-wave is FALSE.

EVENT Q _ Assessment _ Abnormal _ AMI
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 ,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 )

)
))