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

( PM_Sensor_A ) of atrial is ON, and the clock counter (sp) is less than the ventricu-
loatrial (VA) interval and greater than or equal to the VRP and PVARP. In actions of
this event state that the pacemaker's sensor ( PM_Sensor_A ) of atrial sets OFF and
the atrioventricular (AV) counter state ( AV_Count_STATE )setsTRUE.

EVENT tic
WHEN
grd1 : (sp < VRP)

(sp

≥ VRP ∧ sp < Pace _ Int − FixedAV ∧

PM _ Sensor _ A = ON ∧ PM _ Sensor _ V = ON

THEN
act1 : sp := sp + 1

END

The event (tic) of this abstraction progressively increases the current clock
counter sp under the pre-defined pace interval ( Pace_Int ). This event controls the
time line of pacing and sensing events. A guard ( grd 1) of this event provides the re-
quired conditions to increase the clock counter sp by 1 (ms). The last event ( tic_AV )
of this abstraction progressively counts the atrioventricular (AV) interval and in-
creases the current clock counter sp is represented by actions act 1 and act 2, respec-
tively.

EVENT tic _ AV
WHEN
grd1 : AV _ Count < FixedAV
grd2 : AV _ Count _ STATE = TRUE
grd3 : (sp ≥ VRP ∧ sp ≥ PVARP ∧
sp < Pace _ Int − FixedAV)
(sp

≥ Pace _ Int − FixedAV ∧

sp < Pace _ Int)

THEN
act1 : AV _ Count := AV _ Count + 1

act2 : sp := sp + 1

END

A new event Change_Pace_Int is introduced to update the current value of the
pace interval. This event is defined abstractly, which is used in further refinement
levels to modify the pace interval according to the introduction of different operating
modes like hysteresis and rate modulation. This event represents that when pace
changing flag ( Pace_Int_flag ) is TRUE then the pace interval ( Pace_Int ) can be
chosen from URI to LRI ranges.