19612
Vorlesung
WiSe 12/13: Modelchecking
Marcel Kyas
Zusätzl. Angaben / Voraussetzungen
3,4,N
Veranstaltung findet in der ersten Hälfte des Semesters statt.
Kommentar
Inhalt 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 selbständig ein nicht-sequentielles Systems 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. Schließen
18 Termine
Zusätzliche Termine
Do, 18.04.2013 10:00 - 12:00Regelmäßige Termine der Lehrveranstaltung
Mo, 15.10.2012 16:00 - 18:00
Mo, 22.10.2012 16:00 - 18:00
Mo, 29.10.2012 16:00 - 18:00
Mo, 05.11.2012 16:00 - 18:00
Mo, 12.11.2012 16:00 - 18:00
Mo, 19.11.2012 16:00 - 18:00
Mo, 26.11.2012 16:00 - 18:00
Mo, 03.12.2012 16:00 - 18:00
Mo, 10.12.2012 16:00 - 18:00
Mi, 17.10.2012 16:00 - 18:00
Mi, 24.10.2012 16:00 - 18:00
Mi, 31.10.2012 16:00 - 18:00
Mi, 07.11.2012 16:00 - 18:00
Mi, 14.11.2012 16:00 - 18:00
Mi, 21.11.2012 16:00 - 18:00
Mi, 28.11.2012 16:00 - 18:00
Mi, 05.12.2012 16:00 - 18:00
Mi, 12.12.2012 16:00 - 18:00