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

systems. We have captured some missing things in the existing tools related to the
formal methods that are essentially required for developing any highly critical sys-
tem. We have proposed a set of new techniques and tools to model the critical sys-
tems, which cover some set of weakness in the existing approach. No one method or
tool can serve all purposes. From the experience, we have learnt what kinds of tech-
niques can have the most impact. To be attractive to the practitioners, methods and
tools should satisfy the following criteria, where we realise that some of these crite-
ria are ideals, but it is still good to strive for them and some of the basic criteria [ 23 ]
are required in the development of methods and tools:

1. Methods and tools should provide significant benefits for developing a system,
when starting to use them.
2. Helps for writing clear, consistent and unambiguous specifications.
3. It should be possible to amortise the cost of a method or tool over many uses.
For example, it should be possible to derive benefits from a single specification
at several points in a programme life-cycle: in design analysis, code optimisa-
tion, test case generation, and regression testing. Moreover existing developed
specification can be reused for other development processes.
4. Methods and tools should work in conjunction with each other and with com-
mon programming languages and techniques. Developers should not have to
“buy into” a new methodology completely to begin receiving benefits. The use
of tools for formal methods should be integrated with that of tools for traditional
software development, for example, compilers and simulators.
5. Notations and tools should provide a starting point for writing formal specifi-
cations for developers who would not otherwise write them. The knowledge of
formal specifications needed to start realising benefits should be minimal.
6. Methods and tools should support evolutionary system development by allowing
partial specification and analysis of selected aspects of a system.

A new method or tool should have precise strengths and weakness, limitations,
modelling assumptions and to support for ease integration with other technique's,
etc. Clear selection criteria helps the potential users to decide what method or tool
is most appropriate for the particular problem. Given that no formal methods tech-
nique is likely to be suitable for describing and analysing every aspect of a complex
system, a practical approach is to use different methods in combination. Based on
the results of the survey performed in this chapter it is possible to identify the con-
tribution that this topic makes. We have given our motivation for developing new
techniques and tools as follows:

• Development life-cycle methodology : This is the heart of the topic, which presents

a methodology for the critical system development from requirement analysis to
automatic code generation with standard safety assessment approach. It is an ex-
tension of the waterfall model [ 8 , 108 ] with some rigorous approaches to produce
a reliable critical system. This methodology combines the refinement approach
with a verification tool, model checker tool, real-time animator and finally gener-
ates the source code using automatic code generation tools. This kind of approach