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

EVENT Axis_Assessment_QRS_upright_No_QRS_negative
Refines Axis _ Assessment _ QRS _ upright _ No
WHEN
grd1 :¬ (QRS _ Axis _ State(I ) = D _ Upright ∧

QRS _ Axis _ State(aVF) = D _ Upright)

grd2 : QRS _ Axis _ State(I ) = D _ Negative ∧

QRS _ Axis _ State(aVF) = D _ Negative

grd3 : Heart _ State = KO
THEN
act1 : minAngle := 110
act2 : maxAngle := 180
act3 : Axis _ Devi := RAD
END

The event Misc_Disease_Step9_LAD assess miscellaneous diseases like LAFB,
MSCHD, etc. A set of guards is used that defines that the axis deviation is left axis
deviation (LAD) in leads, negative minimum angle is

− 30, negative maximum angle

is − 90 and the heart is in abnormal state.

Misc _ Disease _ Step9 _ LAD
WHEN
grd1 : Axis _ Devi = LAD ∧

minAngle =− 30 ∧

maxAngle =− 90

grd2 : Heart _ State = KO

THEN
act1 : Disease _ step 9 :∈ { LAFB, MSCHD, Some _ Fo r m _ VT, ED _ OC }

END

The event Misc_Disease_Step9_LAD assess several diseases like LPFB, Dextro-
cardia, NV MS-EC. A set of guards is used that defines that the axis deviation is
right axis deviation (RAD) in leads, positive minimum angle is 110, positive maxi-
mum angle is 180 and the heart is in abnormal state.

Misc _ Disease _ Step9 _ RAD
WHEN
grd1 : Axis _ Devi = RAD ∧

minAngle = 110 ∧

180
grd2 : Heart _ State = KO
THEN
act1 : Disease _ step 9 :∈ { LPFB, Dextrocardia, NV _ MSEC }
END

maxAngle =

The event R_Q_Assessment_R_Abnormal_V56_axis_deviation refines R_Q_
Assessment_R_Abnormal_V56 . This event is used to identify the lateral MI. A set of
guards is used that formalises that the state of Q-wave is TRUE in leads V5 and V6,