Biomedical Engineering Reference
In-Depth Information
the developed system. This tool is freely available for download.
1
The use of this
tool is exemplified through the generation of C, C++, Java and C# codes from the
specification of a cardiac pacemaker (see Chap.
9
).
A code translation from Event-B was relatively easy, but its subsequent use pre-
sented more problems. The most important challenging task in the code generation
is the code verification. The reason is that the preservation at the code level of the
properties proved at the architectural level is guaranteed only if—the underlying
platform is correct and—correctness of the final system when filling in the stubs
for internal actions into the automatic generated code. Another important challenge
is to support all formal notations of Event-B. Few formal notations are used at the
abstract level for a system development, those symbols are not directly translatable.
We have also faced a specific challenge related to the non-deterministic behaviour
of a system. Most of the formal specifications are non-deterministic, which are not
safe for an automatic code generation. To make a formal specification determin-
istic before code generation and to verify that the system behaviours are correct
according to the developer, and also comply with non-deterministic system speci-
fications, are challenging tasks in this code generation process. Invariants are used
for defining type definition and safety properties of a system. How to use invariants
corresponding to the safety properties for verifying generated codes is also one kind
of challenge.
7.1.1 Structure of This Chapter
This chapter is organised as follows. Section
7.2
presents related work and Sect.
7.3
depicts an architecture of the translator in a form of a
tool chain
and describes vari-
ous parts of the translation process. Section
7.4
presents use of code generator plug-
ins. Section
7.5
discusses limitations of the tool and finally, Sect.
7.6
summarises
the chapter.
7.2 Related Work
Automatic code generation is a standard technique in the area of Software Engi-
neering. Several tools are developed by research community for generating source
code from graphical modelling tool like UML [
20
,
33
,
36
] to any target program-
ming language like C++ or Java. But automatic source code generation from for-
mal specification to a high-level programming language is supported by few formal
1
Download:
http://eb2all.loria.fr/
.
Search WWH ::
Custom Search