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

inv 8 : NW _ QRS _ Tachycardia _ RT _ State = Regular ∧

Distease _ step 11_ NW _ QRST Ventricular _ Tachycardia,

Sinus _ Tachycardia, AF _ Fixed _ AV _ Conduction,
Supraventricular _ Tachycardia, Atrial _ Tachycardia,
AV N R T , WPW _ Syndrome _ Antidromic,
WPW _ Syndrome _ Orthodromic

∈{

}

⇒ Heart _ State = KO

inv 9 : NW _ QRS _ Tachycardia _ RT _ State = Irregular ∧
Disteavse _ step 11_ NW _ QRST ∈
{ AF _ Variable _ AV _ Conduction _ BBB _ WPW _ Synd _ Anti,
Torsades _ de _ pointes, AF _ BBB _ WPW _ Synd _ Antidromic }
⇒ Heart _ State = KO

A new variable NW_QRS_Tachycardia_RT_State is defined to express the QRS
tachycardia regular or irregular state using inv 1. A variable Disease_step11 is intro-
duced in this refinement to assess arrhythmias from the ECG signals. All rest of the
invariants ( inv 3- inv 9) represents an abnormal state ( KO ) of the heart after analysing
the arrhythmia and related disease. All invariants have similar kinds of proper-
ties. We introduce five new events to assess tachyarrhythmias from the 12-leads
ECG signals in case of abnormal rhythm. Five events are Rhythm_test_FALSE_
Step11 , Step11_N_QRS_Tachycardia_Regular , Step11_N_QRS_Tachycardia_Irreg-
ular , Step11_W_QRS_Tachycardia_Regular and Step11_W_QRS_Tachycardia_

Irregular .
The event Rhythm_test_FALSE_Step11 is used to identify the heart state, sinus
rhythm, heart rate and several diseases that are not identified through the last assess-
ment process. The guards of this event shows that the equidistant of PP interval is
FALSE or the equidistant of RR interval is FALSE, the RR interval is not equal to
the PP interval in leads II, V1, V2, or the positive state of P-wave is FALSE, and the
heart rate is within the range of 1 to 300 bps.

Rhythm _ test _ FA L S E _ Step11
ANY rate
WHERE
grd1 : ( ∀ l · l ∈{ II,V 1 ,V 2 }⇒ PP _ Int _ equidistant(l) = FA L S E ∨
RR _ Int _ equidistant(l) = FA L S E ∨
RR _ Interval(l) = PP _ Interval(l))
P _ Positive(II) = FA L S E

grd2 : rate ∈ 1 .. 300

THEN
act1 : Sinus := No

act2 : Heart _ Rate := rate

act3 : Heart _ State := KO

act4 : Disease _ step 11 Atrial _ Premature _ Beats, Ventricular _ Premature _ Beats,

Bradyarrhythmias, Narrow _ QRS _ Tachycardias, Wide _ QRS _ Tachycardias,
Nodal _ Premature _ Beats

:∈ {

}

END