Theoretical Foundations of the UML

News

  • 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

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, 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.

uml-msc

  • 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.

uml-mpa

  • 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.

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 
MSGs (no slides)
 Exercise 05 Solution 05
6 10 Nov 
Compositional 
Message Sequence Graphs
 Exercise 06 Solution 06
7 11 Nov please see Lecture 6 Exercise 07 Solution 07
8 17 Nov 
Communicating 
Finite-State Machines
(handout)
 Exercise 08 Solution 08
9 18 Nov 
Bounded MSCs and CFMs
 Exercise 09 Solution 09
10 25 Nov 
Realisability
(proof)
 Exercise 10 Solution 10
11 08 Dec 
Safe Realisability
(proof)
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 
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
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.