B2C plugin: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Mathieu
m New page extract from Current Developments
 
imported>Steve
Link to source code at Deploy website added.
 
(One intermediate revision by one other user not shown)
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.
Full B2C source code is available as part of the MIDAS archive at [http://deploy-eprints.ecs.soton.ac.uk/84/ Deploy]. [[User:Steve|Steve]] may also contacted directly for discussion and support.


[[Category:Plugin]]
[[Category:Plugin]]

Latest revision as of 20:27, 8 February 2010

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.

Full B2C source code is available as part of the MIDAS archive at Deploy. Steve may also contacted directly for discussion and support.