EB2ALL: An Automatic Code Generation Tool - Using Event-B for Critical Device Software Systems - page 136

the Event-B constructs are not supported except formal notations of Tables 7.2 , 7.3
and 7.4 . This is our first step toward in the direction of code translation, and it is
our ongoing research work. So in future we will provide more and more Event-B
symbols, that will be supported by this translation tool.
7.6 Summary
This chapter has introduced the main principles, rules and implementation solutions
for the translation tools and code verification techniques for generating the target
programming languages (C, C++, Java and C#) code from the Event-B specifica-
tions [ 17 , 24 - 27 ]. The syntax adopted is restrictive, but it already covers most nu-
meric applications, supports powerful static-analysis methods and generates fast and
safe source code in a target programming language. This chapter is to demonstrate
an architecture of the translators and their formal verification. Many algorithms (e.g.
embedded system, distributed system) are subject to further refinement. The trans-
lator provides useful assistance to human programmers by automatically adding
comments, generating code for each process, optimising expressions and partition-
ing event as well as data structures. The translator generates a separate code for all
events of concrete modules. Systematic studies on partitioning methods using a re-
finement structure in target programming languages (C, C++, Java and C#) style is
an interesting area of future research. This approach may be applicable to massively
parallel processing.
The benefits of developing and enhancing the translation tool presented stem
primarily from their increased support for automated translation between the two
components of a formal model and a target programming language [ 17 , 24 - 26 ].
It has been shown that the Event-B models have been transformed into a deter-
ministic model [ 35 ] for automatically translated to the source code using one more
level of data refinement. The final concrete model provides sufficient refinement
for introducing full determinism and use an easily translatable subset of the nota-
tions [ 9 ]. The Rodin tool supports the development of the translation tool under the
Eclipse framework using all required model information via supported interfaces.
The Rodin tool uses an internal database to handle model information, which al-
lows model generation is based on underlying meaning of a model and reduces the
syntax dependency.
References
1. Abrial, J.-R. (1996). The B-book: Assigning programs to meanings . New York: Cambridge
University Press.
2. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.
3. Arnold, K., Gosling, J., & Holmes, D. (2005). The Java programming language (4th ed.).
Reading: Addison-Wesley.