Abstract
Event-B is a formal modeling method intended to support refinement, an initial system description at a high level of abstraction with detail added in successive understandable steps. The refinement process may be carried to its logical conclusion, specification of all detail needed to define an executable in a high-level language, and automatic generation of source code from the model via a suitable tool. The introduction of the RODIN tool-set allows such extensions to be provided by third-party developers, and translation of Event-B to the C programming language has always been intended. This paper discusses the requirements of such a tool, introduces the B2C extension to RODIN that has been developed to meet these needs, and describes its use on a practical example.
| Translated title of the contribution | Automatic Generation of C from Event-B |
|---|---|
| Original language | English |
| Title of host publication | Workshop on Integration of Model-based Formal Methods and Tools |
| Publisher | http://www.lina.sciences.univ-nantes.fr/apcb/IM_FMT2009/im_fmt2009_proceedings.html |
| Publication status | Published - 2009 |
Bibliographical note
Other page information: -Conference Proceedings/Title of Journal: Workshop on Integration of Model-based Formal Methods and Tools
Other identifier: 2000990