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 and aspects of the UML: message sequence diagrams, message sequence graphs, a logic to reason about MSCs and MSGs, the realisability problem, and, hierachical state machines (also known as Statecharts).

• Sequence diagrams specify the interaction patterns between the system components and are a popular elicitation technique for requirements engineering.

• Hierachical state machines and communicating finite-state machines 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.

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. Consider the problem of mapping requirements specified as message sequence charts/graphs onto system implementations.
4. Algorithms to allow for the verification of 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. During the exercises and lectures we will also provide introductory material.

The course will cover for instance, formal semantics (what does a UML diagram mean? Precisely) 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

Further information

• This course is organized via RWTHmoodle. Please register in RWTHonline to get access. Further organizational information can be found in the Moodle room.
• There will be ***mandatory exercise sheets*** to be handed in. The students need to obtain at least 40% of the total points for the exercise sheets to be admitted to the exams. Please refer to RWTHMoodle for the weekly exercises.
• 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.

Background Literature and Interesting Links

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