Inhalt

[ 921SOENFMSK13 ] KV Formal Methods in Software Development

Versionsauswahl
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 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