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

of atrial chamber is TRUE and the sensed value ( Thr_A ) from the atrial chamber is
less than the standard threshold ( STA_THR_A ) of atrial chamber. The last guard of
this event states that the clock counter sp is greater than or equal to the VRP and
less than the ventriculoatrial (VA) interval. Actions ( act 1- act 2) of this event state
that the actual sensed value ( Thr_A_val ) of atrial chamber is assigned to a variable
( Thr_A ) and sets FALSE state of a variable threshold atrial state ( Thr_A_State ).

EVENT Actuator _ OFF _ V
⊕ : Thr _ A :=

act6 0

⊕ : Thr _ V :=

act7 0

⊕ act8 : Thr _ A _ State := FA L S E

⊕ act9 : Thr _ V _ State := FA L S E

EVENT Sensor _ ON _ A
⊕ act2 : Thr _ A _ State := TRUE

EVENT Sensor _ OFF _ A
⊕ grd3 : Thr _ A ≥ STA _ THR _ A

EVENT Sensor _ OFF _ V
⊕ grd6 : Thr _ V ≥ STA _ THR _ V

⊕ act7 : Thr _ A := 0

⊕ act8 : Thr _ V := 0

⊕ act9 : Thr _ A _ State := FA L S E

⊕ act10 : Thr _ V _ State := FA L S E

We have introduced some new actions and guards in events ( Actuator_OFF_V ,
Sensor_ON_A , Sensor_OFF_A , and Sensor_OFF_V ) to synchronise the sensing
activities using events ( Thr_Value_V and Thr_Value_A ) under the real time con-
straints. These events are already defined in the abstract model. 4

EVENT tic
WHEN
grd1 : (sp < VRP ∧ AV _ Count _ STATE = FA L S E
(sp ≥ VRP ∧ sp < Pace _ Int − FixedAV ∧
PM _ Sensor _ V = ON ∧
PM _ Sensor _ A = ON ∧
Thr _ V _ State = FA L S E ∧
Thr _ V<STA _ THR _ V))

grd2 : AV _ Count _ STATE = FA L S E

THEN

⊕ act2 : Thr _ A _ State := TRUE

⊕ act3 : Thr _ V _ State := TRUE

END

4

⊕ : To add a new guard and an action in the model. : To remove a new guard and an action in
the model.