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

Fig. 2.8 The V-model of safety-critical system development using formal methods

it addresses that the formal methods are not well integrated into established critical
system development processes. There are a number of reasons for this. First, the
application of formal methods requires high abstraction and mathematical skills to
write specifications and conduct proofs, and to read and understand formal specifi-
cations and proofs, especially when they are very complex. Second, existing formal
methods do not offer usable and effective methods to use in the well-established
industrial software process. There are lots of effective tools are available, which are
crucial for formal methods application, but existing tools are not able to support a
complete formal software-development process, although tools supporting the use
of formal methods in limited areas are available in [ 26 , 64 , 88 ]. To make formal
methods more practical and acceptable in industry, some substantial changes must
be made.
This topic proposes a development life-cycle and a set of associated techniques
and tools to develop the highly critical systems using formal techniques from re-
quirements analysis to automatic source code generation. In this context, we have
developed a set of techniques and tools related to the Event-B modelling lan-
guage [ 3 ]. Event-B modelling language is only used for verifying the part of a
system. There is not a set of supporting tools, which can be used for the formal
software development. The proposed techniques and tools have filled all missing
tools and provide a rigorous framework for the system development process. The
proposed approach is evaluated through a “Grand Challenge” case study, relative to
the development of the cardiac pacemaker. This case study is related to the medical
domain. Our main objective is to use this case study to show the effectiveness of our
proposed approach and give the evidence that developed techniques and tools are
applicable for any critical systems.
In this topic, we have provided some possible solutions for the emerging prob-
lems in the area of software engineering related to the development of the critical