Biomedical Engineering Reference
In-Depth Information
LEADS
to
.The
PP_Interval
and
RR_Interval
functions are used to calculate the
PP and RR-intervals.
N
inv
1
:
Sinus
∈
YesNoState
inv
2
:
Heart
_
Rate
∈
1
..
300
inv
3
:
Heart
_
State
∈
HState
inv
4
BOOL
inv
5
:
PP
_
Int
_
equidistant
∈
LEADS
→
BOOL
inv
6
:
P
_
Positive
∈
LEADS
→
BOOL
inv
7
:
PP
_
Interval
∈
LEADS
→ N
inv
8
:
RR
_
Interval
∈
LEADS
→ N
inv
9
:
P
_
Positive(II)
=
FA L S E
⇒
Sinus
=
No
inv
10
:
((
∀
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)
=
:
RR
_
Int
_
equidistant
∈
LEADS
→
PP
_
Interval(l))
P
_
Positive(II)
=
FA L S E )
⇒
Sinus
=
No
inv
11
:
Sinus
=
Ye s
⇒
((
∃
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)
inv
12
:
Heart
_
Rate
∈
60
..
100
∧
Sinus
=
Ye s
Heart
_
State
=
OK
inv
13
:
Heart
_
Rate
∈
1
..
300
\
60
..
100
∧
Sinus
=
Ye s
Heart
_
State
=
KO
inv
14
:
Heart
_
Rate
∈
60
..
100
∧
Sinus
=
No
Heart
_
State
=
KO
A set of invariants (
inv
9-
inv
14) represents the safety properties, and these are
used to verify the required conditions for the ECG interpretation protocol using all
possible behaviour of the heart system and analysis of the signal features, which
are collected from the ECG signals. All these safety properties are designed un-
der the supervision of cardiologist experts to verify the correctness of the formal
model. These invariants in form of safety properties are extracted from the original
protocol.
The invariant (
inv
9) states that if positive visualisation of the P-wave is
FALSE
,
then there is no sinus rhythm. According to the clinical document, lead II is best
for visualisation of the P-waves to determine the presence of sinus rhythm. The
next invariant (
inv
10) is stronger invariant to identify the non-existence of the si-
nus rhythm. This invariant states that if the PP intervals (
PP_Int_equidistant
)or
Search WWH ::
Custom Search