Rodin Plug-ins

For developer support, see Rodin Developer Support

Rodin Plug-in Documentation

Modelling

• Records provide structured types for Event-B.
• 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.
• Feature Modelling Tool (prototype) can be used to build feature models for product lines and configure these to generate product line members.
• Decomposition Plug-in User Guide 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.
• Rose (Structured) Editor a model structured editor.
• Flows plug-in allows the addition of control flow to a machine.
• Modularisation Plug-in provides a mechanism for constructing and proving modular developments.
• Theory Plug-in supersedes the Rule-based Prover plug-in, and provides mechanisms for extending the Event-B language as well as its prover.
• Mode/FT Views plug-in brings modelling of modal and fault tolerance features.
• Project Diagram displays the diagram of a Rodin project.

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
• SMT Plug-in provides interface for SMT solvers.
• Relevance Filter Plug-in Uses heuristics to filter hypotheses shown to the prover

Translation

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

Experimental

• Group Refinement changes the set of refinement laws for one refinement step to facilitate a case of atomicity refinement.

Rodin Plug-in Tutorials

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

Tips & Tricks

• Installing external plug-ins manually