Bei der informationstechnischen Umsetzung von Gescha¨ftsprozessen mit Hilfe von verteilten, service-orientierten Architekturen existieren mehrere sowohl wissenschaftlich als auch industriell relevante Fragestellungen. Neben grundsa¨tzlichen Fragen zur Korrektheit und Kompatibilita¨t verteilter Prozesse spielt auch das Auffinden geeigneter Dienste zur Dienstkomposition eine wichtige Rolle. Grundlage einer solchen Dienstsuche bilden ¨offentliche Schnittstellenbeschreibungen, die zumeist aus einer Liste der implementierten Operationen der Dienste bestehen. Um Fehler bei der Dienstkomposition zu vermeiden, sollten insbesondere bei zustandsbehafteten Diensten (wie zum Beispiel Gescha¨ftsprozessen) zusa¨tzlich Informationen zu der Abfolge der Operationen vorhanden sein. Ein formaler Ansatz zur Modellierung und Analyse der durch einen (verteilten) Gescha¨ftsprozess realisierten Abfolge von Operationen, in Form gesendeter und empfangener Nachrichten, wird in [6, 7] beschrieben. Darin wird das Prozessverhalten aus Sicht eines m¨oglichen Partners wiedergegeben und auf diese Weise eine Art Bedienungsanleitung fu¨r den Prozess bereitgestellt. Diese kann dann zur Schnittstellenbeschreibung genutzt werden und so die Dienstsuche unterstu¨tzen [7]. Abbildung 1 zeigt das Fragment eines Gescha¨ftsprozesses, in diesem Fall der Sprache WS-BPEL [8], zusammen mit der das zugeho¨rige Verhalten beschreibenden Bedienungsanleitung. Die dargestellte Aktivit¨at BiddingSequence setzt ein Ver¨außerungsverfahren um, bei dem in einer Schleife (RepeatUntil) fortlaufend eine Ausschreibung ver¨offentlicht wird (BidRequest), zu der ein Gebot abgegeben werden kann (Nachricht Bid). Die Schleife wird verlassen und das Verfahren mit einer Mitteilung beendet (BidClosure), falls ein Gebot den vordefinierten Mindestverkaufswert u¨bersteigt. Daru¨ber hinaus kann das Verfahren auch durch den Ver¨außerer vorzeitig abgebrochen werden (Nachricht Abort). Die Ausfu¨hrung der Schleife wird dabei durch drei Variablen kontrolliert ($break or $currentBid > $threshold). Zum einen enthalten $currentBid und $threshold Informationen zu dem zuletzt abgegebenen Gebot und dem Mindestverkaufswert (1000). Andererseits wird der vorzeitige Abbruch des Verfahrens durch $break gesteuert. Wie ebenfalls in Abbildung 1 dargestellt, ist die Bedienungsanleitung eines Gescha¨ftsprozesses ein Automat [7]. In diesem
$currentBid = −1 $threshold = 1000 $break = false() RepeatUntil($break or $currentBid > $threshold)
LoopSequence Invoke BidRequest
Pick OnMessage Abort $break = true()
OnMessage Bid $currentBid = $Bid Invoke BidClosure
k red irnLBid idB trean
P k Abort n ir L en BidRequest tr a P g ind BidClosure d i B
?BidRequest + !Abort + !Bid repr¨asentiert ein Pfad eine m¨ogliche Auspra¨gung des von außen sichtbaren Prozessverhaltens, wobei die Kanten des Automaten den gesendeten und empfangenen Nachrichten aus Sicht des jeweiligen Prozesspartners entsprechen. Zus¨atzlich finden sich Integrit¨atsbedingungen an die m¨oglichen Partnerprozesse in Form von Zustandsannotationen.1 Wie leicht zu erkennen ist, beschreibt die angegebene Bedienungsanleitung jedoch nicht alle denkbaren Partner der Aktivit¨at BiddingSequence. So sind beispielsweise Partnerprozesse, die zun¨achst mehrere Gebote (Nachricht Bid) senden, und erst im Anschluss die zugeho¨rigen Ausschreibungen (BidRequest) empfangen, nicht mit erfasst. Auch ist das Ende der Ver¨außerung nach einem den Mindestverkaufswert u¨bersteigenden Gebot oder einem vorzeitigen Abbruch (Nachricht Abort) nicht explizit wiedergegeben.
Die Begru¨ndung dafu¨r ist in dem zur Ableitung der Bedienungsanleitung
angewandten Verfahren zu suchen. Dieses beruht auf einer petrinetzbasierten
Modellierung der Gescha¨ftsprozesse, in der Prozessdaten zugunsten einer
durchfu¨hrbaren Analyse nicht wiedergegeben werden [
Ausgehend von dieser Prozessrepra¨sentation lassen sich die Datenabh¨angigkeiten des bedingten Kontrollflusses analysieren. Fu¨r BiddingSequence f¨allt dabei auf, dass die Bedingung der darin enthaltenen Schleife nur auf Variablen zugreift, die entweder allein durch Konstanten ($break, $threshold) oder zusa¨tzlich durch Nachrichten ($currentBid) definiert sind. Im ersteren Fall wird von statisch quasi-konstanten Variablen gesprochen, und fu¨r Bedingungen die nur auf diese Art von Variablen zugreifen von statisch quasi-konstanten Bedingungen. Der Wert einer solchen Bedingung ha¨ngt nur vom zur Prozesslaufzeit gew¨ahlten Kontrollflusspfad ab, da jeder Pfad zur Bedingung einer Belegung der darin vorkommenden Variablen mit Konstanten entspricht. Daher kann die Bedingung durch Einfu¨gen geeigneter Kontrollabha¨ngigkeiten ersetzt werden.
Die Umstrukturierungsmethode zur Erzeugung der Kontrollabha¨ngigkeiten
erfolgt in zwei Schritten. Zuna¨chst wird eine Schleife oder Verzweigung mit
statisch quasi-konstanter Bedingung in eine Normalform u¨berfu¨hrt. Diese zeichnet
sich dadurch aus, das alle (statischen) Pfade des Kontrollflusses, die fu¨r eine
Bedingungsvariable unterschiedliche Werte definieren, aufgetrennt sind. Zu diesem
Zweck werden, mit Ausnahme des Kopfs einer Schleife, alle Knoten in denen
unterschiedliche Definitionen aufeinandertreffen nacheinander aufgel¨ost. Im
Anschluss kann fu¨r eine Verzweigung die Verzweigungsbedingung auf allen Pfaden
ausgewertet und durch unbedingte Spru¨nge zu den Verzweigungszielen ersetzt
werden. Fu¨r eine Schleife laufen nun hingegen alle Definitionen fu¨r
Bedingungsvariablen im Schleifenkopf zusammen. Um auch diese aufzutrennen, wird die
Schleife im folgenden Schritt durch mehrere Schleifeninstanzen ersetzt. Jede
Instanz repr¨asentiert dabei die Ausfu¨hrung des Schleifenrumpfs fu¨r eine m¨ogliche
Belegung der Bedingungsvariablen mit Konstanten. Demnach k¨onnen die
Schleifenbedingungen in den Instanzen ebenfalls ausgewertet, und durch unbedingte
Spru¨nge zum Austrittsknoten der Schleife oder zu weiteren Instanzen ersetzt
werden. Eine ausfu¨hrliche Beschreibung der Methode ist in [
Nachstehend wird die Erweiterung der Umstrukturierungsmethode beschrieben. Diese soll auch die Elimination von Bedingungen erlauben, in denen Variablen durch eingehende Nachrichten definiert sind. Die Bedingung der Schleife in BiddingSequence entha¨lt, neben den statisch quasi-konstanten Variablen $break und $threshold, auch eine solche Variable ($currentBid). Diese Art von Variablen, und Bedingungen die nur auf diese Variablen zugreifen, werden als dynamisch quasi-konstant bezeichnet. Um die Umstrukturierungsmethode ... auch auf Schleifen und Verzweigungen mit derartigen Bedingungen anwenden zu k¨onnen, wird ein abstrakterer Instanzenbegriff beno¨tigt. Der bisher verwendete Begriff beschreibt die Ausfu¨hrung des Rumpfs einer Schleife bezu¨glich einer Belegung der Bedingungsvariablen mit Konstanten. Im Folgenden verstehen wir unter einer Schleifeninstanz die Ausfu¨hrung des Schleifenrumpfs bezu¨glich einer allgemeinen Zusicherung fu¨r den Zustandsraum der Bedingungsvariablen. Zweifelsohne ist die erstere Begriffsbildung ein Spezialfall der letzteren.
Die Zusicherungen werden dabei aus der betrachteten Bedingung
abgeleitet. Dazu wird diese zun¨achst in eine Klauselform transformiert, aus der die
Grundpr¨adikate der Bedingung bestimmt werden k¨onnen, so (currentBid4 >
threshold1) und (break4) fu¨r die Bedingung in BiddingSequence. Zwei Typen
von Pr¨adikaten mu¨ssen unterschieden werden. Zum einen ko¨nnen Pr¨adikate nur
auf statisch quasi-konstante Variablen zugreifen (break4). In diesen F¨allen
werden, wie bisher, Belegungen der Variablen mit Konstanten als Zusicherungen in
den Instanzen verwendet. Davon zu trennen sind Pr¨adikate, in denen auch
dynamisch quasi-konstante Variablen vorkommen (currentBid4 > threshold1), da
nun das Pr¨adikat auch vom Inhalt eingehender Nachrichten abh¨angig ist. Um
die dadurch gegebenen Datenabh¨angigkeiten mittels Kontrollabha¨ngigkeiten
repr¨asentieren zu k¨onnen, werden Nachrichten nicht mehr nur als Ereignisse
interpretiert, sondern zusa¨tzlich Klassen m¨oglicher Nachrichteninhalte
unterschieden.3 Dies erlaubt die Definition einer Variablen durch eine Nachricht mit
Zusicherungen fu¨r die m¨oglichen Werte der Nachricht zu verfeinern. Im erweiterten
Workflow-Graphen werden dann die Pr¨adikate mit dynamisch quasi-konstanten
Variablen auf Zusicherungen fu¨r die diese Variablen definierenden Nachrichten
zuru¨ckgefu¨hrt. In Abbildung 3 ist das Ergebnis fu¨r die Definition der Variablen
$currentBid innerhalb der Schleife aus BiddingSequence angegeben. Wie zu
erkennen, ist die urspru¨ngliche Definition der Variablen (Knoten 16 in
Abbildung 2) dupliziert und durch zwei komplementa¨re Zusicherungen an die jeweils
definierende Nachricht Bid erga¨nzt worden (assert P , assert not(P )). Die
Zu3 Die explizite Repra¨sentation von Nachrichteninhalten wurde bereits in [
!Abort + !Bid[assert P] + !Bid[assert not(P)] + ?BidRequest
?BidRequest ?BidRequest
?BidRequest + !Bid[assert not(P)] ?BidRequest ?BidRequest + !Bid[assert not(P)]
... !Bid[assert not(P)] sicherungen entsprechen dabei der positiven und negativen Variante des die Variable $currentBid enthaltenen Pr¨adikats der Schleifenbedingung, in denen die Variablen durch ihre Definitionen ersetzt wurden (P = message(Bid) > 1000).
W¨ahrend der Umstrukturierung k¨onnen die damit eingefu¨hrten Zusicherungen fu¨r relevante Nachrichten zur Beschreibung der Schleifeninstanzen genutzt werden. Das Resultat der so erweiterten Umstrukturierung ist fu¨r die Schleife aus BiddingSequence in Abbildung 4 dargestellt. Darin wurde lediglich eine einzige Instanz mit den Zusicherungen break4 = f alse(), threshold1 = 1000 und currentBid4 = message(Bid) assert not(P ) erzeugt, da die Schleifenbedingung nur fu¨r diese Zusicherungen erfu¨llt ist. Abbildung 4 zeigt ebenfalls die aus dem derart umstrukturierten Workflow-Graphen abgeleitete Bedienungsanleitung. Im Vergleich zur urspru¨nglichen Bedienungsanleitung aus Abbildung 1 sind darin nun auch solche Partner erfasst, die zwischen zwei Geboten (Bid) nicht eigens auf eine zugeho¨rige Ausschreibung (Nachricht BidRequest) warten. Zudem sind die zwei Alternativen zum Beenden des Ver¨außerungsverfahrens nun explizit wiedergegeben. So kann ein Partner das Verfahren zum einen durch Senden der Nachricht Abort abbrechen (vergleiche die durch !Abort erreichbaren Zusta¨nde). Andererseits ist, durch die eingefu¨gte Unterscheidung m¨oglicher Inhalte der Nachricht Bid (!Bid[assert message(Bid)>1000], !Bid[assert not(message(Bid)>1000)]), zudem auch das Ende nach einem den Mindestverkaufswert u¨bersteigenden Gebot des Partners repr¨asentiert. 4
In der vorliegenden Arbeit beschreiben wir einen Ansatz zur Erweiterung der
in [
Im selben Moment stellt sich aber auch die Frage nach der Notwendigkeit einer Pr¨azisierung der Prozessmodelle. So bildet die in Abbildung 1 dargestellte Bedienungsanleitung bereits eine korrekte, wenn auch unvollsta¨ndige, Beschreibung des von außen sichtbaren Verhaltens der Aktivit¨at BiddingSequence. Daher kann der Nutzen einer pr¨aziseren Bedienungsanleitung infrage gestellt werden, insbesondere im Hinblick auf die darin ver¨offentlichte, mo¨glicherweise vertrauliche, Information zum Mindestverkaufswert. Anders gestaltet sich die Situation jedoch, falls ein leicht modifizierter Prozess betrachtet wird. Ein Prozess, der beispielsweise keine Ausschreibungen sendet, dass heißt die Aktivit¨at Invoke BidRequest nicht entha¨lt, dafu¨r aber jedes Gebot mit einer entsprechenden Nachricht besta¨tigt, sollte ebenfalls durch eine Bedienungsanleitung beschrieben werden k¨onnen. Die Ableitung einer Bedienungsanleitung ist aber in diesem Fall nicht mehr m¨oglich. Stattdessen kann aufgrund der nichtdeterministischen Abbildung der Schleifenbedingung unter Verwendung des herk¨ommlichen petrinetzbasierten Prozessmodells kein nicht verklemmender Partnerprozess gefunden werden. Eine Pr¨azisierung des Prozessmodells, etwa durch Anwendung der vorgestellten Umstrukturierungsmethode, ist zur Ableitung einer Bedienungsanleitung fu¨r diesen Prozess zwingend erforderlich. Gleichzeitig muss diese nun auch die Information zum Mindestverkaufswert der Ver¨außerung bereitstellen.
In weiterfu¨hrenden Arbeiten wollen wir den vorgestellten Ansatz zun¨achst
evaluieren. Dazu soll sowohl eine Implementierung als auch eine Sammlung
realistischer Beispielprozesse zur Beurteilung der praktischen Relevanz der
Umstrukturierungsmethode verwirklicht werden. In diesem Zusammenhang stellt
sich auch die Frage nach der Abgrenzung zu vergleichbaren Ansa¨tzen der
Pr¨adikatenabstraktion [