|
Formale Methoden der Softwareentwicklung (FMSoft)7.5 ECTS (englische Bezeichnung: Formal Methods of Software Development)
Modulverantwortliche/r: Lutz Schröder Lehrende:
Lutz Schröder, Stefan Milius, Tadeusz Litak
Startsemester: |
WS 2015/2016 | 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: Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:
- Informatik (Bachelor of Arts (2 Fächer))
(Po-Vers. 2010 | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik)
- Informatik (Bachelor of Arts (2 Fächer))
(Po-Vers. 2013 | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik)
- Informatik (Bachelor of Science)
(Po-Vers. 2009s | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
- Informatik (Bachelor of Science)
(Po-Vers. 2009w | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
- Informatik (Master of Science)
(Po-Vers. 2010 | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsmodul Theoretische Informatik)
- 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 |
|
|
|
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|