Terminierungs- und Deadlockanalyse in Komponentensystemen

Komponentensysteme und Service-Orientierte Architekturen sind i.A. verteilte Systeme mit allen Problemen, die aus diesem Bereich bekannt sind. So müssen Sicherheits- und Lebendigkeitsanforderungen sichergestellt werden. In diesem Projekt soll die automatische Prüfung von Lebendigkeitsbedingungen in Komponentensystemen und Service-orientierten Architekturen auf Basis von Web-Services und BPEL-Beschreibungen untersucht werden. Dabei sollen insbesondere keine EInschränkungen an den Grad der Parallelität und keine Einschränkungen bei Prozeduraufrufen (wie. z:B. Beschränkung der Rekursionstiefe) gemacht werden.

Ein klassischer Ansatz für nicht-rekursive Programme ist die automatische Erstellung von Petri-Netzen, die das Verhalten einer Komponente beschreiben. Diese werden dann entsprechend der Architektur zu einem Petri-Netz zusammengesetzt auf dem dann die klassischen Methoden zur Lebendigkeitsanalyse angewendet werden können. Dieser bisher existierende Ansatz hat jedoch zwei entscheidende Nachteile:

• Die Komponentenimplementierung und die Architektur des Komponentensystems muss sicherstellen, dass keine Prozedur rekursiv aufgerufen wird.
• Die Petri-Netze umfassen nur dann alle Verhalten, wenn alle Prozeduren der Komponente (und damit das Komponentensystem selbst) terminiert.
Aus diesem Grund wurde damit begonnen klassische Verfahren zur Terminierungsanalyse von Programmen auf Komponentensysteme zu übertragen, wobei zunächst nur Programme mit ausschließlich nicht-rekursiven Prozeduren betrachtet wurden.