B2C plugin: Difference between revisions

From Event-B
Jump to navigationJump to search
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.