Biomedical Engineering Reference
In-Depth Information
Chapter 7
EB2ALL: An Automatic Code Generation Tool
Abstract The most important step in the software-development life-cycle is the
code implementation. This chapter presents a design architecture of an automatic
code generation tool, which can generate code into several programming languages
(C, C++, Java and C#). This tool is a collection of plug-ins, which are used for
translating the Event-B formal specifications into multiple programming languages.
The translation tool is rigorously developed with safety properties preservation. This
is an essential tool, which supports code implementation phase of our proposed
development life-cycle methodology for developing the critical systems.
7.1 Introduction
Formal methods provide a sound mathematical basis for system requirements
descriptions and aim to produce zero-defect software, by controlling the whole
software-development process, from specification to implementation. The capability
of formal and automated verification of safety properties in formal models, before
transformation into code, has added real value to industrial systems, including hard-
ware systems and software systems. Several constraining requirements are existing
particularly in the embedded domain due to limited size of memory for translat-
ing from formal specifications to a given target programming language (C [ 22 , 29 ],
Sections of this chapter are adapted from the original publication: Méry, D., & Singh, N. K.
(2011). Automatic code generation from Event-B models. In Proceedings of the second
symposium on information and communication technology , SoICT'11, Hanoi (pp. 179-188).
New York: ACM.
ACM COPYRIGHT NOTICE. Copyright © 2011 by the Association for Computing Machinery,
Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom
use is granted without fee provided that copies are not made or distributed for profit or
commercial advantage and that copies bear this notice and the full citation on the first page.
Copyrights for components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to
redistribute to lists, requires prior specific permission and/or a fee. Request permissions from
Publications Dept., ACM, Inc., fax +1 (212) 869-0481, or permissions@acm.org .
 
Search WWH ::




Custom Search