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

for implementation of a system. A selected project always contains some concrete
models, which are refinements of the abstract models. The translation tool automat-
ically filters a set of context and concrete files. If the translation tool is not able
to filter all context and concrete files from the selected project, then immediately
the translation process terminates with an error message, else all the filtered context
and concrete files are passed to the next translation phase for continuing translation
process.

7.3.5 Basic Principles of Code Generation

This phase is the heart of the translation tool. Before this level, all phases are used
as preprocessing steps for obtaining the run-time errors free codes through data re-
finement of the formal specification. Main objective of this phase is to translate
statically checked and proved formal specifications of Event-B model into observa-
tionally equivalent standard programming languages (C, C++, Java and C#). A set
of rules has been generated for producing a source code, which is applicable to all
context and concrete machine modules (i.e. those found to have no further refine-
ment).
The translation tool generates source files as equivalent to the number of concrete
machine files [ 2 ]. Source code generated file has a similar name corresponding to
the concrete machine file, and a file extension generates according to the choice
of a programming language. Source code generated files are saved in the folder
of a particular language (C, C++, Java and C#) in the workspace of the selected
Rodin project. Source code generated file begins with insertion of header comments
containing a time-stamp and the name of selected Rodin project. Some required
header informations are also inserted in the header of the source file according to
the target programming language requirements. For instance, in C++ and C# source
files contain all required header files related to the standard template library (STL)
and Collection class of .NET Framework [ 12 , 37 ], respectively. A Java source file
contains sets definition of the set operations for handling the sets based notations of
Event-B using standard class of Java utilities.
Main cause of failure of this translation tool is unable to parse any predicate. For
example, the current tool is not able to handle relational operator ( ↔ ) and quan-

tifiers ( ). If any predicate expression contains any quantifiers or relational

operators, then the translation process is unable to translate it into a selected pro-
gramming language, and the translation process fails. In case of translation failure,
the tool immediately proceeds with translation of the next module. For avoiding the
errors in the translation process, we have considered mainly two approaches:

∃ and ∀

• To model a system specification using a set of symbols (see Table 7.2 and Ta-

ble 7.3 ), which is supported by the translation tool.

• Transformation of the final concrete models into a supported symbol list (see

Table 7.2 and Table 7.3 ) through the refinement process.