Inhalt

[ 921SOENFMSK13 ] KV Formal Methods in Software Development

Versionsauswahl
Es ist eine neuere Version 2021W dieser LV im Curriculum Masterstudium Wirtschaftsinformatik 2021W 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