50 Jahre Uni Lübeck

Institut für Theoretische Informatik

Spezifikation und Verifikation


Art und Inhalt

Titel: Spezifikation und Verifikation
Veranstalter: Völzer
Einordnung: Master-Studiengang 3. Semester, Pflicht
Inhalt:

Zentrale Bestandteile des Software- bzw. Systementwicklungsprozesses sind Spezifikation und Verifikation. Dabei müssen sehr unterschiedliche Dinge spezifiziert werden: Daten, Operationen, Use cases, Kommunikationsverhalten, Verteiltheit, Aufteilung auf Komponenten etc.

Wir lernen in der Vorlesung einführend einige Spezifikationssprachen und -techniken für verschiedene Spezifikationsziele kennen und sehen dann, wie man darauf aufbauend Systeme verifizieren kann.

Ausgewählte Inhalte:

  • Klassische Spezifikation und Verifikation imperativer sequentieller Programme
  • Spezifikation von Daten und Objekten
  • Spezifikation reaktiver Systeme, model checking
  • Spezifikation von nebenläufigen und verteilten Systemen sowie von Prozessen und Abläufen.
Buchempfehlungen:
  • K. R. Apt and E.-R. Olderog: Verification of Sequential and Concurrent Programs. 2nd ed. Springer 1997
  • W. Reisig: Petrinetze - Eine Einführung. 2. Aufl., Springer 1986

Vorlesung

Veranstalter: Völzer
Umfang: 2 SWS, 4 ECTS
Termine: Mi. 16h – 17.45h, ITCS Seminarraum Nr. 21

Übung

Umfang: 1 SWS
Termine: Mi. 17.45h – 18.30h, ITCS Seminarraum Nr. 21
Übungsblätter: Nur Uniintern zugreifbar