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

inv 1 : Pace _ Int _ flag = FA L S E ∧ Pace _ Sensor = ON ∧ thr ≥ THR ∧

sp > RF ∧ sp < Pace _ Int ∧

thr _ val _ state = TRUE ⇒

Pace _ Actu = OFF

inv 2 : Pace _ Int _ flag = FA L S E ∧ Pace _ Sensor = ON ∧ thr ≥ THR ∧

sp > RF ∧ sp < Pace _ Int ∧

thr _ val _ state = TRUE ⇒
Pace _ Actu = ON

A new event Thr_value is introduced in all the operating modes (AAI, AAT, VVI
and VVT) that obtains a measured value of the heart activities using the pacemaker's
sensor. The guards of this event state that when the pacemaker's sensor is ON, the
current clock counter sp is within the alert period ( Pace_Int RF ) and the state

of threshold value thr_val_state is TRUE then the sensed value th is assigned to
the threshold variable thr and the state of threshold variable thr_val_state becomes
FALSE.

−

EVENT Thr_value
ANY
th
WHERE
grd1

: Pace _ Sensor = ON

grd2 : sp ≥ RF ∧ sp < Pace _ Int

grd3 : thr _ val _ state = TRUE

grd4 : th ∈ N

THEN

act1 : thr := th

act2 : thr _ val _ state := FA L S E

END

THR in the events
( Pace_OFF_with_Sensor and Pace_ON_with_Sensor ). Moreover, we modify the
guard (grd 1 ) of the event (tic) to synchronise the pacing-sensing events with a new
threshold functional behaviour under the real-time constraints.

In this refinement, we have added a new guard thr ≥

grd1 : (sp < RF ∧ Pace _ Sensor = OFF ∧

Pace _ Actu = OFF)

(sp

≥ RF ∧ sp < Pace _ Int ∧

Pace _ Sensor = ON ∧ Pace _ Actu = OFF ∧

thr < THR ∧ thr _ val _ state = FA L S E )