|
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, Tadeusz Litak
Startsemester: |
WS 2014/2015 | 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 (Bachelor of Science)
(Po-Vers. 2009w | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
Dieses Modul ist daneben auch in den Studienfächern "Informatik (Master of Science)" verwendbar. Details
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 2014/2015, 1. Wdh.: SS 2015 (nur für Wiederholer), 2. Wdh.: keine Wiederholung
|
|
|
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|