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

[ 53 ]. This phase is applied for rigorous testing of the formal model under domain
expert's reviews. Real-time animation shows the behaviours of the system using real
environment in early phase of the development without generating the source code.
Such kind of techniques are very useful when domain experts are also involved in
the system development [ 53 ]. Formal models are used to animate with the real-time
animator [ 53 ], in order to verify on given scenarios according to the real system.
This model animator is not part of the validation process, as this can be required to
qualify as software requirements, but it helps us to check models against reality and
to internally verify their suitability.
In Fig. 4.1 , this step also presents feedback loop into the formalisation phase
to correct an unexpected error of the system. The feedback approach is allowed to
modify the formal model and verify it using any theorem prover tool and finally
validate it using a model checker tool. In this phase of the formal development,
most of the errors are discovered by the domain experts. The verification, validation
and real-time animation processes are applied to continue until not find the correct
formal model according to the domain experts.
Most simulation researchers agree that animation may be dangerous too, as the
analysts and users tend to concentrate on a very short simulation runs so the prob-
lems that occur only in long runs go unnoticed. Of course, good analysts, who are
aware of this danger, will continue run long enough to create a rare event until not
cover all possible events, which is then displayed to the users. Each phase of the
methodology is supported by a specific tool.
4.3.6 Code Generation
The final stage of static development is an implementation, in which a program
is constructed to realise the design. This involves the realisation of the major ex-
ecutable components, definition of the concrete data structures, and an implemen-
tation of any minor auxiliary structures or functions that may be assumed in the
design. It is important to verify the design and program against the requirements
specification and design through rigorous reviews. Automatic code generation [ 7 ]is
well known process to get highly verified codes according to the requirements anal-
ysis. It is an important part of the software-development process, for implementing
the final system. There are several reasons for using an automatic code generator
in the development of the safety-critical systems. Automatic code generation tech-
niques produce the executable specification with fewer numbers of implementation
errors than a human programmer. Manual translation process can be error prone and
time consuming. An iterative process for successive changes in the specification and
manual code translation can introduce errors by various ways. The consistency be-
tween the specification and code translation is often lost. This is not the case when
an automatic code generator is used to obtain a source code from the verified speci-
fication. The code generator translates a proved formal model directly into a desired
programming language. It ensures that the generated code is always consistent with