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

The event Axis_Assessment_QRS_upright_Yes_Age_gre_40 refines Axis_Assess-
ment_QRS_upright_Yes . This event is similar to the last event that is also used to
assess the electrical axis. The minimum angle is

−

30 and maximum angle is 90.
A set of guards is used that defines that the QRS axis state is upright in leads I and
aVF, and age is greater than 40 years.

EVENT Axis_Assessment_QRS_upright_Yes_Age_gre_40
Refines Axis _ Assessment _ QRS _ upright _ Ye s
ANY age
WHERE
grd1

: QRS _ Axis _ State(I ) = D _ Upright ∧
QRS _ Axis _ State(aVF) = D _ Upright

grd2 : age ∈ N ∧ age > 40

THEN
act1 : minAngle := − 30

act2 : maxAngle := 90

END

The event Axis_Assessment_QRS_upright_No_QRS_positive refines Axis_As-
sessment_QRS_upright_No . This event is used to determine the electrical axis and
left axis deviation (LAD) in leads. A set of guards is used that defines that the QRS
axis state is not upright in leads I and aVF, the QRS axis state is positive in leads I
and aVF, and the heart is in abnormal state.

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

: QRS _ Axis _ State(I ) = D _ Positive ∧
QRS _ Axis _ State(aVF) = D _ Positive

grd2

grd3 : Heart _ State = KO

THEN
act1 : minAngle := − 30

act2 : maxAngle := − 90

act3 : Axis _ Devi := LAD

END

The event Axis_Assessment_QRS_upright_No_QRS_negative refines Axis_As-
sessment_QRS_upright_No . This event is used to identify the electrical axis and
right axis deviation (RAD) in leads. A set of guards is used that defines that the
QRS axis state is not upright in leads I and aVF, the QRS axis state is negative in
leads I and aVF, and the heart is in abnormal state.