News
- 08.8.2016: The results of the exam will soon be made available through campus office. The exam inspection will take place on Monday, August 15, at 15:00h in our seminar room (Building E1, Room 4201b).
- 01.8.2016: There has been some confusion with the timing of the exam. The dates and times announced on this website are correct. The first exam takes place on Thursday, August 4 at 13:00h in lecture hall AH I.
- 20.7.2016: Please find the results of the evaluation of the lecture and the exercise class below.
- 15.7.2016: During the lecture on Tuesday, July 19, Prof. Katoen will present an old exam.
- 07.7.2016: There will be no exercise class today.
- 28.6.2016: The word (locally) in the statement “Every (locally) communication-closed MSG is regular.” on slide 7 of Lecture 13 needs to be removed.
- 27.6.2016: An old exam is now available in the Exam section on this page.
- 26.5.2016: The last example on page 10 of the slides of lecture 6 was erroneous, and has now been fixed. A new version of the slides is on-line.
- 17.5.2016: By majority vote, the next exercise class will take place on Friday, May 27 at 10:15 in Room 9U09.
- 12.5.2016: Please indicate your preferences for the date of the next exercise class here until Sunday, May 15. We will try to arrange a date which is most convenient for most of you. However, please keep in mind that we also need to organize a room, so the date we will arrange might not coincide with the majority vote.
- 03.5.2016: There was a problem with the campus office settings for this course which affected the exam registration for some of you. That issue should be fixed now. The deadline for exam registration is May 20, but we urge you to register as soon as possible (just to be on the safe side if any further issues should arise). If you still experience problems registering, please let us know as soon as possible.
- 28.4.2016: There will be no lecture and exercise class next week.
- 19.4.2016: The exercise class is now shifted to 16:15 – 17:45 (still in room 9U09 on Thursdays).
- 19.4.2016: The first exam and re-exam are scheduled on 4th, August and 22th, September, respectively.
- 18.4.2016: You can register yourself for the exercise class in Campus Office (first after you have logged in) under Theoretical Foundations of the UML (FUML) (Übung (Ü)) with the link “Zum klassischen Anmeldeverfahren” now.
- 11.4.2016: The lecture will start on Thursday, April 4, at 8:30h in Room 5056 (Building E2). The first exercise sheet will be handed out on Thursday, April 21, and the first exercise class will be given on Thursday, April 28, also in Room 9U09.
- 05.4.2016: We are online!
Schedule
| Type | Day | Time | Hall | Start | Lecturer |
|---|---|---|---|---|---|
| Lecture | Tue | 12:15 – 13:45 | 9U09 | 19.4. | Katoen |
| Thu | 08:30 – 10:00 | 5056 | 14.4. | Katoen | |
| Exercise | Thu | 16:15 – 17:45 | 9U09 | 28.4. | Kaminski, 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:
- Clarify and make precise the semantics of the (treated fragments of the) UML;
- Reason about the basic properties of UML models;
- 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.
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.
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:
- Automata Theory
- Mathematical Logic
- Discrete Mathematics
- Computability and Complexity Theory
Slides and Exercise Sheets
| Date | Lecture | Topic | Handout/Slides | Exercises | Additional material |
| April 14+17 | 1+2 | Intro + Message Sequence Charts | e1 | ||
| April 19 | 3 | Races | e2 | ||
| April 21 | 4 | Message Sequence Graphs | |||
| April 28 | 5 | Emptiness of MSG intersection | blackboard lecture | ||
| May 10 | 6 | Compositional MSGs | e3 | proof | |
| May 12 | 7 | Safe CMSGs | blackboard lecture | ||
| May 24 | 8 | Communicating FSMs |
no handout (due to overlays) |
e4 | |
| May 31 | 9 | Bounded MSCs and CFMs | |||
| June 2 | 10 | Realisability (1) | e5 | proof | |
| June 7 | 11 | Realisability (2) | |||
| June 9 | 12 | Safe Realisability | e6 | proof | |
| June 16 | 13 | Regular MSGs | e7 | ||
| June 21 | 14 | Realising local choice MSGs | e8 | ||
| June 28 | 15 | Propositional dynamic logic | e9 | ||
| June 30 | 16 | Propositional dynamic logic | |||
| July 12 | 17 | Statecharts | e10 | ||
| July 14 | 18 | Statecharts semantics (1) | slides_lecture_18 | ||
| July 19 | 19 | Statecharts semantics (2) / Old Exam | slides_lecture_19 |
Exam
| Date | Time | Location | |
|---|---|---|---|
| First exam | Thu, 4. August, 2016 | 13:00 – 15:00 | AH1 |
| Re-exam | Thu, 22. September, 2016 | 13:00 – 15:00 | AH1 |
An old exam with solutions is available here.
Evaluation results
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
- 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.