Formale Methoden der Softwareentwicklung (FMSoft)7.5 ECTS
(englische Bezeichnung: Formal Methods of Software Development)

Lehrveranstaltungen:

• • Formale Methoden der Softwareentwicklung
    (Vorlesung mit Übung, 4 SWS, Tadeusz Litak et al., Mi, 16:15 - 17:45, Raum n.V.; Fr, 14:15 - 15:45, 02.133-113; Mi, 16.15-17.45: Raum 00.131-128, Cauerstraße 11, EG)

Inhalt:

In the first part of the course, we will engage in the formal verification of reactive systems. Students learn the syntax and semantics of the temporal logics LTL, CTL, and CTL* and their application in the specification of e.g. safety and liveness properties of systems. Simple models of systems are designed and verified using model checkers and dedicated frameworks for asynchronous and synchronous reactive systems, and the algorithms working in the background are explained.

The second part of the course focuses on functional correctness of programs; more precisely, we discuss the theory of pre- and postconditions, Hoare triples, loop invariants, and weakest (liberal) preconditions, in order to introduce automatised correctness proofs using the Hoare calculus.

Lernziele und Kompetenzen:

Students are going to acquire the following competences:

Wissen

• Reproduce the definition of syntax and semantics of temporal logics LTL, CTL, and CTL*.

• Reproduce the definition of semantics of a simple programming languages like IMP, with special focus on axiomatic semantics (Hoare rules).

• Explain how CTL can be characterised in terms of fixpoints.

Verstehen

The students understand the workings of state of the art automatic frameworks, clarifying the role of model checking algorithms, semantics and Hoare calculi in formal verification.

Anwenden

In a series of exercises, the students use state of the art tools for

• model checking

• specification and verification of reactive systems,

• verification of functional correctness or memory safety of simple programs.

Analysieren

• Choose the optimal tool for a given verification or specification problem.

• Differentiate between safety and liveness properties.

• Contrast several related temporal logics (LTL, CTL, CTL*) and properties expressible/inexpressible in each of them.

Literatur:

• G. Winskel: The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.

• M. Huth, M. Ryan: Logic in Computer Science, Cambridge University Press, 2. Aufl., 2004.
  

Weitere Informationen:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:

1. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2010 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik)
2. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2013 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik)
3. Informatik (Bachelor of Science)
   (Po-Vers. 2009s | TechFak | Informatik (Bachelor of Science) | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
4. Informatik (Bachelor of Science)
   (Po-Vers. 2009w | TechFak | Informatik (Bachelor of Science) | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
5. Informatik (Master of Science)
   (Po-Vers. 2010 | TechFak | Informatik (Master of Science) | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsmodul Theoretische Informatik)
6. Mathematik (Bachelor of Science)
   (Po-Vers. 2015w | NatFak | Mathematik (Bachelor of Science) | Module des Nebenfachs | Nebenfach Informatik | Vertiefungsmodule | Vertiefungsmodul Theoretische Informatik)

Studien-/Prüfungsleistungen:

Formale Methoden der Softwareentwicklung (Prüfungsnummer: 151316)

Prüfungsleistung, mehrteilige Prüfung, benotet

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
Die Modulnote setzt sich zu 50% aus dem Ergebnis einer 30-minütigen mündlichen Prüfung am Semesterende und zu 50% aus der Bewertung der Leistungen aus dem Übungsbetrieb zusammen.

Erstablegung: WS 2016/2017, 1. Wdh.: SS 2017 (nur für Wiederholer), 2. Wdh.: keine Wiederholung

1. Prüfer:

Tadeusz Litak,

2. Prüfer:

Stefan Milius