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

under a required time length in the conduction network. A new variable tic is defined
as current clock counter . Invariants ( inv 4- inv 10) are introduced as safety properties,
which define that if the heart state is TRUE then the impulse propagation time and
the impulse propagation velocity be within the standard range of time and velocity
during the impulse conduction throughout the conduction network (see Fig. 8.4 (b)).

inv 1 : CCSpeed _ CCTime _ Flag ∈ BOOL
inv 2 : Cycle _ Length ∈ 500 .. 2000
inv 3

: tic ∈ N

inv 4 : HeartState = TRUE ⇒ CConductionTime(B) ∈ ConductionTime(B)

∧ CConductionSpeed(A → B) ∈ ConductionSpeed(A → B)

inv 5 : HeartState = TRUE ⇒ CConductionTime(C) ∈ ConductionTime(C)

∧ CConductionSpeed(A → C) ∈ ConductionSpeed(A → C)

inv 6 : HeartState = TRUE ⇒ CConductionTime(D) ∈ ConductionTime(D)

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

inv 7 : HeartState = TRUE ⇒ CConductionTime(E) ∈ ConductionTime(E)

∧ CConductionSpeed(D → E) ∈ ConductionSpeed(D → E)

inv 8 : HeartState = TRUE ⇒ CConductionT ime(F ) ∈ ConductionTime(F )

∧ CConductionSpeed(D → F) ∈ ConductionSpeed(D → F)

inv 9 : HeartState = TRUE ⇒ CConductionTime(G) ∈ ConductionTime(G)

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

inv 10 : HeartState = TRUE ⇒ CConductionTime(H ) ∈ ConductionTime(H )

∧ CConductionSpeed(F → H) ∈ ConductionSpeed(F → H)

Events are introduced in this refinement to model the impulse propagation
from SA node towards the Purkinje fibres landmark nodes (G, H) and atria fi-
bres nodes (C). Each event is synchronised through progressive electrical impulse
propagation in the conduction network. We have given formalisation of only one
event HeartConduction_A_B to understand the basic formalisation steps of all other
events. All other events of impulse propagation in the conduction network among
landmark nodes have been modelled in a similar fashion.

EVENT HeartConduction _ A _ B Refines HeartConduction
WHEN
grd1 : ConductionNodeState(A) = TRUE

grd2 : ConductionNodeState(B) = FA L S E

grd3 : CConductionTime(B) ∈ ConductionTime(B)

grd4 : CConductionSpeed(A → B) ∈ ConductionSpeed(A → B)

grd5 : CCSpeed _ CCTime _ Flag = FA L S E

THEN
act1 : ConductionNodeState(B) := TRUE

act2 : CCSpeed _ CCTime _ Flag := TRUE

END

A new event Update_CCSpeed_CCtime is a refinement of the event HeartCon-
duction . This event is used to capture the current electrical impulse propagation