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

The event (tic) of this refinement model progressively increases the current clock
counter sp . We have strengthened the guard of this event to properly synchronise
with new introduced threshold events, and the pacing and sensing activities of both
chambers. Some new actions ( act 2 and act 3) are added in this event. The addi-
tional guards and actions handle the behaviour of the events ( Thr_Value_A and
Thr_Value_V ) to sense the intrinsic activities from the atrial and ventricular cham-
bers.

EVENT tic _ AV
WHEN

⊕ grd4 : PM _ Sensor _ V = ON

⊕ grd5 : Thr _ V _ State = FA L S E

⊕ grd6 : Thr _ V<STA _ THR _ V

⊕ grd7 : PM _ Actuator _ V = OFF

⊕ grd8 : PM _ Sensor _ A = OFF

⊕ grd9 : PM _ Actuator _ A = OFF

THEN

⊕ act3 : Thr _ V _ State := TRUE

END

We have introduced some new guards ( grd 4- grd 9) and an action (act 3 ) in the
event ( tic_AV ) of this refinement. New guards provide more specific conditions and
some specific states of the pacemaker's actuators and sensors to count the atrioven-
tricular (AV) interval. An extra action (act 3 ) sets TRUE state of the variable thresh-
old state of ventricular ( Thr_V_State ).

First Refinement of DVI Mode

In this refinement, we introduce two new variables Thr_V and Thr_V_State to hold
the sensing threshold value as similar to the DDD operating mode. We introduce
few more 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 _ Inta ∧

Thr _ V ≥ STA _ THR _ V ∧

Thr _ V _ State = TRUE ⇒

PM _ Sensor _ V = OFF

inv 3 : Pace _ Int _ flag = FA L S E ∧ PM _ Actuator _ A = ON ⇒

sp ≥ Pace _ Int − FixedAV ∧ sp ≥ VRP ∧ sp < Pace _ Int

The first invariant (inv 1 ) states that when the pacemaker's actuator ( PM_Actu-
ator_V ) of ventricular is ON, then the current clock counter sp is equal to the pace
interval Pace_Int . Second invariant (inv 2 ) represents that the pacemaker's sensor
( PM_Sensor_V ) of ventricular is OFF, when the clock counter sp is greater than
the VRP, less than the pace interval ( Pace_Int ), the sensed value ( Thr_V ) is greater