Hasso-Plattner-Institut25 Jahre HPI
Hasso-Plattner-Institut25 Jahre HPI

Automated Analysis of Formal Models (Sommersemester 2014)

Dozent: Prof. Dr. Holger Giese (Systemanalyse und Modellierung) , Johannes Dyck (Systemanalyse und Modellierung) , Joachim Hänsel (Systemanalyse und Modellierung)

Allgemeine Information

  • Semesterwochenstunden: 2
  • ECTS: 3
  • Benotet: Ja
  • Einschreibefrist: 1.4.2014 - 28.4.2014
  • Lehrform: Seminar
  • Belegungsart: Wahlpflichtmodul

Studiengänge, Modulgruppen & Module

IT-Systems Engineering MA
  • IT-Systems Engineering A
  • IT-Systems Engineering B
  • IT-Systems Engineering C
  • IT-Systems Engineering D
IT-Systems Engineering BA


Complexity is one of the most important challenges of today's software systems and their development. Modeling and model-driven software engineering provide a multitude of concepts to handle complexity in the design and development processes, reducing development costs and improving reusability and maintainability. When models are additionally equipped with formal semantics, these models can also be used as a basis for the automated analysis of the systems they represent. Such formal analysis techniques allow, for example, the verification of properties that could otherwise not be assured by testing or human analysis because of the incompleteness of such methods or the complexity of such systems and properties. However, not all tools for the analysis of formal models are equally suited for all kinds of systems. Rather, they are often tailored to their respective areas of application, yielding specific advantages and disadavantages to be aware of.

This seminar is focused on a number of such tools for the automated analysis of formal models. The students will learn about both general approaches for formal analysis techniques and specific tools employing those formal techniques. During the seminar, each student will be assigned a tool and accompanying literature to familiarize him- or herself with and will evaluate the tool as to its areas of application, its specific advantages and disadvantages and its use in practice.


After the first meeting, the slides - including the topics - will be found under FG Systemanalyse und Modellierung -> Automated Analysis of Formal Models on the respective drive/the internal materials folder.

Lern- und Lehrformen

The course is a seminar, where each student will give a presentation and write a paper about his or her assigned topic. Each topic will focus on a specific tool for the analysis of models. While there will not be any implementation involved, we expect the students to familiarize themselves with their assigned tool and its use and to develop an example to demonstrate the tool's application.

There will be an introductory meeting presenting basic concepts of the analysis of formal models. In addition, we will introduce the topics - with each topic covering a specific tool - to choose from. Students wishing to participate will be asked to name their preferred topic(s), which we will then process to assign the topics in the subsequent meeting(s).

Except for the introductory meetings, there will be no regular meetings during the term. Instead, students will discuss their topics in individual appointments with their supervisor. The date for the presentations and report submissions will be determined in coordination with students and supervisors.


We will grade the students' reports, presentations, and their participation in the seminar.


First/introductory meeting: 15th of April, 13.30, Room A-1.1.

Assignment of topics: 22nd of April (and 29th of April, if necessary), 13.30, Room A-1.1.

Seminar: To be determined.