Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

DAWN: Petrinetzmodelle zur Verifikation verteilter Algorithmen

 

Berlin: Humboldt-Universität, 1997
Informatik-Berichte, 88
German
Book
Fraunhofer ISST ()
case study; distributed algorithms; petri net; temporal logic; verification

Abstract
In dieser Arbeit werden eine Reihe klassischer verteilter Algorithmen unter Verwendung einer einheitlichen Notation (DAWN: Distributed Algorithms` Working Notation) modelliert und mit Hilfe einer Reihe aufeinander abgestimmter formaler Methoden korrekt bewiesen. DAWN bildet die Grundlage einer Methodik zum Entwurf und zur Verifikation verteilter Algorithmen. Die folgenden Prinzipien liegen der Methodik zugrunde: (I) Modellierung von Algorithmen mit Algebraischen Petrinetzen (APN). (II) Externe Transitionen und faire Kanten erweitern APNs um die für verteilten Algorithmen nötigen elementaren Konzepte. (III) Temporale Aussagen spezifizieren die Korrektheit der Algorithmen. Sie werden auf halbgeordneten Abläufen interpretiert. (IV) Integration klassischer Techniken aus der Petrinetz-Theorie mit klassischen Techniken der temporalen Logik. (V) Parametrisierung von Agentennetzwerken durch Parametrisierung der Algebren des Petrinetzes im Modell.

: http://publica.fraunhofer.de/documents/PX-45333.html