B2C plugin: Difference between revisions
imported>Mathieu m New page extract from Current Developments |
imported>Mathieu mNo edit summary |
||
Line 5: | Line 5: | ||
See [http://www.cs.bris.ac.uk/Publications/pub_master.jsp?id=2000990 Paper] for a paper describing B2C in more detail. | See [http://www.cs.bris.ac.uk/Publications/pub_master.jsp?id=2000990 Paper] for a paper describing B2C in more detail. | ||
B2C source code is not currently available for download: contact [[Steve]] directly if it is required. | B2C source code is not currently available for download: contact [[User:Steve|Steve]] directly if it is required. | ||
[[Category:Plugin]] | [[Category:Plugin]] |
Revision as of 12:40, 12 August 2009
The B2C plug-in translates Event-B models to C source code, which may then be compiled using external C development tools. Steve wrote B2C with the specific purpose of translating the MIDAS model, an Event-B implementation of a Virtual Machine instruction set.
B2C supports a sub-set of Event-B that can be easily translated to C form. The user provides a final refinement step that does nothing except restate the model in this translatable form: symbolic constants must be replaced by their literal values, range membership guards are replaced by greater-than and less-than guards, and actions are restated not to use global statements on their left-sides (this because the variable may have been modified by an earlier action, and may not be valid). The manipulations are done within Event-B where they can be checked by the Proof Obligation system, and B2C made as simple as possible to maximise reliability. This re-write process is currently a manual step, but could in principle be done by another plug-in.
See Paper for a paper describing B2C in more detail.
B2C source code is not currently available for download: contact Steve directly if it is required.