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

EVENT HeartOK
WHEN
grd1 :∀ i · i ∈ ConductionNode ⇒ ConductionNodeState(i) = TRUE

grd2 :∀ i · i ∈ ConductionNode ⇒

CConductionTime(i) ∈ ConductionTime(i)

grd3 :∀ i, j · i → j ∈ ConductionPath ⇒

CConductionSpeed(i → j) ∈ ConductionSpeed(i → j)

THEN
act1 : HeartState := TRUE
END

In the two electrode pacemaker, we use two sensors and two actuators for cap-
turing the required behaviour of the cardiac pacemaker. In this section, we consider
to show only actuator and sensor events of the ventricle chamber. Moreover, other
events related to the sensor and actuator of the atrial chamber are same. The events
Actuator _ ON _ V and Sensor _ ON _ V excerpt from the abstract model to describe
ON state of the actuator and sensor of the cardiac pacemaker. A set of guards of
both events enables to set ON state of both actuator and sensor, which allows to
pace and sense in the ventricular chamber under the desired conditions using real-
time constraints.

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

∧ sp ≥ URI

THEN
act1 : PM _ Actuator _ V := ON

act2 : last _ sp := sp

END

EVENT Sensor _ ON _ V
WHEN
grd1

: PM _ Sensor _ V = OFF

grd2 : (sp ≥ VRP ∧ sp < Pace _ Int − FixedAV ∧

PM _ Sensor _ A = ON)
(sp

≥ Pace _ Int − FixedAV ∧

AV _ Count _ STATE = TRUE)

grd3 : PM _ Actuator _ A = OFF

THEN
act1 : PM _ Sensor _ V := ON

END