Praktikum Automatische Verifikation reaktiver Systeme

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

Ort und Zeit

Zeit: montags 14.00-16.00 Uhr, ab 14.10.2002
Raum: Achtung: ab sofort im Hörsaal 3 (00.06.011) !!!


Allgemeine Hinweise

  • Merkblatt 1 (14.10.2002)

  • Aufgabenblätter

  • Aufgabenblatt   1 (14.10.2002)
  • Aufgabenblatt   2 (21.10.2002)
  • Aufgabenblatt   3 (28.10.2002)
  • Aufgabenblatt   4 (04.11.2002)
  • Aufgabenblatt   5 (11.11.2002)
  • Aufgabenblatt   6 (18.11.2002)
  • Aufgabenblatt   7 (25.11.2002)
  • Aufgabenblatt   8 (02.12.2002)
  • Aufgabenblatt   9 (09.12.2002)
  • Aufgabenblatt 10 (16.12.2002)
  •     WEIHNACHTSFERIEN/HEILIGE DREI KÖNIGE
  • Aufgabenblatt 11 (13.01.2003)
  • Aufgabenblatt 12 (20.01.2003)
  • Aufgabenblatt 13 (27.01.2003)


  • 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

                                                                                                        Schneemann


    Zurück zur Hauptseite des Praktikums Automatische Verifikation reaktiver Systeme.
    Stefan Römer ( Last modification: 2002/07/03-10.01 8^) ) access counter