UML-B: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Colin
m →‎Tutorials: remove i
 
(9 intermediate revisions by 3 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. [[UML-B]] works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams.  


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.
Our [https://www.uml-b.org UML-B] website contains more information about installing UML-B and getting started, as well as our current research and collaborations.


==Lectures==
UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine.
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]
* [[Image:IUMLB.png]] [[Event-B Statemachines| State-machine diagrams]] a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.


Lecture 2 - [http://wiki.event-b.org/images/UMLBStateMachineDiagrams.pdf Use of UML-B State Machine Diagrams]
* [[Image:IUMLB.png]] [[Event-B Classdiagrams| Class diagrams]] a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets.


Lecture 3 - [http://wiki.event-b.org/images/UMLBRefinement.pdf How to perform Refinement in UML-B]
==Lectures==


==Tutorials==
* [[Media:iUML-BClassDiagramsLecture.pdf | UML-B Class-diagrams Lecture]] : Lecture slides on the use of UML-B Class-diagrams


A simple tutorial, showing the basics of how to construct a UML-B model using all the diagram types.
* [[Media:iUML-BStatemachinesLecture.pdf | UML-B State-machines Lecture]] : Lecture slides on the use of UML-B State-machines.
[[UML-B Tutorial]]


An illustration showing how to refine statemachines
==Tutorials==
[[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==
* [[iUML-B Class-diagrams Tutorial | UML-B Class-diagrams Tutorial]] : A tutorial on the use of UML-B Class-diagrams.


* [[iUML-B State-machines Tutorial | UML-B State-machines Tutorial]] : A tutorial on the use of UML-B State-machines.


[[UML-B notes for 2.1.0|In version 2.1.0]]
==Guidelines==


[[UML-B notes for 2.0.1|In version 2.0.1]]
* [[UML-B - Modelling a control system]] : Some guidelines on modelling styles for a control system




[[Category:User documentation]]
[[Category:User documentation]]
[[Category:UML-B]]
[[Category:UML-B]]
[[Category:Plugin]]

Latest revision as of 22:12, 30 September 2020

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. UML-B works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams.

Our UML-B website contains more information about installing UML-B and getting started, as well as our current research and collaborations.

UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine.

  • State-machine diagrams a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.
  • Class diagrams a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets.

Lectures

Tutorials

Guidelines

Retrieved from ‘https://wiki.event-b.org/index.php?title=UML-B&oldid=14399’