- 25.10.2021: The lecture material will be uploaded to RWTHmoodle. Make sure that you have access to the Moodle room so that you also receive further announcements. If you have questions, contact us via fuml21*at*i2.informatik.rwth-achen.de.
- 14.09.2021: We are online!
|Lecture||Mon||16:30-18:00||AH I||Nov 8||Katoen|
|Thu||16:30-18:00||AH V||Okt 14|
|Exercise Class||Mon||10:30-12:00||AH V||Okt 25||Quatmann, Salmani|
|Exercise Sheets||Mon||RWTHmoodle||Okt 18|
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 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
- Clarify and make precise the semantics of the (treated fragments of the) UML;
- Reason about the basic properties of UML models;
- Consider the problem of mapping requirements specified as message sequence charts/graphs onto system implementations.
- Algorithms to allow for the verification of properties on UML models.
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).
- Automata Theory
- Mathematical Logic
- Discrete Mathematics
- Computability and Complexity Theory
The lecture material (slides, exercise sheets) will be published in RWTHmoodle during the semester.
|First exam||Feb 7||12:00-14:00||TBA|
- 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 the slides.
- An examination will take place at the end of the course.
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.