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

Abstraction of AAT and VVT Modes

The abstract model of AAT and VVT modes are similar to AAI and VVI
modes. We introduce a new event Pace_ON_with_Sensor in place of event
Pace_OFF_with_Sensor in this abstract model. The guards of this event state, when
the pacemaker's actuator is OFF, the pacemaker's sensor is ON and the current clock
counter sp is greater than or equal to the refractory period RF and less than or equal
to pace interval Pace_Int then it stores the value of current clock counter sp to the
variable last_ss , and the pacemaker's actuator sets ON under the sensing process.
During the alert period ( Pace_Int

RF ), the pacemaker delivers a pacing stimulus
whenever it senses an intrinsic activity from the heart chamber.

−

EVENT Pace_ON_with_Sensor
WHEN
grd1 : Pace _ Actu = OFF

grd2 : Pace _ Sensor = ON

grd3 : sp ≥ RF ∧ sp ≤ Pace _ Int

THEN

act1 : Pace _ Actu := ON

act2 : last _ ss := sp

END

9.7.2 First Refinement: Threshold

The pacemaker control unit delivers stimulation to the heart chamber, on the basis of
measured value under the safety margin. We define a new constant THR as THR ∈

N 1 to hold standard threshold value, and we use the constant nominal threshold
value for modelling that is different for the atria and the ventricular chambers.
The pacemaker's sensor starts sensing after the refractory period RF but pace-
maker's actuator delivers a pacing stimulus when sensing value is greater than or
equal to the standard threshold constant THR . 3 The first invariant is introduced in
operating modes (AAI, VVI) that states that the pacemaker's actuator is OFF, when
the pace changing flag ( Pace_Int_flag ) is FALSE, the pacemaker's sensor is ON; an
obtained sensor value is greater than or equal to the standard threshold value, the
current clock counter sp is within the alert period ( Pace_Int

RF ) and the state of
threshold thr_val_state is TRUE. Similarly, the second invariant is introduced in the
operating modes (AAT, VVT) that states that the pacemaker's actuator is ON, when
the pace changing flag ( Pace_Int_flag ) is FALSE, the pacemaker's sensor is ON,
an obtained sensor value is greater than or equal to the standard threshold constant
THR , the current clock counter sp within the alert period ( Pace_Int

−

− RF ), and the

state of threshold thr_val_state is TRUE.

3 Standard threshold constant values of atria and ventricular chambers are different.