Rodin Plug-ins: Difference between revisions

Revision as of 10:27, 1 February 2011

For developer support, see Rodin Developer Support

Records provide structured types for Event-B.
UML-B provides a 'UML-like' graphical front end for Event-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.

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,

Theory Plug-in provides capabilities to extend the Event-B mathematical language and the Rodin proving infrastructure.
Proof Purger offers to delete unused proofs.
Proof Skeleton View displays the skeleton of existing proofs.
SMT Plug-in provides interface for SMT solvers.
Relevance Filter Plug-in Uses heuristics to filter hypotheses shown to the prover

Multitasking code generation supports generation of multi-tasking Ada code from Event-B.
B2C translates Event-B models to C source code, which may then be compiled using external C development tools.

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

@@ Line 5: / Line 5: @@
 === Modelling ===
 * [[Records_Extension|Records]] provide structured types for Event-B.
-* [[UML-B]] provides a 'UML-like' graphical front end for Event-B,B,
+* [[UML-B]] provides a 'UML-like' graphical front end for Event-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 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))