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

TRUE and a set of coordinate positions ( param ) of neighbouring cells is represented
in third guard. Fourth guard states that the current cell position (m, n) is Passive and
last guard represents that the cell transition state Transition is FALSE . If all guards
satisfy, then the transition state of a cell becomes TRUE .

EVENT HeartConduction _ Cellular
ANY p,q, param
WHERE
grd1 : p → q ∈ ConductionPath

grd2 : CCSpeed _ CCTime _ Flag = TRUE

grd3 : param ={{ m, n } , { m + 1 ,n } , { m − 1 ,n } , { m, n + 1 } , { m, n − 1 }}

grd4 :{ m, n }∈ dom(CellS) ∧ CellS( { m, n } ) = PASSIVE

grd5 : NextCellState = CellS( { m, n } )

grd6 : Transition = FA L S E

THEN
act1 : Transition := TRUE

END

The event HeartConduction_Next_UpdateCell is used to calculate the state of
neighbouring cells and to update the position of the current cell (m, n) . The first
guard of this event represents a set of coordinate positions ( param ) of neighbouring
cells and the next guard ( grd2 ) states that the selected neighbouring cells are a set of
cells (dom(NEXT)) . The last guard presents a transition state Transition is TRUE .
Action of this event calculates a set of the next neighbouring cells in act1. The next
action (act2) sets FALSE of a transition state. The last two actions update the value
of the current cell (m, n) to continuously impulse propagating in the heart using the
conduction network.

EVENT HeartConduction _ Next _ UpdateCell
ANY param
WHERE
grd1 : param ={{ m, n } , { m + 1 ,n } , { m − 1 ,n } , { m, n + 1 } , { m, n − 1 }}

grd2 : param ∈ dom(NEXT)

grd3 : Transition = TRUE

THEN
act1 : NextCellState := NEXT(param)

act2 : Transition := FA L S E

act3 : m :∈ { m − 1 ,m,m + 1 }

act4 : n :∈ { n − 1 ,n,n + 1 }

END

Finally, we have completed the formal specifications of the heart modelling. In
the next section, we present model validation of the heart model using Event-B
model checker ProB tool.