Difference between revisions of "UML-B"
imported>Colin (→FAQ) |
imported>Colin |
||
(21 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 | + | 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:User documentation]] | ||
[[Category:UML-B]] | [[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.