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

to observations of the impulse propagation in the conduction nodes. We define a set
of variables to model the heart and pacemaker models, where four variables ( Con-
ductionNodeState , CConductionTime , CConductionSpeed and HeartState ) are used
to model the heart behaviour, and six variables ( PM _ Actuator _ A , PM _ Actuator _ V ,
PM _ Sensor _ A , PM _ Sensor _ V , Pace _ Int and sp ) are used to express the cardiac
pacemaker behaviour. All these variables are defined using a set of invariants ( inv 1-
inv 7). The cardiac pacemaker variables are introduced for modelling actuators, sen-
sors and timing intervals. A group of invariants ( inv 8, inv 9 and inv 10) presents safety
properties. The invariant inv 8 states that, when the clock counter sp is less than the
VRP and the atrioventricular (AV) counter state AV _ Count _ State is FALSE, then
the pacemaker's actuators and sensors of both chambers are OFF. Similarly, the
next invariants ( inv 9 and inv 10) represent required properties of ON state of the
pacemaker's actuators in both chambers.

inv 1 : ConductionNodeState ∈ ConductionNode → BOOL

inv 2 : CConductionTime ∈ ConductionNode → 0 .. 300

inv 3 : CConductionSpeed ∈ ConductionPath → 0 .. 500

inv 4 BOOL

inv 5 : PM _ Actuator _ A ∈ status ∧ PM _ Actuator _ V ∈ status
inv 6 : PM _ Sensor _ A ∈ status ∧ PM _ Sensor _ V ∈ status
inv 7 : Pace _ Int ∈ URI .. LRI ∧ sp ∈ 1 .. Pace _ Int
inv 8 : sp < VRP ∧ AV _ Count _ STATE = FA L S E ⇒
PM _ Actuator _ V = OFF ∧ PM _ Sensor _ A = OFF ∧
PM _ Sensor _ V = OFF ∧ PM _ Actuator _ A = OFF

: HeartState ∈

: PM _ Actuator _ V = ON ⇒ sp = Pace _ Int ∨ (sp < Pace _ Int ∧
AV _ Count >V _ Blank ∧ AV _ Count ≥ FixedAV)

inv 9

inv 10 : PM _ Actuator _ A = ON ⇒ (sp ≥ Pace _ Int − FixedAV)

The abstract specification of the closed-loop model contains several events re-
lated to the cardiac pacemaker and heart system. There are many events, namely
HeartOK to represent a normal state of the heart, HeartKO to express an abnormal
state of the heart, HeartConduction to trace the current updated value of each land-
mark node in the conduction network, Actuator_ON_V , Actuator_OFF_V , Actua-
tor_ON_A and Actuator_OFF_A to represent ON and OFF states of pacemaker's
actuators for both chambers, Sensor_ON_A , Sensor_OFF_A , Sensor_ON_V , and
Sensor_OFF_V to represent ON and OFF states of pacemaker's sensors for both
chambers, and tic to represent the clock counter.
The event HeartOK expresses desired behaviour of the normal heart, where a set
of guards formulates the required conditions. The first guard ( grd 1) states that all
the landmark nodes must be visited for one cycle during impulse propagation using
conduction network. The second guard specifies that the current impulse propaga-
tion time for each landmark node should be lie in the pre-specified ranges (Chap. 8 ,
Property 1 ). Similarly, the last guard states that the current impulse propagation ve-
locity of each path should lie between pre-defined impulse propagation velocities
(Chap. 8 , Property 2 ). The action predicate ( act 1) denotes the normal state of the
heart, when all these set of guards are satisfied.