B2C plugin

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.