Spezifikationstechniken

Spezifikationstechniken

Vorlesung im Herbsttrimester 1999 an der UniBw München

Dr. Wolfram Kahl

Vorlesungsfolien

Einführung und Z

  • 7. Oktober: Einführung, Erste Schritte in Z: PS, PDF
  • 14. Oktober: Schemakalkül: PS, PDF
  • 21. Oktober: Queens, GUI, Promotion, Große Systeme: PS, PDF
  • 28. Oktober: Verfeinerung und Verifikation in Z: PS, PDF

Computerunterstützte Spezifikation und PVS

Spezifikation nebenläufiger und paralleler Systeme --- Temporallogiken und Modelchecking

  • 2. Dezember: Temporale Logik - Einführung und PLTL: PS, PDF
  • 9. Dezember: Temporale Logik - CTL und CTL*, Modelchecking: PS, PDF
  • 16. Dezember: Modelchecking Anwendungen: PS, PDF
    ``... Automation Surprises'': Paper home page, lokale Kopien: Paper: PDF, Folien: PS,

    PVS-Fingerübung: Ergänzen Sie tamagochi.pvs um die fehlenden Theorien, statten Sie insbesondere bitvector mit sinnvollen Lemmata aus, und beweisen Sie diese sowie alle TCCs.

Algebraische Spezifikationen

Übungsblätter

Scheinerwerb:

Literatur

Links