Projekt: Modellieren und Verifizieren von nebenläufigen Systemen mit höheren Petrinetzen

Laufzeit: seit Oktober 1990

Schlagworte: verteilte Systeme, formale Spezifikation und Verifikation, Petrinetze, temporale Logik

Ziele:

Höhere Petrinetze (gefärbte Netze, Prädikat/Transitions-Netze) erlauben das Modellieren konkreter Datenobjekte unter Beibehaltung der Vorteile klassischer Petrinetze, wie graphische und algebraische Darstellung, Hierarchiebildung, Darstellung von Sichten, Berechnung von Invarianten. In dem Projekt wurden wichtige Erfahrungen bei der Modellierung von konkreten Beispielen gewonnen, wie verteilter, wechselseitiger Ausschluß, verteilte Termination, verteilter GGT usw. Zur Modellierung von verteilten Kontrollalgorithmen wurden gefärbte Entwurfsnetze eingeführt. Diese Netze sind gegenüber herkömmlichen gefärbten Netzen um Spezifikationskonstrukte wie faire und produktive Schaltregeln sowie um Fakten erweitert.Die Darstellung in einem einheitlichen Formalismus ermöglichte eine Systematisierung existierender sowie neuer verteilter Algorithmen. Durch diese Strukturierung konnten Kriterien isoliert werden, die die systematische Entwicklung von verteilten Algorithmen aus einer temporalen Spezifikation unterstützen. Das Entwicklungsverfahren wurde auf das Beispiel des verteilten wechselseitigen Ausschlusses angewendet und wird zur Zeit an dem allgemeineren Problem der verteilten Betriebsmittelvergabe getestet.