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

In our previous models of the cardiac pacemaker and the heart system, we use
the tic event to model a clock, separately. However, in the closed-loop model, we
use a single event tic to specify a common clock for both cardiac pacemaker and
heart environment models. The event (tic) models the clock behaviour, where time
is progressively increased using the current clock counter sp . This event controls
the time line of pacing and sensing events. A guard ( grd 1) of this event provides the
required conditions to increase the clock counter sp by1(ms).

EVENT tic
WHEN
grd1 : (sp < VRP)

(sp

≥ VRP ∧ sp < Pace _ Int − FixedAV ∧

PM _ Sensor _ A = ON ∧ PM _ Sensor _ V = ON

THEN
act1 : sp := sp + 1
END

9.10.2 Chain of Refinements

So far, we have described our abstract model of the closed-loop model [ 50 ]. Each
refinement level is used to introduce a new set of functional properties for modelling
normal and abnormal behaviours of the heart and pacemaker. Rather than presenting
the chain of refinement stages in great detail, we will just give an overview of the
remaining refinement stages, sufficient to explain the rationale of each refinement
stage in formalising the system.

Refinement 1: Introducing threshold in cardiac pacemaker and impulse propaga-
tion in the heart system . This refinement step is known as a conduction model, which
introduces the impulse propagation in the conduction network of the heart. The im-
pulse propagation originates from the SA node and pass through all the landmark
nodes and reached at the Purkinje fibres of the ventricles. Formalising the conduc-
tion model, we introduce a set of events, which supports piecewise development of
the impulse propagation. The electrical impulse passes through several intermediate
landmark nodes and finally sink to the terminal nodes (C, G, H). The conduction
model uses the clock counter to model the real-time system to satisfy the required
temporal properties for the impulse propagation. A set of new events simulates the
desired behaviour of the impulse propagation into the heart conduction network,
where each new refined event formalises impulse flow between two landmark nodes;
for instance, the electrical impulse moves from SA node (A) to AV node (B).
In the refinement of the closed-loop system, the cardiac pacemaker development
introduces sensors behaviour for both atrial and ventricular chambers, which models
to capture the sensing activities using some standard threshold values. The threshold