Inhalt
[ 921SOENFMSK13 ] KV Formal Methods in Software Development
|
|
|
| Es ist eine neuere Version 2024W dieser LV im Curriculum Masterstudium Wirtschaftsinformatik 2024W 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 2013W |
| 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 sind befähigt, Software-Werkzeuge, die diesen Prozess unterstützen, anzuwenden.
|
| 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 Beweis-Assistenten (RISC ProofNavigator), integrierten Verifikations-Umgebungen (RISC ProgramExplorer, KeY), erweiterte statische Checker (ESC/Java2), Model Checker (Spin).
|
| Beurteilungskriterien |
Übungsaufgaben (50%), Abschlussklausur (50%)
|
| Lehrmethoden |
Kombinierte Lehrveranstaltung, die theoretische Stoffvermittlung mit praktischen Demonstrationen von Systemen anhand konkreter Beispiele verbindet.
|
| Abhaltungssprache |
Englisch |
| Literatur |
Ergänzende Literatur:
- 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 |
| Äquivalenzen |
INMSPKVFMSD: KV Formal Methods in Software Development (4,5 ECTS)
|
|
|
|
| Präsenzlehrveranstaltung |
| Teilungsziffer |
- |
| Zuteilungsverfahren |
Direktzuteilung |
|
|
|
