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

10.5.8 Seventh Refinement: Assess T-wave

This refinement is used to assess the pattern of T-wave changes in the 12-leads
ECG signals. The T-wave changes are usually nonspecific [ 16 ]. The T-wave inver-
sion associated with the ST-segment depression or elevation indicates myocardial
ischemia. A new variable T_Normal_Status represents as a boolean state like TRUE
is for normal state, and FALSE is for abnormal state. A variable Disease_step8 is
introduced in this refinement to assess a set of diseases related to T-wave from the
ECG signals. Invariants ( inv 3- inv 8) represent variables in form of total functions
mapping leads (LEADS) to possible other attributes ( T_State , T_State_B , BOOL , N

and T_State_l_d ).
The function T_Wave_State represents the T-wave states like peaked or flat,
or inverted. Similarly, the function T_Wave_State_B also represents the T-wave
states like upright or inverted, or variable using second method of diagnosis of the
T-wave. The function Abnormal_Shaped_ST and Asy_T_Inversion_strain returns
boolean state of the abnormal ST-shape and asymmetric T-wave inversion strain
pattern, respectively. The Function T_inversion calculates deep the T-wave inver-
sion and the last function T_inversion_l_d represents the localised and diffuse T-
inversion.
From inv 9to inv 15 represent an abnormal state of the heart due to finding some
diseases. All these invariants are similar to the previous level of refinements. This
refinement is very complex, and we have formalised two alternate diagnosis for
the ECG signal. We have introduced many events to assess the T-wave from the
ECG signals and to predict the various diseases related to the T-wave. Events
are T_Wave_Assessment_Peaked_V123456 , T_Wave_Assessment_Peaked_V12 , T_
Wave_Assessment_Peaked_V12_MI , T_Wave_Assessment_Flat , T_Wave_Assess-
ment_Inverted_Yes , T_Wave_Assessment_Inverted_No , T_Wave_Assessment_Inver-
ted_Yes_PM , T_Wave_Assessment_B , T_Wave_Assessment_B_DI , T_Inversion_
Likely_Ischemia , T_Inversion_Diffuse_B . All these events estimate a different kinds
of properties from the T-wave signal for obtaining the correct heart disease. A long
textual representation for analysing the T-wave is given in [ 16 ].

inv 1 : T _ Normal _ Status ∈ BOOL
inv 2 : Disease _ step 8 ∈ Disease _ Codes _ Step 8
inv 3 : T _ Wa v e _ State ∈ LEADS → T _ State
inv 4

: T _ Wa v e _ State _ B ∈ LEADS → T _ State _ B

inv 5 : Abnormal _ Shaped _ ST ∈ LEADS → BOOL

inv 6 : Asy _ T _ Inversion _ strain ∈ LEADS → BOOL

inv 7 : T _ inversion ∈ LEADS → N

inv 8 : T _ inversion _ l _ d ∈ LEADS → T _ State _ l _ d

inv 9 : Sinus = Ye s ∧ Disease _ step 8 = Nonspecific ⇒ Heart _ State = KO

inv 10 : Sinus = Ye s ∧ Disease _ step 8 = Nonspecific _ ST _ T _ changes

Heart _ State

= KO