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

EVENT Step11_W_QRS_Tachycardia_Regular Refines Step11 _ W _ QRS _ Tachycardia
WHEN
grd1 : Sinus = No

grd2 : Heart _ State = KO

grd3 : Heart _ Rate ∈ 1 .. 300 \ 60 .. 100

grd4 : Disease _ step 11 = Wide _ QRS _ Tachycardias

grd5 : NW _ QRS _ Tachycardia _ RT _ State = Regular

THEN
act1 : Distease _ step 11_ NW _ QRST :∈ { Ventricular _ Tachycardia,
Supraventricular _ Tachycardia, AV N R T , WPW _ Syndrome _ Orthodromic,
Sinus _ Tachycardia, Atrial _ Tachycardia, AF _ Fixed _ AV _ Conduction,
WPW _ Syndrome _ Antidromic }

END

The event Step11_W_QRS_Tachycardia_Irregular refines Step11_W_QRS_Ta-
chycardia. A list of guards presents that the heart has no sinus rhythm, heart is in
abnormal state, the heart rate is within 1 to 60 or 100 to 300 range, through previous
assessment of the heart has the conditions of wide QRS tachycardia, and the state
of narrow QRS tachycardia is irregular. The action of this event is used to identify
several diseases from the ECG signal that are given in the action.

EVENT Step11_W_QRS_Tachycardia_Irregular Refines Step11 _ W _ QRS _ Tachycardia
WHEN
grd1 : Sinus = No

KO
grd3 : Heart _ Rate ∈ 1 .. 300 \ 60 .. 100
grd4 : Disease _ step 11 = Wide _ QRS _ Tachycardias
grd5 : NW _ QRS _ Tachycardia _ RT _ State = Irregular
THEN
act1 : Distease _ step 11_ NW _ QRST :∈ { AF _ BBB _ WPW _ Synd _ Antidromic,
AF _ Variable _ AV _ Conduction _ BBB _ WPW _ Synd _ Anti, Torsades _ de _ pointes }

grd2 : Heart _ State =

END

Here, we have given required safety properties in form invariants in all refine-
ments. All these properties are derived from the original protocol to verify the cor-
rectness and consistency of the system. These properties are formulated through
logic experts as well as cardiologist experts according to the original protocol. The
main advantage of this technique is that if any property is not holding by the model,
then it helps to find anomalies or to find missing parts of the model such as required
conditions and parameters. A technical report [ 21 ] contains the complete formal
representation of the ECG interpretation protocol.

10.5.12 Proof Statistics

All the proof obligations for all ten refinements are generated and proved using the
Rodin prover [ 29 ]. Table 10.3 shows statistics of the ECG interpretation protocol us-