imported>Colin |
imported>Colin |
Line 6: |
Line 6: |
| | | |
| 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. | | 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. |
− |
| |
− |
| |
− |
| |
− | 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.
| |
− |
| |
− | ==Lectures==
| |
− | These slides give a quick introduction to UML-B explaining the concept of the various diagrams and illustrating their use with some examples
| |
− |
| |
− | Lecture 1 - [http://wiki.event-b.org/images/UMLBClassContextDiagrams.pdf Introduction to UML-B and use of UML-B Class and Context Diagrams]
| |
− |
| |
− | Lecture 2 - [http://wiki.event-b.org/images/UMLBStateMachineDiagrams.pdf Use of UML-B State Machine Diagrams]
| |
− |
| |
− | Lecture 3 - [http://wiki.event-b.org/images/UMLBRefinement.pdf How to perform Refinement in UML-B]
| |
− |
| |
− | ==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]]
| |
− |
| |
− | ==Worked Examples==
| |
− |
| |
− | [[Modelling with UML-B Class and Context Diagrams - Railway Interlocking Safety Requirements]]
| |
− |
| |
− | [[Modelling with UML-B State-machine Diagrams - Aircraft Engines]]
| |
− |
| |
− | ==More detail about the various diagram types.==
| |
− |
| |
− | [[Package Diagram]]
| |
− |
| |
− | [[Context Diagram]]
| |
− |
| |
− | [[Class Diagram]]
| |
− |
| |
− | [[Statemachine Diagram]]
| |
− |
| |
− | [[UML-B_-_Statemachine_Animation|Animation of Statemachine Diagrams]]
| |
− |
| |
− | ==FAQ==
| |
− |
| |
− | [[UML-B FAQ]]
| |
− |
| |
− | ==Migrating old UML-B models to the latest format==
| |
− |
| |
− | (No migration is necessary when upgrading to UML-B version 2.1.0 from 1.1.0)
| |
− |
| |
− | 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==
| |
− |
| |
− | [[UML-B release notes for 2.1.0|In version 2.1.0]]
| |
− |
| |
− | [[UML-B release notes for 2.0.1|In version 2.0.1]]
| |
− |
| |
− | [[UML-B release notes for 1.1.0|In version 1.1.0]]
| |
− |
| |
− | ==Known bugs and workarounds==
| |
− |
| |
− |
| |
− | [[UML-B notes for 2.1.0|In version 2.1.0]]
| |
− |
| |
− | [[UML-B notes for 2.0.1|In version 2.0.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 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.