Contents

The term formal methods stands for languages and methods that allow systems to be modelled precisely at certain levels of abstraction using mathematical means, to formulate requirements for them and to reliably analyse the fulfilment of these properties.

In this proseminar we will cover some basic topics from the field of formal methods, such as modelling languages for systems (different classes of automata for discrete, hybrid and probabilistic systems), specification languages for properties (temporal logics such as CTL*, CTL, LTL), verification techniques (bisimulation), but also techniques used in verification processes (satisfiability checking).

Inhalt

Der Begriff formale Methoden steht für Sprachen und Methoden die es erlauben, Systeme auf bestimmten Abstraktionsebenen mit mathematischen Mitteln präzise zu modellieren, Anforderungen an sie zu formulieren und die Erfüllung dieser Eigenschaften zuverlässig zu analysieren.

In diesem Proseminar behandeln wir einige grundlegende Themen aus dem Bereich der formalen Methoden, wie zum Beispiel Modellierungssprachen für Systeme (unterschiedliche Klassen von Automaten für diskrete, hybride und probabilistische Systeme), Spezifikationssprachen für Eigenschaften (temporäre Logiken wie z.B. CTL*, CTL, LTL, MTL, Hyperproperties), Verifikationstechniken (Deduktion, Model Checking, Bounded Model Checking), aber auch Techniken die in Verifikationsprozessen Verwendung finden (Satisfiability Checking).