Biomedical Engineering Reference
In-Depth Information
EVENT
Change_Pace_Int
WHEN
grd1
:
Pace
_
Int
_
flag
=
TRUE
THEN
act1
:
Pace
_
Int
:∈
URI .. LRI
END
Abstraction of DVI Mode
In DVI operating mode of the two-electrode pacemaker system, the first letter 'D'
represents that the pacemaker paces both atrial and ventricle; second letter 'V' rep-
resents that the pacemaker only senses the ventricle and final letter 'I' represents
that the ventricular sensing inhibits atrial and ventricular pacing [
22
,
35
].
In this subsection, we formalise the operating mode (DVI) of the two-electrode
pacemaker system. Variables, constants and some invariants (
inv
1
, inv
2 and
inv
4-
inv
10) are similar to the previous operating mode; DDD. More invariants are intro-
duced in this operating mode (DVI) as the safety properties. Invariant
(inv
11
)
states
that, when the clock counter
sp
is less than VRP, then the pacemaker's actuator
of both chambers and pacemaker's sensor of ventricular are OFF. Next two invari-
ants (
inv
12 and
inv
13) state that, when the pacemaker's actuator (
PM_Actuator_A
)
of atrial is ON, then the clock counter
sp
is greater than or equal to the ven-
triculoatrial (VA) interval
Pace_Int-FixedAV
and when the pacemaker's actuator
(
PM_Actuator_V
) of ventricular is ON, then the clock counter
sp
is equal to the
pace interval
Pace_Int
, respectively.
inv
11
:
sp < VRP
⇒
PM
_
Actuator
_
A
=
OFF
∧
PM
_
Actuator
_
V
=
OFF
∧
OFF
inv
12
:
Pace
_
Int
_
flag
=
FA L S E
∧
PM
_
Actuator
_
A
=
ON
⇒
sp
≥
Pace
_
Int
−
FixedAV
inv
13
:
Pace
_
Int
_
flag
=
FA L S E
∧
PM
_
Actuator
_
V
=
ON
⇒
sp
=
Pace
_
Int
PM
_
Sensor
_
V
=
In the abstract specification of DVI operating mode, there are eight events
Ac-
tuator_ON_A
to start pacing in atrial,
Actuator_OFF_A
to stop pacing in atrial,
Actuator_ON_V
to start pacing in ventricular,
Actuator_OFF_V
to stop pacing in
ventricular,
Sensor_ON_V
to start sensing in ventricular,
Sensor_OFF_V
to stop
sensing in ventricular,
tic
to increment the current clock counter
sp
under the real
time constraints and
tic_AV
to count the atrioventricular (AV) interval. All these
events are similar to the DDD operating modes, which are already described. The
guards of events are not exactly similar to the DDD operating modes. The guards
and actions are changed according to the requirements of the DVI operating mode.
Abstraction of DDI Mode
In DDI operating mode of the two-electrode pacemaker system, the first letter 'D'
represents that the pacemaker paces both atrial and ventricle; second letter 'D' repre-
Search WWH ::
Custom Search