Type and Content

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.

• 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

Lecture

Exercise

• 1. Übung
• 2. Übung
• 3. Übung
• 4. Übung
• 5. Übung
• 6. Übung
• 7. Übung
• 8. Übung
• 9. Übung
• 10. Übung
• 11. Übung
• 12. Übung