Navigation Fachbereich und Zentren:
wissen.leben | WWU Münster
Formale Spezifikation
-
Ankündigung im HISLSF
- Termin: Mo+Mi 10:15 - 11:45, Leo 18
- Beginn: 16.10.2006
- Klausur: 12.02.2007, 11:45 - 14:00
- Einordnung: Die Veranstaltung kann von Wirtschaftsinformatikern als Ersatz für Software Engineering II belegt werden.
Für Informatiker zählt die Veranstaltung zum Bereich Software-Entwicklung.
- Inhalt:
- Algebraische Spezifikation (OBJ)
- Modell-basierte Spezifikation (Z,B,VDM)
- Korrektheitsbeweise, Hoare-Logik
- Theorembeweiser (Isabelle)
- Model Checking
- Grundlagen, BDDs, SAT
- Logiken (CTL,LTL)
- SMV (oder Spin)
- Alle 14 Tage wird ein Veranstaltungstermin für eine Übung genutzt.
- Folien:
- Kapitel 1+2: Einführung, Algebraische Spezifikation (Stand: 22.11.2006)
- Kapitel 3+4: Grundlagen der Logik, Spezifikationssprache Z (Stand: 22.11.2006)
- Kapitel 5: Theorembeweisen (Stand: 07.11.2006)
- Kapitel 6: Model Checking (Stand: 12.02.2007)
- Übungsaufgaben:
- Beispiele:
- Verweise:
