Formale Methoden der Softwareentwicklung (FMSoft)7.5 ECTS
(englische Bezeichnung: Formal Methods of Software Development)

Lehrveranstaltungen:

• • Formale Methoden der Softwareentwicklung
    (Vorlesung mit Übung, 4 SWS, Tadeusz Litak et al., Di, 12:15 - 13:45, 00.152-113; Mi, 16:15 - 17:45, 00.152-113; Bitte keine fensterlosen Räume planen!)

Inhalt:

Funktionale Korrektheit von Programmen:

• Hoare-Kalkül: Vor- und Nachbedindungen, Hoare-Tripel, Schleifeninvarianten

• Schwächste und schwächste linerale Vorbedingungen

• Spezifikation von Frame Conditions (Umgang mit Methoden in OO Sprachen)

• Automatisierung von Korrektheitsbeweisen mit dem Hoare-Kalkül

• Einfache Beispielprogramme werden erstellt und mit dem verifizierenden Compiler "Dafny" verifiziert
  

Formale Verifikation reaktiver Systeme:

• Temporallogiken: CTL, LTL CTL-Stern

• Spezifikation von Systemeingenschaften (Safety und Liveness)

• Fixpunktcharakterisierung von CTL

• Modelprüfung reaktiver Systeme

• Einfache Systemmodelle und Spezifikationen werden in nuSMV erstellt und verifiziert

Lernziele und Kompetenzen:

Die Studierenden kennen Theorie und Anwendung der Programmverifikation und Verifikation reaktiver Systeme und erklären diese.

Die Studierenden formulieren formale Spezifikationen und verifizieren mit Hilfe eines modernen Werkzeuges die Korrektheit von Programmen.

Die Studierenden erklären die Theorie und Algorithmen, die solchen Werkzeugen zugrunde liegen, und entwickeln selbstständig einfache Werkzeuge, die auf diesen Prinzipien beruhen. Außerdem übertragen die Studierenden die Prinzipien auf andere Anwendungskontexte.

Weitere Informationen:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:

1. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2010 | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik)
2. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2013 | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik)
3. Informatik (Bachelor of Science)
   (Po-Vers. 2009s | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
4. Informatik (Bachelor of Science)
   (Po-Vers. 2009w | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
5. Informatik (Master of Science)
   (Po-Vers. 2010 | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsmodul Theoretische Informatik)
6. Mathematik (Bachelor of Science)
   (Po-Vers. 2015w | Module des Nebenfachs | Nebenfach Informatik | Vertiefungsmodule | Vertiefungsmodul Theoretische Informatik)

Studien-/Prüfungsleistungen:

Formale Methoden der Softwareentwicklung (Prüfungsnummer: 151316)

Prüfungsleistung, mehrteilige Prüfung, benotet

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
Die Modulnote setzt sich zu 50% aus dem Ergebnis einer 30-minütigen mündlichen Prüfung am Semesterende und zu 50% aus der Bewertung der Leistungen aus dem Übungsbetrieb zusammen.

Erstablegung: WS 2015/2016, 1. Wdh.: SS 2016 (nur für Wiederholer), 2. Wdh.: keine Wiederholung

1. Prüfer:

Stefan Milius,

2. Prüfer:

Tadeusz Litak