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: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!
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, 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:
- 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.
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.
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).
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 |
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
-
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 scientific papers.