Systemtheorie 1

Model Checking

Wintersemester 2006/2007

Armin Biere, Robert Brummayer, Toni Jussila

Neuigkeiten

Zweite Nachklausur am Freitag, den 29.6.2007 HS 14, von 13:45 bis 15:15
Erste Nachklausur am Donnerstag, den 8.3.2007 HS 9, von 08:30 bis 10:00

Die Vorlesung beschäftigt sich mit Algorithmen und Datenstrukturen für die Verifikation von Informatik-Systemen mit dem Fokus auf Verteilte Systeme und automatische Methoden. Ein erfolgreicher Besuch der Lehrveranstalung Formale Grundlagen 3 ist sehr empfehlenswert.

Während bei den Formalen Grundlagen 3 der Modellierungsaspekt im Vordergrund steht, sind es in der Systemtheorie 1 die Verifikations-Algorithmen.

Folien

An dieser Stelle sind die Folien zu finden. Ein Skript oder die Verwendung eines Buches ist nicht geplant. Der komplette Foliensatz (handout) enthält alle soweit erstellten Folien, wird aber bis Ende des Semesters unvollständig bleiben. Es wird empfohlen, nur die Handouts der nächsten Vorlesung auszudrucken.

Einführung (slides, handout)
Endliche Automaten und Konformität (slides, handout)
Simulation (slides, handout)
Erreichbarkeit (slides, handout, testhash.c)
Partial Order Reduction (slides, handout)
Fairness (slides, handout)
AIGs (slides, handout, aig4teaching.zip, lg-0.9.tar.gz)
BDDs (slides, handout, bdd4teaching.zip, lg-0.9.tar.gz)

Links

Der Finite State Machine Calculator FSMCalc implementiert die Datenstrukturen und Algorithmen dieser Vorlesung.

Übungen

Die genauen Termine und Ihre Gruppenzuordnung entnehmen Sie bitte dem KUSSS.

Es wird Anwesenheit erwartet, da angekreuzte Beispiele an der Tafel ohne Zuhilfenahme von Unterlagen zu präsentieren sind. Pro Beispiel wird ein Übungsteilnehmer für die Präsentation ausgewählt. Die Übungen müssen schriftlich am Tag der Übung (Donnerstag) bis spätestens 10:30 im Institut abgegeben werden. Im Laufe des Semesters wird dafür ein Postkasten zur Verfügung stehen.

Übungsaufgaben

1. Übung Korrektur: Bsp. 4: I1 und I2 sind nun Mengen.
2. Übung
3. Übung Korrektur: Bsp. 12 b) und c): L(B) statt B
4. Übung
5. Übung
6. Übung exercise24.pml
7. Übung crossing.pml
8. Übung testhashex.c sources.zip
9. Übung
10. Übung
11. Übung