Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.
The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
We support models in Event-B for a limited subset. The support is realized as a plugin for Rodin 3.3 or higher.
Installation of the plugin
After you started Rodin select Help -> Install New Software…
Insert https://momut.org/wp-content/uploads/event-b in the Work with: Field.
Select the checkbox and press Next.
Press Next.
Read the Licence carefully, then tick Accept and press Finish.
If a Warning appears, press Install anyway on the left.
After the Installation, Rodin must be restarted.
Using the plugin
The Installation was successful when you can see this tab when you right click on a machine file. To Convert the machine to a OOAS file, press Convert…
You need to select an Output Directory.
(Optional) It is possible to choose a test markup csv file. The csv file describes which events are observable and which ones are controllable.
The dialog also offers the option to run the test-case generation directly on a MoMuT Server. This service is not yet publicly available. Please contact us if you are interested.
After you selected the Output folder, you can click Finish.
You should find the *.ooas file in the previously defined folder.
Using the OOAS file
If you want to test the generated OOAS file, download MoMuT and unzip it. Create an OUTPUT folder and enter:java -jar MoMuTUml_4.0.0.jar -mode tcg -steps 300 OOAS/m4_buttons.ooas OUTPUT
for a test case generation
Or:java -jar MoMuTUml_4.0.0.jar -animate OOAS/m4_buttons.ooas OUTPUT
for a console-based animator of the model.