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

greater than or equal to 110 ms, the heart has not the symptoms of WPW syndrome,
Brugada Syndrome, RV Dysplasia, and the possibility of any other disease.

EVENT QRS _ Te s t _ Atypical _ RBBB _ IVCD
ANY dis
WHERE
grd1 : QRS _ Int ≥ 110
grd2 : dis ∈ Disease _ Codes _ Step 3 \{ WPW _ Syndrome,
Brugada _ Syndrome, RV _ Dysplasia, NDS 3 }

THEN
act1 : Disease _ step 3 := IVCD
END

10.5.4 Third Refinement: Assess for ST-segment Elevation or
Depression

This refinement provides a criterion for the ST-segments assessment by introduc-
ing some new variables ( ST_seg_ele and ST_depression ) in form of total functions
mapping leads (LEADS) to in invariants ( inv 2- inv 3). The ST-segment for eleva-

tion and ST depression features are calculated by the ST_seg_ele and ST_depression
functions. Invariants ( inv 4- inv 8) are introduced for representing the safety proper-
ties to confirm an abnormal state of the heart ( KO ) when sinus rhythm is Ye s and a
new disease is found in this refinement.

N

inv 1 : Disease _ step 4 ∈ Disease _ Codes _ Step 4
inv 2 : ST _ seg _ ele ∈ LEADS → N
inv 3 : ST _ depression ∈ LEADS → N
inv 4 : Sinus = Ye s ∧ Disease _ step 4 ∈{ Acute _ inferior _ MI,
Acute _ anterior _ MI ⇒
Heart _ State = KO

: Sinus = Ye s ∧ Disease _ step 4 = STEMI

inv 5

Heart _ State = KO

inv 6 : Sinus = Ye s ∧ Disease _ step 4 ∈{ Troponin, CK _ MB }

Heart _ State

= KO

inv 7 : Sinus = Ye s ∧ Disease _ step 4 = Non _ STEMI

Heart _ State

= KO

inv 8 : Sinus = Ye s ∧ Disease _ step 4 = Ischemia

Heart _ State

= KO

Four new events ST_seg_elevation_YES , ST_seg_elevation_NOTCKMB_Yes ,
ST_seg_elevation_NO_TCKMB_No and Acute_IA_MI are defined to cover diag-
nosis related to the ECG signals. All these events are used to interpret about the