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

experts are unable to understand the complex formal specifications, so that we
have proposed a new technique to apply a real-time data set to animate the for-
mal specification and a domain expert can anticipate in the system development.
Another objective is to develop this technique also for requirement traceability
according to the domain experts. For example, through the animation of the for-
mal model using real-time data set, domain experts can help to find the missing
behaviour of a system.

• Automatic source code generation form formal models : Different kinds of code

generation tools are available, and can generate source code into any program-
ming languages but the main constraint is that all those tools are not applicable
to generating the codes from Event-B modelling language. The main objective is
to develop a set of code generation tools, which can support automatic code gen-
eration into several programming languages from Event-B modelling language
and supports in the development life-cycle of a critical system from requirement
analysis to code generation.

• Integration of different approaches : We proposed a new framework to compose

different kinds of formal techniques to model a critical system to overcome the
existing problems. An integration of formal techniques in the development pro-
cess of a critical system provides the modelling concepts with formal semantics
that captures at a high-level of abstraction. Modelling concepts should not be re-
stricted due to apply the verification techniques for checking the correctness of a
system. However, the system specifier should have the freedom to use the intu-
itive modelling concepts neglecting the complexity they impose on verification.
The integration framework should bridge the gap between modelling concepts
and input that is required for verification tools. For instance, integration of theo-
rem prover and model checker can be used for verifying the essential properties.
The compositional reasoning strategies using theorem prover and model check-
ing can reduce the verification effort and to verify the required safety properties.
The model checker helps to discover lots of errors and strengthening the safety
properties through careful cross analysis of the model animation. System specifi-
cations are verified by both the model checker and theorem prover tools to prove
the absence of any error.

References

1. Abdelmoez, W., Nassar, D. M., Shereshevsky, M., Gradetsky, N., Gunnalan, R., Ammar,
H. H., et al. (2004). Error propagation in software architectures. In Proceedings, 10th inter-
national symposium on software metrics (pp. 384-393).
2. Abrial, J.-R. (1996). The B-topic: Assigning programs to meanings . New York: Cambridge
University Press.
3. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.
4. Acuña, S. T., & Juristo, N. (2005). International series in software engineering. Software
process modeling . Berlin: Springer.