Theoretical Foundations of the UML


  • 25.10.2021: The lecture material will be uploaded to RWTHmoodle. Make sure that you have access to the Moodle room so that you also receive further announcements. If you have questions, contact us via fuml21*at*
  • 14.09.2021: We are online!


Type Day  Time Room Start Lecturer
Lecture Mon 16:30-18:00 AH I Nov 8 Katoen
Thu 16:30-18:00 AH V Okt 14
Exercise Class Mon 10:30-12:00 AH V Okt 25 Quatmann, Salmani
Exercise Sheets Mon   RWTHmoodle Okt 18

Content and Motivation

The Unified Modelling Language (UML) — more generally, model-driven engineering — plays an important role in modern software design. The UML basically consists of a set of different notations, each notation focused on a specific aspect of the software system at hand. The aim of this course is to consider some major fragments and aspects of the UML: message sequence diagrams, message sequence graphs, a logic to reason about MSCs and MSGs, the realisability problem, and, hierachical state machines (also known as Statecharts).

  • Sequence diagrams specify the interaction patterns between the system components and are a popular elicitation technique for requirements engineering.


  • Hierachical state machines and communicating finite-state machines are used to describe the behaviour of system components, and are intensively used during the system’s design phases, e.g., in the fields of avionics and automotive industry.


Aims of this Course

The aim of this course is to treat the theoretical underpinnings of the aforementioned UML fragments. In particular, we will present the theories required to:
  1. Clarify and make precise the semantics of the (treated fragments of the) UML;
  2. Reason about the basic properties of UML models;
  3. Consider the problem of mapping requirements specified as message sequence charts/graphs onto system implementations.
  4. Algorithms to allow for the verification of properties on UML models.
It is our firm belief (and experience) that a solid theoretical underpinning is of prime importance to obtain automated tools (such as MSCan) that produce reliable, i.e, verifiable results.


Although the name UML might suggest differently, this is a theoretical course! That is, a solid basis in algorithms and data structures, automata theory, and a bit of theoretical computability and complexity theory is needed to be able to follow this course. During the exercises and lectures we will also provide introductory material.

The course will cover for instance, formal semantics (what does a UML diagram mean? Precisely) and formal verification (is checking certain properties on UML diagrams decidable, and if so, efficiently decidable).

Basic knowledge of the undergraduate courses of the first two years:
  • Automata Theory
  • Mathematical Logic
  • Discrete Mathematics
  • Computability and Complexity Theory

Lecture Material

The lecture material (slides, exercise sheets) will be published in RWTHmoodle during the semester.


  Date Time Location
First exam Feb 7 12:00-14:00 TBA
Re-exam Mar 19 14:00-16:00 TBA


Further information

  • The course will be entirely given in English. The slides and other course material will also be in English.
  • There are no lecture notes (yet); the course material will consist of the slides.
  • An examination will take place at the end of the course.

Background Literature and Interesting Links