Spezifikationstechniken
Vorlesung im Herbsttrimester 2001 an der UniBw München
Dr. Wolfram Kahl
Scheinerwerb
- Klausur ohne Hilfsmittel am 18.12.2001, Gebäude 33, Raum 1101, 15.00 - 16.00 Uhr.
(Z-Glossar und die CASL-SpezifikationList_with_Order(.pdf) werden ausgeteilt.)
Termine
- Vorlesung: Do. 13:15-15:00 Uhr, HS 3101
- Übung: Di. 15:00-15:45 Uhr, HS 1101
Vorlesungsfolien
| Vorlesungsdatum | 2-up | 4-up | Thema |
| HT 2001 |  ,  |
, |
Gesamtausgabe |
| 4. Oktober | , |
, |
Einführung, Erste Schritte in Z |
| 11. Oktober | , |
, |
Schemakalkül |
| 23. Oktober | , |
, |
Framing und Promotion |
| 25. Oktober | , |
, |
Z - Verfeinerung |
| 6./8. November | , |
, |
Algebraische Spezifikationen - Grundlagen |
| 15. November | , |
, |
Algebraische Spezifikationen - Beziehungen zwischen Modellen |
| 22. November | , |
, |
Strukturierte Algebraische Spezifikationen |
| 29. November | , |
, |
Temporale Aussagenlogik linearer Zeit |
| 6. Dezember | , |
, |
Temporale Aussagenlogik verzweigender Zeit, CTL Modelchecking |
| 13. Dezember | , |
, |
Modelchecking Algorithmen, Erfüllbarkeitstest für CTL |
Übungsblätter
- Blatt 1: ,
- Blatt 2: ,
- Blatt 3: ,
- Blatt 4: ,
- Blatt 5: ,
- Blatt 6: ,
Informationen zu AVL-Bäumen sind unter anderem hier, hier und hier zu finden. - Blatt 7: Siehe Markierungen in Folien zur Vorlesung vom 29.11.2001
- Blatt 8: , mutex0.smv, mutex.smv, mutex1.smv
SMV Distribution, 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
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!
- Jim Woodcock, Jim Davies: Using Z, Specification, Refinement, and Proof, Prentice Hall 1996, Prentice Hall International Series in Computer Science
- 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
- KIV
- IBM Linux Scholar Challenge
(
-Viewer) 
(
-Viewer)