Die Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Verwaltung des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Mathematik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Universität Bremen


INHALT & PFAD:
Startseite Detail


Dealock Analysis mit dem CSP-Prover



Datum: 02.11.2005
Uhrzeit: 17:15 -19:00

Ort: MZH 5210


Vortragende(r): Dr. Markus Roggenbach Homepage - Vortragende(r) (University of Wales, Swansea)

CSP-Prover ist ein interaktiver Theorembeweiser, der es erlaubt, Verfeinerungsbeweise in der Prozessalgebra CSP zu führen. CSP-Prover erlaubt insbesondere Beweise über Prozesse mit unendlichem Zustandsraum sowie Beweise über parametrisierte Prozesse. CSP-Prover wurde u.a. eingesetzt, um ausgewählte Protokolle eines elektronischen Zahlungssystems zu verifizieren.

Deadlock-Freiheit kann in CSP auch mittels Refinement ausgedrückt werden. Wesentlich komfortabler ist es jedoch, direkt über Deadlocks reden zu können.

Im Vortrag werden wir eine Erweiterung von CSP-Prover um Deadlock-Analyse vorstellen und anhand konkreter Beispiele demonstrieren.



Ansprechpartner(in) / Einladende(r):
Prof. Dr. Hans-Jörg Kreowski





zurück  

Seitenanfang  -  Impressum Zuletzt geändert durch: teuber [b]   05.05.2006 Admin-Login