Rodin Plug-ins

For developer support, see Rodin Developer Support

Rodin Plug-in Documentation

• UML-B provides a 'UML-like' graphical front end for Event-B,
• B2Latex allows to typeset an event-B model with latex,
• ProB is an animator and model checker for the B-Method,
• AnimB is an animator for the Rodin platform,
• ReqsManagement offer supports for requirements management.
• Parallel Composition using Event-B allows the composition of machines through events for Event-B.
• Refactoring Framework allows the refactoring of elements that are part of file (and also on related files).
• Proof Purger offers to delete unused proofs.
• Proof Skeleton View displays the skeleton of existing proofs.
• Feature Composition Plug-in allows the composition of Event-B features(machines|contexts) and helps the user in resolving conflicts before composition.

Rodin Plug-in Tutorials

• UML-B Tutorial
• Requirements Tutorial,
• Flash Animation Tutorial with animB and Adobe CS3.

Tips & Tricks

• Installing external plug-ins manually