Theoretical Foundations of the UML


  • 14.09.2021: We are online!


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

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