DAWN: Petrinetzmodelle zur Verifikation verteilter Algorithmen

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.