Theoretical Foundations of the UML

News

  • 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 (tentative)

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.

uml-msc

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

uml-mpa

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

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    
May 19 10 Complexity of Realisability FUML20-Lec10 Ex06  
May 25 11 Safe Realisability FUML20-Lec11    
May 26 12 Regular Sets of MSCs      
Jun 8 13 Regular Expressions over MSCs      
Jun 9 14 An Algorithm to Realise Local Choice MSGs      
Jun 15 15 A Logic for MSCs (1)      
Jun 16 16 A Logic for MSCs (2)      
Jun 22 17 Introduction to StateCharts      
Jun 23 18 StateChart Semantics      
Jun 29 19 Discuss former exam      
Jun 30 20        

Exam

  Date Time Location
First exam Jul 23 13:30 – 15:30 Aula 2
Re-exam Sep 2 13:30 – 15:30 Aula 2

In the exams you are allowed to carry printouts of the lecture slides, the proofs and examples which are public on the website. However, exercises and 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