|
Formale Methoden der Softwareentwicklung (FMSoft)7.5 ECTS (englische Bezeichnung: Formal Methods of Software Development)
(Prüfungsordnungsmodul: Vertiefungsmodul Theoretische Informatik)
Modulverantwortliche/r: Lutz Schröder Lehrende:
Lutz Schröder, Stefan Milius, Daniel Gorin
Startsemester: |
WS 2013/2014 | Dauer: |
1 Semester | Turnus: |
jährlich (SS) |
Präsenzzeit: |
56 Std. | Eigenstudium: |
169 Std. | Sprache: |
Deutsch und Englisch |
Lehrveranstaltungen:
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:
www: http://www8.cs.fau.de/ws13:fmsoft
Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
- Informatik (Master of Science)
(Po-Vers. 2010 | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsmodul Theoretische Informatik)
Dieses Modul ist daneben auch in den Studienfächern "Informatik (Bachelor of Science)" verwendbar. Details
Studien-/Prüfungsleistungen:
Formale Methoden der Softwareentwicklung (Prüfungsnummer: 151316)
- Prüfungsleistung, mündliche Prüfung, Dauer (in Minuten): 30, benotet
- Anteil an der Berechnung der Modulnote: 100.0 %
- weitere Erläuterungen:
Die Leistungen der Übung gehen in die Note der mündlichen Prüfung mit ein.
- Erstablegung: WS 2013/2014, 1. Wdh.: SS 2014 (nur für Wiederholer), 2. Wdh.: keine Wiederholung
|
|
|
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|