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

Any interruption in the conduction of electrical impulses from the atria to the
ventricles; it can occur at the level of atria, atrioventricular node, bundle of His, or
Purkinje system. It is a type of heart block in which a blocking is at the atrioventric-
ular (AV) junction. It is known as first degree when atrioventricular (AV) conduction
time is prolonged; it is called second degree or partial when some but not all atrial
impulses reach at the ventricle; and it is called third degree or complete when no
atrial impulses at all reach the ventricle, so that the atria and ventricles act indepen-
dently of each other. There are different kinds of AV blocks [ 24 , 30 ]. To model the
AV block, we introduce an event HeartConduction_Block_B , which formalises the
AV block. The conduction node state ConductionNodeState of a landmark node (B)
is FALSE , which represents a condition for the AV block using guard (grd1) and
actions state that the heart state is FALSE and such kind of heart block is known as
the atrioventricular (AV) nodal block.

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

THEN
act1 : HeartState := FA L S E
act2 : HeartBlocks := AV _ nodal _ blocks
END

Infra-Hisian block describes a block of the distal conduction system (node D).
There are different kinds of Infra-Hisian blocks [ 24 , 30 ]. To model Infra-Hisian
block, an event HeartConduction_Block_B_D is used to formalise the desired con-
ditions for a such kind of blocks through landmark nodes (B, D). Guard (grd1) rep-
resents that the landmark node (D) is FALSE , means it is not visited, or the current
impulse propagation time of a node D is not lain within the standard range, or the
current propagation velocity of a pair B

D is not lain within the standard range.
The actions of this event state that the heart state is FALSE, and the heart block is
the Infra-Hisian block.

→

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

(CConductionTime(D) ∈ ConductionTime(D)) ∨

(CConductionSpeed(B → D) ∈ ConductionSpeed(B → D))

THEN
act1 : HeartState := FA L S E

act2 : HeartBlocks := Infra _ Hisian _ blocks

END