Praktikum Automatische Verifikation reaktiver Systeme

Hinweise zum Praktikumsbetrieb WS 2000/2001         Who's afraid of... AoN [Daft]

Ort und Zeit

Wöchentliche Treffen jeweils am Montag, 15.30-17.00 Uhr, Raum 2705


Allgemeine Hinweise

  • Merkblatt 1 (16.10.2000)

  • Aufgabenblätter

  • Aufgabenblatt   1 (Woche vom 16.10.2000)
  • Aufgabenblatt   2 (Woche vom 23.10.2000)
  • Aufgabenblatt   3 (Woche vom 30.10.2000)
  • Aufgabenblatt   4 (Woche vom 06.11.2000)
  • Aufgabenblatt   5 (Woche vom 13.11.2000)
  • Aufgabenblatt   6 (Woche vom 20.11.2000)
  • Aufgabenblatt   7 (Woche vom 27.11.2000)
  • Aufgabenblatt   8 (Woche vom 04.12.2000)
  • Aufgabenblatt   9 (Woche vom 11.12.2000)
  • Aufgabenblatt 10 (Woche vom 18.12.2000)
  • Aufgabenblatt 11 (Woche vom 08.01.2001)
  • Aufgabenblatt 12 (Woche vom 15.01.2001)
  • Aufgabenblatt 13 (Woche vom 22.01.2001)
  •   Modellierung zu Blatt 13
  • Aufgabenblatt 14 (Woche vom 29.01.2001)


  • Dokumentationen und Beschreibungen der verwendeten Werkzeuge

    Unterlagen zu CCS und zur Concurrency Workbench (CWB)
  • In der SUN-Halle ist eine Version der CWB im Verzeichnis /usr/wiss/roemer/home_sun/CWB abgelegt, die mit dem Kommando cwb gestartet werden kann.
  • Manual The Edinburgh Concurrency Workbench (Version 7) (PostScript)
  • Kurzeinführung A Concurrency Workout (PostScript)
  • Online-Befehlsreferenz CWB-Kommandos

    Hinweise zur Installation für LINUX- und Windows-Anwender
  • Hinweise zum Herunterladen der CWB.
  • Der SML-Compiler muß ebenfalls installiert werden, da die CWB in dieser funktionalen Programmiersprache erstellt worden ist.

    Dokumentationen zu C-Compilerbau-Werkzeugen
  • Bison-Manual Bison - the YACC-compatible Parser Generator, Version 1.20 (PostScript)

    Dokumentationen zu den Petrinetz-basierten Werkzeugen
  • The Kit Online-Dokumentation
  • Kurzübersicht Erläuterungen zur Sprache B(PN)² und CTL/LTL-Model-Checkern (PostScript)

  • Literatur

    [CES86] E. M. Clarke, E. A. Emerson, and A. P. Sistla
    Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications
    ACM Transactions on Programming Languages and Systems, Vol. 8, no. 2, April 1986, pp. 244-263
    [CGP00] E. M. Clarke, O. Grumberg, and D. Peled
    Model Checking
    MIT Press, 2000
    [Esp95] Javier Esparza
    Skript zur Vorlesung Petrinetze
    Sommersemester 1995
    [Mil89] Robin Milner
    Communication and Concurrency
    Prentice-Hall, 1989
    [Rei86] Wolfgang Reisig
    Petrinetze
    Springer, 1986
    [Ste95] Colin Sterling
    Modal and Temporal Properties of Processes
    Preliminary Draft, Edinburgh University, 1995
    [Wal87] Introduction to a Calculus of Communicating Systems
    Technical Report, Edinburgh University 1987, CSR-227-87


    Zurück zur Hauptseite des Praktikums Automatische Verifikation reaktiver Systeme.
    Stefan Römer ( Last modification: 2000/06/29-09:28 8^) ) access counter