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

EVENT Actuator _ ON _ V
WHEN
grd1 : PM _ Actuator _ V = OFF

grd2 : (sp = Pace _ Int)

(sp < Pace _ Int

∧ AV _ Count >V _ Blank ∧

AV _ Count ≥ FixedAV)

grd3 : sp ≥ VRP ∧ sp ≥ PVARP

THEN
act1 : PM _ Actuator _ V := ON
act2 : last _ sp := sp
END

The events Actuator_ON_V and Actuator_OFF_V are used to start and stop the
pacemaker's actuator in the ventricular chamber under the real-time constraints.
In the event ( Actuator_ON_V ), the first guard states that the pacemaker's actuator
( PM_Actuator_V ) of the ventricular is OFF, the next guard (grd 2 ) states that the cur-
rent clock counter sp is either equal to the pace interval Pace_Int or the clock counter
sp is less than the pace interval Pace_Int , the atrioventricular counter is greater than
the blanking period V_Blank and the atrioventricular counter is greater than the fixed
atrioventricular interval FixedAV . The last guard (grd 3 ) states that the clock counter
sp is greater than or equal to the VRP and PVARP. The actions of this event show
that when all guards are true then the pacemaker's actuator ( PM_Actuator_V )of
ventricular sets ON and assigns a value of the clock counter sp into other variable
last_sp .

EVENT Actuator _ OFF _ V
WHEN
grd1 : PM _ Actuator _ V = ON

grd2 : (sp = Pace _ Int)

(sp < Pace _ Int

∧ AV _ Count >V _ Blank ∧

AV _ Count ≥ FixedAV)

grd3 : AV _ Count _ STATE = TRUE

grd4 : PM _ Actuator _ A = OFF

grd5 : PM _ Sensor _ A = OFF

THEN
act1 : PM _ Actuator _ V := OFF

0
act3 : AV _ Count _ STATE := FA L S E
act4 : PM _ Sensor _ V := OFF
act5 : sp := 1
END

act2 : AV _ Count :=

First two guards of the event ( Actuator_OFF_V ) state that the pacemaker's ac-
tuator ( PM_Actuator_V ) of ventricular is ON, and the clock counter (sp) is equal
to the pace interval ( Pace_Int ), or less than the pace interval ( Pace_Int ), the atri-
oventricular (AV) counter ( AV_Count ) is greater than the blanking period ( V_Blank )