Formal Logic Based Heart-Model - Using Event-B for Critical Device Software Systems - page 157

EVENT HeartKO
WHEN
grd1 :∃ i · i ∈ ConductionNode ∧ ConductionNodeState(i) = FA L S E )

(

∃ j · j ∈ ConductionNode ∧

CConductionTime(j) / ∈ ConductionTime(j))

(

∃ m, n · m → n ∈ ConductionPath ∧ CConductionSpeed(m → n)

∈ ConductionSpeed(m → n))

THEN
act1 : HeartState := FA L S E
END

The event HeartConduction formalises the heart behaviour in an abstract manner
by updating the values for impulse propagation time, impulse propagation velocity
and visited state of the landmark nodes non-deterministically. This event is used to
model more concrete behaviour of the heart system at the next level of refinement.

EVENT HeartConduction
BEGIN
act1 : ConductionNodeState :∈ ConductionNode → BOOL

act2 : CConductionTime :∈ ConductionNode → 0 .. 300

act3 : CConductionSpeed :∈ ConductionPath → 0 .. 500

act4 : HeartState :∈ BOOL

END

8.5.3 Refinement 1: Introducing Steps in the Propagation

In the abstract model, we have presented that the impulse propagation time, veloc-
ity and visited landmark nodes have been updated in an atomic step when electrical
impulse fire from the sinus (SA) node and moves towards the Purkinje fibres into
ventricles (G, H nodes) and in the left atria muscle fibres (C node). Our main ob-
jective is to model step by step impulse propagation through all landmark nodes,
where the electrical impulse must pass through a number of intermediate land-
mark nodes before reaching to the terminal nodes (C, G, H). This refinement is
a very simple refinement, where we introduce two extra events SinusNodeFire and
HeartConductionEnd as the refinement of the event HeartConduction . The event
SinusNodeFire models the behaviour of a sinoatrial (SA) node, which originates
electrical impulse for traversing throughout the heart system using the conduction
network (see Fig. 8.4 ). The guards of this event state that if all landmark nodes are
unvisited (means FALSE state) and current impulse propagation time of each node
is 0, and impulse propagation velocity of each path is 0, then the conduction node
state ConductionNodeState of a landmark node A (SA node) sets TRUE and current
impulse propagation time of SA node (A) sets to 0.