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

7.3.8 Compiling and Running the Code
Once automatic translation and verification of the Event-B model is completed, all
additional requirements are added, an execution environment must be provided and
compiled by a suitable target programming language compiler. This final step of
the translation tool is to produce generated files for compiling on-target platform
(Windows, Linux and Mac).
7.4 How to Use Code Generator Plug-ins
To get started using the code generator you should require an Event-B specification.
The code generator requires that all files of the Event-B specifications are syntax
checked in order to generate correct code. Before generating a source code, it has
to ensure that specification is proved and one more level of refinement has been
done to make a deterministic model. The code generator tool box will automatically
type checked for data types and generates a code according to the programming
language.
Figure 7.5 represents a screen shot of translator tools (EB2C, EB2C++, EB2J and
EB2C#) 2 under the Rodin environment [ 17 , 24 - 26 ]. All these tools are developed
as a set of plug-ins under the Eclipse framework. After installation of the EB2C,
EB2C++, EB2J and EB2C# plug-ins, menus Translator/EB2C, /EB2C++, /EB2J,
/EB2C# and tool buttons on the toolbar, will appear. To generate a source code in
any target language of any formal model, a user can click on any menu (EB2C,
EB2C++, EB2J and EB2C#) or a tool button, then a dialog box will appear (see
Fig. 7.5 ). This dialog box presents a list of active projects. A user can select any
project for generating a source code. These tools generate a target language code
for all concrete models of the selected project and also generate a log file for the
code generating process.
7.4.1 Assessment of the Translation Tool
Assessment of this translation tool is given through the code generation of verified
formal specifications of a cardiac pacemaker (see Chap. 9 ). We have illustrated the
use of EB2C, EB2C++, EB2J and EB2C# tools [ 17 , 24 - 26 ] by means of the auto-
matic generation of C, C++, Java and C# codes for the cardiac pacemaker. These
codes are automatically generated in C, C++, Java and C# codes from the verified
specification in less than five seconds. To find a detail process of code generation
from formal specifications in [ 27 ].
2 Download: http://eb2all.loria.fr/ .