UML-B: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Colin
No edit summary
m →‎Tutorials: remove i
 
(5 intermediate revisions by the same user 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 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.
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.  


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.
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.


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.
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.
 
* [[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.
 
* [[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.
 
==Lectures==
 
* [[Media:iUML-BClassDiagramsLecture.pdf | UML-B Class-diagrams Lecture]] : Lecture slides on the use of UML-B Class-diagrams
 
* [[Media:iUML-BStatemachinesLecture.pdf | UML-B State-machines Lecture]] : Lecture slides on the use of UML-B State-machines.
 
==Tutorials==
 
* [[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.
 
==Guidelines==
 
* [[UML-B - Modelling a control system]] : Some guidelines on modelling styles for a control system




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’