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

The bundle of His divides into a right bundle branch and a left bundle branch,
which lead to the heart's lower chambers (the ventricles). For the left and right
ventricles to contract at the same time, an electrical impulse must travel down the
right and left bundle branches at the same speed. If there is a block in one of these
branches, the electrical impulse must travel to the ventricle by a different route.
When this happens, the rate and rhythm of your heartbeat are not affected, but the
impulse is slowed. Even ventricle will still contract, but it will take longer because of
the slowed impulse. This slowed impulse causes one ventricle to contract a fraction
of a second slower than the other [ 24 , 30 ]. The medical terms for bundle branch
block are derived from which branch is affected. If the block is located in the right
bundle branch, it is called Right bundle branch block. If the block is located in the
left bundle branch, it is called Left bundle branch block.
To model the Right bundle branch block, we introduce an event in a similar
fashion like past events. A new event HeartConduction_Block_D_E_G formalises
the Right bundle branch; guard of this event states that the landmark nodes (E or G)
are not visited means FALSE state, or the current impulse propagation time of E and
G nodes are not lain within the standard ranges, or the current impulse propagation
velocity of the pairs D

→ →

G are not lain within the standard range; then
the actions of this event state that the heart state is FALSE and the heart block is the
Right bundle branch block.

E and E

EVENT HeartConduction _ Block _ D _ E _ G Refines HeartKO
WHEN
grd1 : (ConductionNodeState(E) = FA L S E ) ∨

(ConductionNodeState(G) = FA L S E ) ∨

(CConductionTime(E) / ∈ ConductionTime(E)) ∨

(CConductionTime(C) / ∈ ConductionTime(C)) ∨

(CConductionSpeed(D → E) / ∈ ConductionSpeed(D → E)) ∨

(CConductionSpeed(E → G) / ∈ ConductionSpeed(E → G))

THEN
act1 : HeartState := FA L S E

act2 : HeartBlocks := RBBB _ blocks

END

To model the Left bundle branch block, we introduce an event like Right bundle
branch event. This new event HeartConduction_Block_D_F_H formalises the Left
bundle branch. Guard of this event states that the landmark nodes (F or H) are not
visited means FALSE state, or the current impulse propagation time of F and H
nodes are not lain within the standard range, or the current impulse propagation
velocity of the pairs D H are not lain within the standard range.

Then the actions of this event state that the heart state is FALSE, and the heart block
is the Left bundle branch block.

→ F and F →