Formale Methoden der Softwareentwicklung

Dozenten Dr Tadeusz Litak und Christoph Rauch
Umfang Vorlesung+Übung, 4 SWS, ECTS-Credits: 7,5
Zeit und Ort Di, Mi, 16:15 – 17:45, 01.255-128

Slides

The slides are protected by a password the participants of the course can obtain directly from me:

  • Oct 17: and
  • Oct 18:
  • Oct 24:
  • Nov 7:
  • Nov 14:
  • Nov 21: and in the second part
  • Nov 28: and
  • Dec 5:
  • Dec 12:
  • Dec 19:
  • Jan 9:
  • Jan 16:
  • Jan 23:
  • Jan 30:

Tutorials

Tutorial page for FMSoft

<!—

Nachrichten

  • In der ersten Woche findet am Mittwoch die Vorlesung von PD Dr. Milius statt. Die Übungen von Dr. Litak beginnen in der zweiten Woche am Mittwoch und die Vorlesung findet ab der zweiten Woche immer donnerstags statt.
  • Material zu Dynamic Frames: Folien, Handout, Paper von I.T.Kassios

Übungen

Please see dedicated webpage for these. –>

A general description

See here.

Contents

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.

  • Tools we are planning to use for the first part of the material include at least the model checker nuSMV/nuXmv.
  • Tools we are planning to use for the second part of the material include at least the framework frama-c
  • Depending on whether there is more interest in the first or in the second part (and on other factors), we will devote the remaining tutorials either to SCADE or to VeriFast, correspondingly.

Literatur

  • G. Winskel: The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.
  • Ch. Baier, J-P. Katoen, Principles of Model Checking, The MIT Press, 2008.
  • M. Huth, M. Ryan: Logic in Computer Science, Cambridge University Press, 2. Aufl., 2004.