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

cells must be in Active . Similarly, the last property ( axm 10) presents that if a cell at
( x,y )is Passive , then and if all the neighbouring cells in 2D is not Active , then a set
of neighbouring cells must be in Passive .

axm 7 :∀ param · param ∈ P (NeighbouringCells) ∧ CellS( { x,y } ) = ACTIVE
⇒ NEXT(param) = REFRACTORY

:∀ param · param ∈ P (NeighbouringCells) ∧ CellS( { x,y } ) =
REFRACTORY

axm 8

⇒ NEXT(param) = PASSIVE

axm 9 :∀ param · param ∈ P (NeighbouringCells) ∧{ x,y }∈ param ∧

CellS( { x,y } ) = PASSIVE ⇒ ((CellS( { x + 1 ,y } ) = ACTIVE ∨

CellS( { x − 1 ,y } ) = ACTIVE ∨ CellS( { x,y + 1 } ) = ACTIVE ∨

CellS( { x,y − 1 } ) = ACTIVE) ⇒ NEXT(param) = ACTIVE)

axm 10 :∀ param · param ∈ P (NeighbouringCells) ∧{ x,y }∈ param ∧

CellS( { x,y } ) = PASSIVE ⇒ ((CellS( { x + 1 ,y } ) = ACTIVE ∧

CellS( { x − 1 ,y } ) = ACTIVE ∧ CellS( { x,y + 1 } ) = ACTIVE ∧

CellS( { x,y − 1 } ) = ACTIVE ⇒ NEXT(param) = PASSIVE)

Each cell in the heart muscle must have one of the states: Active , Passive or
Refractory . Initially, all cells have Passive state. In this state, a cell is discharged
electrically and has no influences on its neighbouring cells. When electrical impulse
propagates, then the cell would be charged and eventually activated ( Active state).
Now, the cell transmits the electrical impulse to its neighbour cells. The electrical
impulse is propagated to all cells in the heart muscle. After an activation, the cell
would be discharged and enter into the Refractory state in which a cell cannot be
reactivated after a moment, a cell changes its state to the Passive state, in which the
cell awaits next impulse (see Fig. 8.9 ).
To model the dynamic behaviour of the cell automata, we declare four variables
m , n , Transition and NextCellState . Two variables m and n represent current position
of the active cell during impulse propagation. The variable Transition is defined as
boolean to set the transition state TRUE or FALSE to model the behaviour of a tissue.
Last variable NextCellState is used to store the values of next neighbouring positions
after every transition.

inv 1 : m ∈ Z

inv 2 : n ∈ Z

inv 3 : Transition ∈ BOOL

inv 4 : NextCellState ∈ CellStates

To implement the dynamic behaviour of a cell in two-dimensions, we introduce
two events HeartConduction_Cellular to make transition TRUE for the electrical
conduction at the cell level and HeartConduction_Next_UpdateCell to calculate sta-
tus of the neighbouring cells and update the current position (m, n) of the cell. The
event HeartConduction_Cellular is used to set the boolean states of the variable
Transition . The first guard of this event states that any path ( p → q ) is one of the
pair from a set of pairs of the conduction network. The next guard ( grd2 ) states that
the current impulse propagation speed and velocity flag CCSpeed_CCTime_Flag is