Biomedical Engineering Reference
In-Depth Information
techniques like Classic B [
2
] and Vienna Development Method (VDM) [
11
,
28
].
The VDM [
11
,
28
] is a set of techniques and tools based on formal specifica-
tion languageāthe VDM Specification Language (VDM-SL). Extended version of
VDM tool (VDM++) supports modelling of object-oriented and concurrent systems.
VDM tools attract both industrial and academic people in the area of formal based
development. VDM tools provide features for analysing models, testing and prov-
ing properties of models, and generating program codes from the validated VDM
models.
A tool vMAGIC [
30
] is based on Java library that is used for automatic code gen-
eration for VHDL. According to the paper, this tool is very usable and reliable, but
a lot of useful features are not implemented yet. This tool is continued under devel-
opment for adding new features that will be able to do semantic operations as well.
In the area of model-driven software engineering, a tool PADL2Java [
13
] has been
developed that translates PADL models into Java code. PADL is a process algebraic
architectural description language equipped with a rigorous semantics and transfor-
mation rules into multi-threaded object-oriented software, which is employed in the
verification tool TwoTowers [
8
]. This tool provides the code generation approach
and code synthesising techniques.
SPARK [
5
] is a formally-defined programming language based on a restricted
subset of the Ada language [
23
], intended to be secure and to support the develop-
ment of high integrity software related to the critical systems. It describes desired
behaviour of the system components and to verify the expected runtime require-
ments. Main features of this language are to support strong static typing, static and
run-time checking, object-oriented programming, exception handling, parallel tasks,
etc. Static verification tools allow to check the absence of general run-time errors
like numerical overflow or division by zero and that the user-specified properties
hold. The proofs will either be generated automatically or developed with the pro-
grammer's assistance for the more complex cases.
From Classic-B [
1
] notation to 'C', C++ and ADA language translation tool has
been developed by D. Bert et al. [
9
]. This paper presents a methodology for trans-
lating a formal specification based-on Classic-B modelling language. Before gen-
erating the 'C' code, the specification model must be restated into an intermediate
language 'B0'. The intermediate language 'B0' is restricted set of Classic-B formal
notations. This tool is particularly designed for generating a 'C' code for an embed-
ded system. This tool is not able to handle any complex expressions in the specifica-
tion, so, this tool has very limited use. In the area of code generation from Event-B
model to 'C' code is proposed by Stephen Wright [
38
]. But this tool is particularly
designed for MIDAS [
38
] project. This tool also supports a subset of Event-B for-
mal notations with a very simple expression form. This tool is no more usable for
any Event-B formal specification. Edmunds et al. [
18
,
19
] have presented a way
for generating code, for concurrent programs, from Event-B specifications. Authors
aim to integrate their code generation approach with existing Event-B methodology
and tools.
As for as we know that there is no any mature translation tool existing, which
can translate directly from Event-B formal specification into any target language
Search WWH ::
Custom Search