EB2Algo
The EB2Algo plugin generates sequential algorithms from verified Event-B models.
Prerequisites
The EB2Algo tool is written entirely in Java and built on the Eclipse platform using RODIN source code. It is a plugin for the RODIN development tool, so all you need is a properly installed RODIN.
Download EB2Algo
EB2Algo is available for Windows, Mac, and Linux computers. The EB2Algo tool can be downloaded here: EB2Algo
Installing
To get started with the EB2Algo tool, first download the plug-in as a zip file. To install the plug-in, place it in the plugins directory of the RODIN installation. The plugin will not appear until your workspace has been restarted (Restart RODIN).
Evaluation
EB2Algo has been used to generate sequential algorithms for a total of 25 Rodin projects developed J. R. Abrial and D. Cansell.
Archive of 25 Rodin Projects can be accessed from ANR-EBRP project site.
Dutch Flag Example
Event-B project: Dutch Flag
Generated sequential algorithm: Dutch Flag
Sequential Algorithms Generated by EB2Algo
Abrial Examples: JRAExamples
Cansell Exmaples: CansellExamples