Formale Methoden des Softwareentwurfs (V+Ü, 5 CP)

(vormals: Formale Grundlagen der Informatik 3 (V+Ü, 6 CP))

Allgemeines

Form der Lehrveranstaltung: V2+Ü2
Veranstalter: Prof. Dr. Stefan Katzenbeisser, Dr. Sebastian Gabmeyer
Zeit: Montag, 16:15 - 18:50 Uhr
Raum: S101/A1 (Achtung: am 17. Juli in L402/1, L402/2)
Beginn: Mo, 24. April 2017
Klausur: 26.09.2017

Inhalte der Vorlesung

  • Modellierung nebenläufiger Software mit der Sprache ProMeLa
  • Formalisierung von Sicherheits- und Lebendigkeitseigenschaften mit temporaler Aussagenlogik 
  • theoretische Grundlagen von Modellprüfungsverfahren 
  • Verifikation von ProMeLa Programmen mittels des Modellprüfers SPIN 
  • Syntax, Semantik und Sequenzenkalkül für typisierte Logik erster Stufe 
  • Grundlagen der kontraktbasierten Softwarespezifikationssprache JML 
  • Dynamische Logik als eine Programmlogik erster Stufe 
  • Formale Programmverifikation durch symbolische Ausführung und Invariantenschließen 
  • Werkzeugunterstützte Verifikation von Java-Programen mit dem KeY System

Übungen

Verantwortlich für die Übungen ist Sebastian Gabmeyer. Die Organisation des Übungsbetriebs findet über den Moodle-Kurs statt.

  • Dienstag, 11:40 – 13:20 (Raum S103|175) (T: Maximillian Müller)
  • Dienstag, 11:40 – 13:20 (Raum S110|211) (T: Christian Fischer)
  • Dienstag, 15:20 –17:00 (Raum S103|112) (T: Maximillian Müller)
  • Dienstag, 15:20 –17:00 (Raum S103|12) (T: Daniel Günther)
  • Dienstag, 15:20 –17:00 (Raum S215|404K) (T: André Challier)
  • Mittwoch, 13:30 – 15:10 (Raum S101|A2) (T: David Richter)
  • Freitag, 11:40 –13:20 (Raum S103|175) (T: Dorothea Treitz)
  • Freitag, 11:40 –13:20 (Raum S113|118) (T: Jannis Weil)

Materialien

Sämtliche Materialien der Veranstaltung (Folien, Übungen, Hinweise zu Tools, etc.) werden über das Moodle zur Veranstaltung zur Verfügung gestellt.

Der Moodle-Kurs ist hier erreichbar: Moodle Kurs

Literaturhinweise

Ausgewählte Kapitel aus den folgenden Standardwerken:

  • E. M. Clarke, O. Grumberg, and D. Peled. Model checking. MIT press, 1999.
  • M. Ben-Ari. Principles of the Spin model checker. Springer Science & Business Media, 2008.
  • G. Holzmann. Spin model checker, the: primer and reference manual. Addison-Wesley Professional, 2003.
  • B. Beckert, R. Hähnle, and P. H. Schmitt. Verification of object-oriented software: The KeY approach. Springer-Verlag, 2007.

zum Seitenanfangzum Seitenanfang

A A A | Drucken Print | Impressum Impressum | Kontakt Contact | Last edited: 2 months ago