UML-B

From Event-B
Jump to navigationJump to search

Return to Rodin Plug-ins

UML-B provides a 'UML-like' graphical front end for Event-B. It adds support for class-oriented and state machine modelling but also provides visualisation of existing Event-B modelling concepts. UML-B is similar to UML but is a new notation with its own meta-model. UML-B provides tool support, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems which are indicated on the relevant UML-B diagram element.

To start using UML-B, first enter the UML-B 'perspective' using the normal eclipse features (e.g. Window - open perspective - other). You should see a dolphin icon in the top right corner when you are in the UML-B perspective. Create a new UML-B project using the UML-B new project wizard (e.g. File - New - Project - UML-B Project). This will create a new UML-B Project and open a Package Diagram with an empty canvas ready for you to start drawing Machines and Contexts.

Tutorials

A simple tutorial, showing the basics of how to construct a UML-B model using all the diagram types. UML-B Tutorial

An illustration showing how to refine statemachines Refinement of Statemachines

More detail about the various diagram types.

Package Diagram

Context Diagram

Class Diagram

Statemachine Diagram

Animation of Statemachine Diagrams

FAQ

UML-B FAQ

Migrating old UML-B models to the latest format

Upgrading to a later version of UML-B may mean that your existing models no longer match the UML-B metamodel. This will usually occur when the UML-B version number has increased in the first or second number. e.g. 0.4.x to 0.5.x.

Models that were created using UML-B version 0.4.x can be migrated to the current format using the built-in migration tool which is invoked by right clicking on the *.umlb model file in your UML-B project. If the model needs migrating, the tool will delete all the diagrams in the project, reformat the model file and re-create the package diagram from it. You can then re-create your other diagrams using the open diagram buttons in the properties views or pop-up menus.


Models that were created using UML-B versions prior to 0.4.0 can not be migrated to the latest format and should be re-entered.

What's new

In version 1.1.0

TBD: some versions missing here

In version 0.5.8

Known bugs and workarounds

In version 0.5.8

In version 0.4.4