Background - Using Event-B for Critical Device Software Systems - page 39

is very useful to develop the whole system using formal techniques and to verify
the complex properties of a system and to discover the potential problems.

• Environment modelling : The most challenging problem is an environment mod-

elling, for instance, to validate and verify the correct behaviour of a system model,
requires an interactive formal model (an environment formal model). For exam-
ple, a cardiac pacemaker or cardioverter-defibrillators (ICDs) formal models re-
quire a heart model to verify the correctness of the developed system. No any
tools and techniques are available to provide an environment modelling to verify
the developed system model. The main objective is to use formal approach for
modelling the medical device and biological environment to verify the correct-
ness of the medical systems.
To model a biological environment (the heart) for a cardiac pacemaker or
cardioverter-defibrillators (ICDs), we propose a method for modelling a math-
ematical heart model based on logico-mathematical theory. The heart model is
based on electrocardiography analysis [ 7 , 41 , 69 ], which models the heart sys-
tem at cellular level [ 106 ]. The main key feature of this heart model is the
representation of all the possible morphological states of the electrocardiogram
(ECG) [ 6 , 7 ]. The morphological states represent the normal and abnormal states
of the electrocardiogram (ECG). The morphological representation generates any
kind of heart model (patients model or normal heart model using ECG). This
model can observe a failure of impulse generation and failure of impulse propa-
gation.

• Refinement chart : There are several ways to handle the design complexity of a

system. Refinement technique is the most common approach, which facilitates to
build a system gradually. We have discovered a very simple way to present the
whole system based on operational behavioural using a refinement chart. The re-
finement chart is a graphical representation of a complex system using layering
approach, where functional blocks are divided into multiple simpler blocks in a
new refinement level, without changing the original behaviour of the system. The
final goal to use this refinement chart is to obtain a specification that is detailed
enough to be effectively implemented, but also to correctly describe the require-
ments of a system. The purpose of the refinement chart is to provide an easily
manageable representation for different refinements of a system. The refinement
chart offers a clear view of assistance in “system” integration. This approach also
gives a clear view about the system assembling based on the operating modes and
different kinds of features. For example, if a developer does not want to provide
any particular feature in any system, then using the refinement chart, it is possible
to find that removable feature easily and not to include in the final development
system. However, it can also provide the information that, which other parts will
be affect-able, when we remove the particular operating modes.

• Real-time animator : Lots of formal methods based animator are available for dif-

ferent formal languages. But all kinds of animator use only toy-data sets. No any
tool is available for real-time data testing without generating the source code of
the system. We have provided an architecture to use a set of real-time data for
animation using formal specification. Here, we have discovered that the medical