Difference between revisions of "UML-B"

From Event-B
Jump to navigationJump to search
imported>Colin
(add tutorial page)
imported>Colin
(30 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 
Return to [[Rodin Plug-ins]]
 
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.  
+
UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. Two versions of UML-B are available.
  
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.
+
The original [[original UML-B|UML-B]] where a complete project is modelled in a diagrammatic project. A separate Event-B project is then generated for verification. This provides a high degree of hiding of the Event-B models although it is still necessary to annotate the diagrams with invariants guards and actions. Beginners who are not familiar with formal modelling may prefer this version.
  
A simple tutorial, showing how to construct a UML-B model.
+
A new version called [[iUML-B]] (i for integrated) embeds diagrams in the Event-B models. This allows the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams. Those more familiar with Event-B may prefer this version.
  
[[Tutorial]]
 
  
More detail about the various diagram types.
+
[[Category:User documentation]]
 
+
[[Category:UML-B]]
[[Package Diagram]]
+
[[Category:Plugin]]
 
 
[[Context Diagram]]
 
 
 
[[Class Diagram]]
 
 
 
[[Statemachine Diagram]]
 

Revision as of 15:00, 10 December 2012

Return to Rodin Plug-ins

UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. Two versions of UML-B are available.

The original UML-B where a complete project is modelled in a diagrammatic project. A separate Event-B project is then generated for verification. This provides a high degree of hiding of the Event-B models although it is still necessary to annotate the diagrams with invariants guards and actions. Beginners who are not familiar with formal modelling may prefer this version.

A new version called iUML-B (i for integrated) embeds diagrams in the Event-B models. This allows the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams. Those more familiar with Event-B may prefer this version.