News
 The result of reexam on 16. March is now online. The inspection is on Wednesday (18. March) from 14:0015:00 at the seminar room of our chair.
 The reexam 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:0015: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 reexam 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 
Reexam  Mon, 16. March, 2015  13:15 – 16:15  AH4/AH5 
Schedule
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, 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 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 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
Slides
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 
Exercise 05  Solution 05 
6  10 Nov 
Compositional 
Exercise 06  Solution 06 
7  11 Nov  please see Lecture 6  Exercise 07  Solution 07 
8  17 Nov 
Communicating 
Exercise 08  Solution 08 
9  18 Nov 
Bounded MSCs and CFMs 
Exercise 09  Solution 09 
10  25 Nov 
Realisability 
Exercise 10  Solution 10 
11  08 Dec 
Safe Realisability 

12  09 Dec 
Regular MSCs 

13  15 Dec 
Realising localchoice MSGs 

14  16 Dec  please see Lecture 13  
15  05 Jan 
A Logic for MSCs 

16  06 Jan 
PDL verification problems 

17  13 Jan 
Statecharts 

18  26 Jan 
Statecharts Semantics (1) 

19  27 Jan 
Statecharts Semantics (2) 

20  2nd Feb  Exam February 2010 
Exam
Date  Time  Location  

First exam  Tue, 10. February, 2015  11:15 – 13:15  Fo 1 
Reexam  Mon, 16. March, 2015  13:15 – 16:15  AH4/AH5 
 Registration via this Campus page
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, McGrawHill, 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.