Automatic Generation of C from Event-B

Wright Steve

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)


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 contributionAutomatic Generation of C from Event-B
Original languageEnglish
Title of host publicationWorkshop on Integration of Model-based Formal Methods and Tools
Publication statusPublished - 2009

Bibliographical note

Other page information: -
Conference Proceedings/Title of Journal: Workshop on Integration of Model-based Formal Methods and Tools
Other identifier: 2000990


Dive into the research topics of 'Automatic Generation of C from Event-B'. Together they form a unique fingerprint.

Cite this