Modelchecking

Organisationseinheit
Freie Universität Berlin/Mathematik und Informatik/Informatik

Bereich

Studienbereich Theoretische Informatik

Zugangsvoraussetzungen

Erfolgreiche Absolvierung des Moduls Höhere Algorithmik

Qualifikationsziele

Die Studentinnen und Studenten können Systeme, Protokolle und verteilte Algorithmen selbstständig modellieren, Anforderungen in temporalen Logiken formalisieren, Echtzeitmodelle entwickeln und Echtzeitanforderungen formulieren. Sie sind in der Lage, für die Anforderungen geeignete Abstraktionen zu finden und Spezifikationen mit Hilfe eines Modellüberprüfers zu beweisen.

Inhalte

Unterschied zwischen Programmieren und Modellieren
Modellieren reaktiver Systeme in SPIN und Promela
Spezifizieren von Anforderungen in temporalen Logiken
Automatentheoretische Modelle von Systemen und Spezifikationen
Entscheidungsverfahren für temporale Logiken
Symbolisches Modelchecking und Binäre Entscheidungsdiagramme
Modelchecking mit NuSMV
Automatenmodelle mit Zeit
Modellchecking von Zeitautomaten mit Uppaal
Formale Methoden zur Abstraktion und dem Nachweis der erhaltenen Eigenschaften.

Miniprojekt: Es soll selbstständig ein nicht sequentielles System oder ein nicht sequentieller Algorithmus modelliert, dessen Anforderungen formalisiert und schließlich das Modell bezüglich der Anforderungen mit Hilfe von geeigneten Modellüberprüfern verifiziert werden. Diese Leistung wird durch Abgabe der Modelle und eines schriftlichen Berichts nachgewiesen.

Lehr- und Lernformen

Aktive Teilnahme

Vorlesung
2 SWS
Teilnahme empfohlen

Bearbeitung der Übungsaufgaben und Bearbeitung eines Miniprojekts

Übung
2 SWS
Teilnahme empfohlen

Bearbeitung der Übungsaufgaben und Bearbeitung eines Miniprojekts

Projektseminar
2 SWS
Teilnahme empfohlen

Bearbeitung der Übungsaufgaben und Bearbeitung eines Miniprojekts

Aufwand

Präsenzzeit V	30 Stunden
Vor- und Nachbereitung V	30 Stunden
Präsenzzeit Ü	30 Stunden
Vor- und Nachbereitung Ü	30 Stunden
Präsenzzeit PrS	30 Stunden
Vor- und Nachbereitung PrS	30 Stunden
Prüfungsvorbereitung und Prüfung	120 Stunden

Modulprüfung
Projektbericht (ca. 20 Seiten) mit mündlicher Präsentation (ca. 15 Minuten)

Differenzierte Bewertung
differenzierte Bewertung

Modulsprache
Deutsch (ggf. Englisch)

Arbeitsaufwand (Stunden)
300

Leistungspunkte (LP)
10

Dauer des Moduls
Ein Semester

Häufigkeit des Angebots
Jedes Wintersersemester

Verwendbarkeit

Masterstudiengang Informatik