Biomedical Engineering Reference
In-Depth Information
(C, C++, Java and C#). We have developed a tool that supports automatic trans-
lation into several target languages (C, C++, Java and C#) from Event-B formal
specifications. This tool also supports the only subset of Event-B [
2
] formal nota-
tions, but it is much richer than previously developed tools [
9
,
38
]. This chapter dis-
cusses the code generation approach underlying EB2C, EB2C++, EB2J and EB2C#
tools [
17
,
25
]. This is our first step toward in the direction of code generation from
the Event-B formal specification, and our aim is to improve this tool to meet the
industrial requirements.
7.3 A Basic Framework of Translator
A translator tool is developed as a set of plug-ins for the Rodin Tool [
32
], which can
generate the source codes from a formal specification into many programming lan-
guages (C, C++, Java and C#). The translation tool is named as EB2ALL, which is a
group of four kinds of different plug-ins, called EB2C, EB2C++, EB2J and EB2C#.
All these tools have common architecture and a set of protocols for generating a
source code. The translation process consists in transforming the concrete part of
Event-B project into a semantically equivalent text written in any target program-
ming language. This section proposes an architecture for the Event-B translator;
different parts of the translator have been shown in Fig.
7.1
and this architecture sup-
ports translation for several target programming languages like C, C++, Java and C#.
The translator tool is customised for each new target programming language to gen-
erate an efficient code, which can support various types of execution platforms. The
proposed architecture is able to generate a verified code, which also comply with
the behaviour of formal specifications. The translation tool is implemented in the
Eclipse framework as a set of plug-ins for Event-B. The basic description of trans-
lation process is given as follows:
7.3.1 Selection of a Rodin Project
Formal development of a system in Event-B modelling language is provided by an
open and extensible Eclipse-based IDE called Rodin [
32
], which supports system
specifications and verification. A visual interface and a set of plug-ins help to spec-
ify and to prove a system under logico-mathematical theory. A proof manager is
integrated in Rodin tool. Event-B models and all proof-related informations of a
system project are always stored in the Rodin database. The translator tool is im-
plemented as a set of plug-ins under the Eclipse development framework, using the
recommended interfaces to traverse the statically checked internal database, thus
decoupling the tool from the syntax of the Event-B notation by accessing its un-
derlying meaning. The syntax of the mathematical notation, that is, expressions,
predicates, and assignments, are maintained in the form of an abstract syntax tree.
Search WWH ::
Custom Search