Spezifikationstechniken

Vorlesung im Herbsttrimester 1999 an der UniBw München

Dr. Wolfram Kahl

 

 

Vorlesungsfolien

• Insgesamt: 2up, PS, 2up, PDF, 4up, PS

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

• 4. November: PVS Einführung: PS, PDF
  wift-tutorial.ps; zugehörige Phonebook-Spezifikationen in phones.dmp mittels M-x undump-pvs-file entpacken.
• 11. November: PVS Sprache und Teile des Prelude: PS, PDF
• 18. November: PVS Beweiser I: PS, PDF - Grundwissen-Folien groß: PS, PDF
• 25. November: PVS Beweiser II, Fallstudie Abwicklungssatz: PS, PDF
  A Less Elementary Tutorial ..., unwinding.dmp

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

• 23. Dezember: Modularisierung und Verfeinerung in Algebraischen Spezifikationen: PS, PDF
  Doug Smith: Mechanizing the Development of Software

Übungsblätter

• Blatt 1: Aufgabenstellung und die fehlerhafte Spezifikation
• Blatt 2: Aufgabenstellung und für Aufgabe 5 Telephonbuch.zed
• Blatt 3: Aufgabenstellung
• Blatt 4: Aufgabenstellung
• Blatt 5: Aufgabenstellung, Tutorial der Vorlesung: wift-tutorial.ps
• Blatt 6: Aufgabenstellung
• Blatt 7: Aufgabenstellung, PVS-Theorien: ggt_kgv.pvs und queues.pvs
  ggt_kgv_2.pvs enthält nützliche Hilfsaussagen und Hinweise zu den geforderten Beweisen.
  ggt_kgv_2.prf_PART1 enthält etliche der Beweise. Verwendung: Datei als ggt_kgv_2.prf in demselben Verzeichnis wie ggt_kgv_2.pvs ablegen und PVS anschliessend starten.
  Die fehlenden Beweise bleiben als Übungsaufgabe!
  ggt_kgv_2.prf enthält alle Beweise
• Blatt 8: Aufgabenstellung
  Lösung Codierung in PVS: PVS-Spezifikation PVS-Beweise
• Blatt 9: Aufgabenstellung

Scheinerwerb:

• Klausur am 19. Januar 2000, 13-15 Uhr, ohne Hilfsmittel
  (Z-Glossar und PVS-Übersicht werden ausgeteilt)

Literatur

• Jonathan Jacky: The way of Z, practical programming with formal methods, Cambridge University Press 1997, ISBN 0-521-55976-6

 

• Erhältlich in der Lehrbuchsammlung der Fakultätsbibliothek!
• Kurzfassung Z-Notation
• E. Allen Emerson: Temporal and Modal Logic, pp. 995-1072 in Handbook of Theoretical Computer Science, Volume B, edited by J. van Leeuwen, Elsevier Science Publishers, 1990

Links

• Werkzeuge und Tutorials: lokale Kopie
• Hinweise zu installierter Software beschreibt die vorhandenen Installationen der Werkzeuge der Vorlesung auf dem kommsrv.rz.unibw-muenchen.de
• Z:
  • Z archive
  • ZTC: Z type checker
  • ZANS: Z animation system
  • ISO Committee Drafts of Z standard: Final CD, August 24, 1999 - local copies: fcd.ps.gz, fcd.pdf, fcd.zip
    list of known mistakes
• PVS
  • PVS Homepage