Beschreibungssprachen für Geschäftsprozesse liegen zumeist in Form einer syntaktischen XML-Spezifikation vor und ihre Bedeutung ist nur umgangssprachlich formuliert, d.h. sie haben keine formale Semantik. Aufgrund der fehlenden Semantik enthalten diese Sprachen einerseits Unschärfen und anderseits ist eine Analyse von Prozessen, die in einer dieser Sprachen spezifiziert sind, mit Hilfe formaler Methoden nur schwer möglich. Stellvertretend für alle diese Sprachen untersuchen wir in diesem Projekt die Business Process Execution Language for Web Services (BPEL) und das Web Service Choreography Interface (WSCI) und entwickeln für sie eine formale Semantik. Die erarbeiteten Ansätze zur Formalisierung haben einen ganz allgemeinen Charakter und lassen sich auf alle anderen Beschreibungssprachen für Geschäftsprozesse übertragen.
Als Modellierungsmethoden verwenden wir Petrinetze und Abstract State Machines (ASMs).
Petrinetze sind ein etablierter Formalismus zur Beschreibung von Geschäftsprozessen. Sie eignen sich hervorragend, um die Kausalität der Aktivitäten und damit das dynamische Verhalten eines Geschäftsprozesses zu modellieren. Mit ASMs lassen sich vor allem Strukturen und Datenaspekte adäquat abbilden. Neben der Formalisierung der Sprachen ist der Vergleich der beiden Ansätze ein weiterer Aspekt des Projektes.
Ein weiterer interessanter Aspekt ist die Frage der Korrektheit, der von uns entwickelten formalen Semantiken. Es ist nicht möglich, formal zu beweisen, dass die Semantik die zentralen semantischen Eigenschaften der Spezifikation bewahrt, denn sowohl BPEL als auch WSCI liegen in einer informalen Spezifikation vor. Aus diesem Grund können wir nur die Plausibilität anhand der informalen Spezifikation prüfen. Hier unterscheiden sich die beiden Formalismen: Da mit ASMs Systeme auf jedem beliebigen Abstraktionsgrad formal beschrieben werden können, ist ein Vergleich des ASM-Modells mit der informalen Spezifikation direkt möglich. Das Petrinetz-Modell eines konkreten Prozesses muss hingegen simuliert und temporallogische Eigenschaften der Abläufe mit dem Verhalten des Prozesses verglichen werden.
Für die Sprache BPEL haben wir einen Compiler implementiert, der einen BPEL-Prozess in ein Petrinetz entsprechend der am Lehrstuhl entwickelten Petrinetz-Semantik für BPEL transformiert. Aufbauend auf diesem Werkzeug wollen wir im Projekt Tools4BPEL die Sprache BPEL und BPEL-Prozesse analysieren.
Aktuell: Die Entwicklung der Semantiken für BPEL ist abgeschlossen. Die Arbeiten werden im Projekt Tools4BPEL aufgegriffen und weitergeführt. Interessierte Studenten sind zur Mitarbeit in diesem Projekt eingeladen.