EB2Py
The EB2Py plugin generates python codes from verified Event-B models.
Prerequisites
The EB2Py 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 EB2Py
EB2Py is available for Windows, Mac, and Linux computers. The EB2Py tool can be downloaded here: EB2Py
Installing
To get started with the EB2Py 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
EB2Py has been used to generate python codes for several complex critical systems like cardiac pacemaker, cardiac resynchronization therapy or multisite pacing device, insulin infusion pump, automatic rover protection system, etc.
Cardiac Resynchronization Therapy (CRT) Example