Formale Systeme II: Anwendung
Vorlesung im Sommersemester 2023
Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich
| Zielgruppe: | Master Informatik |
|---|---|
| Umfang: | 3 SWS, 5 ETCS, optional weitere 3 SWS / 5 ECTS (s.u.) |
| Vertiefungsfächer: | Theoretische Grundlagen und Softwaretechnik und Übersetzerbau |
| Ort: | SR 236 in Geb. 50.34 |
| Zeit: | Dienstag, 11:30 - 13:00 Uhr Freitag, 11:30 - 13:00 Uhr |
| Erstmals: | 18.04.2023 |
| Veranstaltungs-Nr.: | 2400093 |
Überblick
Methoden für die formale Spezifikation und Verifikation - zumeist auf der Basis von Logik und Deduktion - haben einen hohen Entwicklungsstand erreicht. Es ist zu erwarten, dass sie zukünftig traditionelle Softwareentwicklungsmethoden ergänzen und teilweise ersetzen werden. Formale Methoden haben den Bereich akademischer Fallstudien hinter sich gelassen, und die Softwareindustrie zeigt ernsthaftes Interesse.
Nahezu sämtliche formale Spezifikations- und Verifikationsverfahren haben zwar die gleichen theoretisch-logischen Grundlagen, wie man sie etwa in der Vorlesung "Formale Systeme" kennenlernt. Zum erfolgreichen praktischen Einsatz müssen die Verfahren aber auf die jeweiligen Anwendungen und deren charakteristischen Eigenschaften abgestimmt sein. An die Anwendung angepasst sein müssen dabei sowohl die zur Spezifikation verwendeten Sprachen als auch die zur Verifikation verwendeten Kalküle.
Auch stellt sich bei der praktischen Anwendung die Frage nach der Skalierbarkeit, Effizienz und Benutzbarkeit (Usability) der Verfahren und Werkzeuge.
Praktischer Anteil
Die Veranstaltung soll Teilnehmer:innen befähigen, ein differenziertes Bild über die Einsatzmöglichkeiten formaler Systeme aufzubauen. Daher hat diese Vorlesung zwei Anteile:
- Vorlesungs-Einheiten zur Einführung der theoretischen Grundlagen.
Frage-Einheiten und Diskussionsrunden im Plenum ergänzen diese. Es stehen Video-Aufzeichnungen für diese Inhalte zur Verfügung. - Praktische Übungen.
Jede(r) Teilnehmer(in) soll jedes Werkzeug installieren und in kleinen Aufgaben Erfahrungen mit der Formalen Methode sammeln. Dazu werden in Einzel- und Gruppenarbeit Aufgaben mit den verschiedenen Werkzeugen gelöst.
Angedachte Themen sind
- Verifikation funktionaler Eigenschaften imperativer und objekt-orientierter Programme (KeY-System)
- Systemmodellierung durch Verfeinerung (Event-B mit Rodin)
- (Probabilistisches) Model Checking (SPIN und PRISM)
- Interaktives Theorembeweisen in Logiken höherer Stufe (Isabelle/HOL)
- Techniken zur statischen Analyse von Programmen (bspw. Abstrakte Interpretation)
- Beweise von Programmeigenschaften durch Typsysteme
- Software Bounded Model Checking (bspw. JJBMC)
- Spezifikation und Verifikation von Sicherheitseigenschaften (KeY, JIF)
Vorlesungsbegleitendes Forschungspraktikum
In diesem Semester bieten wir neben der Vorlesung ein optionales begleitendes Forschungspraktikum im Umfang von insgesamt fünf Leistungspunkten (LP) (davon 2 Schlüsselqualifikation (SQ)) an. Zu Beginn der Vorlesung werden Themen vorgestellt, für die sich die Teilnehmer:innen in der ersten Vorlesungswoche bewerben können (die Plätze sind begrenzt!). Das Forschungspraktikum basiert thematisch auf in der gekoppelten Vorlesung vermittelten Inhalten. Die praktische Forschungsaktivität ist Teil einer (größeren) Forschungsaktivität des Lehrstuhls und trägt zu deren Erfolg bei.
Weitere Informationen zum Forschungspraktikum ...
Materialien und Lektüre zu den einzelnen Themen ...
finden Sie im zugehörigen ILIAS-Kurs.