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

The event Step11_N_QRS_Tachycardia_Regular refines Step11_N_QRS_Ta-
chycardia. This event assesses the different kinds of diseases like sinus tachycardia,
AVNRT, etc. A set of guards of this event is used to formalise the required condi-
tions. These conditions present that the heart has no sinus rhythm, the heart is in
abnormal state, the heart rate is within 1 to 60 or 100 to 300 range, through previous
assessment the heart has the conditions of narrow QRS tachycardia, and the state of
narrow QRS tachycardia is regular.

EVENT Step11_N_QRS_Tachycardia_Regular Refines Step11 _ N _ QRS _ Tachycardia
WHEN
grd1 : Sinus = No

grd2 : Heart _ State = KO

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

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

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

THEN
act1 : Distease _ step 11_ NW _ QRST Sinus _ Tachycardia, AV N R T ,

AF _ Fixed _ AV _ Conduction, AT _ Paroxysmal _ NParoxysmal,
WPW _ Syndrome _ OCMT

:∈ {

}

END

The event Step11_N_QRS_Tachycardia_Irregular refines Step11_N_QRS_Ta-
chycardia. The action of this event specifies to identify several diseases using ECG
signal. The guards of this event state 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 the heart has the conditions of narrow QRS tachycardia, and the state of
narrow QRS tachycardia is irregular.

EVENT Step11_N_QRS_Tachycardia_Irregular Refines Step11 _ N _ QRS _ Tachycardia
WHEN
grd1 : Sinus = No

grd2 : Heart _ State = KO

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

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

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

THEN
act1 : Distease _ step 11_ NW _ QRST AF _ Variable _ AV _ Conduction,

Atrail _ Fibrillation, AT _ Variable _ AV _ Block, Multifocal _ Atrial _ Tachycardia

:∈ {

}

END

The event Step11_W_QRS_Tachycardia_Regular refines Step11_W_QRS_Ta-
chycardia. As similar to the last event, the action of this event also specifies to
identify several diseases from the ECG signal. A set of guards presents required
conditions. These required conditions show 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 the heart has the conditions of wide QRS tachycardia, and the
state of narrow QRS tachycardia is regular.