Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2013 / Formale Spezifikation und Verifikation


Inhaltsbereich

Formale Spezifikation und Verifikation

Vorlesung, 3-std., Mo 12-14, Mi 16-18, Hofmann; Übungen 2-std., Schöpp

Aktuelles

  • Informationen zur Nachklausur am 8.10.:
    • Ort: Hörsaal 2U01, Leopoldstr. 13, Haus 2
    • Einlass: ca. 14:15 Uhr
    • Beginn: 14:30 Uhr; Nach Beginn ist kein Einlass mehr möglich.
    • Bearbeitungszeit: 120 Minuten
    • Die Klausur findet ohne Hilfsmittel statt. Insbesondere sind keine schriftlichen Unterlagen, keine Taschenrechner oder andere Rechner, keine Mobiltelefone oder andere Kommunikationsmittel erlaubt.
    • Mitzubringen sind:
      • gültiger Immatrikulationsnachweis für dieses Semester
      • gültiger Personalausweis oder Pass mit Lichtbild
      • Schreibzeug (keine Rot- und Grünstifte, kein Bleistift)
      • Eigenes Papier ist nicht erforderlich und darf für die Prüfung nicht benutzt werden.
  • Der Termin für die Nachholklausur steht nun fest. Bitte melden Sie sich bis zum 1. Oktober über UniWorX an.
  • ...

Inhalt

In der Vorlesung werden Spezifikationsformalismen, Konzepte der Systemmodellierung, Grundtechniken für die Automatisierung der Verifikation, Typsysteme und statische Analyse eingeführt.

Die Vorlesung wurde in dieser Form schon einmal im WS2009/10 gehalten. Die dort abgelegten Materialien, insbesondere Folien, werden auch dieses Mal verwendet und ggf. überarbeitet.


Organisation


Zeit und Ort

Veranstaltung  Zeit  Ort Beginn
Vorlesung Mo, 12–14 c.t. Hörsaal B U101 (Oettingenstr. 67) 15.04.2013
Vorlesung Mi, 16–18 c.t. Hörsaal B U101 (Oettingenstr. 67) 17.04.2013
Übung Do, 10–12 c.t. Raum 218, Amalienstr. 73a 25.04.2013
Übung Fr, 12–14 c.t. Hörsaal B045 (Theresienstr. 39) 26.04.2013

Planung

Da die Vorlesung trotz der zwei wöchentlichen Vorlesungstermine insgesamt nur den Umfang von 3 SWS hat, findet die Vorlesung nur an den untenstehenden Terminen statt. Die Übungen finden dagegen durchgehend wöchentlich statt.

Nr. Datum Thema Folien Hinweise
1. 15.04. Organisatorisches, Aussagenlogik
Syntax, Semantik, Sudoku
Folien Kapitel 1 (1-22)
2. 22.04. KNF, DNF, Tseitin Übersetzung,
DPLL-Algorithmus, SAT-Solver, OCAML Frontend
Folien Kapitel 1
(23-39)
3. 24.04. Verifikation von Carry-Lookahead Addierwerk. Modellierung nebenlaeufiger Systeme mit Aussagenlogik ("bounded model checking") am Beispiel von Semaphor und Peterson Algorithmus.
In cnf.tgz wurde ein Programm sema2.ml neu eingefuegt, welches einen fehlerhaften Semaphor modelliert, der nicht atomar getestet und gesetzt wird.
Folien Kapitel 1
(40-51)
4. 29.04. Binäre Entscheidungsdiagramme BDDs Folien Kapitel 1 (52-63)
5. 06.05. BDDs: Implementierung, Verwendung Folien Kapitel 1 (64-72)
6. 08.05. Modellierung verteilter Systeme mit BDDs, Fixpunktiteration. Einf. Kapitel 2 (Model Checking) , Syntax und Semantik von CTL. Folien Kapitel 1 (72--Schluss). Folien Kapitel 2 (79-91)
7. 15.05. Formale Semantik von CTL. Labelling Algorithmus, am Beispiel an der Tafel detailliert durchgefuehrt. Folien Kapitel 2 (92-105)
8. 27.05. Linearzeit-Algorithmus für CTL Model Checking unter Verwendung von starken Zusammenhangskomponenten und Tarjan's Algorithmus. Vorstellung des SMV Systems. Folien Kapitel 2 (106-121)
9. 29.05. Weitere SMV Beispiele, CTL mit Fairness, Alternating Bit Protokoll. Folien Kapitel 2 (122-137)
10. 17.06. Alternating Bit Protokoll in NuSMV implementiert. Symbolisches Model-Checking fuer CTL, noch ohne Fairness. Folien Kapitel 2
(138-142). Implementierung.
11. 19.06. Symbolisches Model-Checking für CTL mit Fairness (Fehler auf Folie 65 im Beweistext wurde mittlerweile behoben.). Bounded Model Checking, LTL, Büchi Automaten. Kapitel 3 Einfuehrung. Folien Kapitel 2 (143-157). Folien Kapitel 3 (159-164)
12. 24.06. Wdh. Fairness bei Symbolischem Model Checking für CTL. Programmanalyse "Reaching Definitions", Datenflussgleichungen & constraintbasiert. Analyse "Available Expressions". Unterschied groesster vs kleinster Fixpunkt. Folien Kapitel 3 (165-180)
13. 26.06. Fixpunkttheorie, Satz von Knaster-Tarski, Berechnung von Fixpunkten durch Iteration bei endlicher Höhe, Lösung von Gleichungssystemen mit Fixpunkten.  (Hierzu wurden 5 neue Folien, alle mit Nummer 180 erstellt). Liveness von Variablen als Beispiel einer Rückwärtsanalyse. Einführung: Formulierung von Analysen als Typsystem. Folien Kapitel 3 (180-185 (10 Folien!))
14. 01.07. Formulierung von Analysen als Typsystem: Typregeln, -herleitungen, operationelle Semantik, Instrumentierung der op. Sem., semantische Korrektheit, Typinferenz. Folien Kapitel 3 (186-198)
15. 03.07. Typ- und Effektsysteme. Einfache funktionale Sprache. Einfaches Typsystem. Inferenz mit "Algorithmus W". Folien Kapitel 3 (199-209)
16. 08.07. Erläuterung der Unifikation (Funktion U). Neue Folie dazu eingestellt.  Polymorphie Typinferenz, Kontrollflussanalyse als Typsystem. Operationelle Semantik. Folien Kapitel 3
(207-219)
17. 10.07. Korrektheitsresultate für Typsysteme. Typsysteme für Seiteneffekte, Effektpolymorphie am Beispiel von Exceptions. Folien Kapitel 3 (219-236)
18. 15.07. Zusammenfassung u. Wdh Typsysteme. Hoare-Logik: Regeln, Korrektheit u. Vollständigkeit. Floyd-Hoare als Datenfluss-Version von Hoare-Logik. Neue Folien! Folien Kapitel 3 (239-248)
19. 17.07. Klausurwiederholung. Hoare-Logik für Prozeduren. Die drei Folien  249,250,251 bitte noch selbststaendig durcharbeiten.

Materialien

Eine Übersicht über alle Materialien finden Sie hier.


Übungen

Hausaufgaben sind einzeln abzugeben, sie werden korrigiert und bewertet. Die Aufgaben sind einzeln mit der erreichbaren Punktzahl gekennzeichnet. Die erreichten Übungspunkte werden auf bestandene Klausuren als Bonus angerechnet. Dabei entsprechen 100% der Übungspunkte einem Bonus in Höhe von etwa einer Klausuraufgabe (10%-14%).

Hinweis: Sie dürfen Lösungsansätze mit Kommilitonen diskutieren, jedoch muss jeder Teilnehmer seine Abgabe allein erstellen. Plagiate werden geahndet.

 


Literatur


Klausur

Bitte beachten Sie die Hinweise zur Neuregelung für die Dokumentation der Prüfungen.

Erstklausur

  • Termin: 25.07., 9-12 Uhr
  • Raum: Hörsaal A 240, Hauptgebäude
  • Die Klausur findet ohne Hilfsmittel statt. Insbesondere sind keine schriftlichen Unterlagen, keine Taschenrechner oder andere Rechner, keine Mobiltelefone oder andere Kommunikationsmittel erlaubt.

Nachklausur

  • Termin: 8.10. 14-17 Uhr
  • Raum: Hörsaal 2U01, Leopoldstr. 13, Haus 2
  • Die Klausur findet ohne Hilfsmittel statt. Insbesondere sind keine schriftlichen Unterlagen, keine Taschenrechner oder andere Rechner, keine Mobiltelefone oder andere Kommunikationsmittel erlaubt.

 

Artikelaktionen


Funktionsleiste