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

Automated Analysis of Formal Models (Sommersemester 2017)

Dozent: Prof. Dr. Holger Giese (Systemanalyse und Modellierung) , Johannes Dyck (Systemanalyse und Modellierung)

Allgemeine Information

  • Semesterwochenstunden: 2
  • ECTS: 3
  • Benotet: Ja
  • Einschreibefrist: 28.04.2014
  • Lehrform: Seminar
  • Belegungsart: Wahlpflichtmodul

Studiengänge, Modulgruppen & Module

IT-Systems Engineering MA
  • SAMT: Software Architecture & Modeling Technology
    • HPI-SAMT-K Konzepte und Methoden
  • SAMT: Software Architecture & Modeling Technology
    • HPI-SAMT-S Spezialisierung
  • SAMT: Software Architecture & Modeling Technology
    • HPI-SAMT-T Techniken und Werkzeuge
  • IT-Systems Engineering
    • HPI-ITSE-A Analyse
  • IT-Systems Engineering
    • HPI-ITSE-E Entwurf
  • IT-Systems Engineering
    • HPI-ITSE-K Konstruktion
  • IT-Systems Engineering
    • HPI-ITSE-M Maintenance


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 the systems. 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 disadvantages to be aware of.

This seminar is focused on a number of tools for the automated analysis of formal models. Students will learn about 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 with respect to its areas of application, its specific advantages and disadvantages, and its use in practice.


The slides of the introductory meeting - including the seminar 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 formal models. While there will not necessarily 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 subsequently assign the topics.


We will grade the student's reports (50%) and presentations (50%). Participation in the seminar during other students' presentations in the form of questions and feedback will also be required.


The first and introductory meeting will be on Tuesday, 25th of April, 11:00-12:30 in room A-2.2. We will not have a meeting on the 18th of April.

Besides individual feedback meetings with supervisors (and the first meeting), there will not be any regular meetings during the semester. All presentations will be given on one day (date to be determined) near or after the end of lectures in the semester.