The Cardiac Pacemaker - Using Event-B for Critical Device Software Systems - page 211

than or equal to the standard threshold ( STA_THR_V ) value of ventricular chamber
and the threshold ventricular state ( Thr_V_State ) is TRUE. The last invariant ( inv 3)
states that, when the pacemaker's actuator of atrial chambers is ON, then the current
clock counter sp is within the ventriculoatrial (VA) interval ( Pace_Int FixedAV )

and greater than or equal to the VRP and less than the pace interval Pace_Int .
In this refinement, we introduce a new event ( Thr_Value_V ) for sensing the in-
trinsic activities of the ventricular chamber, and it is similar to the first refinement
of DDD operating mode. This event is synchronised with all other events of this
operating mode under all the safety properties and real time constraints. The other
events tic and tic_AV are also modified in this refinement to synchronise sensors and
actuators behaviour.

−

First Refinement of DDI Mode

We introduce some new variables ( Thr_A , Thr_V , Thr_A_State and Thr_V_State )as
similar to the refinement of the DDD operating modes. In this refinement, we intro-
duce some new invariants except some defined common invariants (see Table 9.2 ).

inv 1 : Pace _ Int _ flag = FA L S E ∧ PM _ Actuator _ V = ON ⇒ sp = Pace _ Int
inv 2 : Pace _ Int _ flag = FA L S E ∧ sp > VRP ∧ sp < Pace _ Int − FixedAV ⇒
PM _ Actuator _ A = OFF
inv 3 : Pace _ Int _ flag = FA L S E ∧ PM _ Actuator _ A = ON ⇒
sp = Pace _ Int − FixedAV

The first invariant states that 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 .
The next invariant (inv 2 ) states that the pacemaker's actuator ( PM_Actuator_A )of
atrial is OFF, when the current clock counter sp is greater than the VRP and less
than the ventriculoatrial (VA) interval. The last invariant states that, when the pace-
maker's actuator of atrial chamber is ON, then the current clock counter sp is equal
to ventriculoatrial (VA) interval ( Pace_Int FixedAV ).

In this refinement, we introduce two new events ( Thr_Value_V and Thr_Value_A )
for sensing the intrinsic activities from the ventricular and atrial chambers that are
similar to the first refinement of DDD operating mode. These events are synchro-
nised with all other events of this operating mode under all the safety properties and
real time constraints. Other events are also modified in this refinement to synchro-
nise the sensors and actuators behaviour as similar to the DDD operating mode.

−

First Refinement of VDD Mode

We introduce four new variables ( Thr_A , Thr_V , Thr_A_State and Thr_V_State )as
similar to the refinement of the DDD operating mode. In this refinement, we in-
troduce an extra invariant except some defined common invariants (see Table 9.2 ).