News
- 10.06.2020: In order to attend the exam, every registered participant of the course needs to register the exam via RWTHonline as soon as possible. The fixed dates of the exams are to be announced.
- 18.05.2020: There will be no lecturing or exercise class activities in the week after Pentecost (“excursion week” in Aachen), i.e., week 23 (June 1 – 5).
- 15.04.2020: Home assignments:
- weekly assignments: about 4 exercises per assignment to be solved
- groups of maximally three students together work on assignments
- solutions: hand in via RWTHmoodle as pdf-file
- first assignment available: Monday April 20, 10:00 am
- solution due at start next week: Monday April 27, 09:00 am
- first on-line exercise class video: Wednesday April 29, 02:30 pm
- in that video, the solutions to the home assignments will be explained
- pdf-solutions of the home assignments will be made available after the exercise video
- this scheme is repeated on a weekly basis until the beginning of July
- there will be about 10 home assignments and 20 lectures
- there is no lecture+exercise class in the week following Pentecost
- 06.04.2020: Students are supposed to hand in the solutions to the weekly exercise sheets via RWTHmoodle, where interactions with the lecturers will also be possible. To this end, the students have to register for the course (both lecture and exercise) at RWTHonline.
- 06.04.2020: We are looking for 1-2 student assistants who would be mainly working on the correction of exercise sheets. Applicants of the job are expected with a background in theoretical computer science (mathematical logic, formal language, automata theory, computability & complexity theory, etc.). Drop us an email (Chen <chenms@cs.rwth-aachen.de>, Salmani <salmani@cs.rwth-aachen.de>) if you are interested.
- 18.03.2020: We are online!
Schedule
| Type | Day | Available Time | Access | Start | Lecturer |
|---|---|---|---|---|---|
| Lecture (slide-casts) | Mon | 16:30 | RWTHmoodle | Apr 20 | Katoen |
| Tue | 10:30 | Apr 21 | |||
| Exercise (slide-casts) | Wed | 14:30 | RWTHmoodle | Apr 29 | |
| Exercise Sheets | Mon | 10:00 | RWTHmoodle | Apr 20 | Chen, Salmani |
| Q&A Session | Thu | 16:00 | Zoom ID: 369 366 110 (Password: FUML-QA) | Apr 23 |
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.
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).
- Automata Theory
- Mathematical Logic
- Discrete Mathematics
- Computability and Complexity Theory
Slides and Exercise Sheets
| Date | Lecture | Topic | Handout/Slides | Exercises | Additional material |
| Apr 20 | 1 | Introduction and Message Sequence Charts | FUML20-Lec01 | ||
| Apr 21 | 2 | Races in MSCs | FUML20-Lec02 | Ex01 | |
| Apr 27 | 3 | Message Sequence Graphs | FUML20-Lec03 | Ex02 | correction |
| Apr 28 | 4 | The Emptiness Problem for MSGs | FUML20-Lec04 | ||
| May 4 | 5 | Compositional MSGs | FUML20-Lec05 | Ex03 | |
| May 5 | 6 | Decision Procedure for Safe CMSGs | FUML20-Lec06 | Ex04 | |
| May 11 | 7 | Communicating Finite-State Machines | FUML20-Lec07 | ||
| May 12 | 8 | Bounded MSCs and CFMs | FUML20-Lec08 | Ex05 | |
| May 18 | 9 | Realisability | FUML20-Lec09 | correction | |
| May 19 | 10 | Complexity of Realisability | FUML20-Lec10 | Ex06 | |
| May 25 | 11 | Safe Realisability | FUML20-Lec11 | ||
| May 26 | 12 | Regularity and Realisability | FUML20-Lec12 | Ex07 | |
| Jun 8 | 13 | Local-Choice MSGs and Regular Expressions on MSCs | FUML20-Lec13 | ||
| Jun 9 | 14 | Realising Local-Choice MSGs | FUML20-Lec14 | Ex08 | |
| Jun 15 | 15 | A Logic for MSCs (1) | FUML20-Lec15 | ||
| Jun 16 | 16 | A Logic for MSCs (2) | FUML20-Lec16 | Ex09 | |
| Jun 22 | 17 | Introduction to StateCharts | FUML20-Lec17 | ||
| Jun 23 | 18 | StateChart Semantics | FUML20-Lec18 | Ex10 | |
| Jul 16 | Discuss former exams | Live at the Q&A Session |
Exam
| Date | Time | Location | |
|---|---|---|---|
| First exam | Sep 03 | 12:00 – 14:00 | H01 |
| Re-exam | Oct 22 | 12:00 – 14:00 | Großer Hörsaal AM |
In the exams you are allowed to carry ONLY a double-sided, hand-written A4 paper for your own reference. Extra materials, e.g., printouts of the lecture slides, the exercise sheets or solutions to the exercises, are NOT permitted.
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 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.