Biomedical Engineering Reference
In-Depth Information
C++ [
37
], Java [
3
,
21
] and C# [
31
]). To overcome such kinds of problems, first,
a compromise must be found between the expressiveness of the formal implementa-
tion language and the simplicity of the translation process. Another compromise is
also necessary between formal models, which generally favour the readability and
the simplicity of the verification process, over the code efficiency.
The code generation process consists in several stages: formal implementations
are translated into programs in a given programming language using a
tool chain
of a translator, and then these programs are compiled. This approach offers several
advantages: the translation process is as simple as possible, and it can be validated in
an easy way; secondly having a formal specification of a system suggests as a next
step to use it during the testing phase. Software testing tries to check the correctness
of a system with respect to its specification in program states that are chosen for
the test. The simplicity of the translation ensures the traceability between formal
specification and executed code.
This chapter describes a tool translating Event-B specification into any given tar-
get programming language. The structure of Event-B and the nature of tool has
been developed to support for direct-translation from Event-B formal specifica-
tion into any target programming language. We provide a rigorous translation tool
EB2ALL [
17
,
25
] for Event-B specification to target programming language that
can easily be adapted in any domain and gives freedom for developers to adjust at
best their integer representation for overcoming memory-related problems.
The EB2ALL code generator supports automatic generation of C, C++, Java and
C# code from Event-B [
2
] formal specifications. The tool EB2ALL is a collection
of plug-ins, which are named as EB2C, EB2C++, EB2J and EB2C# [
17
,
25
]. All
these tools are used as plug-in features for the Rodin development tool [
32
]. Rodin
development tool is an open and extensible Eclipse-based IDE, which is a platform
for Event-B specification and verification.
We present a multi-phased translation process from the Event-B [
2
] models.
The Event-B models support
set-theoretical
notations that are impossible to di-
rectly translate into any target programming language. The translator automatically
rewrites partially formal notations of Event-B [
2
], that can be easily translatable into
a programming language. Any target programming language source code is then au-
tomatically generated from the model via using an appropriate translation phase of
the tool. The final translated code is applicable to compile into an executable code
using the conventional compilation tools.
A developer can also use translated code to extend the functionality of a sys-
tem by inserting extra code or some new functionalities that are not included in
the Event-B formal development. Some parts of the implementation code are not
supported by the code generator, and a user wants to implement some existing com-
ponents more efficiently are main reasons for inserting extra code into the automat-
ically generated code. Moreover, it offers a flexible way for Event-B designer to
generate C, C++, Java and C# codes. Due to manual intervention in the generated
source code, we propose a code verification technique using the meta-proof and
software model checking tools like BLAST [
10
] for verifying desired behaviours of
Search WWH ::
Custom Search