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

In our abstract specification, there are four events Pace_ON to start pacing,
Pace_OFF to stop pacing, tic to increment the current clock counter under the time
constraints and Change_Pace_Int to update the pace interval. The events Pace_ON
and Pace_OFF start and stop the pulse stimulating into the heart chamber, respec-
tively. The guards of these events synchronise ON and OFF states of the pacemaker
system under the time constraints. The action part of event Pace_ON sets ON state
of the pacemaker's actuator and assigns the value of current clock counter sp to a
new variable last_sp . Similarly, an action part of the event Pace_OFF sets OFF state
of the pacemaker's actuator and resets the current clock counter variable sp to 1.

EVENT Pace_ON
WHEN
grd1

: Pace _ Actu = OFF

: sp = Pace _ Int

grd2

THEN

act1 : Pace _ Actu := ON

act2 : last _ sp := sp

END

EVENT Pace_OFF
WHEN
grd1 : Pace _ Actu = ON

grd2 : sp = Pace _ Int

THEN

act1 : Pace _ Actu := OFF

act2 : sp := 1

END

EVENT tic
WHEN
grd1 : sp < Pace _ Int

THEN

act1 : sp := sp + 1

END

The pacing and sensing events update a state every millisecond. We model this
increment by the event tic , that increments time in 1 ms. The event tic progressively
increases the current clock counter sp under pre-defined pace interval Pace_Int .The
predicate in guard (grd 1 ) of the event tic represents an upper bound time limit.

EVENT Change_Pace_Int
WHEN
grd1 : Pace _ Int _ flag = TRUE

THEN

act1 : Pace _ Int :∈ URI .. LRI

END