News
 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:0011: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:0012: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:0012: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 communicationclosedness implies regularity” should be “Local communicationclosedness implies realizability”. As discussed in the lecture and the exercise class, MSGs can be local communicationclosed 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 deregister 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:3017: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!
Schedule
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, modeldriven 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 finitestate 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
 Clarify and make precise the semantics of the (treated fragments of the) UML;
 Reason about the basic properties of UML models;
 Consider the problem of mapping requirements specified as message sequence charts/graphs onto system implementations.
 Algorithms to allow for the verification of properties on UML models.
Prerequisites
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).
 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_Lec68  
Nov 7  7  Compositional MSGs  Undecidability_Proof  ex3  
Nov 13  8  Compositional MSGs  
Nov 14  9  Communicating FiniteState 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 
Exam
Date  Time  Location  

First exam  Tue, 06. February 2018  14:00 – 16:00  AH I, AH II 
Reexam  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

D. Harel and M. Politi, Modeling Reactive Systems with Statecharts: The STATEMATE Approach, McGrawHill, 1998.
 Benedikt Bollig – Formal Models of Communicating Systems, Springer, 2006 (Chapter 7, 8 and 9).
 The course will however be mainly based on scientific papers.