Biomedical Engineering Reference
In-Depth Information
Ta b l e 9 . 2
Common invariants list
Modes
Common invariants
1.
Pace
_
Int
_
flag
=
FA L S E
∧
sp > Pace
_
Int
−
FixedAV
∧
sp < Pace
_
Int
DDD
∧
AV
_
Count
_
STATE
=
TRUE
⇒
VDD
DDI
DVI
PM
_
Sensor
_
V
=
ON
DDD
2.
Pace
_
Int
_
flag
=
FA L S E
∧
sp > VRP
∧
sp < Pace
_
Int
−
FixedAV
⇒
PM
_
Sensor
_
V
=
ON
DVI
DDD
3.
Pace
_
Int
_
flag
=
FA L S E
∧
PM
_
Actuator
_
V
=
ON
⇒
(sp
=
Pace
_
Int)
∨
(sp < Pace
_
Int
∧
AV
_
Count >V
_
Blank
∧
VDD
AV
_
Count
≥
FixedAV)
4.
Pace
_
Int
_
flag
=
FA L S E
∧
sp > Pace
_
Int
−
FixedAV
∧
sp < Pace
_
Int
∧
AV
_
Count
_
STATE
=
TRUE
⇒
PM
_
Sensor
_
A
=
OFF
DDD
5.
Pace
_
Int
_
flag
=
FA L S E
∧
sp > Pace
_
Int
−
FixedAV
∧
sp < Pace
_
Int
∧
AV
_
Count
_
STATE
=
TRUE
⇒
DVI
DDI
PM
_
Actuator
_
A
=
OFF
DVI
6.
Pace
_
Int
_
flag
=
FA L S E
∧
sp > Pace
_
Int
−
FixedAV
∧
sp < Pace
_
Int
∧
AV
_
Count
_
STATE
=
TRUE
⇒
DDI
PM
_
Actuator
_
V
=
OFF
safety properties and real time constraints. The guards of the event (
Thr_Value_V
)
are introduced as to fulfil all the requirements of the sensing intrinsic activities from
the ventricular chamber and actions (
act
1-
act
2) of this event state that the actual
sensed value from a chamber is assigned to the variable
Thr_V
and sets FALSE
state of the variable threshold ventricular state (
Thr_V_State
), respectively.
EVENT Thr
_
Va l u e
_
A
ANY
Thr
_
A
_
val
WHERE
grd1
:
Thr
_
A
_
val
∈ N
grd2
:
PM
_
Sensor
_
A
=
ON
grd3
:
Thr
_
A
_
State
=
TRUE
grd4
:
Thr
_
A<STA
_
THR
_
A
grd5
:
(sp
≥
VRP
∧
sp < Pace
_
Int
−
FixedAV)
THEN
act1
:
Thr
_
A
:=
Thr
_
A
_
val
act2
:
Thr
_
A
_
State
:=
FA L S E
END
In the event
Thr_Value_A
, the guards (
grd
2-
grd
4) state that the pacemaker's
sensor (
PM_Sensor_A
) of atrial chamber is ON; the threshold state (
Thr_A_State
)
Search WWH ::
Custom Search