Schedule
Type
Day
Time
Place
Start
Lecturer
News
05.03.2010 | New results for the exam. | |
01.03.2010 | The repetition exam will be oral on 01.04 without having accessing to the slides or exercises. | |
01.03.2010 | You may come on Friday (05.03) from 11:00 - 12:00 to review your exam sheets in room 4201b. | |
01.03.2010 | You may find the results of the exam above. | |
15.02.2010 | You are allowed to take only the slides with you in the exam on Feb. 18. | |
05.02.2010 | Questions regarding the whole course will be answered on Feb. 11 from 10:30 to 12:00 at room 4203 and 4207. | |
05.02.2010 | There will be **no** questions about OCL in the exam, therefore the last exercise class on Feb. 10th is canceled. You are also not required to solve Ex09, and the solutions are uploaded for reference. | |
25.01.2010 | The tomorrow lecture will be in room 5052 at the usual time. | |
25.01.2010 | (obsolete!) The last exercise lecture will be on 10'th of February. Questions regarding the whole course will be answered on the same date. | |
23.01.2010 | The lecture on Monday, 25'th of January will start at 16:00. | |
13.01.2010 | There will be no lecture on Monday January 18'th. | |
12.01.2010 | The exam will take place on Thursday February 18 from 14:00 until 15:30 in room AH1. | |
23.11.2009 | The finite automaton in the lecture today for the universally-3-bounded CFM is here. | |
10.11.2009
(Important!) | Students that want to participate in the exam need to register via the CAMPUS system. Firm deadline for registration: November 30. Bachelor students should directly contact the lecturer for exam registration. | |
04.11.2009 | There will be *no* exercise class on 11.11. Ex.3a and 3b will be available today and on 11.11, respectively. The solutions for both will be explained on 18.11. | |
26.10.2009 | A new version of the lecture 2 slides are available, where partial order is redefined to be reflexive. | |
19.10.2009 | Lecture on Tuesday (20.10.2009 - at 8:15) will be held in the room 2002 located near the main entrance of the Informatik building. It is the new seminar room of the chair I11. |
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 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).
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
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.
Slides and exercise sheets
Date
Lecture
Subject
Slides
Nov 23
9
Realisability (2)
(*): The slides have been updated. Please find the details in "News".
Exercise
Exercise Sheet
Solutions
Due
Additional background literature
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.
(The course will however be mainly based on recent scientific papers.)