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

equals 857 milliseconds. In the context, the axioms ( axm 3 and axm 4) represent the
upper rate interval (URI) and lower rate interval (LRI). Additionally, we define an
enumerated set status of an electrode as ON or OFF states. Finally, we introduce
some basic initial properties using defined constants of the system by axioms ( axm 6
and axm 7).

axm 1 : LRL ∈ 30 .. 175

axm 2 : URL ∈ 50 .. 175

axm 3 : URI ∈ N ∧ URI = 60000 /URL

1

axm 4 : LRI ∈ N ∧ LRI = 60000 /LRL 1

axm 5 : status ={ ON, OFF }

axm 6 : LRL < URL

axm 7 : URI < LRI

In the one-electrode pacemaker system, the pacemaker delivers a pacing stimu-
lus in the atrial or the ventricular chamber. In our initial model, we formalise the
functional behaviours of the pacemaker system, where a new variable Pace_Actu
is a pacemaker's actuator, represents the presence or absence of pulse. A variable
Pace_Int is an interval between two paces, which is initialised by the system be-
fore starting the pacing process. A variable sp represents the current clock counter
and a variable last_sp represents the last interval (in ms) between two paces. An
invariant (inv 5 ) states that the clock counter sp should be less than or equal to the
lower rate interval (LRI). The next two invariants ( inv 6 , inv 7) introduce two vari-
ables Pace_Int_flag and last_sp . The variable Pace_Int_flag is defined as a boolean
type to represent changing state of the pacing interval ( Pace_Int ), and the variable
last_sp is used to store an interval between last two heart beats or paces. An in-
variant (inv 8 ) represents safety properties: the pacemaker delivers a pacing stimulus
into the heart chamber between upper rate interval (URI) and lower rate interval
(LRI). Similarly, the next invariant (inv 9 ) represents the states of the pacemaker's
actuator under the heart environment as the safety properties, and state that it is
never activated between two heart beats, means pacemaker's actuator is OFF during
pace interval Pace_Int , and pace changing flag is FALSE. The last invariant (inv 10 )
states that if pace changing flag is FALSE and the pacemaker's actuator is ON, then
the current clock counter sp is equal to the pace interval Pace_Int .

: Pace _ Actu ∈ status

inv 1

inv 2 : Pace _ Int ∈ URI .. LRI

inv 3 : sp ∈ 1 .. N

inv 4 : last _ sp ∈ N

inv 5 : sp ≤ LRI

inv 6 : Pace _ Int _ flag ∈ BOOL

inv 7 : last _ sp ∈ N

inv 8 : last _ sp ≥ URI ∧ last _ sp ≤ LRI

inv 9 : Pace _ Int _ flag = FA L S E ∧ sp < Pace _ Int ⇒ Pace _ Actu = OFF

inv 10 : Pace _ Int _ flag = FA L S E ∧ Pace _ Actu = ON ⇒ sp = Pace _ Int