close

Anmelden

Neues Passwort anfordern?

Anmeldung mit OpenID

Effiziente Implementierung und Validierung der Basisalgorithmen

EinbettenHerunterladen
Universit¨
at Rostock
Studienarbeit
Effiziente Implementierung und Validierung der
Basisalgorithmen fu
¨ r Bedienungsanleitungen mit impliziter
Formelrepr¨
asentation
eingereicht am
22. M¨arz 2010
von
Andreas Lehmann
geboren am 12. Juli 1983 in G¨orlitz
Matrikel-Nr. 5203872
bei
Fakult¨
at f¨
ur Informatik und Elektrotechnik
Institut f¨
ur Informatik
Lehrstuhl Theorie der Programmiersprachen und Programmierung
Gutachter:
Prof. Dr. Karsten Wolf
Betreuer:
Niels Lohmann
Zusammenfassung
In dem Paper Petrifying Operating Guidelines for Services“ [LW10b] wurde eine impli”
zite Formeldarstellung von Bedienungsanleitungen (englisch Operating Guidelines) vorgestellt. Eine Bedienungsanleitung zu einem Service (zum Beispiel Buchen eines Fluges)
beschreibt eine Menge von Services (zum Beispiel Reiseb¨
uros), die diesen nutzen k¨onnen.
Zu dieser neuen Repr¨
asentation von Bedienungsanleitungen wurden grob Algorithmen
skizziert, zum Beispiel f¨
ur das Matching. Ein Service C passt (matcht) zu einer Bedienungsanleitung, wenn C zu der Bedienungsanleitung geh¨ort (Element der Menge ist).
In dieser Arbeit soll es darum gehen, f¨
ur die Aufgaben Matching, Accordance (ist eine
¨
Bedienungsanleitung Teilmenge einer anderen) und Aquivalenz
(beide Bedienungsanleitungen/Mengen sind identisch) effiziente Algorithmen zu finden und diese zu implementieren.
Inhaltsverzeichnis
1 Einleitung
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 Ziel der Studienarbeit . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2 Grundlagen
2.1 Serviceautomaten . . . . . . .
2.2 Annotierte Serviceautomaten
2.3 Bedienungsanleitungen . . . .
2.4 Algorithmen . . . . . . . . . .
3 Algorithmen fu
¨ r die
3.1 Matching . . . .
3.2 Accordance . . .
¨
3.3 Aquivalenz
. . .
explizite
. . . . . .
. . . . . .
. . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4
4
7
8
. 8
. 13
. 14
. 15
Formeldarstellung
18
. . . . . . . . . . . . . . . . . . . . . . . . . . 18
. . . . . . . . . . . . . . . . . . . . . . . . . . 20
. . . . . . . . . . . . . . . . . . . . . . . . . . 21
4 Implizite Formeldarstellung
4.1 Regelm¨
aßigkeiten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Mengenzuordnung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Algorithmen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
23
23
25
27
5 Algorithmen fu
29
¨ r die implizite Formeldarstellung
5.1 Datenstrukturen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5.2 Algorithmen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
6 Benchmark
40
6.1 Erstellung der Dateien . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6.2 Benchmarkverfahren . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6.3 Auswertung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
7 Zusammenfassung
48
Literaturverzeichnis
49
Erkl¨
arung
51
3
1 Einleitung
1.1 Motivation
Mit der Service orientierten Architektur (SOA) [Pap01] reagiert die Informationstechnik auf die Notwendigkeit von verteilten Systemen beziehungsweise Prozessen. Im Gegensatz zu klassischen EDV-Landschaften, in denen ein Softwareprodukt zumeist den
gesamten Gesch¨aftsprozess des Unternehmens abbildete, bedarf es heute vieler kleiner
flexibler Bausteine. Diese Bausteine in der EDV-Umgebung eines Unternehmens orientieren sich an dessen logischen Gesch¨aftsprozessen, welche durch Komposition den
gesamten Gesch¨
aftsprozess abbilden. Gesch¨aftsprozesse kapseln logische Aufgabe innerhalb eines Unternehmens. Sie erm¨oglichen es, auf entstehende Ver¨anderungen schnell
und flexibel zu reagieren. Diese Ver¨anderungen k¨onnen zum einen durch externe (aus
Sicht des Unternehmens) Regularien (zum Beispiel in liberalisierten M¨arkten) aber auch
durch Fusionen und strategische Partnerschaften mit anderen Unternehmen auftreten.
Allen diesen Ver¨
anderungen ist gemein, dass sie den Ablauf beziehungsweise die Struktur des globalen Gesch¨
aftsprozesses beeintr¨achtigen werden, zum Beispiel durch Ersatz
der Verwaltung einer Firma durch die des neuen Partners, oder aber die Anpassung an
juristische Rahmenbedingungen.
M¨
ussen die notwendigen Anpassungen an einer monolithischen EDV-Struktur vorgenommen werden, entsteht eine erhebliche Komplexit¨at. Der aus dieser Komplexit¨at resultierende Zeitaufwand stellt einen Wettbewerbsnachteil am Markt dar. W¨
urde der gesamte
Gesch¨aftsprozess des Unternehmens allerdings in einer Komposition (auch Orchestrierung genannt) von modularen Gesch¨aftsprozessen organisiert, liegt andererseits der Verdacht nah, dass sich eine Ver¨
anderung lediglich auf eine Teilmenge der Gesch¨aftsprozesse
auswirken wird. Folglich wird auch nur eine Anpassung beziehungsweise ein Austausch)
dieser Gesch¨
aftsprozesse notwendig sein. Die so gewonnene Zeit stellt einen Wettbewerbsvorteil am Markt dar.
In der Informationstechnik werden Gesch¨aftsprozesse (zum Beispiel der Abschluss eines Vertrages) beziehungsweise ihre Abbildung als Services bezeichnet. Eine verbreitete
Form von Services, bez¨
uglich ihrer Implementierung, sind Webservices [Got00]. Ein Unternehmen kann dar¨
uber hinaus seine logischen Gesch¨aftsprozesse (bis hin zum gesamten
Gesch¨aftsprozess) in Form von Services anderen Unternehmen zur Verf¨
ugung stellen, in
der Regel u
¨ber das Internet. Andere Unternehmen k¨onnen so mit angebotenen Services
ihren eigenen Gesch¨
aftsprozess unterst¨
utzen, oder aber aus der Orchestrierung einen
v¨ollig neuen Gesch¨
aftsprozess schaffen, welcher wiederum ebenfalls anderen Unternehmen, zum Beispiel als Webservice, angeboten werden kann. Aus diesem Konzept ergeben
sich drei Rollen (siehe Abbildung 1.1) in der Service orientierten Architektur:
4
1 Einleitung
• der Broker (Service Broker) u
¨bernimmt die Verwaltung der vorhandenen Services,
• der Anbieter (Service Provider) bietet (min.) einen Service an und
• der Interessent (Service Requester) fragt (min.) einen gebotenen Service nach und
m¨
ochte ihn nutzen.
Sofern der Interessent nicht nur einen Service nutzen m¨ochte, sondern durch Orchestrierung weiterer Services (angebotenen oder eigenen) einen komplexeren Service schaffen
m¨ochte, m¨
ussen gewisse Bedingungen erf¨
ullt sein. Die Orchestrierung von heterogenen
Services soll einen funktionierenden Service schaffen. Folglich m¨
ussen die verwendeten
Services geeignet (zum Beispiel ohne Deadlocks) miteinander zusammenarbeiten k¨onnen.
Jeder einzelne Service besitzt eine Beschreibung seiner Funktionalit¨at. Formen der Beschreibung sind zum Beispiel UML [OMG07], BPMN [OMG06] und WS-BPEL [A+ 07].
Diese in der Industrie verbreiteten Beschreibungssprachen sind bestenfalls semi-formal,
das heißt sie gestatten keine formale Analyse. Die formale Analyse wird aber ben¨otigt,
um eine Aussage dar¨
uber treffen zu k¨onnen, ob zwei oder mehrere Services vern¨
unftig
miteinander arbeiten k¨
onnen.
Es gibt eine Reihe von M¨
oglichkeiten, den Industriestandard WS-BPEL in formale Sys¨
teme zu u
uhren, eine Ubersicht
dar¨
uber bietet zum Beispiel [BK06]. Eines dieser
¨berf¨
¨
Verfahren ist die Uberf¨
uhrung in Workflownetze [Aal97, Aal98], einer Klasse von Petrinetzen [Rei86]. Workflownetze bilden im Wesentlichen den Kern des Gesch¨aftsprozesses
ab. Um die vor allem bei der Komposition anfallende Kommunikation formal abbilden
zu k¨onnen, nutzt man offene Netze [MRS05, LMW07]. Diese erweitern die Workflow¨
netze um ein Interface, welches die Kommunikation beschreibt. Eine Uberf¨
uhrung von
WS-BPEL in offene Netze ist m¨
oglich [Loh08]. Um eine Aussage u
¨ber das Verhalten
von Services zu machen, wird ein Formalismus ben¨otigt, der das Verhalten beschreiben
kann. In dem gew¨
ahlten Rahmen wird das Verhalten eines offenen Netzes mittels eines
Serviceautomaten [LMW07] beschrieben. Diese vernachl¨assigen weitestgehend die innere
¨
Struktur des Service und konzentrieren sich auf die Kommunikation. Eine Uberf¨
uhrung
Abbildung 1.1: Service orientierte Architektur.
5
1 Einleitung
eines offenen Netzes in einen Serviceautomaten ist nur dann sinnvoll, wenn der zugrunde liegende Service bedienbar ist [Wol09]. Ist ein Service nicht bedienbar, wurde
er mit grundlegenden Fehlern spezifiziert, das heißt es wird keinen einzigen Partnerservice geben, der mit diesem Service zusammenarbeiten kann. Bedienbarkeit ist also eine
grundlegende Voraussetzung f¨
ur jeden Service (zum Beispiel f¨
ur den Broker, diesen aufzunehmen). Nachfolgend wird Bedienbarkeit vorausgesetzt, wenn von Services die Rede
ist.
M¨ochte der Interessent einen Service mit einem anderen Service benutzen, muss er wissen, ob die Komposition geeignet arbeiten wird. Eine formale Forderung daf¨
ur ist zum
Beispiel, dass die Komposition keinen ungewollten Deadlock besitzt [Mas09]. Damit der
Broker diese Frage beantworten kann, ben¨otigt er gewisse Informationen u
¨ber die beiden
zu komponierenden Services. Da es sich bei den Services um Gesch¨aftsprozesse verschiedener Unternehmen handeln und der eigentliche Gesch¨aftsprozess zu den Geheimnissen
des Unternehmens z¨
ahlen d¨
urfte, liegt es auf der Hand, dass kein Anbieter Interesse
an der Offenlegung der internen Struktur hat. Da die Informationen dennoch ben¨otigt
werden, gibt es verschiedene Konzepte, die beiden Forderungen:
• die Entscheidbarkeit der vern¨
unftigen Zusammenarbeit
• bei gleichzeitiger Wahrung der Gesch¨aftsgeheimnisse
zu vereinen. Entweder wird dem Broker ein Public View oder eine Bedienungsanleitung [LMW07] zur Verf¨
ugung gestellt. Da das Konzept der Bedienungsanleitungen dem
der Public Views u
berlegen
ist, wird sich die Arbeit weitergehend mit diesen besch¨aftigen.
¨
Eine Bedienungsanleitung beschreibt alle m¨oglichen geeigneten Partner eines Services.
Stellt der Anbieter dem Broker die Bedienungsanleitung seines angebotenen Services
zur Verf¨
ugung, so kann der Broker diese einem potentiellen Interessenten zur Verf¨
ugung
stellen.
Die beiden Services funktionieren genau dann (zum Beispiel ungewollt deadlockfrei)
zusammen, wenn der Service zu der Bedienungsanleitung passt (das sogenannte Matching). Als Beispiel kann man sich ein Service zum Buchen eines Fluges vorstellen, den
ein Reiseb¨
uroservice nutzen m¨
ochte. Die Bedienungsanleitung des Flugbuchungsservice
beschreibt nun alle Reiseb¨
uroservices, die (deadlockfrei) mit dem Flugbuchungsservice
zusammenarbeiten k¨
onnen. Der genannte Reiseb¨
uroservice pr¨
uft nun folglich, ob er zu
dieser Menge geh¨
ort.
Eine weitere interessante Anwendung von Bedienungsanleitung ist die Frage nach der
Austauschbarkeit zweier Services zur Entwurfsentscheidung [SMB09]. F¨
ur weitergehende
Austauschbarkeitsentscheidungen, zum Beispiel zur Laufzeit, sei auf [LLSW09] verwiesen. Ein Service ist genau dann mit einem anderen Service austauschbar, wenn (min.) alle
Partner (gegebenenfalls beschr¨
ankt auf realisierte) des alten Services auch Partner des
neuen Service sind. Verfahren um dieses zu pr¨
ufen, sind Accordance (Teilmengenbezie¨
hung) und Aquivalenz.
Im oben genannten Beispiel kann es also sein, dass eine Fluglinie
ihren Gesch¨
aftsprozess umstellt und sich dadurch ihr Flugbuchungsservice ver¨andert.
Bevor sie diesen allerdings gegen¨
uber dem Broker updatet, sollte sie pr¨
ufen, ob alle Rei-
6
1 Einleitung
seb¨
uros (die den bisherigen Flugbuchungsservice nutzen), auch den neuen Service nutzen
k¨onnen. Die beiden Konzepte:
¨
• einen passenden Partner finden (beziehungsweise Uberpr¨
ufung, ob zwei Services
zueinander passen) und
• Austauschbarkeit zur Entwurfsentscheidung
sind Gegenstand dieser Studienarbeit.
1.2 Ziel der Studienarbeit
Ziel der Studienarbeit ist die effiziente Implementierung der Aufgaben Matching, Accor¨
dance und Aquivalenz
f¨
ur Bedienungsanleitungen mit impliziter Formeldarstellung.
Nach der formalen Definition der zugrunde liegenden Theorie u
¨ber Services, Bedienungs¨
anleitungen, den Konzepten f¨
ur das Matching, Accordance und die Aquivalenz
in Kapitel 2, wird in Kapitel 3 der existierende Ansatz vorgestellt werden. Der bestehende
Ansatz [LMW07], umgesetzt im Tool Fiona [MW08], arbeitet mit der expliziten Formeldarstellung. Die notwendige Theorie daf¨
ur wird in Kapitel 2 geliefert werden, so dass
sich das Kapitel 3 auf die Algorithmen und Datenstrukturen von Fiona f¨
ur die Aufgaben
¨
Matching, Accordance und Aquivalenz
konzentrieren wird.
In Kapitel 4 werden die in [LW10b] vorgestellte implizite Formeldarstellung und eine
daf¨
ur geeignete Datenrepr¨
asentation ebenso wie die dort beschriebenen Algorithmen
vorgestellt. Mit dieser Basis kann in Kapitel 5 die daraus entstandene Implementierung
Cosme eingef¨
uhrt werden. Kapitel 5 wird den Schwerpunkt auf die Algorithmen und
Datenstrukturen und die damit verbundenen Designentscheidungen legen.
Mit den beiden Tools Fiona und Cosme bietet sich eine direkte Vergleichsm¨oglichkeit, so
dass in Kapitel 6 entsprechende Benchmarks u
¨ber die Laufzeiten und Speichermengen
pr¨asentiert werden. Im letzten Kapitel 7 folgt die Zusammenfassung der Arbeit und ein
Ausblick auf weitergehende Entwicklungen.
7
2 Grundlagen
2.1 Serviceautomaten
Um Services beschreiben zu k¨
onnen, gibt es eine Reihe von Konzepten, zum Beispiel
WS-BPEL [A+ 07], UML [OMG07] und BPMN [OMG06]. Diese Konzepte sind allerdings
bestenfalls semi-formal und eignen sich daher nicht f¨
ur automatisierte Analyseverfahren.
Ein Formalismus um das Verhalten von Services beschreiben zu k¨onnen, sind Serviceau¨
tomaten [LMW07]. Eine Uberf¨
uhrung des Industriestandards WS-BPEL (Web ServicesBusiness Process Execution Language) in Serviceautomaten ist m¨oglich [Loh08].
Definition 1 (Serviceautomat)
Sei K eine Menge von Nachrichtenkan¨
alen und τ ∈
/ K ein ausgewiesenes Element f¨
ur
einen internen Schritt des Automaten. Ein Serviceautomat A = [Q, I, O, δ, q0 , Ω] ist
definiert als:
• Q ist eine Menge von Zust¨
anden,
• I ⊆ K ist eine endliche Menge von Inputkan¨
alen,
• O ⊆ K ist eine endliche Menge von Outputkan¨
alen,
• δ ⊆ Q × (I ∪ O ∪ {τ }) × Q ist eine Transitionsrelation,
• q0 ∈ Q ist der Anfangszustand und
• Ω ⊆ Q als Menge der Endzust¨
ande.
Ein Serviceautomat ist genau dann endlich, wenn Q endlich ist.
F¨
ur alle Endzust¨
ande q ∈ Ω und deren Transitions¨
uberg¨
angen [q, x, q ] muss gelten, dass
x ∈ I. In den Endzust¨
anden kann demnach nur noch empfangen aber nicht mehr gesendet
werden.
Das Interface ist definiert als Iio := I ∪ O und außerdem soll gelten, dass die In- und
Outpkan¨
ale disjunkt sind I ∩ O = ∅.putkan¨
ale disjunkt sind I ∩ O = ∅.
Die Menge der aktivierten Transitions¨
uberg¨ange sei en(q) := {x | [q, x, q ] ∈ δ}. Die
Liste der vorhandenen Kanten sei Kanten(q) := {[q, x, q ] ∈ δ}.
Ein Serviceautomat ist deterministisch, genau dann, wenn f¨
ur alle Zust¨
ande q, q , q und
alle Kan¨
ale x, [q, x, q ] ∈ δ und [q, x, q ] ∈ δ gilt: q = q .
Das Label einer Transition [q, x, q ] ∈ δ ist x. Die Schreibweise f¨
ur einen Transitix
ons¨
ubergang vom Zustand q mit dem Label x in einen Zustand q sei q → q . Das Ergebnis
¨
dieses Ubergangs
ist ein Zustand.
8
2 Grundlagen
Die Erreichbarkeit von Zust¨
anden ist induktiv definiert. Ein Zustand q ist genau dann
von einem Zustand q erreichbar, falls
• ∃[q, x, q ] ∈ δ und ∧ q von q erreichbar oder
• q=q.
Ein Serviceautomat ist genau dann reagierend, wenn f¨
ur jeden Zustand q ein Zustand
q erreichbar ist, welcher entweder ein Endzustand (q ∈ Ω) oder aber eine Transition
aktiviert, deren Label ungleich τ ist.
Beispiel
Abbildung 2.1 zeigt einen Serviceautomaten A = [Q, I, O, δ, q0 , Ω]. Die Zust¨ande sind als
Knoten und die Transition als gerichtete Kanten visualisiert. Den Labels der Transitionen
wird dabei ein !“ f¨
ur Sendetransitionen (x ∈ O) und ein ?“ f¨
ur Empfangstransitionen
”
”
(x ∈ I) vorangestellt. Endzust¨
ande werden doppelt eingekreist (hier: a5 , a7 und a8 ). Der
Startzustand ist a0 . Der Serviceautomat A ist nicht deterministisch, wegen der doppelten
τ -Transitionen des Zustandes a1 . Die Menge der aktivierten Transitions¨
uberg¨ange f¨
ur
den Zustand a3 besteht aus dem Element b ∈ Iio .
Nachfolgend wird von reagierenden Serviceautomaten ausgegangen. Das stellt in der Praxis keine Einschr¨
ankung dar, denn Serviceautomaten, welche nicht reagieren, w¨
urden
f¨
ur immer“ nicht mehr kommunizieren. Das zugrunde liegende Kommunikationsmo”
dell ist asynchron, im Gegensatz zu klassischen I/O-Automaten [Lyn96]. Es existieren
weder blockierende Sendekonzepte, noch wird die Reihenfolge der Nachrichteneing¨ange
ber¨
ucksichtigt, wie es bei kommunizierenden, endlichen Automaten [BZ83] der Fall ist.
Die Semantik der hier verwendeten Kommunikation ist implizit in der Definiton 3 gegeben.
Mit Hilfe der Serviceautomaten kann entschieden werden, ob zwei Services vern¨
unftig
zusammenarbeiten k¨
onnen. Formal bedeutet dass, dass deren Komposition deadlockfrei
und beschr¨
ankt sein muss. In dem Fall spricht man von bedienbaren Services. Die Kom-
a0
?x
a1
τ
a2
τ
a6
!a
!c
a3
a7
a4
a8
?z
!b
?y
a5
SA
Abbildung 2.1: Ein Serviceautomat [LW10b].
9
2 Grundlagen
position zweier Serviceautomaten ist ein Transitionssystem. Deren Verifikation geschieht
auf Basis des Petrinetzformalismus [Rei86] und dem Tool LoLA [Sch00]. Bevor zwei Serviceautomaten komponiert werden k¨onnen, werden zwei weitere Konzepte ben¨otigt.
Definition 2 (Interfacekompatibilit¨
at von Serviceautomaten, Partner)
Zwei Serviceautomaten A1 und A2 sind genau dann interfacekompatibel, wenn die Interfaces zu einander passen (IA1 = OA2 und IA2 = OA1 ). Sind zwei Serviceautomaten
interfacekompatibel heißen sie Partner.
F¨
ur die nachfolgenden Definitionen wird das Konzept der Multimengen (siehe [LW10b])
M : I ∪ O → N ben¨
otigt. F¨
ur die Darstellung der Multimengen wird die Listenform
gew¨ahlt (zum Beispiel [a, a, b] ist eine Multimenge mit [a, a, b](a) = 2, [a, a, b](b) = 1
und [a, a, b](x) = 0 f¨
ur alle anderen x). Die leere Multimenge wird mit [ ] dargestellt.
Die bin¨are Operation + wird elementweise ausgef¨
uhrt. Mit Bags(Iio ) ist die Menge aller
Multimengen u
ber
I
gemeint.
¨
io
Definition 3 (Komposition von Serviceautomaten)
Die Komposition A1 ⊕ A2 zweier Partner-Serviceautomaten A1 und A2 ist ein Transitionssystem. Das Transitionssystem besteht aus:
• einer Menge von Zust¨
anden QA1 ⊕A2 := QA1 × Bags(IioA1 ) × QA2 ,
• einem Startzustand q0A1 ⊕A2 := [qA1 , [ ], qA2 ],
• einer Menge von Endzust¨
anden ΩA1 ⊕A2 := [ΩA1 × {[ ]} × ΩA2 ] und
• einer Transitionsrelation δA1 ⊕A2 .
Die Transitionsrelation δA1 ⊕A2 ist induktiv definiert:
¨
• [[qA1 , M, qA2 ], [qA1 , M, qA2 ]], falls [qA1 , τ, qA1 ] ∈ δA1 (interner Ubergang
in A),
¨
• [[qA1 , M, qA2 ], [qA1 , M, qA2 ]], falls [qA2 , τ, qA2 ] ∈ δA2 (interner Ubergang
in B),
• [[qA1 , M, qA2 ], [qA1 , M + [c], qA2 ]], falls [qA1 , c, qA1 ] ∈ δA1 und c ∈ IoutA1 (Senden
von A),
• [[qA1 , M, qA2 ], [qA1 , M + [c], qA2 ]], falls [qA2 , c, qA2 ] ∈ δA2 und c ∈ IoutA2 (Senden
von B),
• [[qA1 , M + [c], qA2 ], [qA1 , M, qA2 ]], falls [qA1 , c, qA1 ] ∈ δA1 , c ∈ M und c ∈ IinA1
(Empfang von A) und
• [[qA1 , M + [c], qA2 ], [qA1 , M, qA2 ]], falls [qA2 , c, qA2 ] ∈ δA2 , c ∈ M und c ∈ IinA2
(Empfang von B)
Ein Deadlock in der Komposition zweier Serviceautomaten charakterisiert einen Zustand, in dem es nicht weiter geht, die Komposition aber nicht beendet ist. F¨
ur einen konkreten Anwendungsfall k¨
onnte das bedeuten, dass ein Reiseb¨
uroservice auf die Antwort
10
2 Grundlagen
eines Flugbuchungsservice wartet, um seine Urlaubsbuchung fertig stellen zu k¨onnen,
der Fluchbuchungsservice seinerseits aber auf eine (weitere) Information des Reiseb¨
uros
wartet.
Definition 4 (Deadlock)
In einer Komposition A1 ⊕ A2 wird ein Zustand q, der nicht zu den Endzust¨
anden
ort und keine Nachfolger hat (en(qA1 ⊕A2 ) = ∅) Deadlock oder auch
(q ∈
/ ΩA1 ⊕A2 ) geh¨
Verklemmung genannt.
Neben der Deadlockfreiheit ist auch eine Beschr¨ankung der Kommunikation erforderlich.
Das bedeutet, dass in jedem Zustand der Komposition die Anzahl der Elemente eines
jeden Nachrichtenkanals beschr¨
ankt sein muss. Es d¨
urfen sich zum Beispiel nicht unendlich viele Emails gleichzeitig im Postfach befinden. In der Praxis ist das durch die physische Beschr¨
ankung aller Kommunikationsmittel ohnehin gegeben. Die Beschr¨ankung
der Kommunikation ist dabei nicht nur eine Frage des Platzes, sondern auch der Zeit.
Ein Service, der unendlich viel kommunizieren w¨
urde, br¨auchte nicht nur unendlich viel
Platz, sondern auch unendlich viel Zeit. Allerdings kann ein Service mit einem anderen
Service gegebenenfalls unendlich lange kommunizieren, ohne unbeschr¨ankten Platz zu
ben¨otigen. Ein solches Ph¨
anomen wird als Livelock bezeichnet, es ist aber nicht Gegenstand dieser Arbeit.
Definition 5 (k-beschr¨
ankte Kommunikation)
Eine Komposition A1 ⊕ A2 ist genau dann k-beschr¨ankt, wenn f¨
ur alle vom Anfangszustand erreichbaren Zust¨
ande [qA1 , M, qA2 ] und alle Label x gilt, dass diese maximal
k-fach in der Multimenge auftreten (M (x) ≤ k).
F¨
ur k-beschr¨
ankte Kommunikation ist die Komposition zweier endlicher Serviceautomaten endlich und damit berechenbar. Basierend auf diesen Definitionen k¨onnen die Begriff
Bedienbarkeit und Strategie definiert werden.
Definition 6 (k-Strategie)
Ein Serviceautomat A2 ist genau dann eine k-Strategie f¨
ur einen Serviceautomat A1 ,
wenn deren Komposition A1 ⊕ A2 k-beschr¨
ankt ist und alle Zust¨
ande q , die vom Startzustand q0A1 ⊕A2 aus erreichbar sind, keine Deadlocks sind.
Die Menge aller k-Strategien eines Serviceautomaten A sei Stratk (A).
Definition 7 (Bedienbarkeit)
Ein Serviceautomat A ist genau dann bedienbar, wenn ein Partner-Serviceautomat AP
existiert, der eine k-Strategie f¨
ur A ist.
11
2 Grundlagen
Beispiel
Abbildung 2.2 zeigt zwei Partner-Serviceautomaten A und B, sowie deren 1-beschr¨ankte
Komposition A ⊕ B. Der Startzustand der Komposition ist [a0 , [ ], b0 ] und die Endzust¨ande sind [a7 , [ ], b4 ] und [a5 , [ ], b4 ]. Die Abbildung zeigt dabei nur Zust¨ande, die
von dem Startzustand aus erreichbar sind.
Strategien sind symmetrisch, es gilt demnach: ist ein Serviceautomat A1 Strategie eines Serviceautomat A2 , dann ist auch A2 eine Strategie f¨
ur A1 . Durch die M¨oglichkeit
¨
von internen Uberg¨
angen“ innerhalb des Services ist die Menge aller Strategien eines
”
bedienbaren Service unendlich.
Aus Sicht des Brokers, in der Service orientierten Architektur [Pap01] als Teil des Service
orientierten Computing, sind alle Strategien eines gegebenen Service von Interesse, um
deren gemeinsame Verwendbarkeit entscheiden zu k¨onnen. Um nicht f¨
ur jede Anfrage
eines Interessenten, mit dem Service C1 , die Bedienbarkeit zu allen, dem Broker bekannten und in Frage kommenden Services C2 , durch die Komposition A2 ⊕ A1 entscheiden
zu m¨
ussen, wird eine geeignete Repr¨asentation aller Strategien eines Service ben¨otigt.
A1 und A2 seien die Serviceautomaten der Services C1 und C2 .
Da die Menge aller Strategien eines bedienbaren Service unendlich groß ist, wird eine endliche Beschreibung dieser unendlichen Menge ben¨otigt. Daf¨
ur muss das Konzept der Serviceautomaten zu annotierten Serviceautomaten erweitert werden. Mit einigen zus¨
atzlichen Definitionen wird sich die Bedienungsanleitung als die gesuchte Repr¨asentation erweisen.
a0, [], b0
a0, [x], b1
a1, [ ], b1
a0
a2, [ ], b1
a6, [ ], b1
a3, [a], b1
a7, [c], b1
?x
b0
a1
τ
a2
τ
!x
a6
!a
b1
a3
a7
a4
a8
a3, [ ], b2
a4, [b], b2
a3, [y], b3
a7, [ ], b4
b2
!y
?z
!b
a4, [a,b], b1
?a
!c
?c
a4, [b, y], b3
b3
a5, [b], b3
?y
a4, [y], b4
?b
a5
A
b4
a5, [ ], b4
B
Abbildung 2.2: Zwei Serviceautomaten und deren Komposition [LW10b].
12
A⊕B
2 Grundlagen
2.2 Annotierte Serviceautomaten
Ein annotierter Serviceautomat ist ein um Boolesche Formeln erg¨anzter Serviceautomat.
Dabei werden den Zust¨
anden des Serviceautomaten Boolesche Formeln zugewiesen.
Definition 8 (Boolesche Formel)
Eine Boolesche Formel F kann in diesem Kontext aus folgenden Elementen gebildet
werden:
• Menge der g¨
ultigen Literale: Iio ∪ {τ, f inal},
• Menge der g¨
ultigen Funktionen: ∨ (Boolesches Oder) und ∧ (Boolesches Und) und
• den Wahrheitswerte f alse und true
Die Literale der Booleschen Formeln bestehen aus den Kan¨alen des Interfaces und dem
ausgewiesenem Literal final“. Zur Bildung zusammengesetzter Formeln ist keine Nega”
tion zugelassen. Dadurch existiert eine Monotonie in den Formeln. Diese Monotonie ist
sowohl Voraussetzung f¨
ur die Berechenbarkeit der Bedienungsanleitung, als auch f¨
ur die
in Kapitel 4 beschriebene implizite Formelrepr¨asentation.
Definition 9 (Annotierter Serviceautomat)
Ein annotierter Serviceautomat B := [A, Φ] erweitert einen deterministischen Serviceautomaten A um eine Annotation Φ, die jedem Zustand q ∈ A eine Boolesche Formel zuweist. Die Formel Φ(q) besteht dabei maximal aus den Literalen en(q) und dem
zus¨
atzlichem Literal final. Die Endzust¨
ande des Serviceautomaten werden bei annotierten Serviceautomaten nicht mehr ben¨
otigt. Die u
¨brigen Elemente eines Serviceautomaten
werden nachfolgend mit B statt A indiziert, ein Zustand eines annotierten Automaten
B ist demnach qB .
Die Annotation der annotierten Serviceautomaten schr¨ankt die erlaubten Literale zus¨atzlich
¨
ein. Eine Formel beschreibt die f¨
ur ihren Zustand notwendigen Uberg¨
ange, um einen
Deadlock zu vermeiden. Ausgehend von den annotierten Formel ist f¨
ur nachfolgende
Betrachtungen deren Erf¨
ullbarkeit in Abh¨angigkeit eines anderen Serviceautomaten von
Interesse.
Definition 10 (Formelerfu
¨ llbarkeit)
Sei B ein annotierter Serviceautomat. Ein Zustand qA eines Partner-Serviceautomaten
A erf¨
ullt die annotierte Formel Φ(qB ) (qA |= Φ(qB )), genau dann, wenn Φ(qB ) wahr ist
unter der Belegung β(x) f¨
ur alle Literale x.


wahr, falls x = final und qA ∈ ΩA ,
β(x) := wahr, falls x ∈ en(qA ),


falsch, sonst.
13
2 Grundlagen
Eine Formel ist genau dann g¨
ultig, wenn der zu vergleichende Zustand alle in der Formel
¨
charakterisierten Uberg¨
ange aufweißt und dessen Zugeh¨origkeit zu den Endzust¨anden
mit dem Literal final“ korrespondiert. Die erstellten Formeln werden so Deadlocksitua”
tionen in den Zustandspaaren vermeiden.
2.3 Bedienungsanleitungen
Die Erstellung einer Bedienungsanleitung f¨
ur einen Service C ist nicht Gegenstand dieser
Arbeit. Eine ausf¨
uhrliche Beschreibung liefern Lohmann, Massuthe und Wolf [LMW07].
Das Konzept der schwachen Simulationsrelation wird in weiteren Definitionen und Kapiteln ben¨
otigt und ist Grundlage f¨
ur die Einf¨
uhrung des Matchingbegriffs.
Definition 11 (Schwache Simulationsrelation)
ur zwei Serviceautomaten A1 und
Eine schwache Simulationsrelation ρ ⊆ QA1 × QA2 f¨
A2 ist induktiv definiert:
• die Anfangszust¨
ande stehen in Relation [q0A1 , q0A2 ] ∈ ρ,
• falls x = τ , [qA1 , qA2 ] ∈ ρ, [qA1 , x, qA1 ] ∈ δA1 und [qA2 , x, qA2 ] ∈ δA2 , dann auch
[qA1 , qA2 ] ∈ ρ und
• falls x = τ , [qA1 , qA2 ] ∈
und [qA1 , τ, qA1 ] ∈ δA1 , dann auch [qA1 , qA2 ] ∈ .
¨
τ -Uberg¨
ange werden gesondert behandelt. Der Serviceautomat QA2 ben¨
otigt zur Simula¨
tion des Serviceautomaten QAa folglich nicht dessen τ -Uberg¨
ange.
Mit Hilfe der schwachen Simulationsrelation kann das Matching zwischen einem annotierten Serviceautomaten B und einem Serviceautomaten A definiert werden. Aus dem
Matching l¨
asst sich anschließend die Menge aller matchenden Automaten ableiten, welche
neben der Menge aller Strategien die Definition der Bedienungsanleitung erm¨oglicht.
Definition 12 (Matching)
Ein Serviceautomat A matcht genau dann mit einem annotierten Serviceautomaten B,
wenn gilt:
• es existiert eine schwache Simulationsrelation ρ ⊆ QA × QB und
• f¨
ur alle Zustandspaare [qA , qB ] ∈ ρ gilt: qA |= Φ(qB ).
Die Menge aller Serviceautomaten, die mit dem annotierten Serviceautomaten B matchen, sei Match(B).
Die Matching-Definition erm¨
oglicht eine endliche Beschreibung der m¨oglicherweise unendlich großen Menge an passenden Serviceautomaten. Zusammen mit der Menge aller
Strategien kann nun die Bedienungsanleitung definiert werden. Eine Bedienungsanleitung ist ein annotierter Serviceautomat, der die Strategiemenge eines Service exakt beschreibt.
14
2 Grundlagen
Definition 13 (Bedienungsanleitung)
Ein deterministischer, τ -freier annotierter Serviceautomat B ist eine k-Bedienungsanleitung OGk (A) = B (f¨
ur Operating Guideline“) f¨
ur einen Serviceautomat A, falls gilt:
”
Match(OGk (A)) = Stratk (A).
F¨
ur jeden endlichen Serviceautomaten, der eine k-Strategie besitzt, kann eine k-Bedienungsanleitung erstellt werden [LMW07].
Beispiel
Abbildung 2.3 zeigt eine 1-Bedienungsanleitung OG1 (A) := [C, Φ] f¨
ur den Serviceautomaten A aus Abbildung 2.1. Die Kanten, die keinen Zielknoten besitzen, zeigen auf den
ausgewiesenen Zustand (respektive Knoten) c10 . Die annotierten Formeln charakterisieren die ben¨
otigten Transitions¨
uberg¨ange, die ein zu matchender Serviceautomat besitzen
muss. Im Startzustand c0 geht aus der Annotation Φ(q0 ) hervor, dass ein zu matchender
Serviceautomat in seinem Startzustand eine Sendetransition x ∈ O ben¨otigt.
2.4 Algorithmen
Mit der Bedienungsanleitung OG(P ) (des Providers) kann die Frage, ob ein Service
R (des Requesters) mit dem Service P bedienbar ist, effizient u
uft werden. Die¨berpr¨
¨
se Uberpr¨
ufung ist das in Definition 12 beschriebene Matching. Bedienungsanleitungen
erm¨oglichen des Weiteren die Entscheidung, ob ein Service C1 durch einen Service C2
ausgetauscht werden kann. Ein Service C1 kann ausgetauscht werden, falls der neue Service C2 Partner zu allen Partnern des alten Service C1 ist. Formal bedeutet das, dass
die Menge der Strategien von C1 Teilmenge der Strategien von C2 ist. Diese Entscheidung wird Simulation oder auch Accordance [LW10b] genannt. Die Entscheidung wird
dabei nicht auf der (unendlichen) Strategiemenge getroffen, sondern auf der Matching¨
menge. Mit Hilfe dieser Definition kann Aquivalenz
von Services, beziehungsweise deren
¨
Bedienungsanleitungen definiert und entschieden werden. Aquivalenz
ist beidseitige Accordance.
c0: !x
!x
c1: ?c ∧ (?a ∨ ?b)
?c
c2: !z ∨ final
!z
c3: final
?a
?b
c4: !y ∨ ?a
c7: !y ∨ ?b
?a
!y
c5: ?a
?b
!y
c8: !y
?a
!y
c6: final
c9: ?b
?b
[C, Φ]
Abbildung 2.3: Eine 1-Bedienungsanleitung f¨
ur A aus Abbildung 2.1 [LW10b].
15
2 Grundlagen
2.4.1 Matching
Matcht ein Serviceautomat A mit einer Bedienungsanleitung OG(C), dann kann der
Service, dessen Verhalten A beschreibt, deadlockfrei mit dem Service C, aus dem die
Bedienungsanleitung entstanden ist, zusammenarbeiten. Diese Entscheidung f¨allt bei
jedem Request beim Broker in der Service orientierten Architektur an. Der Broker, der
eine Vielzahl an Services zu verwalten hat, muss die Entscheidung demnach schnell
treffen k¨
onnen.
Definition 14 (Matching)
Ein Serviceautomat A matcht genau dann zu einer k-Bedienungsanleitung OG(C) = B,
wenn:
• eine schwache Simulationsrelation
• f¨
ur jeden Zustand [qA , qB ] ∈
⊆ QA × QB existiert und
gilt: qA |= Φ(qB ).
Daf¨
ur nutzt man eine koordinierte Tiefensuche [Sed88, CR90] durch die Serviceautomaten und pr¨
uft f¨
ur jeden entstehenden Zustand die Formelerf¨
ullbarkeit. Koordinierte
Tiefensuche bedeutet, dass bereits besuchte Elemente nicht verarbeitet werden.
2.4.2 Accordance
¨
Uberdeckt
eine Bedienungsanleitung OG(C1 ) eine Bedienungsanleitung OG(C2 ), dann
ist der Service C1 Strategie aller Strategien von C2 . Ist diese Frage entschieden, kann
ein Requester den Service C1 dem Service C2 vorziehen, respektive C2 durch C1 ersetzen. Diese Austauschentscheidung wird zur Entwurfszeit getroffen. F¨
ur weitergehende
Austauschentscheidung, zum Beispiel zur Laufzeit, siehe [LLSW09].
Definition 15 (Accordance)
Eine k-Bedienungsanleitung OG(C1 ) = B1 u
¨berdeckt, simuliert genau dann eine kBedienungsanleitung OG(C2 ) = B2 (Schreibweise: OG(C2 ) OG(C1 )), wenn:
• eine schwache Simulationsrelation
• f¨
ur jeden Zustand [qB2 , qB1 ] ∈
⊆ QB2 × QB1 existiert und
gilt: ΦB2 (qB2 ) ⇒ ΦB2 (qB1 ).
Daf¨
ur nutzt man eine koordinierte Tiefensuche [Sed88, CR90] durch die Serviceautomaten und pr¨
uft f¨
ur jeden entstehenden Zustand die Formelimplikation.
16
2 Grundlagen
¨
2.4.3 Aquivalenz
¨
Die Aquivalenz
ist beidseitige Accordance. Sind zwei Bedienungsanleitung ¨aquivalent,
¨
repr¨asentieren sie die gleiche Strategiemenge. Neben der Aquivalenz,
die aus Parallelentwicklung entstehen kann, hat bereits ein Service C mehrere Bedienungsanleitungen.
¨
Definition 16 (Aquivalenz)
Zwei k-Bedienungsanleitungen OG1 und OG2 sind genau dann ¨aquivalent (Schreibweise:
OG1 ≡ OG2 ), wenn gilt:
• OG2
OG1 und
• OG1
OG2 .
Allen genannten Algorithmen liegt die Verarbeitung der Booleschen Formeln und die
damit verbundene Komplexit¨
at zugrunde. Es gab bereits Ans¨atze, unter anderem die
Formeln mit Hilfe von BDDs darzustellen [KMW07]. Das brachte allerdings nicht den
gew¨
unschten Erfolg. In dem Paper Petrifying Operating Guidelines for Services“ [LW10b]
”
wird eine implizite Repr¨
asentation der Formeln eingef¨
uhrt. Dieses Konzept wird in Kapitel 4 vorgestellt und in Kapitel 5 wird eine effiziente Implementierung daf¨
ur gezeigt.
17
3 Algorithmen fu
¨ r die explizite Formeldarstellung
Fiona [MW08] ist der Name des Tools, welches unter anderem die Aufgaben Matching,
¨
Accordance und Aquivalenz
f¨
ur Bedienungsanleitungen und Services bearbeiten kann.
Die Algorithmen sind in Fiona als Proof-of-Konzept implementiert, das heißt, dass es in
erster Linie um deren Machbarkeit ging und weniger um eine effiziente Implementierung.
Fiona ist in der Programmiersprache C++ geschrieben und Teil der Service-Tech-Familie
(Details unter http://service-technology.org).
In diesem Kapitel werden die implementierten Algorithmen f¨
ur die genannten Aufgaben
vorgestellt und bez¨
uglich ihrer Komplexit¨at betrachtet.
3.1 Matching
Gegeben sind ein Serviceautomat A f¨
ur einen Service, der mit der Bedienungsanleitung
OG(C) = B auf Matching gepr¨
uft werden soll. Fiona bearbeitet die beiden Schritte, f¨
ur
das in Definition 14 beschriebene Matching, innerhalb einer Funktion. Dabei wird die
schwache Simulationsrelation sukzessiv aufgebaut und f¨
ur jeden entstehenden Zustand
dessen Erf¨
ullbarkeit gepr¨
uft. Das hat den Vorteil, dass gr¨oßere (schwache) Simulationsrelationen bearbeitet werden k¨
onnen, da im Falle eines vorzeitigen Abbruchs nicht die
gesamte schwache Simulationsrelation im Arbeitsspeicher vorgehalten werden musste.
Die konkrete Abarbeitung besteht aus zwei Schritten:
1. Berechnen des Startzustandes q0A und
2. pr¨
ufen, ob matcht(q0A , q0B ) wahr ist
Komplexit¨
atsbetrachtung fu
¨ r Algorithmus 1
Die eigentliche Zustandsexploration des Serviceautomaten A erfolgt dabei in Zeile 20.
Das Backtracking dieser Exploration geschieht in den Zeilen 9, 17 und 25. Bei diesen Berechnungen handelt es sich im Wesentlichen um Funktionalit¨aten des Tools LoLA [Sch00].
Bei dem Algorithmus 1 f¨
allt auf, dass die Auswertung, ob ein Zustand q ∈ ⊆ QA × QB
g¨
ultig im Sinne der Erf¨
ullbarkeit, ist, erst ganz am Ende (Z. 27f.) ausgef¨
uhrt wird. Das
bedeutet, dass in einem Zustand q gegebenenfalls in Pfade rekursiv abgestiegen wird
(Z. 14, 22), gleichwohl bereits f¨
ur q entschieden werden k¨onnte, dass er ung¨
ultig ist.
Dadurch wird gegebenenfalls deutlich mehr exploriert und damit berechnet, als unbedingt notwendig. Da es sich um einen rekursiven Algorithmus handelt, ist der Overhead
f¨
ur jeden zus¨
atzlichen Aufruf entsprechend groß (Funktionsaufruf, Stackverwaltung, et
cetera). Dieses Vorgehen arbeitet gegen den Vorteil, der durch den sukzessiven Aufbau
18
3 Algorithmen f¨
ur die explizite Formeldarstellung
Algorithmus 1 Matcht ein Serviceautomat A mit einer Bedienungsanleitung OG(C) :=
B
procedure matcht(qA , qB : states)
1: for all [qA , x, qA ] ∈ Kanten(qA ) do
2:
if x ∈
/ en(qB ) then
3:
return false
x
4:
gehe Kante x in A (qA : qA → qA )
5:
if x = τ then
x
6:
gehe Kante x in B (qB : qB → qB )
7:
if qA bekannt then
8:
if qB bekannt in qA then
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
x−1
gehe Kante x in A zur¨
uck (qA : qA → qA )
if x = τ then
x−1
gehe Kante x in B zur¨
uck (qB : qB → qB )
else
f¨
uge qB dem Wissen von qA hinzu
if not matcht(qA , qB ) then
return false
else
x−1
gehe Kante x in A1 zur¨
uck (qA : qA → qA )
x−1
gehe Kante x in B zur¨
uck (qB : qB → qB )
else
berechne neuen Zustand qA
anden von qA hinzu
f¨
uge qB den bekannten Zust¨
if not matcht(qA , qB ) then
return false
else
x−1
gehe Kante x in A zur¨
uck (qA : qA → qA )
x−1
26:
gehe Kante x in B zur¨
uck (qB : qB → qB )
27:
if τ ∈
/ en(qA ) then
28:
berechne Zuweisung von qA (β(qA ))
29:
if not (β(qA ) |= Φ(qB )) then
30:
return false
31: return true
entsteht. Die Entscheidungen, ob gewisse Elemente in einer Menge vorhanden sind (Z. 2,
27), haben lineare Komplexit¨
at, da dabei Listen durchsucht werden. F¨
ur die Verwaltung
der bereits bearbeiteten Zust¨
ande der Bedienungsanleitung innerhalb eines Zustandes
in dem Serviceautomat kommt ein Rot-Schwarz-Baum zur Anwendung. Genau genommen verwendet Fiona STL-Strukturen, deren Map-Implementierung in der Regel ein
Rot-Schwarz-Baum ist. Dessen Komplexit¨at beim Einf¨
ugen und Suchen ist logarithmisch [Sed88, CR90]. Die Entscheidung, ob ein explorierter Zustand des Serviceautomaten A bereits bekannt ist (Z. 7), erfolgt mit Algorithmen und Datenstrukturen des
Tools LoLA und ist von logarithmischer Komplexit¨at. Die Berechnung der Zuweisung
(Z. 28) hat linearen Aufwand in der L¨ange der aktivierten Transitionen und die Aus-
19
3 Algorithmen f¨
ur die explizite Formeldarstellung
wertung der G¨
ultigkeit (Z. 29) ist ebenfalls linear in der L¨ange der Formel. Bei den
Vergleichen der Kanten (Z. 2, 5, 10, 27) f¨allt auf, dass dort Zeichenketten miteinander
verglichen werden. Diese Zeichenketten sind die Namen der Kommunikationspl¨atze. Bei
konkreten Services werden in der Regel sprechende Namen“ verwendet, was zu linearen
”
Vergleichen f¨
uhrt.
3.2 Accordance
Diese beiden Schritte, f¨
ur die in Definition 15 beschriebene Accordance, werden innerhalb
einer Funktion bearbeitet. Der beim Matching beschriebene Vorteil bez¨
uglich der Zustandsexploration existiert nicht, da die beiden Bedienungsanleitungen bereits komplett
im Speicher vorhanden sein m¨
ussen.
Algorithmus 2 Simuliert eine Bedienungsanleitung OG2 = B2 eine Bedienungsanleitung OG1 = B1
procedure simuliert(qB1 , qB2 : states)
1: if (qB1 , qB2 ) bereits verarbeitet then
2:
return true
3: else
4:
merke (qB1 , qB2 ) als bereits bearbeitet
5: if not (Φ1 (qB1 ) ⇒ Φ2 (qB2 )) then
6:
return false
7: for all [qB1 , x, qB1 ] ∈ Kanten(qB1 ) do
8:
if [qB2 , x, qB2 ] ∈
/ Kanten(qB2 ) then
9:
return false
10:
if not simuliert(qB1 , qB2 ) then
11:
return false
12: return true
Komplexit¨
atsbetrachtung fu
¨ r Algorithmus 2
Analog zu dem Algorithmus 1 f¨
allt auf, dass auch im Algorithmus 2 ggf. unn¨otig weit
exploriert wird. Die Ursache ist hier allerdings eine andere: die Implikation wird zwar
am Anfang (Z. 5) gepr¨
uft, allerdings wird von dem aktuellem Zustand auch rekursiv
¨
abgestiegen, falls dieser nicht alle ben¨otigten Uberg¨
ange aufweist. Die Komplexit¨at der
Entscheidung, ob ein Zustandspaar bereits bekannt ist (Z. 1), ist logarithmisch, da ein
Rot-Schwarz-Baum zum Einsatz kommt. Das Gleiche gilt f¨
ur das Hinzuf¨
ugen eines neuen
¨
Zustandspaares (Z. 4). Der Uberpr¨
ufung der Implikation (Z. 5) geht eine Umwandlung
der beiden annotierten Formeln in die Konjunktive Normalform voraus. Dieser Vorgang
ist im schlechtesten Fall exponentiell aufwendig. Es existieren zwar Algorithmen um die
Gr¨oße der Formeln bei der Transformation linear zu behalten, diese sind allerdings nicht
in Fiona implementiert. Demnach ist die Entscheidung der Implikation insgesamt gegebenenfalls ebenfalls exponentiell aufwendig. Die eigentliche Implikationsentscheidung
20
3 Algorithmen f¨
ur die explizite Formeldarstellung
ist mit quadratischem Aufwand implementiert. Es f¨allt auf, dass stets vollst¨andig u
¨ber
alle Klauseln und Literale iteriert wird, auch wenn das nicht n¨otig w¨are. Der in Fiona implementierte Vergleich in Zeile 8 ist linear, die zugrunde liegenden Zeichenketten
verursachen allerdings die gleichen Probleme, die bereits beim Matching-Algorithmus 1
beschrieben worden sind.
¨
3.3 Aquivalenz
¨
Die beiden Schritte, f¨
ur die in Definition 16 beschriebene Aquivalenz,
werden innerhalb einer Funktion bearbeitet. Der Vorteil der Zustandsexploration (siehe MatchingAlgorithmus 1) besteht hier, analog zum Simulationsalgorithmus 2, nicht. Zur Entschei¨
dung der Aquivalenz
kann eine beidseitige Implikation genutzt werden. Theoretisch ist
¨
die Aquivalenzentscheidung auch mittels zweier Aufrufe des Simulationsalgorithmus 2
m¨oglich, allerdings erfordert dieses Vorgehen den redundanten Aufbau der schwachen
Simulationsrelation.
Algorithmus 3 Charakterisieren zwei Bedienungsanleitungen die gleichen Strategien
procedure aequivalent(qB1 , qB2 : states)
1: if (qB1 , qB2 ) bereits verarbeitet then
2:
return true
3: else
4:
merke (qB1 , qB2 ) als bereits verarbeitet
5: if not ((Φ2 (qB2 ) ⇒ Φ1 (qB1 )) ∧ (Φ1 (qB1 ) ⇒ Φ2 (qB2 ))) then
6:
return false
7: for all x ∈ en(qB1 ) do
8:
if x ∈
/ en(qB2 ) then
9:
return false
10: for all x ∈ en(qB2 ) do
11:
if x ∈
/ en(qB1 ) then
12:
return false
13: for all [qB1 , x, qB1 ] ∈ Kanten(qB1 ) do
14:
if not aequivalent(qB1 , qB2 ) then
15:
return false
16: return true
Komplexit¨
atsbetrachtung fu
¨ r Algorithmus 3
¨
Analog zu dem Simulationsalgorithmus 2 wird auch beim Aquivalenzalgorithmus
3 erst
rekursiv abgestiegen, bevor die Vollst¨andigkeit des aktuellen Zustandspaares entschieden
wird. Die Komplexit¨
at der Entscheidung, ob ein Zustandspaar bereits bekannt ist (Z. 1),
ist logarithmisch, da ein Rot-Schwarz-Baum zum Einsatz kommt. Das Gleiche gilt f¨
ur
¨
das Hinzuf¨
ugen eines neuen Zustandspaares (Z. 4). Der Uberpr¨
ufung der beiderseitigen
Implikation geht eine Umwandlung der beiden annotierten Formeln in die Konjunktive
Normalform voraus. Dieser Vorgang ist im schlechtesten Fall exponentiell aufwendig.
21
3 Algorithmen f¨
ur die explizite Formeldarstellung
Demnach ist die Entscheidung der Implikation im Worstcase ebenfalls exponentiell aufwendig. Der Vergleich, ob die Kantenmengen en(qB1 ) und en(qB2 ) identisch sind, ist sehr
aufwendig implementiert. Zuerst (Z. 7-9) wird f¨
ur jede Kante der Bedienungsanleitung
B1 gepr¨
uft, ob diese auch in B2 existiert und anschließend (Z. 10-12) noch einmal um¨
gekehrt. Da die inneren Vergleiche (Z. 8, 11) ebenfalls linear sind, ist diese Uberpr¨
ufung
von quadratischer Komplexit¨
at je Richtung. Analog zu den beiden anderen Algorithmen
(1, 2) ist jeder einzelne Vergleich (der quadratisch vielen) wieder linear in der L¨ange der
Zeichenketten.
22
4 Implizite Formeldarstellung
In diesem Kapitel wird die in [LW10b] vorgestellte Repr¨asentation der annotierten Formeln einer Bedienungsanleitung vorgestellt. Die Definitionen und Erkenntnisse sind weitestgehend aus dieser Arbeit entnommen.
Ausgang der neuen Repr¨
asentation sind Regelm¨aßigkeiten der Formeln einer Bedienungsanleitung. Voraussetzung f¨
ur die Regelm¨aßigkeiten sind folgende (nicht einschr¨ankende)
Forderungen an jede annotierte Formel ϕ:
• ϕ ist in konjunktiver Normalform
• ϕ ist reduziert
Die Regelm¨
aßigkeiten sind:
1. Alle Literale die auf Sendetransitionen basieren sind in jeder Klausel positiv.
2. Alle Literale in ϕ sind positiv.
3. Falls in einer Klausel f inal steht, dann existiert in dieser Klausel kein Literal einer
Empfangstransition.
4. Es existiert ein Zusammenhang zwischen den Pfaden des Automaten und den Literalen der Empfangstransitionen.
Nachfolgend werden die genannten Regelm¨aßigkeiten formalisiert und kurz begr¨
undet,
ausf¨
uhrliche Details und Beweise k¨onnen in [LW10b] nachgelesen werden.
4.1 Regelm¨
aßigkeiten
4.1.1 Sendeliterale sind positiv
Die Idee dahinter ist, q kann nicht Teil eines Deadlocks sein, falls ein aktivierter xSende¨
ubergang in einem Zustand q existiert. Folglich muss bereits die x-Klausel die
¨
Erf¨
ullbarkeit der Formel Φ(q) sicherstellen, ungeachtet weiterer Uberg¨
ange.
Lemma 4.1 (Erfu
¨ llbarkeit)
Sei B der annotierte Serviceautomat einer Bedienungsanleitung f¨
ur einen Service, q ∈
QB und x ∈ O. Dann wird die Formel Φ(q) durch diese Zuweisung erf¨
ullt:
β(q)(x) =
true,
false,
f¨
ur x,
sonst.
23
4 Implizite Formeldarstellung
4.1.2 Alle Literale sind positiv
Negative Literale f¨
uhren zu nicht monotonen Formeln. Die Monotonie kann inhaltlich als
¨
zus¨atzliche Option verstanden werden, d.h. ein zus¨atzlicher Ubergang
kann einen nicht
finalen Zustand in einen finalen Zustand u
uhren.
¨berf¨
Lemma 4.2 (Keine negierten Literale)
Sei B der annotierte Serviceautomat einer Bedienungsanleitung f¨
ur einen Service, q ∈
QB und Li ∈ Φ(q) eine Klausel. Dann enth¨
alt Li keine negierten Literale.
Wie Massuthe [Mas09] zeigte, ist die die Monotonie der Formeln ohnehin eine notwendige
Voraussetzung f¨
ur die Erstellung von Bedienungsanleitungen.
4.1.3 Final- und Empfangsliterale schließen sich aus
Ein Zustand ist sinnvollerweise nur dann ein Endzustand (finaler Zustand), wenn keine
Nachrichten mehr offen sind. Eine Nachricht ist offen, falls ein Service eine Nachricht
versendet, sein Partner diese aber noch nicht empfangen hat. Sind noch Nachrichten
offen, ist der Partner (respektive die Komposition) nicht im Endzustand. In Situationen
(=Zust¨
anden), in denen keine Nachrichten mehr offen sind, sind alle Empfangstransitionen deaktiviert und k¨
onnen demnach auch keinen Deadlock vermeiden.
Lemma 4.3 (Ausschluss von Empfangs- und Finalliteralen)
Sei B der annotierte Serviceautomat einer Bedienungsanleitung f¨
ur einen Service, q ∈
QB und Li ∈ Φ(q) eine Klausel. Dann gilt: (f inal ∈ Li ) ⇒ Li ∩ I = ∅.
4.1.4 Zusammenhang zwischen Pfaden und Empfangsliteralen
Hierzu gibt es insgesamt zwei Regelm¨aßigkeiten, wobei die Zweite eine Form der Umkehrung der ersten ist. Die erste Beobachtung lautet: Falls eine Klausel (eines Zustandes)
”
mit einem Empfangsliteral x existiert, so existiert ein reiner x-Pfad zu einem anderen
Zustand, mit einer Klausel, dessen Empfangsliterale Teilmenge des Ausgangszustandes
ohne das x-Literal sind.“ Das Empfangen von x kann einer Strategie S nur solange dabei
helfen einen Deadlock zu verlassen/vermeiden, wie x-Nachrichten offen sind. Wie in den
Grundlagen gezeigt, kann jede x-Nachricht maximal k-mal in einem Zustand offen sein.
¨
Nach dem Empfang der k-ten Nachricht kann kein weiterer Ubergang
in C (dem Service
aus der die Bedienungsanleitung entstanden ist) realisiert werden. Folglich tritt dieses
Problem auch in allen x-Nachfolgern von q auf, nur letztendlich ohne die M¨oglichkeit ein
weiteres x zu empfangen.
24
4 Implizite Formeldarstellung
Lemma 4.4 (Pfadexistenz)
Sei B der annotierte Serviceautomat einer Bedienungsanleitung f¨
ur einen Service, q ∈
QB und Li ∈ Φ(q) eine Klausel. Falls L ein Element x ∈ I enth¨
alt, dann existiert ein
Pfad π mit den Eigenschaften:
• π startet in q,
• π besteht nur aus x-beschrifteten Transitionen und
• π endet in einem Zustand q , f¨
ur den gilt: ∃L ∈ Φ(q ) : L ∩ I ⊆ (L ∩ I)\ {x}
Nachfolgend bezeichnet lab(π) die Menge aller Pfadtransitionen f¨
ur einen Pfad π und
len(π) die L¨
ange des Pfades.
Als Folgerung aus der obigen Definition ergibt sich, dass f¨
ur jede Klausel L eines Zustandes q ein Pfad von q nach q existiert. Im Zustand (=q ) existiert eine Klausel L mit den
Eigenschaften, dass L und die Empfangsliterale disjunkt sind, sowie die Schnittmenge
von L und den Empfangsliteralen Obermenge von lab(π) ist.
Lemma 4.5 (Pfadbedingungen)
Sei B der annotierte Serviceautomat einer Bedienungsanleitung f¨
ur einen Service, q ∈
QB und Li ∈ Φ(q) eine Klausel. Dann existiert f¨
ur jede Klausel L in Φ(q) ein Pfad von q
nach q . F¨
ur Φ(q ) gilt, dass eine Klausel L existiert, die disjunkt zu dem Empfangsliteralen ist (L ∩I = ∅) und deren Pfadtransitionen lab(π) Teilmenge der Empfangsliteralen
sind (L ∩ I ⊇ lab(π)).
Die eingangs erw¨
ahnte Umkehrung besagt, dass falls der Empfang einer x-Nachricht
in einem Zustand q zur Vermeidung von Deadlocks beitr¨agt, gilt dieses auch f¨
ur die
entsprechenden Vorg¨
angerzust¨
ande. Die M¨oglichkeit, ein x zu empfangen, besteht dann
f¨
ur die Vorg¨
angerzust¨
ande nicht.
Lemma 4.6 (Klauselzusammenhang fu
¨ r den Pfad)
Sei B der annotierte Serviceautomat einer Bedienungsanleitung f¨
ur einen Service und
[q, x, q ] ∈ δ mit x ∈ I eine Transition. Dann existiert f¨
ur jede Klausel L ∈ Φ(q ) eine
Klausel L ∈ Φ(q), so dass L ∩ I ⊆ (L ∩ I) ∪ {x}.
4.2 Mengenzuordnung
Ausgehend von den beschriebenen Beobachtungen ist es m¨oglich, drei Mengen von
Zust¨anden zu definieren.
Definition 17 (S, F und T )
Sei B der annotierte Serviceautomat einer Bedienungsanleitung f¨
ur einen Service und L
eine Klausel. Dann enthalten die Mengen S, F und T die folgenden Zust¨
ande:
• S := {q | q ∈ QB , ∃L ∈ Φ(q), L ⊆ O}
25
4 Implizite Formeldarstellung
• F := {q | q ∈ QB , ∃L ∈ Φ(q), f inal ∈ L}
• T := {q | q ∈ QB , Φ(q) = ∅}
Die Menge S charakterisiert dabei die Zust¨ande, in denen gesendet werden muss. Dies
genau dann ist der Fall, wenn die annotierte Formel Φ(q) eines Zustandes q eine Klausel
L enth¨alt, deren Literale ausschließlich Sendeliterale (O) sind. F ist analog zu S definiert,
wobei f¨
ur die Zuordnung zur Menge F eine Klausel L ∈ Φ(q) das Literal f inal enthalten
muss. In der Menge T sind die stets wahren-Zust¨ande (englisch true) enthalten, also die,
in denen es keine Formel gibt. Die R¨
uck¨
uberf¨
uhrung der impliziten in die die explizite
Formelrepr¨
asentation funktioniert nach folgendem Schema.
Definition 18 (Bit-Bedienungsanleitung)
Eine Bit-Bedienungsanleitung OG(C) := [B, S, F, T ] f¨
ur einen Service C ist eine Bedienungsanleitung nach Definition 13, deren Annotation Φ durch die Mengen S, F und T
aus Definition 17 ersetzt wird.
Beispiel
F¨
ur die Bedienungsanleitung in Abbildung 2.3 enthalten die Mengen S, F und T folgende
Zust¨ande:
• S = {c0 , c8 },
• F = {c2 , c3 , c6 } und
• T = {c10 }.
Lemma 4.7 (Ru
¨ cku
¨ berfu
¨ hrung)
Sei [B, S, F, T ] eine Bedienungsanleitung f¨
ur einen Service. Dann wird f¨
ur alle Zust¨
ande
q ∈ QB die annotierte Formel wie folgt gebildet:
Φ(q) =
∅,
{O ∩ en(q)} ,
falls q ∈ T,
falls q ∈ S,
Sonst gilt:
π
Φ(q) ≡ (O ∩ en(q)) ∪ lab(π) | q → q , len(π) > 0, q ∈ S ∪ F, lab(π) ⊆ I ∪F,
wobei F wie folgt in Abh¨
angigkeit von F definiert ist:
F :=
{(O ∩ en(q)) ∪ {f inal}} ,
∅,
falls q ∈ F,
sonst.
26
4 Implizite Formeldarstellung
Die so generierten Klauselmengen sind nicht zwangsl¨aufig reduziert.
Als Datenstruktur werden f¨
ur diese Repr¨asentation zwei Bits pro Zustand ben¨otigt,
da die Mengen S, F und T paarweise disjunkt sind. Das reduziert die Komplexit¨at
der Repr¨
asentation eines annotierten Serviceautomaten B einer Bedienungsanleitung f¨
ur
einen Service C von O(| B || C |) auf O(| B |) f¨
ur eine Bedienungsanleitung [B, S, F, T ].
Der Grund daf¨
ur ist die konstante Darstellung der Formeln statt deren linearen (in der
L¨ange des Service C) Repr¨
asentation.
4.3 Algorithmen
In diesem Abschnitt werden die f¨
ur diese Studienarbeit relevanten Algorithmen in Anlehnung an [LW10b] vorgestellt. Auf dieser Grundlage ist die in Kapitel 5 vorgestellte
Implementierung entstanden.
4.3.1 Matching
Das in Definition 14 beschriebene Matchingverfahren f¨
ur die neue Repr¨asentation arbeitet wie in Algorithmus 4 beschrieben. Dabei ist B der annotierte Serviceautomat
einer Bedienungsanleitung und A der Serviceautomat eines Service C, dessen Matching
entschieden werden soll.
Algorithmus 4 Pr¨
ufe Formelerf¨
ullbarkeit in der impliziten Repr¨asentation
procedure matcht(qB , qA : states)
1: if en(qA ) ∩ OB = ∅ then
2:
return true
3: if qB ∈ F und qA ∈
/ ΩA then
4:
return false
5: if qB ∈ S then
6:
return false
π
7: if (∃π : qB −
→ q , q ∈ S ∪ F, ∅ = lab(π) ⊆ IB \ en(qA )) then
8:
return false
9: return true
4.3.2 Accordance
Das in Definition 15 beschriebene Accordanceverfahren f¨
ur die neue Repr¨asentation ist
im Algorithmus 5 beschrieben. Dabei ist [B1 , S1 , F1 , T1 ] die vermeintlich kleinere und
[B2 , S2 , F2 , T2 ] die vermeintlich gr¨
oßere Bedienungsanleitung.
27
4 Implizite Formeldarstellung
Algorithmus 5 Pr¨
ufe Formelimplikation in der impliziten Repr¨asentation
procedure simuliert(qB1 , qB2 : states)
1: if not ((qB2 ∈ S2 ) ⇒ qB1 ∈ S1 ) then
2:
return false
3: if not ((qB2 ∈ F2 ) ⇒ qB1 ∈ S1 ∪ F1 ) then
4:
return false
5: if not ((qB1 ∈ T1 ) ⇒ qB2 ∈ T2 ) then
6:
return false
7: return true
¨
4.3.3 Aquivalenz
¨
Das in Definition 16 beschriebene Aquivalenzverfahren
f¨
ur die neue Repr¨asentation implementiert der Algorithmus 6.
Algorithmus 6 Pr¨
ufe Formel¨
aquivalenz in der impliziten Repr¨asentation
procedure aequivalent(qB1 , qB2 : states)
1: if not ((qB1 ∈ S1 ) ⇔ qB2 ∈ S2 ) then
2:
return false
3: if not ((qB1 ∈ F1 ) ⇔ qB2 ∈ F2 ) then
4:
return false
5: if not ((qB1 ∈ T1 ) ⇔ qB2 ∈ T2 ) then
6:
return false
7: return true
28
5 Algorithmen fu
¨ r die implizite Formeldarstellung
Basierend auf der in Kapitel 4 vorgestellten impliziten Formelrepr¨asentation und dem
existierenden Tool Fiona in Kapitel 3 wird in diesem Kapitel das Ergebnis dieser Studienarbeit vorgestellt. Das hier vorgestellte Tool wird mit Cosme“ bezeichnet. Cosme
”
steht dabei f¨
ur C(hecking) O(perating guidelines for) S(imulation,) M(atching and)
”
E(quivalence)“ und konzentriert sich auch ausschließlich auf diese Anwendungsgebiete.
Mit Cosme ist es demnach m¨
oglich
1. zwei gegebene Bedienungsanleitung auf Simulation,
¨
2. zwei gegebene Bedienungsanleitung auf Aquivalenz
und
3. einen Service mit einer Bedienungsanleitung auf Matching
zu u
ufen.
¨berpr¨
In diesem Kapitel wird f¨
ur den Begriff Accordance h¨aufig der Begriff Simulation verwendet. Ist die schwache Simulationsrelation gemeint, wird dies explizit erw¨ahnt.
Zu Beginn werden die ben¨
otigten und zum Teil neu geschaffenen Datenstrukturen vor¨
gestellt. Danach folgt ein Uberblick u
¨ber die notwendigen Arbeitsschritte der einzelnen
Anwendungsgebiete. Anschließend werden die verwendeten Algorithmen vorgestellt und
die wichtigsten Designentscheidungen begr¨
undet. Zu der Vorstellung der Algorithmen
geh¨ort eine zu Kapitel 3 vergleichbare Komplexit¨atsbetrachtung.
5.1 Datenstrukturen
5.1.1 BitSetC
Mit Hilfe der BitSetC-Klasse k¨
onnen beliebig lange Bitsets verwaltet werden. Bitsets sind
eine effiziente Implementierung von Mengen. Der Basistyp ist standardm¨aßig 32-Bit lang,
so dass 32 verschiedene Elemente unterschieden werden k¨onnen. Mit den Bitsets ist es
m¨oglich, Mengenvergleiche mit linearem Aufwand in der L¨ange des Basistyps vorzunehmen. Da in der Praxis Services, hier die Serviceautomaten und Bedienungsanleitungen,
selten mehr als 32 Interfacenamen besitzen, ist der Aufwand in diesen Instanzen konstant.
5.1.2 Label
Die Label-Klasse verwaltet die Interfacenamen der Services und weist ihnen eindeutige
Nummern (ID) zu. Diese Nummern beginnen bei 0 und sind fortlaufend. Die 0 ist da-
29
5 Algorithmen f¨
ur die implizite Formeldarstellung
¨
bei f¨
ur den internen Ubergang
τ der Serviceautomaten reserviert. Die restlichen Labels
werden in der Reihenfolge des Parsevorgangs vergeben. So ist sichergestellt, dass alle
Labels eines Typs vor den Labeln des anderen Typs stehen, also zum Beispiel, dass die
Nummern der Inputlabels kleiner als die der Outputlabel ist. Ein Transitions¨
ubergang
mit dem Label !x“ bekommt zum Beispiel die Nummer eins, sofern die Outputlabels
”
zuerst geparst werden. Beispiele daf¨
ur sind die Abbildungen 5.1 und 5.2.
Abbildung 5.1: mInterface f¨
ur Serviceautomat A aus Abbildung 2.1
ID
Name
0
τ
1
!x
2
!y
3
!z
4
?a
5
?b
6
?c
Abbildung 5.2: mInterface f¨
ur Serviceautomat C aus Abbildung 2.3
ID
Name
0
τ
1
!x
2
!y
3
!z
4
?a
5
?b
6
?c
5.1.3 Service
Die Struktur der Klasse Service ist an die Implementierung von Wendy [LW10a] angelehnt. Das gilt im Insbesonderen f¨
ur die Speicherung der Transitionsrelation und der
Markierungen. Ein Objekt der Klasse Service besteht aus den Elementen:
• mInterface, Menge der vorhandenen Label-IDs,
• mMarkings, Array der Markierung des Service und
• mSize, Indikator der Anzahl der Markierungen.
Jeder Zustand (ein Knoten in der Abbildung 2.1) ist ein Objekt der Klasse ServiceMarking. Diese bestehen aus:
• mEnabledTransitions, BitSetC der aktivierten Transitions¨
uberg¨ange (Definition 1),
• mIsFinal, Bit zur Kennzeichnung, ob es sich um einen Finalzustand handelt,
• mSuccessors, Array von Nachfolgerknoten (deren Indizes),
• mLabels, Array von Labels (deren Indizes) zu den Nachfolgerknoten und
• mOutDegree, L¨
angenindikator der Elemente mSuccessors und mLabels.
Die beiden Arrays mSuccessors und mLabels bilden die Transitionsrelation einer Markierung ab. Eine Transition [q, x, q ] ∈ δ ist ein Eintrag in der Markierung q. Dabei steht
im Array mLabels im Index i die Nummer des Labels x und im Array mSuccessors (im
gleichen Index) die Nummer des Zustandes q . Daraus geht hervor, dass die Zust¨ande
30
5 Algorithmen f¨
ur die implizite Formeldarstellung
(Markierungen, Knoten) des Service nummeriert sind. Diese Nummerierung ergibt sich
aus der Parsereihenfolge der Eingabedaten. Das Array mLabels ist sortiert und damit
auch das Array mSuccessors. Abbildung 5.3 zeigt die Abbildung der Graphenstruktur f¨
ur
den Serviceautomat A aus Abbildung 2.1, das Interface veranschaulicht Abbildung 5.1
und das BitSetC-Objekt f¨
ur Zustand a1 ist exemplarisch: 1000000 . . . 0. Die 1 bedeutet,
dass das Label τ vorhanden ist. Sofern das niederwertigste Bit (LSB) ganz links steht.
Die L¨ange des Bitvektors entspricht dem Basistyp, hier 32 Bit.
Abbildung 5.3: mMarkings f¨
ur Serviceautomat A aus Abbildung 2.1
Index
mLabels
mSuccessors
mOutDegree
mIsFinal
0
1
0
1
0
1
0
2
0
6
2
0
2
4
3
1
0
3
5
4
1
0
4
2
5
1
0
5
0
1
6
6
7
1
0
7
3
8
1
1
8
0
1
5.1.4 Operating Guideline
Da Bedienungsanleitung auf Serviceautomat basieren, ist die Struktur der Klasse der
OperatingGuideline vergleichbar mit der Klasse Service. Sie besteht aus:
• mInterface, Menge der vorhandenen Label-IDs,
• mInputInterface, BitSetC der Inputlabels (1 an den entsprechenden Indizes),
• mOutputInterface, BitSetC der Outputlabels (1 an den entsprechenden Indizes),
• mMarkings, Array der Markierung der Bedienungsanleitung und
• mSize, Indikator der Anzahl der Markierungen.
Jeder Zustand (ein Knoten in der Abbildung 2.3) ist ein Objekt der Klasse ServiceMarking. Die Klasse ServiceMarking umfasst:
• mCheckedPaths, BitSetC der u
uften Transitions¨
uberg¨ange,
¨berpr¨
• mSBit, Bit zur Kennzeichnung, ob q ∈ S (Definition 17),
• mFBit, Bit zur Kennzeichnung, ob q ∈ F (Definition 17),
• mTBit, Bit zur Kennzeichnung, ob q ∈ T (Definition 17),
• mSuccessors, Array von Nachfolgerknoten (deren Indizes),
• mLabels, Array von Labels (deren Indizes) zu den Nachfolgerknoten und
• mOutDegree, L¨
angenindikator der Elemente mSuccessors und mLabels.
Die Anmerkungen zu den Transitionsarrays mLabels und mSuccessors, welche beim
Service beschrieben sind, gelten auch f¨
ur Bedienungsanleitungen. Das BitSetC-Objekt
31
5 Algorithmen f¨
ur die implizite Formeldarstellung
mCheckedPaths wird lediglich beim Matching ben¨otigt und wird auch nur in diesem
Anwendungsfall berechnet. Abbildung 5.4 zeigt die Repr¨asentation der Graphenstruktur
f¨
ur den annotierten Serviceautomaten der Bedienungsanleitung [C, Φ] aus Abbildung 2.3,
das Interface veranschaulicht Abbildung 5.2.
Abbildung 5.4: mMarkings f¨
ur Serviceautomat C aus Abbildung 2.3
Index
mLabels
mSuccessors
mOutDegree
mSBit
mFBit
mTBit
0
1
1
4
1
0
0
4
7
1
5
4
3
0
0
0
6
2
2
3
3
4
0
1
0
3
3
0
1
0
4
2
5
4
8
4
0
0
0
5
4
6
3
0
0
0
6
3
0
0
0
7
2
9
5
8
4
0
0
0
8
2
6
4
1
0
0
9
5
6
3
0
0
0
10
5
0
0
1
5.1.5 RBTreeStack
Die Klasse RBTreeStack ist eine neu entwickelte Datenstruktur, um die rekursiven Algorithmen iterativ umsetzen zu k¨
onnen. In allen Anwendungsf¨allen wird eine koordinierte
Tiefensuche ben¨
otigt. Daf¨
ur ist es notwendig, entscheiden zu k¨onnen, ob ein Element
bereits verarbeitet worden ist. Diese Aufgabe u
¨bernimmt der Rot-Schwarz-Baum in der
Datenstruktur. Die logarithmische Komplexit¨at beim Einf¨
ugen und Suchen (die Suche
geht dem Einf¨
ugen voraus) ist f¨
ur diese Anwendung optimal. Von einer perfekten Hashtabelle, deren Konstruktion fraglich ist, abgesehen. Ungeachtet dessen, ob man einen
rekursiven oder iterativen Algorithmus verwendet, wird eine entsprechende Datenstruktur ben¨
otigt (siehe zum Beispiel Zeile 7 in Algorithmus 1). Der durch die Rekursion
implizit gegebene Stack muss in der iterativen Variante explizit modelliert werden. Eine erneute Datenhaltung der Elemente innerhalb des Stacks ist dabei redundant. Aus
¨
dieser Uberlegung
ist die Klasse RBTreeStack entstanden. Sie spart durch zwei Ideen
Arbeitsspeicher:
1. Schl¨
ussel und Nutzdaten sind identisch und
2. Stack und Suchdaten sind identisch.
Folglich wird neben den notwendigen Datentypstrukturen (Pointern) nur ein einziges
Mal das Nutzdatum gespeichert. Das Nutzdatum besteht in dieser Implementierung aus
zwei Indizes, zum Beispiel denen zweier Markierungen.
Die Klasse besitzt im Wesentlich zwei Methoden:
1. add(a, b) zum Hinzuf¨
ugen eines Zustandspaares und
2. pop(a, b) zur R¨
uckgabe des obersten Zustandspaares.
32
5 Algorithmen f¨
ur die implizite Formeldarstellung
Beispiel
F¨
ur einen Aufruf der Form RBTreeStack.add(a, b) pr¨
uft der Rot-Schwarz-Baum-Teil
der RBTreeStack-Klasse, ob das Paar (a, b) bereits im Baum vorhanden ist. Ist das der
Fall, wird es abgewiesen. Handelt es sich stattdessen um ein neues Paar, wird dieses
dem Baum hinzugef¨
ugt und dessen Vorg¨anger (V ) wird das bisherige Stackelement.
Das zentrale Stackelement des Baumes wird anschließend auf das neue Paar gesetzt.
Abbildung 5.5 zeigt den RBTreeStack der durch den Aufruf der Befehle:
1. RBTreeStack.add(0, 0),
2. RBTreeStack.add(3, 1),
3. RBTreeStack.add(5, 2),
4. RBTreeStack.add(4, 1),
5. RBTreeStack.add(2, 2) und
6. RBTreeStack.add(1, 0) entsteht.
Nach dem Aufruf RBTreeStack.pop(a, b), wobei a und b zwei Referenzen sind, ist
a = 1 und b = 0. Der Stackpointer zeigt abschließend auf den Knoten (1, 0). Das neue
Stackelement wird dann der Vorg¨
angerknoten (2, 2) des Knoten (1, 0).
Abbildung 5.5: RBTreeStack
33
5 Algorithmen f¨
ur die implizite Formeldarstellung
5.2 Algorithmen
¨
5.2.1 Simulation / Aquivalenz
¨
Da die Abl¨
aufe f¨
ur die Entscheidungen Simulation (Accordance) und Aquivalenz
sehr
¨ahnlich sind, werden sie in diesem Abschnitt gemeinsam vorgestellt. Cosme erwartet die
Bedienungsanleitungen im Bitformat der Service-Tech-Familie, genauer dem Wendyformat f¨
ur Bit-Bedienungsanleitungen (typischerweise .og). Wie diese erstellt werden, kann
in Kapitel 6 nachgelesen werden. F¨
ur die Entscheidung, ob B1 B2 oder B1 ≡ B2 wird
folgendes Schema angewandt:
1. Parsen der Bedienungsanleitung B1 ,
2. Parsen der Bedienungsanleitung B2 und
¨
3. Simulationsalgorithmus 7 beziehungsweise Aquivalenzalgorithmus
8 aufrufen.
Parsen einer Bedienungsanleitung
F¨
ur den Parsevorgang wird der Referenzparser (verf¨
ugbar unter http://svn.gna.org/
viewcvs/service-tech/trunk/meta/reference/) der Service-Tech-Familie verwendet.
Ausgehend von der Struktur der Dateien ergibt sich folgende Bearbeitungsreihenfolge:
1. Einlesen des Interfaces und
2. Einlesen der Knoten.
Die Namen der Interfacepl¨
atze werden in einem globalen Label-Objekt gespeichert und
dadurch nummeriert. Sofern eine zweite Bedienungsanleitung geparst wird, ist das globale Label-Objekt bereits gef¨
ullt. Enth¨alt die zweite Bedienungsanleitung die gleichen
Interfaces, wird denen die gleiche Nummer zugewiesen. Existiert ein Interface in einer
Bedienungsanleitungen als Input- und Outputinterface, bricht das Tool ab, da dies der
Voraussetzung von disjunkten Interfaces (Definition 1) widerspricht. Existiert ein Interface in der einen Bedienungsanleitung als Input- und in der anderen als Outputinterface,
sind die Bedienungsanleitungen nicht vergleichbar (Basis daf¨
ur ist Definition 2). Jeder
Knoten der Bedienungsanleitung wird nach folgendem Schema verarbeitet:
1. Die Nummer des Knoten wird in eine fortlaufende Nummer u
¨bersetzt,
2. die Bits werden gespeichert und
3. die Liste der Transitions¨
uberg¨ange wird sortiert gespeichert.
Das sortierte Speichern der Transitions¨
uberg¨ange verursacht einen logarithmischen Aufwand, der zun¨
achst einen Overhead darstellt. Die schnellste Implementierung der Speicherung der Transitions¨
uberg¨
ange kann in konstanter Zeit realisiert werden, zum Beispiel
als Liste. Die Rechtfertigung daf¨
ur wird im folgenden Abschnitt gegeben.
34
5 Algorithmen f¨
ur die implizite Formeldarstellung
Simulationsalgorithmus
Der Simulationsalgorithmus 7 ist eine direkte Implementierung des Algorithmus 5.
Algorithmus 7 Simuliert eine Bedienungsanleitung [B2 , S2 , F2 , T2 ] eine Bedienungsanleitung [B1 , S1 , F1 , T1 ]
procedure simuliert([B1 , S1 , F1 , T1 ], [B2 , S2 , F2 , T2 ] : OGs)
1: ToDo := leerer RBTreeStack
2: f¨
uge (q0B1 , q0B2 ) zu ToDo hinzu
3: while ToDo do
4:
entnimm oberstes Paar (qB1 , qB2 )
5:
if qB1 ∈ S1 und qB2 ∈
/ S2 then
6:
return false
7:
if qB2 ∈ F2 und qB1 ∈
/ F1 und qB1 ∈
/ S1 then
8:
return false
9:
if qB1 ∈ T1 und qB2 ∈
/ T2 then
10:
return false
11:
if | Kanten(qB1 ) | > | Kanten(qB2 ) | then
12:
return false
13:
for all [qB1 , x, qB1 ] ∈ Kanten(qB1 ) do
14:
if [qB2 , x, qB2 ] ∈ Kanten(qB2 ) then
15:
f¨
uge (qB1 , qB2 ) zu ToDo hinzu
16:
else
17:
return false
18: return true
¨
Aquivalenzalgorithmus
¨
Der Aquivalenzalgorithmus
8 ist eine direkte Implementierung des Algorithmus 6.
Komplexit¨
atsbetrachtung fu
¨ r die Algorithmen 7 und 8
Die ToDo-Liste ist ein RBTreeStack. Das Hinzuf¨
ugen der Indizes eines Zustandspaares
(Z. 1, 14) ist demnach von logarithmischer Komplexit¨at. Die Komplexit¨at der Entnahme
(Z. 3) des obersten Elementes in dem RBTreeStack ist konstant O(1). Das Pr¨
ufen der
annotierten Bits (Z. 4-9) ist, wie in Kapitel 4 gezeigt, ebenfalls von konstantem Auf¨
wand. Die Uberpr¨
ufung in Zeile 10 ist nicht notwendig, erm¨oglicht aber mit konstantem
Aufwand eine Vermeidung der linearen Iteration (Z. 12-16), falls nicht gen¨
ugend Tran¨
sitions¨
uberg¨
ange vorhanden sind. Voraussetzung f¨
ur die Richtigkeit dieser Uberpr¨
ufung
ist der Determinismus der Transitionsrelation (Definition 13). Die Iteration u
¨ber die
Transitions¨
uberg¨
ange ist linear, mit konstantem Faktor 1. Das heißt, dass u
¨ber jedes
Element beider Bedienungsanleitungen maximal einmal iteriert wird. Grundlage daf¨
ur
ist die Sortierung der Transitions¨
uberg¨ange beim Parsen. Der dort erh¨ohte Aufwand bei
35
5 Algorithmen f¨
ur die implizite Formeldarstellung
Algorithmus 8 Sind zwei Bedienungsanleitungen ¨aquivalent
procedure aequivalent([B1 , S1 , F1 , T1 ], [B2 , S2 , F2 , T2 ] : OGs)
1: ToDo := leerer RBTreeStack
2: f¨
uge (q0B1 , q0B2 ) zu ToDo hinzu
3: while ToDo nicht leer do
4:
entnimm oberstes Element (qB1 , qB2 )
5:
if qB1 ∈ S1 und qB2 ∈
/ S2 then
6:
return false
7:
if qB1 ∈ F1 und qB2 ∈
/ F2 then
8:
return false
9:
if qB1 ∈ T1 und qB2 ∈
/ T2 then
10:
return false
11:
if | Kanten(qB1 ) | = | Kanten(qB2 ) | then
12:
return false
13:
for all [qB1 , x, qB1 ] ∈ Kanten(qB1 ) do
14:
if [qB2 , x, qB2 ] ∈ Kanten(qB2 ) then
15:
f¨
uge (qB1 , qB2 ) zu ToDo hinzu
16:
else
17:
return false
18: return true
der Verwaltung (O(log(n)) gegen¨
uber O(1)) wird hier u
¨ber kompensiert. Mit der Sortierung ergibt sich eine Gesamtkomplexit¨at von O(n + log(n)) gegen¨
uber O(1 + n2 ) f¨
ur
die unsortierte Variante.
5.2.2 Matching
Um zu entscheiden, ob ein Serviceautomat A eines Service C und eine Bedienungsanleitung [B, S, F, T ] zusammen matchen, wird eine Bedienungsanleitung im Wendy-BitFormat und ein offenes Netz (typischerweise .owfn) ben¨otigt. Offene Netze [MRS05,
LMW07] sind eine Spezialisierung von Workflownetzen [Aal97, Aal98], f¨
ur die in der
Service-Tech-Familie ebenfalls ein Referenzparser (verf¨
ugbar unter http://svn.gna.
org/viewcvs/service-tech/trunk/meta/reference/) existiert. F¨
ur die Matchingentscheidung wird folgendes Schema angewendet:
1. Parsen des Service C,
2. Parsen der Bedienungsanleitung [B, S, F, T ],
3. Setzen der Bitvektoren mEnabledTransitions f¨
ur den Service,
4. Setzen der Bitvektoren mCheckedPaths f¨
ur die Bedienungsanleitung,
5. Matchingalgorithmus 9 aufrufen.
Das Setzen der Bitvektoren mEnabledTransitions f¨
ur den Service ist von linear Komplexit¨at in der Gr¨
oße des Interfaces. Das Setzen der Bitvektoren mCheckedPaths erfolgt
initial nach folgendem Schema:
36
5 Algorithmen f¨
ur die implizite Formeldarstellung
1. Anlegen eines Eins-Bitvektor in der L¨ange des globalen Interfaces und
2. entfernen des Inputinterfaces von diesem.
Parsen eines Service
Da die Eingabe ein offenes Netz ist, wird statt eines Service ein offenes Netz geparst.
F¨
ur diesen Parsevorgang wird die Petrinetz-API (verf¨
ugbar unter http://svn.gna.
org/viewcvs/service-tech/trunk/pnapi/) der Service-Tech-Familie verwendet. Das
so entstehende Petrinetz wird an LoLA [Sch00] u
¨bergeben, um den Erreichbarkeitsgraph
des Petrinetzes erstellen zu lassen. Dieser Erreichbarkeitsgraph ist letztlich die Eingabe
f¨
ur den Serviceparser in Cosme. Zwischen der Verarbeitung des offenen Netzes und der
¨
Ubergabe
an LoLA werden die Interfacepl¨atze (des Petrinetzes) in dem globalen LabelObjekt gespeichert, damit diese beim Parsevorgang von Cosme zur Verf¨
ugung stehen.
Der Ablauf sieht wie folgt aus:
1. Parsen des offenen Netzes in ein Petrinetz,
2. Labels bestimmen,
3. Petrinetz an LoLA-Format anpassen,
4. Erreichbarkeitsgraph des Petrinetzes mit LoLA berechnen und
5. Erreichbarkeitsgraph mit Cosme parsen.
Jede Markierung des Graphen wir nach diesem Schema verarbeitet:
1. Nummer der Markierung als Index u
¨bernehmen und
2. die Liste der Transitions¨
uberg¨ange sortiert speichern.
Die Rechtfertigung f¨
ur die Sortierung erfolgt nachfolgend. Im Gegensatz zu den Transitions¨
uberg¨
angen einer Bedienungsanleitung, der ein deterministischer Serviceautomat
zu Grunde liegt, k¨
onnen bei einem Service Transitionen mehrfach auftreten.
Matchingalgorithmus
Der Matchingalgorithmus 9 basiert auf dem Algorithmus 4, wobei der in Algorithmus 4
vorgestellte Teil in den Algorithmen 10 und 11 implementiert ist. Die Auftrennung leitet
¨
sich aus der Logik der Algorithmen ab und soll die Ubersichtlichkeit
wahren. F¨
ur den
Algorithmus 11 sei cp(qB ) die Menge der u
uften Pfade (mCheckedPaths) f¨
ur den
¨berpr¨
Zustand qB .
Komplexit¨
atsbetrachtung fu
¨ r Algorithmus 9
Die ToDo-Liste ist ein RBTreeStack. Das Hinzuf¨
ugen der Indizes eines Zustandspaares (Z. 1, 8, 11) ist demnach von logarithmischer Komplexit¨at. Die Komplexit¨at der
37
5 Algorithmen f¨
ur die implizite Formeldarstellung
Algorithmus 9 Matcht ein Serviceautomat A mit einer Bedienungsanleitung [B, S, F, T ]
procedure matcht(A : Serviceautomat, [B, S, F, T ] : OG)
1: ToDo := leerer RBTreeStack
2: f¨
uge (q0A , q0B ) zu ToDo hinzu
3: while ToDo nicht leer do
4:
entnimm oberstes Element (qA , qB )
5:
if not matchtZustandspaar(qA , qB ) then
6:
return false
7:
for all [qA , x, qA ] ∈ Kanten(qA ) do
8:
if x = τ then
x
9:
f¨
uge (qA → qA , qB ) zu ToDo hinzu
10:
else
11:
if [qB , x, qB ] ∈ Kanten(qB ) then
12:
f¨
uge (qA , qB ) zu ToDo hinzu
13:
else
14:
return false
15: return true
Algorithmus 10 Matcht das Zustandspaar (qA , qB )
procedure matchtZustandspaar(qA , qB : states)
1: if qB ∈ T then
2:
return true
3: if en(qA ) ∩ OB = ∅ then
4:
return true
5: if qB ∈ F und qA ∈
/ ΩA then
6:
return false
7: if qB ∈ S then
8:
return false
9: if existiertPfad(qB , IB \ en(qA )) then
10:
return false
11: return true
Entnahme (Z. 3) des obersten Elementes in dem RBTreeStack ist konstant O(1). Die
Iteration u
uberg¨ange (Z. 6, 10) ist linear, mit konstantem Faktor
¨ber die Transitions¨
1. Das heißt, dass u
¨ber jedes Element der Bedienungsanleitung und des Service maximal einmal iteriert wird. Grundlage daf¨
ur ist die Sortierung der Transitions¨
uberg¨ange
beim Parsen. Der dort erh¨
ohte Aufwand bei der Verwaltung (O(log(n)) gegen¨
uber O(1))
wird hier u
¨ber kompensiert. Mit der Sortierung ergibt sich eine Gesamtkomplexit¨at von
O(n + log(n)) gegen¨
uber O(1 + n2 ) f¨
ur die unsortierte Variante. Der Algorithmus 10
¨
u
ufung des Matching. Die Bitver¨bernimmt den ersten und trivialen Teil der Uberpr¨
gleiche in den Zeilen 1, 5 und 7 sind von konstanter Komplexit¨at. Der Vergleich der
aktivierten Transitions¨
uberg¨
ange ist linear in der L¨ange des Basistyps der Bitvektoren.
Sofern weniger als 32 Interfaces verwendet werden ist der Aufwand in O(1). Den zweiten
¨
und Weg basierten Teil der Uberpr¨
ufung des Matching u
¨bernimmt der Algorithmus 11.
Die Teilmengenvergleiche (Z. 1, 11), sowie deren Zuweisungen (Z. 3, 13) sind nach obiger
38
5 Algorithmen f¨
ur die implizite Formeldarstellung
Algorithmus 11 Existiert ein Pfad von qA u
¨ber I
procedure existiertPfad(qA : state, I : BitSetC)
1: ToDo := leerer RBTreeStack
2: if I ⊆ cp(qA ) then
3:
return false
4: cp(qA ) := cp(qA ) ∪ I
5: for all [qA , x, qA ] ∈ Kanten(qA ) do
6:
if x ∈ I then
7:
f¨
uge (qA ) zu ToDo hinzu
8: while ToDo nicht leer do
9:
entnimm oberstes Element (qA )
10:
if qA ∈ S ∪ F then
11:
return true
12:
if I ⊆ cp(qA ) then
13:
return false
14:
cp(qA ) := cp(qA ) ∪ I
15:
for all [qA , x, qA ] ∈ Kanten(qA ) do
16:
if x ∈ I then
17:
f¨
uge (qA ) zu ToDo hinzu
18: return false
Voraussetzung konstant. Das Iterieren u
uberg¨ange (Z. 4,
¨ber die aktivierten Transitions¨
14) ist ebenfalls konstant. Um zu pr¨
ufen, ob ein Transitions¨
ubergang zul¨assig ist (Z. 5,
15), wird konstante Zeit ben¨
otigt. Durch die Verwendung der Bitvektoren mCheckedPaths werden die notwendigen Pfad¨
uberpr¨
ufungen auf das Minimum reduziert. In den
meisten F¨
allen liefert bereits die Auswertung in Zeile 1 die ben¨otigte Antwort.
39
6 Benchmark
In diesem Kapitel werden die beiden Programme Fiona und Cosme hinsichtlich ihrer
Laufzeit und ihres Arbeitsspeicherbedarfes miteinander verglichen. Dabei kommen sechzehn verschiedene Services und deren Bedienungsanleitungen zum Einsatz. Im ersten Teil
wird gezeigt, wie die Dateien im Umfeld der Service-Tech-Familie zu erstellen sind. Der
zweite Teil beschreibt das Benchmarkverfahren und pr¨asentiert dessen Ergebnisse. Die
Interpretation der Benchmarkergebnisse erfolgt im dritten Teil des Kapitels. Gegeben
sind die Ausgangsnetze, deren Platzanzahl in der Spalte zwei und deren Transitionsanzahl in der Spalte drei in der Tabelle 6.1 zu finden sind. Die vierte Spalte enth¨alt
die Pl¨atze, die Spalte f¨
unf die Transitionen der zu den Ausgangsnetzen passenden Partnernetze. Der Umfang der Bedienungsanleitungen der Ausgangsnetze ist in den Spalten
sechs und sieben aufgef¨
uhrt. Die Gr¨oße des Interface kann in den Spalten acht (Output,
beziehungsweise Senden) und neun (Input, respektive Empfangen) abgelesen werden. Die
Tabellen sind nach der Spalte sieben sortiert, um eine schnelle Vergleichbarkeit zwischen
Aufgabengr¨
oße und L¨
osungsressourcen zu erhalten. Die in Kapitel 5 erw¨ahnte Voraussetzung, dass die Gr¨
oße des Interface kleiner als der Basistyps der BitSetC-Objekte (32)
ist, gilt f¨
ur alle hier verwendeten Services.
6.1 Erstellung der Dateien
Exemplarisch wird f¨
ur das offene Netz QR.owfn beschrieben, wie dessen Partner QRpartner.owfn und dessen Bedienungsanleitungen QR.bits.og und QR.cnf.og erstellt werden:
1. wendy --waitstatesOnly --succeedingSendingEvent --quitAsSoonAsPossible
QR.owfn --sa=QR-partner.sa
2. sa2sm QR-partner.sa QR-partner.owfn
3. wendy QR.owfn --og
4. wendyFormula2bits -i QR.og -o QR.bits.og
5. wendy2Fiona -i QR.og -o QR.cnf.og
Das Ergebnis von Schritt zwei ist der in Tabelle 6.1 beschriebene Partnerservice. Die
Bedienungsanleitung aus Schritt drei dient als Grundlage f¨
ur die Erstellung der Tool
spezifischen Bedienungsanleitungen, welche in den Schritten vier (Cosme) und f¨
unf (Fiona) erzeugt werden. Die tempor¨
aren Ergebnisse aus den Schritten eins und drei werden
nachfolgend nicht mehr ben¨
otigt. F¨
ur die Tabellen 6.2, 6.3 und 6.4 wird die Umwandlung in das passende Format (Schritt vier beziehungsweise f¨
unf) nicht ber¨
ucksichtigt. Da
40
6 Benchmark
Fiona in der Lage ist, aus den Ausgangsdateien ihrerseits die passenden Bedienungsanleitungen zu erzeugen, ist die Umwandlung f¨
ur Fiona nicht notwendig. Die Umwandlung
in das Bitformat ist entgegen fr¨
uheren Versionen nicht mehr Bestandteil von Wendy. Da
dies aber m¨
oglich ist, wird auch bei Cosme auf die Ber¨
ucksichtigung der Umwandlungsdauer verzichtet. Die Gr¨
oßenordnung der Umwandlung liegt f¨
ur die Bedienungsanleitung
AP.og bei 166 ms (f¨
ur Fiona) und 96 ms (f¨
ur Cosme) und f¨
ur TP.og bei 4.607 ms respektive 2.005 ms.
Tabelle 6.1: Daten¨
ubersicht
Name
IM
SD
MC
RE
AS
LA
PH
BH
TR
PO
RS
CN
DG
AP
QR
TP
o. Netz
Pl¨
atze
6
5
9
15
22
34
22
65
90
74
38
76
40
132
42
162
o. Netz
Trans.
4
3
5
8
13
17
10
80
123
96
33
98
23
88
21
248
Partner
Pl¨
atze
4
3
8
13
13
13
13
19
21
21
36
23
30
23
39
133
Partner
Trans.
1
0
3
7
6
6
6
15
11
10
41
11
16
11
19
165
OG
Knoten
3
3
7
10
16
20
67
96
110
168
369
576
11.376
1.536
11.264
57.996
OG
Trans.
2
6
18
41
67
84
243
567
731
1.182
3.083
4.859
13.838
15.115
145.811
691.414
Out
In
2
1
3
3
3
3
3
2
3
4
2
4
5
2
8
5
0
1
1
3
3
3
3
5
6
6
8
7
9
9
11
11
6.2 Benchmarkverfahren
Um f¨
ur die Partnernetze und die Bedienungsanleitungen das Matching zu entscheiden,
werden die Programme wie folgt aufgerufen:
• fiona -t match QR.cnf.og QR-partner.owfn
• cosme --matching -a QR.bits.og -c QR-partner.owfn
¨
Die Simulation respektive die Aquivalenz
wird mittels der Aufrufe
• fiona -t simulation/equivalence QR.cnf.og QR.cnf.og
• cosme -simulation/equivalence -a QR.bits.og -b QR.bits.og
41
6 Benchmark
entschieden. Zur Ermittlung der Zeiten in den Tabellen 6.2, 6.3 und 6.4 (Spalten Fiona (ms) und Cosme (ms)), wurden die oben genannten Befehle 20 mal hintereinander
ausgef¨
uhrt und deren Dauer mit dem Unixbefehl time gemessen (Real-Wert). Dieser
Vorgang wurde f¨
unf mal wiederholt und der beste Lauf gewertet. Die Spalten enthalten
folglich die Dauer von 20 Entscheidungen der gestellten Aufgabe, eine Aufgabe dauerte
1
demnach im Mittel 20
der eingetragenen Zeit. F¨
ur die Ermittlung des Speicherbedarfs
kam die Option –stats“ beim Tool Cosme und eine entsprechende Implementierung
”
beim Tool Fiona zum Einsatz. Die Speicherermittlung erfolgt dabei unmittelbar vor
dem Verlassen der main-Methode. Einen exemplarischen Aufruf f¨
ur Cosme zeigt die Abbildung 6.1. Die Werte in den Spalten Fiona (KB) und Cosme (KB) sind der allokierte
Speicher eines Aufrufs. Zur Ermittlung dieser Werte wurde jedes Beispiel f¨
unf Mal ausgef¨
uhrt und der beste Wert u
¨bernommen. Die Prozentspalten in den Tabellen 6.2, 6.3
und 6.4 charakterisieren das Verh¨altnis zwischen Fiona und Cosme. In Tabelle 6.2 besagt der Eintrag in der ersten Prozentspalte (5) in Zeile 16, dass Cosme 4,67% der Zeit
von Fiona zur Entscheidung der Simulation ben¨otigt hat. Die Spalte 8 in der gleichen
Zeile und Tabelle besagt, dass Cosme daf¨
ur 6,31% des von Fiona ben¨otigten Speichers
verwendet hat. Die besten und schlechtesten Werte sind jeweils fett gedruckt.
6.2.1 Simulation
Die beiden Bedienungsanleitungen sind bei der Simulation identisch. Dies bedeutet,
¨
dass die Simulation erf¨
ullt ist. Durch die Aquivalenz
der beiden Bedienungsanleitungen
m¨
ussen die Algorithmen die gesamte Bedienungsanleitung verarbeiten, was einen Vergleich zwischen den Gr¨
oßen (Knotenanzahl und Verzweigungsgrad) und den eingesetzten
Ressourcen erm¨
oglicht. Die Erstellung von minimierten Bedienungsanleitungen, die die
gleiche Menge an Strategien charakterisieren, aber nicht notwendigerweise strukturell
vergleichbar sind, war nicht f¨
ur alle Bedienungsanleitungen m¨oglich. Ein Vergleich zwi-
Abbildung 6.1: Cosmeaufruf
42
6 Benchmark
schen den Ausgangsbedienungsanleitungen (wie oben beschrieben) und den reduzierten
Bedienungsanleitungen h¨
atte eine interessante Erg¨anzung dargestellt. Die Berechnungszeiten f¨
ur die Bedienungsanleitungen, zu denen eine minimierte Bedienungsanleitung
erstellt werden konnte, waren nahezu identisch. Dies l¨asst such durch den geringen Grad
der realisierbaren Minimalisierung dieser Bedienungsanleitungen erkl¨aren.
Tabelle 6.2: Simulationsbenchmark
Name
IM
SD
MC
RE
AS
LA
PH
BH
TR
PO
RS
CN
DG
AP
QR
TP
Fiona
(ms)
382
406
418
441
500
532
716
1.589
1.463
1.877
6.058
7.785
22.456
30.338
232.616
1.345.853
Cosme
(ms)
372
368
368
356
356
372
379
443
453
487
716
925
1.714
2.239
14.941
62.894
Ratio
(%)
97,38
90,64
88,04
80,73
71,20
69,92
52,93
27,88
30,96
25,95
11,82
11,88
7,63
7,38
6,42
4,67
Fiona
(KB)
1.584
1.588
1.588
1.596
1.580
1.616
1.640
1.844
1.840
1.944
2.900
3.564
7.328
1.668
1.676
273.764
Cosme
(KB)
1.272
1.272
1.240
1.280
1.284
1.272
1.296
1.288
1.280
1.292
1.344
1.392
1.604
1.636
4.496
17.272
Ratio
(%)
80,30
80,10
78,09
80,20
81,27
78,71
79,02
69,85
69,57
66,46
46,34
39,06
21,89
98,08
268,26
6,31
Der Speicherbedarf in den Beispielen AP und QR bei Fiona ist auff¨allig. Die parallele Beobachtung des Systems mit dem Unixbefehl top zeigte bei Beispiel QR einen Verbrauch
von zirka 41.600 KB an. Eine entsprechende Beobachtung war bei Beispiel AP wegen der
geringen Laufzeit nicht m¨
oglich. Der Testlauf mit der minimierten Bedienungsanleitung
f¨
ur QR, welche die gleiche Knotenanzahl besitzt, best¨atigte den mit top beobachteten
Wert ebenfalls. L¨
asst man diese offensichtlichen Messfehler außen vor, erkennt man, dass
Cosme in allen Beispielen schneller und platzsparender arbeitet als Fiona. Die Einsparungen in der Laufzeit reichen von knapp 3% f¨
ur kleine Beispiele bis u
¨ber 95% bei dem
gr¨oßten Beispiel. Der Speicherbedarf liegt durchschnittlich 20% unter dem Fionawert f¨
ur
die kleinen Beispiele und bis zu knapp 94% f¨
ur das Beispiel TP.
¨
6.2.2 Aquivalenz
Die beiden Bedienungsanleitungen sind identisch und folglich a¨quivalent. Begr¨
undet wird
diese Wahl analog zur Simulation mit der direkten Vergleichbarkeit zwischen der Gr¨oße
43
6 Benchmark
der Bedienungsanleitungen und den eingesetzten Ressourcen f¨
ur die Entscheidung, sowie
der fehlenden Verf¨
ugbarkeit aller minimierten Bedienungsanleitungen. Die Abbildung 6.2
visualisiert die Tabelle 6.3. Dabei ist die Laufzeit u
¨ber der Anzahl der Transitionen (siehe
Tabelle 6.1, Spalte sieben) abgetragen. Der ben¨otigte Speicher wird durch die Fl¨ache der
Kreise veranschaulicht.
¨
Tabelle 6.3: Aquivalenzbenchmark
Name
IM
SD
MC
RE
AS
LA
PH
BH
TR
PO
RS
CN
DG
AP
QR
TP
Fiona
(ms)
404
402
421
444
518
534
742
1.704
1.542
2.200
6.677
8.491
24.818
32.779
251.403
1.446.601
Cosme
(ms)
366
366
374
368
375
371
376
413
452
479
723
932
1.721
2.244
14.905
62.936
Ratio
(%)
90,59
91,04
88,84
82,88
72,39
69,48
50,67
24,24
29,31
21,77
10,83
10,98
6,93
6,85
5,93
4,35
Fiona
(KB)
1.596
1.596
1.604
1.590
1.596
1.616
1.652
1.860
1.856
1.960
2.912
3.576
7.348
9.948
60.400
273.784
Cosme
(KB)
1.272
1.272
1.260
1.280
1.284
1.272
1.268
1.280
1.280
1.292
1.344
1.392
1.604
1.636
4.496
17.272
Ratio
(%)
79,70
79,70
78,55
80,50
80,45
78,71
76,76
68,82
68,97
65,92
46,15
38,93
21,83
16,45
7,44
6,31
¨
Die ben¨otigten Ressourcen von Cosme f¨
ur die Aquivalenzentscheidung
sind nahezu identisch mit denen der Simulation. Dieses Ergebnis war auf Grund der sehr ¨ahnlichen Algorithmen zu erwarten. Die Bearbeitungszeit von Fiona erh¨oht sich zwischen knapp einem
und gut 14%, bei einem Median von zirka 6%. Dieser Offset verbessert das Verh¨altnis
zwischen Cosme und Fiona zus¨
atzlich.
44
¨
Abbildung 6.2: Aquivalenzbenchmark
6 Benchmark
45
6 Benchmark
6.2.3 Matching
F¨
ur die Matchingentscheidungen werden die Partnernetze aus Schritt zwei mit den Bedienungsanleitungen aus Schritt drei der Dateierstellung verwendet. Die Bedienungsanleitungen wurden demnach so gew¨ahlt, dass diese zueinander matchen. Das Paar f¨
ur
Beispiel SD kann nicht gematcht werden, da das Partnernetz keine Transitionen besitzt.
Auf die Ermittlung des Speicherbedarfs wurde daher verzichtet.
Tabelle 6.4: Matchingbenchmark
Name
IM
SD
MC
RE
AS
LA
PH
BH
TR
PO
RS
CN
DG
AP
QR
TP
Fiona
(ms)
518
455
510
543
566
581
653
1.098
1.035
1.098
2.658
3.384
9.044
12.535
92.386
496.457
Cosme
(ms)
849
386
850
870
870
867
862
932
907
891
1.075
1.111
1.532
1.771
8.107
32.598
Ratio
(%)
163,90
84,84
166,67
160,22
153,71
149,23
132,01
84,88
87,63
81,15
40,44
32,83
16,94
14,13
8,78
6,57
Fiona
(KB)
1.908
0.000
1.924
1.932
1.940
1.940
1.968
2.092
2.076
2.128
2.636
2.916
4.804
6.108
31.640
140.212
Cosme
(KB)
1.536
0.000
1.544
1.560
1.560
1.564
1.560
1.600
1.590
1.590
1.700
1.660
1.828
1.844
3.696
11.680
Ratio
(%)
80,50
0,00
80,25
80,75
80,41
80,62
79,27
76,48
76,59
74,72
64,49
56,93
38,05
30,19
11,68
8,33
Beim Matching f¨
allt auf, dass Fiona in sechs der sechzehn F¨alle schneller als Cosme
ist. Dabei ist der Geschwindigkeitsvorsprung in der Gr¨oßenordnung des Faktors 1,5. Mit
zunehmender Gr¨
oße der Beispiele kippt dieses Verh¨altnis allerdings, bis zu einem Faktor
von gut 15 zu Gunsten von Cosme. Cosme bearbeitet durchgehend s¨amtliche Beispiele
platzsparender als Fiona, wobei sich der ben¨otigte Platz zwischen 80% und gut 8%
in Abh¨
angigkeit der Gr¨
oße der Aufgabe bewegt. Die Platzersparnis ist beim Matching
allerdings nicht aussagekr¨
aftig, da der Platzbedarf von LoLA nicht mit ber¨
ucksichtigt
wird.
6.3 Auswertung
¨
Die gestiegene Laufzeit (Aquivalenz
versus Simulation) bei Fiona ist auf die doppelte
Implikationspr¨
ufung zur¨
uckzuf¨
uhren. In Beispiel TP erkennt man eine Differenz von
46
6 Benchmark
knapp 101s, die f¨
ur diesen zus¨
atzlichen Schritt anf¨allt. Zieht man diese 101 s von den
gemessenen 1.345 s (der Simulationsdauer) ab, erh¨alt man eine gute N¨aherung f¨
ur den
Aufwand, den die Erstellung der Simulationsrelation verursacht. Dieser liegt mit 1.244 s
zirka 20 mal u
ur das gr¨oßte Beispiel, ist ein
¨ber dem Wert von Cosme. Dieser Faktor, f¨
Indikator f¨
ur die Richtigkeit der wesentlichen Designunterschiede:
• Iterative statt rekursiver Algorithmen und
• kompaktere Datenstrukturen.
Effekte, wie die fr¨
uhzeitige Erkennung einer unn¨otigen Expansion des Zustandsraumes,
sind hier noch nicht ber¨
ucksichtigt, da die Beispiele stets die komplette Simualtionsrelation ben¨
otigten. In einem entsprechenden Benchmarkszenario w¨
urde der Vorsprung
¨
von Cosme demnach steigen. Uberraschend
ist der durchg¨angig geringe Platzbedarf von
Cosme (sieht man von einem Ausreißer bei der Simulation ab), zumal die Speichereffizienz nach Massuthe [Mas09] Hauptaugenmerk der Entwicklung von Fiona war. Die f¨
ur
kleinere Beispiele schnellere Bearbeitungszeit von Fiona resultiert aus dem sukzessivem
Aufbau der Simulationsrelation. In den kleineren Beispielen ist der Overhead des Aufrufs von LoLA von Cosme nicht mehr aufzuholen. Einer st¨andigen Nutzung von Cosme,
auch f¨
ur kleine Anwendungsf¨
alle, widersprechen diese Beispiele mit konkreten Laufzeiten
im Millisekundenbereich (zirka 25 ms) dennoch nicht. Die These, mit dem sukzessivem
Aufbau Speicherplatz zu sparen und damit gr¨oßere Beispiele bearbeiten zu k¨onnen, kann
anhand der vorliegenden Testf¨
alle nicht best¨atigt werden. Der sequentielle Aufruf von
LoLA und Cosme sollte in der Lage sein, gr¨oßere Anwendungsf¨alle zu entscheiden.
47
7 Zusammenfassung
Mit der Implementierung Cosme“ wurde gezeigt, dass sich die in der Theorie geschaf”
fenen Geschwindigkeitsvorteile (siehe Kapitel 4) in die Praxis u
¨bernehmen lassen. Wie
Kapitel 6 zeigt, resultiert der realisierte Geschwindigkeits- und Speicherplatzvorteil nicht
allein aus der Umstellung der Formelrepr¨asentation, sondern auch aus der Wahl geeigneter Speicherstrukturen und der Verwendung iterativer Algorithmen. Mit Zeitersparnissen
bis zu 95% lassen sich elementare Arbeitsschritte in der serviceorientierten Architektur
deutlich beschleunigen. Eine Umstellung der Bedienungsanleitungen auf das Bitformat,
zum Beispiel beim Broker, w¨
urde demnach dessen Hauptaufgabe, die Suche nach geeigneten Partnern, erheblich verk¨
urzen.
¨
Zu Beginn der Arbeit stand die Uberlegung,
das Konzept des sukzessiven Aufbaus der
Simulationsrelation ebenfalls in Cosme zu verwenden. Die Benchmarks in Kapitel 6
rechtfertigen nachtr¨
aglich die Entscheidung, davon abzusehen und diese Aufgabe spezialisierten Tools, zum Beispiel LoLA, zu u
¨berlassen. Dies vereinfacht zum Einen die
¨
Ubersichtlichkeit
der Algorithmen und Datenstrukturen innerhalb von Cosme, zum Anderen kann so stets von Weiterentwicklungen dieser Spezialtools profitiert werden, ohne deren Weiterentwicklung selbst implementieren zu m¨
ussen. Die Service-Tech-Familie
profitiert so von den Konzepten der Modularisierung und Spezialisierung der einzelnen
Tools. Momentan sollte der sukzessive Aufbau demnach kein Kriterium einer Weiterentwicklung sein.
Eine Idee f¨
ur die Weiterentwicklung w¨are gegebenenfalls die Anpassung des Matchingvorgangs an eine Stapelverarbeitung. In der Praxis wird der Broker f¨
ur einen eingehenden Service ein ganzes Portfolio an Bedienungsanleitungen u
berpr¨
u
fen.
F¨
ur jede in
¨
Frage kommende Bedienungsanleitung muss dann der Matchingalgorithmus aufgerufen
werden. Momentan ist der Matchingalgorithmus darauf spezialisiert, dass genau eine
Bedienungsanleitung mit einem Service gematcht werden soll. Genauer gesagt ist es die
Erstellung der Bitvektoren, die darauf spezialisiert ist. Im Zuge einer Weiterentwicklung
m¨
usste gepr¨
uft werden, ob die sequentielle Ausf¨
uhrung f¨
ur das gesamte Portfolio nicht
durch eine Stapelverarbeitung weiter beschleunigt werden k¨onnte. Ausgangspunkt der
¨
Uberlegung
ist es, den Service nur einmal zu parsen und dessen Erreichbarkeitsgraph
einmalig zu berechnen.
Aufbauend auf der vorgestellten Implementierung ist die Entwicklung eines spezialisierten Serviceregisters f¨
ur den Broker denkbar. Dieses m¨
usste die Bedienungsanleitungen
im Bitformat in einer geeigneten Datenrepr¨asentation (also Datenbankimplementierung)
verwalten. Cosme k¨
onnte dann direkt auf diesem Serviceregister aufsetzen, um die Auf¨
gaben Matching, Accordance und Aquivalenz
noch effizienter zu entscheiden.
48
Literaturverzeichnis
[A+ 07]
Alves, Alexandre u. a.: Web Services Business Process Execution Language
Version 2.0 / OASIS. 2007. – OASIS Standard
[Aal97]
Aalst, Wil M. P. d.: Verification of Workflow Nets. In: ICATPN, 1997, S.
407–426
[Aal98]
Aalst, Wil M. P. d.: The Application of Petri Nets to Workflow Management. In: Journal of Circuits, Systems, and Computers 8 (1998), Nr. 1, S.
21–66
[BK06]
Breugel, Van ; Koshkina, Maria: Models and Verification of BPEL. 2006
[BZ83]
Brand, Daniel ; Zafiropulo, Pitro: On Communicating Finite-State Machines. In: J. ACM 30 (1983), Nr. 2, S. 323–342
[CR90]
Cormen, T. H. ; Rivest, C. E. Leisersonand R. L.: Introduction to Algorithms. Cambridge, MA : MIT Press, 1990
[Got00]
Gottschalk, Karl: Web Services Architecture Overview / IBM developerWorks. 2000. – IBM Whitepaper. – http://ibm.com/developerWorks/web/
library/w-ovr
[KMW07] Kaschner, Kathrin ; Massuthe, Peter ; Wolf, Karsten: Symbolic Representation of Operating Guidelines for Services. In: Petri Net Newsletter 72
(2007), April, S. 21–28
[LLSW09] Liske, Nannette ; Lohmann, Niels ; Stahl, Christian ; Wolf, Karsten:
Another Approach to Service Instance Migration. In: Baresi, Luciano
(Hrsg.) ; Chi, Chi-Hung (Hrsg.) ; Suzuki, Jun (Hrsg.): Service-Oriented
Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings Bd. 5900, Springer-Verlag, November 2009 (Lecture Notes in Computer Science), S. 607–621
[LMW07] Lohmann, Niels ; Massuthe, Peter ; Wolf, Karsten: Operating Guidelines
for Finite-State Services. In: PETRI NETS 2007 Bd. 4546, Springer, 2007
(LNCS), S. 321–341
[Loh08]
Lohmann, Niels: A Feature-Complete Petri Net Semantics for WS-BPEL
2.0. In: WS-FM 2007 Bd. 4937, Springer, 2008 (LNCS), S. 77–91
[LW10a]
Lohmann, Niels ; Weinberg, Daniela: Wendy: A tool to synthesize partners for services. In: Lilius, Johan (Hrsg.) ; Penczek, Wojciech (Hrsg.):
31st International Conference on Applications and Theory of Petri Nets and
Other Models of Concurrency, PETRI NETS 2010, Braga, Portugal, June
49
Literaturverzeichnis
21-25, 2010 Bd. 380, Springer-Verlag, Juni 2010 (Lecture Notes in Computer Science)
[LW10b]
Lohmann, Niels ; Wolf, Karsten: Petrifying Operating Guidelines for Services. In: Fundam. Inform. (2010). – (Accepted for publication in January
2010)
[Lyn96]
Lynch, Nancy A.: Distributed Algorithms. Morgan Kaufmann, 1996
[Mas09]
Massuthe, Peter: Operating Guidelines for Services, Humboldt-Universit¨at
zu Berlin, Mathematisch-Naturwissenschaftliche Fakult¨at II; Eindhoven University of Technology, Dissertation, April 2009. – ISBN 978-90-386-1702-2
[MRS05]
Massuthe, Peter ; Reisig, Wolfgang ; Schmidt, Karsten: An Operating
Guideline Approach to the SOA. In: AMCT 1 (2005), Nr. 3, S. 35–43
[MW08]
Massuthe, Peter ; Weinberg, Daniela: Fiona: A Tool to Analyze Interacting Open Nets. In: Lohmann, Niels (Hrsg.) ; Wolf, Karsten (Hrsg.):
Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26–27, 2008 Bd. 380,
CEUR-WS.org, September 2008 (CEUR Workshop Proceedings), S. 99–104
[OMG06] OMG: Business Process Modeling Notation (BPMN) Version 1.0 / OMG.
2006. – OMG Final Adopted Specification
[OMG07] OMG: Unified Modeling Language (UML) / OMG. 2007. – Version 2.1.2
[Pap01]
Papazoglou, Mike P.: Agent-oriented technology in support of e-business.
In: Commun. ACM 44 (2001), Nr. 4
[Rei86]
Reisig, Wolfgang: Petrinetze, Eine Einf¨
uhrung, 2. Auflage. Springer, 1986
[Sch00]
Schmidt, Karsten: LoLA: A Low Level Analyser. In: Nielsen, Mogens
(Hrsg.) ; Simpson, Dan (Hrsg.): Application and Theory of Petri Nets 2000:
21st International Conference, ICATPN 2000, Aarhus, Denmark, June 2000.
Proceedings Bd. 1825, Springer-Verlag, Juni 2000 (Lecture Notes in Computer
Science), S. 465–474
[Sed88]
Sedgewick, R.: Algorithms. Reading, MA : Addison-Wesley, 1988
[SMB09]
Stahl, Christian ; Massuthe, Peter ; Bretschneider, Jan: Deciding Substitutability of Services with Operating Guidelines. In: Transactions on Petri
Nets and Other Models of Concurrency II, Special Issue on Concurrency in
Process-Aware Information Systems 2 (2009), M¨arz, Nr. 5460, S. 172–191
[Wol09]
Wolf, Karsten: Does my service have partners? In: LNCS ToPNoC 5460
(2009), M¨
arz, Nr. II, S. 152–171. – Special Issue on Concurrency in ProcessAware Information Systems
50
Erkl¨
arung
Hiermit versichere ich (Andreas Lehmann), dass ich die vorliegende Studienarbeit Effi”
ziente Implementierung und Validierung der Basisalgorithmen f¨
ur Bedienungsanleitungen mit impliziter Formelrepr¨
asentation“ selbstst¨andig verfasst und keine anderen als
die angegebenen Quellen und Hilfsmittel benutzt habe, alle Ausf¨
uhrungen, die anderen
Schriften w¨
ortlich oder sinngem¨
aß entnommen wurden, kenntlich gemacht sind und die
Arbeit in gleicher oder a
¨hnlicher Fassung noch nicht Bestandteil einer Studien- oder
Pr¨
ufungsleistung war.
Rostock, den 22. M¨
arz 2010
51
Document
Kategorie
Seele and Geist
Seitenansichten
6
Dateigröße
2 632 KB
Tags
1/--Seiten
melden