Rodin User’s Handbook v.2.8: Rodin

Rodin Handbook

This work is sponsored by the Deploy Project

This work is sponsored by the ADVANCE Project

Creative Commons License

This work is licensed under a Creative Commons Attribution 3.0 Unported License

Rodin

Rodin User’s Handbook v.2.8

2.2.5 Rodin

Rodin (3.1) is the name of the tool platform for Event-B. It allows formal Event-B models to be created with an editor. It generates proof obligations (3.2.7) that can be discharged either automatically or interactively.

Rodin is a modular software and many extensions are available. These include alternative editors, document generators, team support, and extensions (called plugins) some of which include support decomposition and records. An up-to-date list of plugins is maintained in the Rodin Wiki (1.1.2)¹.

Footnotes

These links were valid at the time of the writing of this document: http://wiki.event-b.org/index.php/Rodin_plugins http://wiki.event-b.org/index.php/Installing_external_plugins_manually

Rodin User’s Handbook v.2.8 : Tutorial : Before Getting Started : Rodin