Spezifikationstechniken

Vorlesung im Herbsttrimester 2000 an der UniBw München

Dr. Wolfram Kahl

 

 

Scheinerwerb

• Klausur ohne Hilfsmittel, 17. Januar, 13:00 Uhr bis 15:00 Uhr, Komplexraum 2210A, Geb.35
  (Z-Glossar (.pdf) und die CASL-Spezifikation List_with_Order (.pdf) werden ausgeteilt)

Vorlesungsfolien

Alle Vorlesungsfolien in einer Datei: -2up.ps, -2up.pdf, -4up.ps, -4up.pdf

Vorlesungsdatum	Dateien	Thema
9. Oktober	.ps, .pdf	Einführung, Erste Schritte in Z
16. Oktober	.ps, .pdf	Schemakalkül
23. Oktober	.ps, .pdf	Schematypen, ``Promotion'', Z-Fallstudie
30. Oktober	.ps, .pdf	Z: Verfeinerung
6. November	.ps, .pdf	Algebraische Spezifikationen: Grundlagen
13. November	.ps, .pdf	Algebraische Spezifikationen: Initiale Modelle
20. November	.ps, .pdf	Algebraische Spezifikationen: Strukturierung
27. November	.ps, .pdf	Alg. Spez.: Verfeinerung, Temporale Logik: Einführung
4. Dezember	.ps, .pdf	Temporale Logik: Vergangenheit, verzweigende Zeit, CTL, SMV
11. Dezember	.ps, .pdf	Modelchecking Algorithmen, Tableau-Erfüllbarkeitstest, BDDs
18. Dezember	.ps, .pdf	KIV

 

Übungsblätter

 

Alle Übungsblätter in einer Datei: .ps, .pdf, -2up.ps, -2up.pdf

• Blatt 1: .ps, .pdf
• Blatt 2: .ps, .pdf
• Blatt 3: .ps, .pdf
• Blatt 4: .ps, .pdf
• Blatt 5: .ps, .pdf
• Blatt 6: .ps, .pdf
  Lösungsvorschläge zu Aufgabe 11: Code.casl, Code.ps, Code.pdf, HTree.casl, HTree.ps, HTree.pdf
• Blatt 7: .ps, .pdf
• Blatt 8: .ps, .pdf
• Blatt 9: .ps, .pdf - mutex0.smv, mutex.smv, mutex1.smv
• Blatt 10: .ps, .pdf - abp.smv, Sets.lhs, FiniteMaps.lhs
• Blatt 11: .ps, .pdf

Literatur

• Helmuth Partsch: Requirements-Engineering systematisch, Modellbildung für softwaregestützte Systeme, Springer 1998, Erhältlich in der Lehrbuchsammlung der Fakultätsbibliothek!
   
• Jonathan Jacky: The way of Z, practical programming with formal methods, Cambridge University Press 1997, ISBN 0-521-55976-6

 

• Erhältlich in derLehrbuchsammlung der Fakultätsbibliothek!

 
• Michael R. A. Huth and Mark D. Ryan: Logic in Computer Science, Modelling and Reasoning about Systems, Cambridge University Press, 2000, ISBN: 0-521-65200-6 hardback, 0-521-65602-9 paperback

Links

• Seite über Formale Methoden in der Virtual Library
• Die Spezifikationsnotation Z:
  • Z archive
  • Kurzfassung Z-Notation: .ps, .pdf
  • Lokale Ressourcen und weitere Links zu Z
• Die Algebraische Spezifikationssprache CASL der Common Framework Initiaive CoFI
• SMV von der Model Checking Gruppe an der CMU, lokale Kopien (nur von der UniBwM aus erreichbar):
  • smv.r2.5.4.tar.gz
  • Manual: .ps.gz, .ps, .pdf
  • Linux binary: smv-linux.gz
  • Emacs mode: smv-mode.el
  • NT binary: smv-nt2.5.zip
• KIV