Principles of Verification and Model Checking

Modulnummer: Q08-16
Englischer Titel: Principles of Verification and Model Checking
Leistungspunkte: 8
Lehrperson: Stietel/Rybicki

Empfohlene Vorkenntnisse

Keine

Zwingende Voraussetzungen

Keine

Inhalt

Verification is a domain which has for goal to expose potential design errors of programs and algorithms.
Model checking is a branch of verification and is divided in three steps: modelling the system, expressing the properties the system should satisfy and effectively checking if the model satisfies the properties.
For the modelling part, we will use transition system and spend some time on how to model programs. We will also see how to deal with parallel ones.
Next, we will use linear temporal logic (LTL) in order to express properties of programs. We will also spend time on how to describe relevant properties in LTL.
Finally for the checking if a model satisfies a property; we will study an automata based technique.

Erforderliche Arbeitsleistungen für LP-Vergabe und Prüfungszulassung

- aktive Teilnahme
- Bearbeitung von Übungsaufgaben

Lehrveranstaltungen

Vorlesung: 2 SWS 3 LP
Übung: 2 SWS 4 LP
MAP: 1 LP

Zugeordneter Vertiefungsschwerpunkt

Algorithmen und Modelle: ja
Modellbasierte Systementwicklung: nein
Daten- und Wissensmanagement: nein
Ohne Vertiefungsschwerpunkt: nein

Sprache im Modul

Deutsch: nein
Englisch: ja

Angeboten für Studiengänge

M. Sc.: ja
M. Ed.: ja
Wirtschaftsmaster: ja

Angeboten im

Wintersemester: nein
Sommersemester: ja

Turnus

Unregelmäßig