Rodin Plug-ins

From Event-B
Revision as of 14:49, 24 September 2010 by imported>Fages
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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.
  • Flows plug-in allows the addition of control flow to a machine.
  • Modularisation Plug-in provides a mechanism for constructing and proving modular developments.
  • SMT Plug-in provides interface for SMT solvers.
Animation
Documentation
  • ReqsManagement offer supports for requirements management.
  • B2Latex allows to typeset an event-B model with latex,
Proof
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

Tips & Tricks