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