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

(
(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 )

)
))

THEN
act1 : Disease _ step 4 :∈ { Acute _ inferior _ MI, Acute _ anterior _ MI }
END

10.5.5 Fourth Refinement: Assess for Pathologic Q-wave

This refinement only introduces new guidelines to interpret Q-wave feature of the
ECG signal and assessment-related diseases to the Q-wave and R-wave [ 16 ]. Some
new variables are represented by a set of invariants ( inv 1- inv 2) to handle the re-
quired features of the Q-wave and R-wave to diagnose the ECG signal. The func-
tions Q_Normal_Status and R_Normal_Status represent the normal state of the Q
and R-waves in a boolean type. The next three invariants ( inv 3- inv 5) are used to de-
clare new variables in form of total functions mapping leads (LEADS) to , and

an invariant ( inv 6) is also total function mapping leads (LEAD) to BOOL .The
functions Q_Width , Q_Depth and R_Depth calculate the Q-wave width, Q-wave
depth and R-wave depth, respectively. The last function Q_Wave_State represents
the boolean state of the Q-wave for all leads. Two other new variables Age_of_Inf
and Mice_State represent infarction age and miscellaneous states. An enumerated
set of infarction age and miscellaneous states define as Age_of_Infarct

N

= { recent ,

indeterminate , old } and Mice_State5 { Exclude _ Mimics _ MI , late _ transition , nor-

mal _ variant , borderline _ Qs , NMS }, respectively in the context. The variable Dis-
ease_step5 represents a group of diseases of this refinement level as analysis of the
Q-wave from the ECG signals. Some invariants ( inv 10- inv 13) are introduced as rep-
resenting the safety properties to confirm an abnormal state of the heart ( KO ). All
invariants have similar form for checking the heart state under the various disease
conditions. These invariants state that if the sinus rhythm is Ye s and a new disease
is found, then the heart must be in the abnormal ( KO ) state.

=

: Q _ Normal _ Status ∈ BOOL

inv 1

inv 2 : R _ Normal _ Status ∈ BOOL

inv 3 : Q _ Width ∈ LEADS → N

inv 4 : Q _ Depth ∈ LEADS → N

inv 5 : R _ Depth ∈ LEADS → N

inv 6 : Q _ Wa v e _ State ∈ LEADS → BOOL

inv 7 : Age _ of _ Inf ∈ Age _ of _ Infarct

inv 8 : Mice _ State ∈ Mice _ State 5

inv 9 : Disease _ step 5 ∈ Disease _ Codes _ Step 5