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