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

ease_step9 have been defined here for assessment of the electrical axis. A new vari-
able QRS_Axis_State is defined as a total function mapping from leads (LEADS) to
QRS_directions . This function represents the QRS-axis direction of the leads. Two
invariants ( inv 6- inv 7) represent the safety properties in assessment of the correct
axis. These invariants are verifying an abnormal state of the heart ( KO ) using axis
position.

inv 1 90 .. 180

inv 2 : maxAngle ∈− 90 .. 180
inv 3 : Axis _ Devi ∈ Axis _ deviation
inv 4 : Disease _ step 9 ∈ Disease _ Codes _ Step 9
inv 5 : QRS _ Axis _ State ∈ LEADS → QRS _ directions
inv 6 : Disease _ step 9 ∈{ LPFB, Dextrocardia, NV _ MSEC }∧
maxAngle = 180 ∧ minAngle = 110
Heart _ State = KO

: minAngle ∈−

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

∧ maxAngle =− 90 ∧ minAngle =− 30

Heart _ State

= KO

In this refinement level, we introduce various events for assessing different kinds
of features from 12 leads ECG signal corresponding to the angle. Following events
are introduced in this refinement: Axis_Assessment_QRS_upright_Yes_Age_less_40 ,
Axis_Assessment_QRS_upright_Yes_Age_gre_40 , Axis_Assessment_QRS_upright_
No_QRS_positive , Axis_Assessment_QRS_upright_No_QRS_negative , Misc_Dis-
ease_Step9_LAD ,

Misc_Disease_Step9_RAD , R_Q_Assessment_R_Abnormal_

V56_axis_deviation .
The event Axis_Assessment_QRS_upright_Yes_Age_less_40 refines Axis_As-
sessment_QRS_upright_Yes . This event is used to find the electrical axis. A set
of guards is used that specifies that the QRS axis state is upright in leads I and aVF,
and age is less than 40 years.

EVENT Axis_Assessment_QRS_upright_Yes_Age_less_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 := 0

act2 : maxAngle := 110

END