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

inv 11 : Pace _ Int _ flag = FA L S E ∧ sp <(Pace _ Int − FixedAV) ∧

Atria _ state = FA L S E ⇒

PM _ Actuator _ V = OFF ∧

PM _ Actuator _ A = OFF

inv 12 : Pace _ Int _ flag = FA L S E ∧ sp >(Pace _ Int − FixedAV) ∧

sp < Pace _ Int ∧

Atria _ state = TRUE ⇒

PM _ Actuator _ A = OFF ∧

PM _ Actuator _ V = OFF
inv 13 : Pace _ Int _ flag = FA L S E ∧ PM _ Actuator _ A = ON ⇒
sp = Pace _ Int − FixedAV
inv 14 : Pace _ Int _ flag = FA L S E ∧ PM _ Actuator _ V = ON ⇒ sp = Pace _ Int

In the abstract specification of DOO operating mode, there are five events
Pace_ON_A to start pacing in atrial, Pace_OFF_A to stop pacing in atrial,
Pace_ON_V to start pacing in ventricular, Pace_OFF_V to stop pacing in ventricu-
lar and tic to increment the current clock counter sp under the real time constraints.
These events are similar to the previously described events but guards, and actions
are changed according to the requirements of the DOO operating mode.

9.8.2 First Refinement: Threshold

The pacemaker control unit delivers stimulation to the heart chambers, on the basis
of measured threshold value under the safety margin. We define two new constants
STA_THR_A and STA_THR_V to hold the standard threshold value in axioms ( axm 1
and axm 2). The threshold constants are different for the atrial and the ventricular
chambers.

axm 1 : STA _ THR _ A ∈ nat 1 ∧ STA _ THR _ A = 75
axm 1 : STA _ THR _ V ∈ nat 1 ∧ STA _ THR _ V = 250

The pacemaker's sensor starts sensing after the refractory period but the pace-
maker's actuator delivers a pacing stimulus, when sensing value is greater than or
equal to the standard threshold constants STA_THR_A or STA_THR_V . In the DOO
operating mode only the pacemaker's actuators paces in the atrial and ventricular
chambers under the automatic pace interval without using any pacemaker's sensors,
so in this mode none of the refinement is given related to the threshold. Table 9.2
shows a list of invariants common in this refinement of other operating modes. First
column shows the group of operating modes and second column shows correspond-
ing common invariants.