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

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

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

(CConductionTime(F ) / ∈ ConductionTime(F )) ∨

(CConductionTime(H ) / ∈ ConductionTime(H )) ∨

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

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

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

8.5.6 Refinement 4: Getting a Cellular Model

This last refinement introduces cellular level modelling into the heart model. The
cellular level modelling is used to model the electrical impulse propagation at the
cell level. The formalisation uses cellular automata theory to model the micro-
structure based cell model. To formalise the cellular automata, we introduce math-
ematical properties (see Definitions 2 and 3 ) in a context model. In a biological
system, each cell has one of the following states: Active , Passive or Refractory .
To define cell states, we declare an enumerated set CellStates . We have assumed
grid of cells in a square format. Due to square geometry of the cells, we define a
constant NeighbouringCells to represent a set of coordinated positions of the neigh-
bouring cells. A new function NEXT is used to define neighbouring cell's state. This
function maps from the power-set of NeighbouringCells to a cell's state CellStates .
A new function CellS is defined as to map from NeighbouringCells to CellStates .
This function maps various states like Active , Passive and Refractory to the neigh-
bouring cells.

: partition(CellStates, { PASSIVE } , { ACTIVE } , { REFRACTORY } )

axm 1

axm 2 : x ∈ Z

axm 3 : y ∈ Z

axm 4 : NeighbouringCells =

{{ x,y } , { x + 1 ,y } , { x − 1 ,y } , { x,y + 1 } , { x,y − 1 }}

axm 5 : NEXT ∈ P (NeighbouringCells) → CellStates

axm 6 : CellS ∈ NeighbouringCells → CellStates

A set of properties ( axm 7- axm 10) is introduced to specify the desired behaviour
of the biological cell automata in two-dimensions. All these properties implement
the state transition of a cell and formalise the transitions automaton (see Fig. 8.9 ).
The first property ( axm 1) states that if the neighbouring cells are in Active state,
then the NEXT state of the cell must be Refractory . The second property ( axm 8)
represents that if the neighbouring cells are in the Refractory state, then the NEXT
state of the cell must be Passive . Third property ( axm 9) states that if a cell at ( x,y )is
Passive , then if all the neighbouring cells in 2D is Active , then a set of neighbouring