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

time CConductionTime and the current electrical impulse propagation speed CC-
conductionSpeed during a progressive conduction flow into the heart system in the
conduction network.

EVENT Update _ CCSpeed _ CCtime Refines HeartConduction
ANY i, j, CSpeed, CTime
WHERE
grd1 : i ∈ ConductionNode

grd2 : j ∈ ConductionNode

grd3 : i → j ∈ ConductionPath

grd4 : CSpeed ∈ 0 .. 500

grd5 : CTime ∈ 0 .. 300

grd6 : CCSpeed _ CCTime _ Flag = TRUE

grd7 : HeartState = FA L S E

grd8 : tic = CTime

THEN
act1 : CConductionTime(j) := CTime

act2 : CConductionSpeed(i → j) := CSpeed

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

END

The electrical impulse propagates at every millisecond. But the impulse propaga-
tion time and velocity are different for each landmark node. The progressive incre-
ment of the independent logical clock is modelled through event tic , that increments
timein1ms.Theevent Clock_Counter progressively increases the current clock
counter tic under pre-defined cycle length Cycle _ Length . The predicate in guard
( grd1 ) of event Clock_Counter represents an upper bound time limit. The current
clock counter tic is reset to 0 by the event HeartConductionEnd . An extra guard
is added in the event HeartConductionEnd as tic

Cycle _ Length to reset all the
parametric values of the heart system for starting a fresh new impulse propagation
cycle.

=

EVENT Clock _ Counter
WHEN
grd1 : tic < Cycle _ Length

THEN
act1 : tic := tic + 1

END

We have defined the event Clock_Counter as a type of Convergent and the sys-
tem variant is defined as Cycle _ length

tic , which generates the convergence proof
obligations to verify that the time is progressing with the electrical impulse propa-
gation. It means that the electrical impulse is propagating in the conduction network
corresponding to the clock counter.

−