Inhalt
[ 921SOENFMSK13 ] KV Formal Methods in Software Development
|
|
|
| Es ist eine neuere Version 2022W dieser LV im Curriculum Masterstudium Wirtschaftsinformatik 2023W vorhanden. |
|
 |
| Workload |
Ausbildungslevel |
Studienfachbereich |
VerantwortlicheR |
Semesterstunden |
Anbietende Uni |
| 4,5 ECTS |
M1 - Master 1. Jahr |
Informatik |
Wolfgang Schreiner |
3 SSt |
Johannes Kepler Universität Linz |
|
|
|
| Detailinformationen |
| Quellcurriculum |
Masterstudium Computer Science 2021S |
| Ziele |
Die Studierenden verstehen die grundlegenden Konzepte der formalen Spezifikation von Programmen und Systemen sowie des formalen Schließens über die Korrektheit von Implementierungen in Bezug auf die Spezifikation. Sie können Programme und Systeme formal spezifizieren und konkrete Software-Werkzeuge anwenden, um die Korrektheit in Bezug auf die Spezifikation sicherzustellen.
|
| Lehrinhalte |
Rolle formaler Methoden in der Software-Entwicklung, Spezifikation und Verifikation imperativer Programme (Hoare-Kalkül, Dijkstras Kalkül der schwächsten Vorbedingungen und stärksten Nachbedingungen, Relationen-Kalkül), Spezifikation und Verifikation von Java Programmen (Java Modeling Language JML), Spezifikation und Verifikation von nebenläufigen Systemen (Transitions-Systeme, temporale Logik); praktischer Umgang mit Model Checkern (RISCAL), Laufzeit-Checkern (JML/OpenJML), erweiterten statischen Checkern (ESC/Java2), automatischen Verifikations-Systemen (OpenJML), integrierten Verifikations-Umgebungen (RISC ProgramExplorer, KeY), Model Checkern für nebenläufige Systeme (Spin).
|
| Beurteilungskriterien |
Laufende Übungsaufgaben (50%), Abschlussklausur zu Semesterende (50%)
|
| Lehrmethoden |
Kombinierte Lehrveranstaltung, die die theoretische Stoffvermittlung mit praktischen Demonstrationen von Systemen anhand konkreter Beispiele verbindet.
|
| Abhaltungssprache |
Englisch |
| Literatur |
Ergänzende Literatur:
- Schreiner, Wolfgang: Thinking Programs (manuscript). Chapter "Programs", 2020.
- Apt, Krzysztof et al: Verification of Sequential and Concurrent Programs, 3rd edition, Springer, 2009.
- Beckert, B.; Hähnle, R.; Schmitt, P. H. (Eds.): Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, 2007.
- Huth, M.; Ryan, M.: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press, Cambridge, 2nd edition, 2004.
- Schumann, J. M.: Automated Theorem Proving in Software Engineering. Springer, Berlin, 2001.
Spezialliteratur in Form von Originalarbeiten.
|
| Lehrinhalte wechselnd? |
Nein |
| Sonstige Informationen |
https://risc.jku.at/courses/
|
| Äquivalenzen |
INMSPKVFMSD: KV Formal Methods in Software Development (4,5 ECTS)
|
|
|
|
| Präsenzlehrveranstaltung |
| Teilungsziffer |
- |
| Zuteilungsverfahren |
Direktzuteilung |
|
|
|
