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

EVENT Rhythm _ test _ TRUE
ANY rate
WHERE
grd1 : ( ∃ l · l ∈{ II,V 1 ,V 2 }∧ PP _ Int _ equidistant(l) = TRUE ∧

RR _ Int _ equidistant(l) = TRUE ∧

RR _ Interval(l) = PP _ Interval(l)) ∧

P _ Positive(II) = TRUE

grd2 : rate ∈ 60 .. 100
THEN
act1 : Sinus := Ye s
act2 : Heart _ Rate := rate
act3 : Heart _ State := OK
END

EVENT Rhythm _ test _ FA L S E
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

: Heart _ Rate := rate

act2

act3 : Heart _ State := KO

END

EVENT Rhythm _ test _ TRUE _ abRate
ANY rate
WHERE
grd1 : ( ∃ l · l ∈{ II,V 1 ,V 2 }∧ PP _ Int _ equidistant(l) = TRUE ∧
RR _ Int _ equidistant(l) = TRUE ∧
RR _ Interval(l) = PP _ Interval(l)) ∧
P _ Positive(II) = TRUE

grd2 : rate ∈ 1 .. 300 \ 60 .. 100

THEN
act1 : Sinus := Ye s

act2 : Heart _ Rate := rate

act3 : Heart _ State := KO

END

In the abstract model, we have seen that the sinus rhythm and heart rate are intro-
duced for the ECG interpretation in a single atomic step. This provides for a clear
and simple specification of the essence of the basic ECG interpretation protocol and
predicts the heart state ( OK or KO ). However, in the real protocol, the ECG interpre-
tation and heart state prediction is not atomic. Instead, the ECG interpretation and