Biomedical Engineering Reference
In-Depth Information
sents that the pacemaker senses both atrial and ventricle and final letter 'I' represents
two conditional meaning that depends on atrial and ventricular sensing; first, atrial
sensing inhibits atrial pacing and does not trigger ventricular pacing and second,
ventricular sensing inhibits ventricular and atrial pacing [
22
,
35
].
We formalise the operating mode DDI of the two-electrode pacemaker system.
Variables, constants and some invariants (
inv
1-
inv
10) are similar to the previous
operating mode; DDD. Invariant (
inv
11) states that, when the clock counter
sp
is
less than the VRP, and the atrioventricular (AV) counter state (
AV_Count_STATE
)is
TRUE, then the pacemaker's actuators and sensors of both chambers are OFF. The
next invariant (
inv
12) represents that, when the pacemaker's actuator of ventricular
is ON, then the clock counter
sp
is equal to the pace interval
Pace_Int
.
inv
11
:
sp < VRP
∧
AV
_
Count
_
STATE
=
FA L S E
⇒
PM
_
Actuator
_
A
=
OFF
∧
PM
_
Actuator
_
V
=
OFF
∧
PM
_
Sensor
_
A
=
OFF
∧
PM
_
Sensor
_
V
=
OFF
inv
12
:
Pace
_
Int
_
flag
=
FA L S E
∧
PM
_
Actuator
_
V
=
ON
⇒
sp
=
Pace
_
Int
In the abstract specification of the DDI operating mode, there are ten events ex-
actly similar to the DDD operating mode, which are already described. The guards
and actions of the events are changed according to the DDI operating mode require-
ments.
Abstraction of VDD Mode
In VDD operating mode of the two-electrode pacemaker system, the first letter 'V'
represents that the pacemaker only paces ventricle; second letter 'D' represents that
the pacemaker senses both atrial and ventricle and final letter 'D' represents two
conditional meanings that depend on atrial and ventricular sensing; first, atrial sens-
ing triggers ventricular pacing and second, ventricular sensing inhibits ventricular
pacing [
22
,
35
].
In this model, we formalise the functional behaviours of the pacemaker system
in VDD operating mode, where all variables, constants and invariants (
inv
2-
inv
10)
are similar to the previously described DDD operating mode. Here, a new invariant
(inv
11
)
states that, when the clock counter
sp
is less than VRP and the atrioventricu-
lar (AV) counter state (
AV_Count_STATE
) is FALSE, then the pacemaker's actuator
(
PM_Actuator_V
) of the ventricular is OFF, and the pacemaker's sensors of both
chambers are OFF. Next invariant (
inv
12) represents that, when the pacemaker's ac-
tuator (
PM_Actuator_V
) of ventricular is ON, then the clock counter
sp
is either
equal to the pace interval
Pace_Int
or the clock counter
sp
is less than the pace in-
terval
Pace_Int
and the atrioventricular (AV) counter (
AV_Count
) is greater than the
Search WWH ::
Custom Search