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

Fig. 8.9 State transition of

a cell

becomes discharged and enters the Refractory state within which the cell cannot be
reactivated. After a time, the cell changes its state to the Passive statetoawaitthe
next impulse.

8.5 Functional Formal Modelling of the Heart

To formalise the heart model, we have used the Event-B modelling language [ 1 , 38 ],
although the proposed idea can be formalised using any kind of formal-methods
tool such as Z, ASM, TLA + or VDM. Event-B modelling language supports the
refinement approach [ 4 ] that helps to verify the correctness of the system in an
incremental way.
The heart model development is expressed in an abstract and general way. The
initial model formalises the system requirements and environmental assumptions,
whereas the subsequent models introduce design decisions for the resulting system.
Following summary informations present global view of the heart system develop-
ment, which help to understand the whole modelling approach.
Initial model : This is an observation model, which specifies a heart state in the form
of true and false , where true represents a normal rhythm and false represents an
abnormal rhythm of the heart.
Refinement 1 : This is a conduction model of the heart, which specifies beginning
of the impulse propagation at SA node and ending of the impulse propagation at
Purkinje fibres in both left and right ventricles.
Refinement 2 : This model specifies impulse propagation between landmark nodes
with global clock counter to model a real-time system to satisfy the temporal
properties of impulse propagation.
Refinement 3 : This is a perturbation model of the heart, which specifies perturbation
in the heart conduction system and helps to discover exact block into the heart
conduction system.
Refinement 4 : This is a simulation model of the heart, which introduces impulse
propagation at the cellular level using cellular automata.

8.5.1 The Context and Initial Model

Event-B models are described in terms of two major components: context and ma-
chine . The context contains the static part of the model, whereas the machine con-