Biomedical Engineering Reference
In-Depth Information
Fig. 10.1
A typical one-cycle ECG tracing
parameters are: PR-interval, P-wave, QRS duration, Q-wave, R-wave, ST-segment,
T-wave, Axis, QT-interval. All these parameters have several characteristics that are
used for diagnosis.
10.5 Formal Development of the ECG Interpretation
10.5.1 Abstract Model: Assessing Rhythm and Rate
We begin by defining the Event-B context. The context uses sets and constants
to define axioms and theorems. Axioms and theorems represent the logical the-
ory of a system. The logical theory is the static properties and properties of the
target system. In the context, we define constants
LEADS
,
HState
and
Ye s N o -
State
that are related to an enumerated set of the ECG leads, normal and abnor-
mal states of the heart and yes-no states, respectively. These constants are ex-
tracted from the ECG interpretation protocol [
9
,
10
,
13
,
16
]. The standard 12-
lead electrocardiogram is a representation of the heart's electrical activity recorded
from electrodes on the body surface. A set of leads is represented as
LEADS
=
{
I,II, III, aVR, aVL, aVF,V
1
,V
2
,V
3
,V
4
,V
5
,V
6
}
. Normal and abnormal states
of the heart are represented by
HState
={
OK, KO
}
and yes-no states are represented
by
YesNoState
={
Ye s, No
}
. Figure
10.2
depicts an incremental formal development
Search WWH ::
Custom Search