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

EVENT R _ Assessment _ Normal
ANY age
WHERE
grd1 : R _ Depth(V 1 ) ≥ 0 ∧ R _ Depth(V 1 ) ≤ 6000 ∧ age > 30

grd2 : R _ Depth(V 2 )> 200 ∧ R _ Depth(V 2 ) ≤ 12000 ∧ age < 30

grd3 : R _ Depth(V 3 ) ≥ 1000 ∧ R _ Depth(V 3 ) ≤ 24000 ∧ age > 30

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

The event R_Assessment_Abnormal is used to identify the miscellaneous states
of the heart, when the R-wave of the ECG signal is abnormal.

EVENT R _ Assessment _ Abnormal
WHEN
grd1 : R _ Normal _ Status = FA L S E
THEN
act1 : Mice _ State :∈ { late _ transition, normal _ variant }
END

The event R_Q_Assessment_R_Abnormal_V1234 is used to determine the ante-
rior MI, LVH and emphysema with miscellaneous state Exclude Mimics MI. A set
guards shows that the normal state of the R-wave is FALSE, the state of Q-wave is
TRUE in leads V1 to V4.

EVENT R _ Q _ Assessment _ R _ Abnormal _ V1234
WHEN
grd1 : R _ Normal _ Status = FA L S E

grd2 : Q _ Wa v e _ State(V 1 ) = TRUE ∧

Q _ Wa v e _ State(V 2 ) = TRUE ∧

Q _ Wa v e _ State(V 3 ) = TRUE ∧

Q _ Wa v e _ State(V 4 ) = TRUE

THEN
act1 : Disease _ step 5 :∈ { anterior _ MI, LVH , emphysema }

act1 : Mice _ State := Exclude _ Mimics _ MI

END

The event R_Q_Assessment_R_Abnormal_V56 diagnose the lateral MI and Hy-
pertrophic cardiomyopathy. The guards of this event state that the state of Q-wave
is TRUE in leads V5 and V6, and the heart state is in abnormal state ( KO ).