Praktikum Automatische Verifikation reaktiver Systeme

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

Ort und Zeit

Zeit: Montags 14.30-16.00 s.t., ab 15.10.2001
Raum: 2710 (Stammgelände)


Allgemeine Hinweise

  • Merkblatt 1 (15.10.2001)

  • Aufgabenblätter

  • Aufgabenblatt   1 (15.10.2001)
  • Aufgabenblatt   2 (22.10.2001)
  • Aufgabenblatt   3 (29.10.2001)
  • Aufgabenblatt   4 (05.11.2001)
  • Aufgabenblatt   5 (12.11.2001)
  • Aufgabenblatt   6 (19.11.2001)
  • Aufgabenblatt   7 (26.11.2001)
  • Aufgabenblatt   8 (03.12.2001)
  • Aufgabenblatt   9 (10.12.2001)
  • Aufgabenblatt 10 (17.12.2001)
  • Aufgabenblatt 11 (07.01.2002)
  • Modellierung zu Blatt 11
  • Aufgabenblatt 12 (14.01.2002)
  • Aufgabenblatt 13 (21.01.2002)
  • Aufgabenblatt 14 (28.01.2002)


  • 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
    [Kie01] Astrid Kiehn
    Skript zur Vorlesung Nichtsequentielle Systeme und nebenläufige Prozesse
    Sommersemester 2001
    (zu finden in der SUN-Halle unter ~kiehn/skript-TT-MM-JJ.ps)
    [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: 2001/06/15-15:05 8^) ) access counter