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

Invariant (inv 1 ) states that the pacemaker's sensor ( PM_Sensor_A )ofatrialisON,
when the clock counter sp is greater than the VRP and less than the pace inter-
val ( Pace_Int ) and the atrioventricular (AV) counter state ( AV_Count_STATE )is
FALSE.

inv 1 : Pace _ Int _ flag = FA L S E ∧ sp > VRP ∧ sp < Pace _ Int ∧

AV _ Count _ STATE = FA L S E ⇒

PM _ Sensor _ A = ON

In this refinement, we introduce two new events ( Thr_Value_V and Thr_Value_A )
as similar to the DDD operating mode. These events are synchronised with all other
events of this operating mode under all the safety properties and real time con-
straints. Some guards and actions are added in the old events as defined in the DDD
operating mode.

9.8.3 Second Refinement of DDD Mode: Hysteresis

In the two electrode pacemaker, hysteresis mode is applicable only in the DDD op-
erating mode. Hysteresis is a programmed feature whereby the pacemaker paces at
a faster rate than the sensing rate. For example, pacing at 80 pulses a minute with a
hysteresis rate of 55 means that the pacemaker will be inhibited at all rates down to
55 beats per minute, having been activated at a rate below 55, the pacemaker then
switches on and paces at 80 pulses a minute [ 22 , 39 ]. The application of the hystere-
sis interval provides consistent pacing of the atrial or ventricle, or prevents constant
pacing of the atrial or ventricle. The main purpose of hysteresis is to allow a patient
to have his or her own underlying rhythm as much as possible. Two new variables
( Hyt_Pace_Int_flag , HYT_State ) are introduced to define functional properties of the
hysteresis operating modes. Both variables are defined as a boolean type. The hys-
teresis state HYT_State is used to set the hysteresis functional parameter as TRUE
or FALSE, to apply the hysteresis operating modes.

inv 1 : Hyt _ Pace _ Int _ flag ∈ BOOL
inv 2 : HYT _ State ∈ BOOL

A new event Hyt_Pace_Updating is introduced to implement the functional
properties of the hysteresis operating modes, which is a refinement of the event
Change_Pace_Int . In the hysteresis operating modes, the pacemaker is trying to
maintain own heart rhythm as much as possible. Hence, this event can change
the pacing interval and sets pacing length longer than existing, which changes the
pacing length of the cardiac pacemaker. This event is only used for updating the
pacing interval ( Pace_Int ). Guards of this event state that the pace changing flag
( Pace_Int_flag ) is TRUE, the hysteresis pacing flag ( Hyt_Pace_Int_flag )isTRUE