Difference between revisions of "UML-B"
imported>Colin (New page: 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 co...) |
imported>Colin |
||
(33 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
− | + | 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 [[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 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. |
− | |||
− | [[ | + | [[Category:User documentation]] |
+ | [[Category:UML-B]] | ||
+ | [[Category:Plugin]] |
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.