Rodin Plug-ins

For developer support, see Rodin Developer Support

Rodin Plug-in Documentation

Modelling

• UML-B provides a 'UML-like' graphical front end for Event-B,B,
• Parallel Composition using Event-B allows the composition of machines through events for Event-B.
• Feature Composition Plug-in allows the composition of Event-B features(machines|contexts) and helps the user in resolving conflicts before composition.
• Decomposition Plug-in allows the decomposition of Event-B machines/contexts (shared variables (A-style) and shared events decomposition (B-style))
• Refactoring Framework allows the refactoring of elements that are part of file (and also on related files).
• Pattern allows the reusing of existing models within a development in order to save the modelling and proving effort.
• Text Editor allows editing the source code of a model.
• Flows plug-in allows the addition of control flow to a machine.
• Modularisation Plug-in provides a mechanism for constructing and proving modular developments.

Animation

• ProB is an animator and model checker for the B-Method,
• AnimB is an animator for the Rodin platform,
• UML-B - Statemachine Animation provides an animation (using Pro-B) of UML-B State-machines,

Documentation

• ReqsManagement offer supports for requirements management.
• B2Latex allows to typeset an event-B model with latex,

Proof

• Proof Purger offers to delete unused proofs.
• Proof Skeleton View displays the skeleton of existing proofs.
• Rule-based Prover Plug-in

Translation

• B2C translates Event-B models to C source code, which may then be compiled using external C development tools.

Rodin Plug-in Tutorials

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

Tips & Tricks

• Installing external plug-ins manually