• The oral exam will take place on tuesday 26.02.2008 at our chair (precise times will be announced later on this page). If you want to participate in the exam and fulfill the requirements (50% of the points from the exercises and (at least) onesummary of a leacture) please write an email to Carsten Kern.
• For students which are close to but below 50% of the points in the exercises we offer to do a second lecture summary to improve their score from the exercises. If you are interested please write an email to Carsten Kern to fix a date for doing a second summary.

 

Students who need to get a certificate (Schein) in the end of the course have to fulfill the following conditions:

People who want to participate in the exercises of this course have to do a 7-12 page summary of one of the lectures. The actual (preliminary) dates for the students already registered for the exercises are listed below.

• If you are not yet registered, please send an email to Carsten Kern and you will be assigned a date for the summary.

• If your name is misspelled please contact Carsten Kern.

A LaTeX-template for writing the summary is available here.

 

 (*) this PDF was not reviewed

 

 

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

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.

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):

message sequence charts, message passing automata, realizability, statecharts, model checking, causality, orthogonality, hierarchical modeling, OCL, semantics, undecidability, tools.

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.

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