Home Detail

Dealock Analysis with the CSP-Prover

Lecturer: Dr. Markus Roggenbach (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.

back