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

EVENT SinusNodeFire Refines HeartConduction
WHEN
grd1 :∀ n · n ∈ ConductionNode ⇒ ConductionNodeState(n) = FA L S E

grd2 :∀ n · n ∈ ConductionNode ⇒ CConductionTime(n) = 0

grd3 :∀ n, m · n ∈ ConductionNode ∧ m ∈ ConductionNode ∧

n → m ∈ ConductionPath ⇒ CConductionSpeed(n → m) = 0

THEN
act1 : ConductionNodeState(A) := TRUE

act2 : CConductionTime(A) := 0
END

The next event HeartConductionEnd represents end state of the impulse propa-
gation into Purkinje fibres of ventricles (G, H nodes) and left atria muscle (node C).
This event resets all variables for generating next impulse at the SA node. The ac-
tions of this event reset all conduction node state as FALSE , current impulse prop-
agation time of all landmark nodes reset to 0, current impulse propagation velocity
of all landmark nodes reset to 0, and the heart state sets as FALSE . All these actions
are required before originating the next electrical impulse from the SA node (A).

EVENT HeartConductionEnd Refines HeartConduction
BEGIN
act1 : ConductionNodeState := { A → FA L S E ,B → FA L S E ,

C → FA L S E ,D → FA L S E ,E → FA L S E ,F → FA L S E ,

G → FA L S E ,H → FA L S E }

act2 : CConductionTime := { A → 0 ,B → 0 ,C → 0 ,D → 0 ,

E → 0 ,F → 0 ,G → 0 ,H → 0 }

act3 : CConductionSpeed := { A → B → 0 ,A → C → 0 ,B → D → 0 ,

D → E → 0 ,D → F → 0 ,E → G → 0 ,F → H → 0 }

act4 : HeartState := FA L S E
END

8.5.4 Refinement 2: Impulse Propagation

In the second refinement, we introduce several events as a refinement of the event
HeartConduction to model the impulse propagation into the heart conduction net-
work. New events formalise impulse flow between two landmark nodes separately;
for instance, electrical impulse moves from SA node (A) to AV node (B). This
level of refinement introduces seven events for modelling the whole conduction
path from originating nodes (A) to the ending nodes (C, G, H). A variable CC-
Speed_CCTime_Flag is introduced as a boolean type to capture the value of current
impulse propagation time and current impulse propagation velocity. A new variable
Cycle_Length declares a time interval for the single heart beat, which may change
in every cycle of an electrocardiogram (ECG). This refinement also introduces a
logical clock to synchronise all states of the heart system and checks the heart states