Theoretical Foundations of the UML


  • The result of re-exam on 16. March is now online. The inspection is on Wednesday (18. March) from 14:00-15:00 at the seminar room of our chair.  
  • The re-exam on 16. March takes place in AH4 in the computer science building.
  • The result of the 1st exam is now online. The time for inspection is on Tuesday (24. Feb) from 14:00-15:30 at the seminar room of our chair. 
  • The exams are open book exams. The only allowed material is a copy of the lecture slides (with your own notes). No other materials (i.e. exercises, solutions) are admitted. The exam on 10. Feb takes place in Fo1, which is near the Main building of RWTH.
  • There will be a class on Monday 2nd of Feb’15. The exam paper from 2010 will be discussed. The list of students who get enough points in exercise classes is here.
  • The date for re-exam is now determined.
  • The slides for Lecture 6 and 7 is updated.
  • L2P has been created for the course.
  • Urgent: due to the Fachschaftvollersammlung of Fachschaft I (the plenary session of the student community) on 4. Nov (which starts from 10:00), the lecture on 4. Nov is canceled! Instead of this, there will be a lecture on 11. Nov.
  • The question 2 of exercise series 2 is rephrased.
  • The first exercise sheet is now online and updated. There is a box prepared  to collect your solutions in front of the secretary’s room (room 4213, E1,  2nd floor) in our chair.  Please hand in the exercise before the first exercise class (i.e. 16:15 on 29. Oct). Please note that any solutions handed in thereafter  will not be corrected and evaluated.  Also note that there is no lecture next week. (Updated: 24. Oct)
  • We have scheduled the following dates for the written exams:
Date Time Location
First exam Tue, 10. February, 2015 11:15 – 13:15 Fo 1
Re-exam Mon, 16. March, 2015 13:15 – 16:15 AH4/AH5


Type Day Time Hall Start Lecturer
Lecture Mon 13:15 – 14:45 AH 4
13 Oct Katoen
Tue 10:00 – 11:30 5056 14 Oct Katoen
Exercise Wed 16:15 – 17:45 AH 6
29 Oct Chakraborty, Wu

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 of the UML: sequence diagrams, hierachical state machines (also known as Statecharts), and the OCL (short for Object Constraint Language).

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


  • Hierachical state machines and message passing automata 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.


  • Finally, the OCL allows to specify properties of system components, ranging from pre- and postconditions to invariants and more complex properties

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. Algorithms to allow for the verification of such 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 complexity theory is needed to be able to follow this course.

The course will cover for instance, formal semantics (how to precisly lay down the meaning of UML diagrams) 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 (Vordiplom):
  • Automata Theory
  • Mathematical Logic
  • Discrete Mathematics
  • Complexity Theory


No. Date Subject/Slides Exercises Solutions
1 13 Oct Introduction Exercise 01 Solution 01
2 14 Oct
Message Sequence Charts
Exercise 02 Solution 02
3 20 Oct Races Exercise 03 Solution 03
4 21 Oct
Message Sequence Graphs
Exercise 04 Solution 04
5 3 Nov
Language Intersection of 
MSGs (no slides)
Exercise 05 Solution 05
6 10 Nov
Message Sequence Graphs
Exercise 06 Solution 06
7 11 Nov please see Lecture 6 Exercise 07 Solution 07
8 17 Nov
Finite-State Machines

Exercise 08 Solution 08
9 18 Nov
Bounded MSCs and CFMs
Exercise 09 Solution 09
10 25 Nov
Exercise 10 Solution 10
11 08 Dec
Safe Realisability
12 09 Dec
Regular MSCs
13 15 Dec
Realising local-choice MSGs
14 16 Dec please see Lecture 13
15 05 Jan
A Logic for MSCs
16 06 Jan
PDL verification problems
(please see Lecture 15)
17 13 Jan
18 26 Jan
Statecharts Semantics (1)
19 27 Jan
Statecharts Semantics (2)
20 2nd Feb Exam February 2010


Date Time Location
First exam Tue, 10. February, 2015 11:15 – 13:15 Fo 1
Re-exam Mon, 16. March, 2015 13:15 – 16:15 AH4/AH5

Evaluation results

  • Lectures (TBD)
  • Exercises (TBD)

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 slides. 
  • An examination will take place at the end of the course.

Background Literature and Interesting Links

  • Jos Warmer and Anneke Kleppe, Object Constraint Language, The: Precise Modeling with UML. Addison Wesley, 2001.
  • D. Harel and M. Politi, Modeling Reactive Systems with Statecharts: The STATEMATE Approach, McGraw-Hill, 1998.
  • Benedikt Bollig – Formal Models of Communicating Systems, Springer, 2006 (Chapter 7, 8 and 9)
  • The course will however be mainly based on recent scientific papers.