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

10.5.11 Tenth Refinement: Assess Arrhythmias

This is the final refinement of the ECG interpretation of the system. In this refine-
ment, we introduce different kinds of tachyarrhythmias and give the protocols for
assessment as follows:

• Narrow complex tachycardia: Gives the differential diagnosis of narrow QRS

complex tachycardia.

• Wide complex tachycardia: Gives the differential diagnosis of wide QRS complex

tachycardia.

inv 1 : NW _ QRS _ Tachycardia _ RT _ State ∈
NW _ QRS _ Tachycardia _ RI

: Disease _ step 11 ∈ Misc _ Disease _ Codes _ Step 11

inv 2

inv 3 : Sinus = Ye s ∧ Disease _ step 11 ∈

{ Ventricular _ Premature _ Beats, Nodal _ Premature _ Beats,

Bradyarrhythmias, Narrow _ QRS _ Tachycardias,
Wide _ QRS _ Tachycardias, Atrial _ Premature _ Beats }

⇒ Heart _ State = KO

inv 4 : Sinus = Ye s ∧ Distease _ step 11_ NW _ QRST ∈

{ Sinus _ Tachycardia, Supraventricular _ Tachycardia,

WPW _ Syndrome _ Orthodromic, Torsades _ de _ pointes,
Atrial _ Tachycardia, AF _ Fixed _ AV _ Conduction, AV N R T ,
Ventricular _ Tachycardia, WPW _ Syndrome _ Antidromic,
AF _ Variable _ AV _ Conduction _ BBB _ WPW _ Synd _ Anti,
AF _ BBB _ WPW _ Synd _ Antidromic }

⇒ Heart _ State = KO

inv 5 : Sinus = Ye s ∧ Distease _ step 11_ NW _ QRST ∈

{ AF _ Variable _ AV _ Conduction, AV N R T ,

AT _ Paroxysmal _ NParoxysmal, AT _ Variable _ AV _ Block,
AF _ Fixed _ AV _ Conduction, WPW _ Syndrome _ OCMT,
Sinus _ Tachycardia, Multifocal _ Atrial _ Tachycardia,
Atrail _ Fibrillation }
⇒ Heart _ State = KO

inv 6 : NW _ QRS _ Tachycardia _ RT _ State = Regular ∧
Distease _ step 11_ NW _ QRST ∈{ Sinus _ Tachycardia,
WPW _ Syndrome _ OCMT, AF _ Fixed _ AV _ Conduction,
AV N R T , AT _ Paroxysmal _ NParoxysmal }
⇒ Heart _ State = KO

inv 7 : NW _ QRS _ Tachycardia _ RT _ State = Irregular ∧

Distease _ step 11_ NW _ QRST Atrail _ Fibrillation,

AT _ Variable _ AV _ Block, AF _ Variable _ AV _ Conduction,
Multifocal _ Atrial _ Tachycardia

∈{

}

⇒ Heart _ State = KO