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

represents the current clock counter . A variable last_sp represents the last interval
(in ms) between two paces, and a safety property in invariant ( inv 7) states that the
last interval must be between PVARP and pace interval Pace_Int . Another new vari-
able AV_Count_STATE is defined as a boolean type to control the atrioventricular
(AV) interval state and the next variable AV_Count is defined as a natural number to
count the atrioventricular (AV) interval. A variable ( Pace_Int_flag ) is defined as a
boolean type to represent changing state of the pace interval ( Pace_Int ). Invariants
( inv 11, inv 12 and inv 13) represent the safety properties. The invariant inv 11 states
that, when the clock counter sp is less than VRP and atrioventricular (AV) counter
state AV_Count_State is FALSE, then the pacemaker's actuators and sensors of both
chambers are OFF. Similarly, the next invariants ( inv 12 and inv 13) represent the
conditions of ON state of the pacemaker's actuators in the both chambers.

inv 1 : PM _ Actuator _ A ∈ status

inv 2 : PM _ Actuator _ V ∈ status

inv 3 status

inv 4 : PM _ Sensor _ V ∈ status
inv 5 : Pace _ Int ∈ URI .. LRI
inv 6 : sp ∈ 1 .. Pace _ Int
inv 7 : last _ sp ≥ PVARP ∧ last _ sp ≤ Pace _ Int
inv 8 : AV _ Count _ STATE ∈ BOOL
inv 9 : AV _ Count ∈ N
inv 10 : Pace _ Int _ flag ∈ BOOL

: PM _ Sensor _ A ∈

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

PM _ Actuator _ V =

OFF ∧

PM _ Sensor _ A = OFF ∧

PM _ Sensor _ V = OFF ∧

PM _ Actuator _ A = 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)

inv 13 : Pace _ Int _ flag = FA L S E ∧ PM _ Actuator _ A = ON

(sp

≥ Pace _ Int − FixedAV)

In the abstract specification of DDD operating mode, there are ten events Ac-
tuator_ON_A to start pacing in atrial, Actuator_OFF_A to stop pacing in atrial,
Actuator_ON_V to start pacing in ventricular, Actuator_OFF_V to stop pacing in
ventricular, Sensor_ON_V to start sensing in ventricular, Sensor_OFF_V to stop
sensing 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.