Zur Hauptnavigation Zum Inhaltsbereich Zur Suche Zum Seitenfuß

Spezifikation und Verifikation
(Mastervertiefung Sommersemester 2014)

Veranstalter: Frank Heitmann
Zeit und Ort: Mittwoch, 12-14 und Freitag, 10-12 in C-221

Aktuelles:

  • [28. Mai] Literaturtipp für das LTL Model Checking: Automatentheorie und Logik von Martin Hofmann und Martin Lange. Springer, 2011. (Für uns insb. Kapitel 5 (ganz) und 11 (ohne 11.3) sowie der Satz 9.4 und das Korollar 9.5 aus Kapitel 9.)
  • [26. April] Foliensatz 1 zu CTL und LTL ist online. Als Literaturtipp: Logic in Computer Science. Modelling and Reasoning about Systems von Michael Huth und Mark Ryan. 2. Auflage, Cambridge University Press, 2004. Da findet ihr viel schönes zu LTL und CTL und zu weiteren Themen - und vorher auch zur Aussagen- und Prädikatenlogik.
  • [2. April] Foliensatz 0 ist online. Viel Spaß! :)

Termine:

  • 11. Juli, Freitag:
    • Inhalt: Programmverifikation (mit Axiomatischer Semantik)
  • 4. Juli, Freitag:
    • Inhalt: Überprüfen von Eigenschaften bei Petri Netzen (Teil 2)
  • 27. Juni, Freitag:
    • Inhalt: Model Checking Tools (insb. Spin)
  • 20. Juni, Freitag:
    • Inhalt: Kurzpräsentationen der Gruppen (Teil 2/2)
  • 18. Juni, Mittwoch:
    • Inhalt: Kurzpräsentationen der Gruppen (Teil 1/2)
  • 6. Juni, Freitag:
    • Inhalt: Überprüfen von Eigenschaften bei Petri Netzen
    • Aufgabe: Viel an eurem Thema arbeiten. Nächstes Mal gibt's Vorträge!
  • 30. Mai, Freitag:
    • Inhalt: LTL Model Checking (Fortsetzung; Foliensatz 3 unten)
      Einige Gruppen stellen ihre bisherigen Ergebnisse vor und allgemeine Diskussion.
    • Aufgabe: Weiter an eurem Thema arbeiten und die Hausaufgaben aus der VL.
  • 23. Mai, Freitag:
    • Inhalt: LTL Model Checking. (Foliensatz 3 unten)
    • Aufgabe: Weiter an eurem Thema arbeiten und die Hausaufgaben aus der VL.
  • 16. Mai, Freitag:
    • Inhalt: CTL Model Checking. (Foliensatz 2 unten)
    • Aufgabe: Weiter an eurem Thema arbeiten.
  • 9. Mai, Freitag:
    • Inhalt: Darstellung eurer bisherigen Ergebnisse/Pläne
    • Aufgabe: Weiter an eurem Thema arbeiten.
  • 25. April, Freitag:
    • Inhalt: CTL und LTL. Syntax und Semantik. (Foliensatz 1 unten)
    • Aufgabe: Weitere Einarbeitung in das Thema. Kleinen Bericht dazu vorbereiten (bis 9. Mai; ich meld mich im Laufe der nächsten Woche noch via Email bei euch)
  • 11. April, Freitag:
    • Inhalt: Themenvergabe
    • Aufgabe: Einarbeiten in das Thema (bis Freitag, 25. April)
  • 2. April, Mittwoch:
    • Inhalt: Organisatorisches. Ablauf. Einleitung. (Foliensatz 0 unten)
    • Aufgabe: Paper anschauen und ein Thema auswählen; evtl. schon einarbeiten (bis Freitag, 18. April)

Folien:

Kommentare/Inhalte:

Für Details zum Inhalt (und Ablauf) siehe den Foliensatz 0 oben. Nachfolgend die Absätze, die man auch im KVV finden kann.

Als InformatikerInnen sind wir alle in der Lage Software zu entwickeln. Wie man allerdings die Korrektheit von Software (oder zumindest wichtiger Teile davon) garantiert, ist ein schwieriges Problem. Gerade wenn es um Software in kritischen Einsatzszenarien geht, wie bspw. Software in medizinischen Kontexten, in der Raumfahrt, im Sicherheitsbereich oder Software, die viele Nutzer oder viel Geld betrifft, wird die Korrektheit von Software von besonderer Bedeutung.

In der Vorlesung sollen Hintergründe sogenannter formaler Methoden vorgestellt werden, die eine Zusicherung bzgl. der Korrektheit ermöglichen. Im Vordergrund stehen dabei Ansätze aus den Bereichen Model Checking und Theorem Proving. Kenntnisse dieser Ansätze ermöglichen einerseits die Nutzung zugehöriger Werkzeuge, die einem dann bei der Implementierung von Software (und Hardware) unterstützen können, andererseits aber auch ein tieferes Verständnis sowie die eigene Herstellung solcher Werkzeuge.

Als Vorkenntnisse sind Kenntnisse einer imperativen/objektorientierten Programmiersprache wie C/C++ oder Java hilfreich, sowie eine Grundausbildung in Mathematik und theoretischer Informatik wie sie bspw. in Hamburg in den Modulen DM und FGI1 geschieht.

Lernziel:

Erlernt werden sollen die Grundlagen und Hintergründe aktueller Ansätze zur Verifikation von Programmen. Desweiteren sollen aktuelle Werkzeuge vorgestellt werden, die den Entwurf funktional korrekter Software unterstützen.

Die ZuhörerInnen sollen nach der Veranstaltung in der Lage sein in wichtigen Fällen auf Werkzeuge zur Verifikation zurückgreifen zu können, um zu gewährleisten, dass selbst geschriebene Software/Hardware ihren Anforderungen genügt. Desweiteren sollen die TeilnehmerInnen auch die theoretischen Grundlagen dieser Werkzeuge kennenlernen sowie in der Lage sein solche Werkzeuge theoretisch oder praktisch zu entwickeln.

Vorgehen:

In der Vorlesung werden die Grundlagen und Hintergründe von Programmiersprachen und aktueller Werkzeuge zur Programmverifikation beleuchtet. Die integrierten Übungen erlauben das praktische Ausprobieren dieser Werkzeuge sowie die prototypische Implementierung eines eigenen Werkzeuges bzw. von Teilen eines solchen. Statt einer Implementierung können in den Übungen alternativ auch theoretische Fragestellungen untersucht werden.

Literatur:

Siehe Foliensatz 0 oben.
Impressum
Letzte Änderung: 10:57 23.06.2015   Seitenanfang