Theoretical Foundations of the UML


  • 16.02.2018: The correction of the second exam has been completed. Please find your result in the L2P. The review for the exam will take place on Monday, 19.03, from 10:00-11:00 in the seminar room of our chair (E1, room 4201b). Please bring your BlueCard.
  • 10.03.2018: The second exam takes place on Monday, 12.03, at 13:00 in AH 5.
  • 13.02.2018: The correction of the first exam has been completed. Please find your result in the L2P. The review for the exam will take place on Wednesday, 28.02, from 10:00-12:00 in room 5056. To prevent long queues, we partitioned the groups based on their matriculation number as shown below. Please bring your BlueCard.
    Matriculation number Time
    000 001 — 374 000 10:00 to 11:00
    374 001 — 999 999 11:00 to 12:00
  • 05.02.2018: The first exam takes place on Tuesday, 06.02, at 14:00. We partitioned all participants into two groups based on their matriculation number as follows:
    Matriculation number Room
    000 001 — 374 000 AH 1
    374 001 — 999 999 AH 2
  • 30.01.2018: On Friday, 02.02., from 10:00-12:00 you can come by our offices (E1, rooms 4205 and 4206) to ask questions about the lecture, the exercises and the exam. Please send an email beforehand to Tim Quatmann and Matthias Volk to allow us prepare for your questions.
  • 19.01.2018: the former exam that is to be discussed on Tuesday January 30 has been put online (see below in the scheduling plan).
    In the exams you are allowed to carry printouts of the lecture slides, the proofs and examples which are public on the website. However, exercises and solutions to the exercises are not permitted.
  • 15.01.2018: there was a flaw in the definition of connected MSC in Lecture 15 and in the following theorem [Morin 2002] on slide 31 (realisable should be regular). The slides have been updated accordingly. Exercise 2 from sheet 9 has been updated as well since it referred to the uncorrected definition of connected MSCs.
  • 14.01.2018: There are no lectures on January 22+23.
  • 10.01.2018: On slide 5 of lecture 15, “Local communication-closedness implies regularity” should be “Local communication-closedness implies realizability”. As discussed in the lecture and the exercise class, MSGs can be local communication-closed but not regular.
  • 07.01.2018: the results of the lecture evaluation by the students are very positive. Thanks for the useful feedback. A summary of the evaluation can be found here.
  • 21.12.2017: on slide 29 of lecture 15, “if for each vertex (v,v’) in G” should be “if for each edge (v,v’) in G”.
  • 17.12.2017: During the first lectures you have been informed that admission to the TFUML exam requires a certain percentage of points to be obtained in the exercises. However, this requirement is not fixed in the corresponding module specification and thus invalid. For this reason, every registered participant is automatically admitted. Therefore, if you are not intending to attend the exam please de-register via CampusOffice in order to avoid a “not passed” due to not showing up. Although the exercises are no longer mandatory for the exam admission, we will continue to correct them and discuss them in the exercise classes. We firmly believe that actively solving the exercises is truly important so as to pass the exam. Furthermore the bonus point rule still persists. If you gain at least 70% of all exercise points you obtain a 0.3 bonus on your exam grade.
  • 06.12.2017: Since there is no lecture in the next week, there will also not be a new exercise sheet. The current sheet (Exercise 7) has to be handed in until December 19th at 15:30. There is also no exercise class on December 12th.
  • 04.12.2017: Note that there are no lectures on December 11+12. There will however be lectures on December 18+19.
  • 28.11.2017: The definition of weak CFM has been slightly adapted in the slides of Lecture 11+12.
  • 17.11.2017: The time and place of the first exam slightly changed. The first exam will take place on Tuesday, 6.2.2018, at 14:00 in lecture halls AH I and AH II.
  • 03.11.2017: There is a room change for the lecture on Monday, 6.11: the lecture will take place in room 5054.
  • 26.10.2017: There was a typo on slide 13 of lecture 3 and slide 18 of lecture 4; new versions of these slides have been uploaded.
  • 17.10.2017: The first exercise sheet is online. You should solve it in groups of 3 students and hand it in before the exercise class on Tuesday. You need at least 40% of the points to be admitted to the exam. If you gain at least 70% of the points you get a 0.3 bonus on your grade for the exam.
  • 16.10.2017: Note there are no lectures on 17.10, 23.10, and 24.10; the next lecture takes place on Monday October 30.
  • 10.10.2017: The date of the exercise class changed to Tue, 15:30-17:00 in AH II. An overview of the schedule can be found below. The first exercise class is on October 24th.
  • 09.10.2017: Questions concerning the lectures or exercises can be posted in the L2P forum.
  • 27.9.2017: We are online!


Type Day Time Hall Start Lecturer
Lecture Mon 10:15 – 11:45 AH II 09.10. Katoen
  Tue 10:15 – 11:45 AH I 10.10. Katoen
Exercise Tue 15:30 – 17:00 AH II 24.10. Quatmann, Volk

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

Slides and Exercise Sheets

Date Lecture Topic Handout/Slides Exercises Additional material
Oct 9 1 Message Sequence Charts  TFUML17_Lec1+2    
Oct 10 3 Races  TFUML17_Lec3    
Oct 16 4 Message Sequence Graphs  TFUML17_Lec4 ex1  
Oct 30 5 Undecidability of MSG intersection black board lecture ex2  
Nov 6 6 Compositional MSGs  TFUML17_Lec6-8    
Nov 7 7 Compositional MSGs  Undecidability_Proof ex3  
Nov 13 8 Compositional MSGs      
Nov 14 9 Communicating Finite-State Machines  TFUML17_Lec9  ex4  
Nov 21 10 Bounded MSCs and CFMs  TFUML17_Lec10 ex5  
Nov 27 11 Realisability  TFUML_Lec11+12    
Nov 28 12 Realisability   ex6  proof
Dec 4 13 Safe Realisability  TFUMLl17_Lec13    proofs
Dec 5 14 Regular Sets of MSCs  TFUML17_Lec14 ex7  
Dec 18 15 Regular Expressions over MSCs  TFUML17_Lec15    
Dec 19 16 An Algorithm to Realise Local Choice MSGs  TFUML17_Lec16 ex8  example
Jan 8 17 A Logic for MSCs (1)  TFUML17 Lec17+18 ex9  
Jan 9 18 A Logic for MSCs (2)      
Jan 15 19 Introduction to StateCharts  TFUML17_Lec19    
Jan 16 20 StateChart Semantics  TFUML17_Lec20 ex10  
Jan 30 21 Discuss former exam  TFUML_old_exam    


  Date Time Location
First exam Tue, 06. February 2018 14:00 – 16:00 AH I, AH II
Re-exam Mon, 12. March, 2018 13:00 – 15:00 AH V

In the exams you are allowed to carry printouts of the lecture slides, the proofs and examples which are public on the website. However, exercises and solutions to the exercises are not permitted.

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