Introduc-on to UML-‐B - Class Diagrams and Context Diagrams - May 2010

Oct 26, 2026

An introductory guide to UML-B, presenting its purpose as a graphical front-end for Event-B through the Rodin plug-in and its dedicated meta-model. The material explains how UML-B provides visualisation, faster class-oriented modelling, and inferred structuring constructs such as classes and hierarchical state machines. It also walks through getting started with installation, using the project wizard, disabling automated translation for larger models, and modelling a university degree registration example with parameters, guards, actions, constructors/destructors, and invariants.

LanguageEnglish

CategoryTechnology

FormatPDF

Pages19

Reading Time48 min

AccessFree to download

What is UML-B?

What are the benefits?

Getting Started

Class-oriented problems

An Event-B model of a class-oriented problem

Example - modelling with UML-B

Introduc-on to UML-‐B, UML-‐B Class Diagrams, UML-‐B Context Diagrams May, 2010 Colin Snook University of Southampton 1/19 What is UML-‐B? A Graphical front-‐end for Event-‐B ► Plug-‐in for Rodin Not UML … ► Has its own meta-‐model (abstract syntax) ► Seman-cs inherited from transla-on to Event-‐B … but has some similari-es with UML ► Class Diagrams ► State Machine Diagrams Translator generates Event-‐B automa-cally 2/19 What are the beneﬁts? Visualisa-on ► Helps understanding ► communica-on Faster modelling (allows you to experiment) ► One drawing node = several lines of B ► Extra informa-on inferred from posi-on of elements (e.g. if contained in a class or statemachine) Provides structuring constructs ► Class ► Hierarchical state-‐machines 3/19 Ge^ng Started Install UML-‐B using the Rodin update site ► Help – Install, select the main Rodin update site, wait for it to retrieve the categories, select UML-‐B Modelling Environment under Modelling Extensions. UML-‐B Perspec-ve UML-‐B New Project Wizard ► Opens a project diagram for you ► Add machines and contexts ► Double click on a machine to open a class diagram ► or on a context to open a context diagram Look for this icon UML-‐B Menu ► Disable automa-c transla-on (Recommended for larger models) UML-‐B toolbar bubon ► Save and translate 4/19 Class-‐oriented problems In Event-‐B models, oden ﬁnd a pabern ► Set I (or could be constant or variable) ► Variables v ∈ I → T ► Events e (i, .. ) when i ∈ I,… then v(i) := x I is a set of instances of a class v is a set of values, one for each instance (a class abribute) e is a ‘family’ of iden-cal events to assign values to v (a class event) I.e . trying to represent class-‐oriented problems 5/19 An Event-‐B model of a class-‐oriented problem class abribute (or associa-on) constructor class event destructor 6/19 Example -‐ modelling with UML-‐B In a university degree programme, students are registered on degree courses . Students must be enrolled to be registered in a course . Courses can be removed from the degree programme . There is no need to consider mul-ple degree programmes -‐ just assume we are modelling a single degree programme . 7/19 Example -‐ modelling with UML-‐B In a university degree programme, students are registered on degree courses . Students must be enrolled to be registered in a course . Courses can be removed from the degree programme . 8/19 Example -‐ modelling with UML-‐B In a university degree programme, students are registered on degree courses . Students must be enrolled to be registered in a course . Courses can be removed from the degree programme . parameter: c ∈ degree_course guard: self ↦ c ∉ register ac-on: register ≔ register ∪ {self ↦ c} guard: register[{self}] = ∅ guard: register ▷ {self} = ∅ constructor 9/19 Adding an Invariant Enrolled students must be 18 . guard: self ⋅ age ≥ 18 Transla-on: ∀self · ((self∈ enroll)⇒(age(self) ≥ 18)) 10/19

FAQs

What is UML-B in relation to Event-B?

UML-B is a graphical front-end for Event-B, implemented as a Rodin plug-in. It has its own meta-model and inherits semantics via translation into Event-B automatically.

What benefits does UML-B provide for modelling?

UML-B improves understanding through visualisation and supports faster modelling by allowing one diagram node to generate several Event-B lines. It also infers extra information from element positions within classes or state machines and provides structuring constructs like classes and hierarchical state machines.

How do you start using UML-B with Rodin?

Install UML-B using the Rodin update site, selecting UML-B Modelling Environment under Modelling Extensions. Then create a new project with the UML-B New Project Wizard, add machines and contexts, and open class or context diagrams via double-click. For larger models, use the menu option to disable automated translation (recommended).

How is a class-oriented problem modelled in UML-B?

The guide describes representing class instances with a set I and mapping it to values v using the type of class attributes. It models class events as families of events that assign values to v, and uses constructors/destructors and event actions/guards to update state accordingly.

Oct 26, 2026

Upload by Blue Pony