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

Sequential Algorithms Generated by EB2Algo