Praktikum Automatische Verifikation reaktiver Systeme

Hinweise zum Praktikumsbetrieb WS 2003/2004         Who's afraid of... AoN [Daft]

Ort und Zeit

Zeit: Montags 14.00-15.30 Uhr s.t., ab 20.10.2003
Raum: MI-03.09.014


Allgemeine Hinweise

  • Merkblatt 1 (20.10.2003)

  • Aufgabenblätter

  • Aufgabenblatt   1 (20.10.2003)
  • Aufgabenblatt   2 (27.10.2003)
  • Aufgabenblatt   3 (03.11.2003)
  • Aufgabenblatt   4 (10.11.2003)
  • Aufgabenblatt   5 (17.11.2003)
  • Aufgabenblatt   6 (24.11.2003)
  • Aufgabenblatt   7 (01.12.2003)
  • Aufgabenblatt   8 (08.12.2003)
  • Aufgabenblatt   9 (15.12.2003)
  • Aufgabenblatt 10 (15.12.2003)
  •     WEIHNACHTSFERIEN/HEILIGE DREI KÖNIGE
  • Aufgabenblatt 11 (12.01.2004)
  • Aufgabenblatt 12 (19.01.2004)
  • Aufgabenblatt 13 (26.01.2004)
  • Aufgabenblatt 14 (02.02.2004)


  • 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
    [Kie02] Astrid Kiehn
    Vorlesung Nichtsequentielle Systeme und nebenläufige Prozesse (mit Vorlesungsunterlagen)
    Sommersemester 2002
    [Kin01] Ekkart Kindler
    Vorlesung Petrinetze (mit Vorlesungsunterlagen)
    Wintersemester 2001/2002
    [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: 2003/06/18-11.01 8^) ) access counter