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

blanking period ( V_Blank ), and greater than or equal to the fixed atrioventricular
(AV) period ( FixedAV ).

inv 11 : sp < VRP ∧ AV _ Count _ STATE = FA L S E ⇒

PM _ Actuator _ V = OFF ∧

PM _ Sensor _ A = OFF ∧

PM _ Sensor _ V = OFF

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

(sp Pace _ Int

(sp < Pace _ Int

=

∧
AV _ Count >V _ Blank ∧

AV _ Count ≥ FixedAV))

In the abstract specification of VDD operating mode, there are eight events Ac-
tuator_ON_V to start pacing in ventricular, Actuator_OFF_V to stop pacing in ven-
tricular, Sensor_ON_V to start sensing in ventricular, Sensor_OFF_V to stop sens-
ing in ventricular, Sensor_ON_A to star sensing in atrial, Sensor_OFF_A to stop
sensing in atrial, tic to increment the current clock counter sp under the real time
constraints and tic_AV to count the atrioventricular (AV) interval. All these events
are similar to the DDD operating modes, which are already described.

Abstraction of DOO Mode

In DOO operating mode of the two-electrode pacemaker system, the first letter 'D'
represents that the pacemaker paces both atrial and ventricle, second letter 'O' rep-
resents that the pacemaker does not sense the atrial and ventricular chambers and
final letter 'O' represents that there is no any inhibits or triggers modes in both
chambers [ 22 , 35 ].
In this model, we formalise the functional behaviours of the pacemaker system
of DOO operating mode, where all variables, constants and invariants ( inv 1 , inv 2
and inv 5- inv 10) are similar to the previous operating mode; DDD. New invariant
(inv 11 ) states that the pacemaker's actuator of the atrial and ventricular chambers
are OFF, when the clock counter sp is less than the ventriculoatrial (VA) interval,
and the atrial state ( Atria_state ) is FALSE. The next invariant ( inv 12) states that
the pacemaker's actuators of both chambers are OFF, when the clock counter sp
is greater than the atrioventricular (AV) interval, and the atrial state ( Atria_state )
is TRUE. The last invariants ( inv 13 and inv 14) state that, when the pacemaker's
actuator of atrial is ON, then the clock counter sp is greater than or equal to the
ventriculoatrial (VA) interval ( Pace_Int-FixedAV ) and when the pacemaker's actua-
tor of the ventricular is ON, then the clock counter sp is equal to the pace interval
Pace_Int , respectively.