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

We introduce extra events Pace_OFF_with_Sensor and Sense_ON in the abstrac-
tion model of the AAI and VVI modes. The guards of event Pace_OFF_with_Sensor
state that, when the pacemaker's actuator is OFF, pacemaker's sensor is ON and
current clock counter sp is greater than or equal to the refractory period RF then it
stores the value of the current clock counter sp to the new variable last_ss , resets
the current clock counter sp to 1 and sets OFF state of the pacemaker's sensor. It
means that during the alert period ( Pace_Int RF ), the pacemaker inhibits a pacing

stimulus and resets the current clock counter whenever it senses an intrinsic activity
from the heart chamber.

−

EVENT Pace_OFF_with_Sensor
WHEN
grd1 : Pace _ Actu = OFF

grd2 : Pace _ Sensor = ON

grd3 : sp ≥ RF

THEN

act1 : last _ ss := sp

act2 1

act3 : Pace _ Sensor := OFF

: sp :=

END

The event Sense_ON starts the sensing process of pacemaker's sensor when the
sensor is OFF and the current clock counter sp is greater than or equal to the re-
fractory period RF and lower than the pace interval Pace_Int . We have added some
new guards in the events Pace_OFF of AAI and VVI operating modes to control
the sensor under the current clock counter sp .

EVENT Sense_ON
WHEN
grd1 : Pace _ Sensor = OFF
grd2 : sp ≥ RF
grd3 : sp < Pace _ Int

THEN

: Pace _ Actu := ON

act1

END

We have added more real time constraints in the guard (grd 1 ) of the event tic
in all operating modes that control the progressive increment of the current clock
counter sp as follows:

grd1 : (sp < RF ∧ Pace _ Sensor = OFF ∧

Pace _ Actu = OFF)

(sp

≥ RF ∧ sp < Pace _ Int ∧

Pace _ Sensor = ON ∧ Pace _ Actu = OFF)