Critical System Development Methodology - Using Event-B for Critical Device Software Systems - page 65

4.3 Overview of the Methodology
In recent years, the critical systems have grown more complex and providing cer-
tification assurance, is a common crucial issue for certification bodies [ 23 , 28 , 35 ,
36 , 43 ]. Under consideration of all kinds of requirements of certification bodies,
we propose a novel development methodology that addresses the issue of certi-
fication for all kinds of critical systems, which is an extension of the waterfall
model [ 3 , 6 , 63 , 67 ] for developing a critical software system using formal methods
and standard safety assessment approaches [ 47 ] from requirement analysis to final
system implementation.
This development process is based on refinement approach, where we have intro-
duced some new steps for designing the complete system using formal verification,
validation and real-time animation [ 53 ]. All these steps are not only used in the de-
velopment life-cycle, but they are also validating the correctness of a system, and
all these processes are moreover verified by safety assessment techniques, which
comply with software standards. Basic architecture of the methodology is depicted
in Fig. 4.1 , which may be used in the development process of a critical system [ 55 ].
In this development methodology, we have considered mainly two types of devel-
opment: static development and dynamic development. Each phase includes captur-
ing of requirements. The static development refers to the straight-forward process,
which produces a program, and dynamic development refers to the activities that
improve the quality of the program using refinement approach until it satisfies user
requirements. In order to reach the required safety level and gain reliability, we
have used standard safety assessment approaches in the development process, and
also ensuring traceability between the different stages of the system development in
order to reduce the validation effort. Different phases of the methodology are shown
in Fig. 4.1 which is used in the development process of a critical system. Seven main
phases of proposed methodology are described as follows:
4.3.1 Informal Requirements
The first activity of static development captures user requirements as completely
as possible, which is an initial phase of the proposed methodology, presents an in-
formal requirements of a given system. Software requirements specifications are
widely used in a restricted form of natural language. Natural language is convenient
because it allows non-technical users to understand systems requirements. On the
other hand, the lack of precise semantics increases the possibility of errors being
introduced due to interpretation mistakes and inherent ambiguities. Under or over
specification are also common problems when using a natural language. Software
requirements specification consists of the categorisation and structuring of the in-
formal requirements fragment described in the requirements document to produce
categorised requirements fragments. The main objective of informal requirements is
to provide a precise, yet understandable description of the safety-relevant behaviour