Information Technology Reference
In-Depth Information
composition. Section 4.3 introduces the method to check whether
there is any mediator to glue two partially compatible services, and
Section 4.4 introduces the method to generate the mediator.
4.2 PETRI NET FORMALISM FOR BPEL SERVICE,
MEDIATION, AND COMPATIBILITY
Using Petri nets to model BPEL processes is not a new idea. However,
our formalism separates control flow with the message exchange and
provides a unified formalism to describe services, their composition,
and a mediator. We also provide a new correctness criterion regarding
service composition. These can be viewed as novel developments in
applying Petri nets to this area.
4.2.1 CPN Formalism for BPEL Process
To formally analyze the compatibility and mediation issue in BPEL
services composition, we first define a formal model. Then, we present
how to transform a BPEL process to this model. Service workflow net is
an extension of workflow nets defined in Chapter 2, with the capability
of describing message exchanges among services, based on the concept
of colored Petri nets.
Definition 4.1. (Service Workflow Net, SWF-net)
A service work-
flow net is a colored Petri net P
ð
;
T
;
F
; S;
C
Þ
, where
1. P is a finite set of places satisfying
(a) P
P
M
¼
1
;
(b) P
I
is a set of internal places, and
(c) P
M
is a set of message places satisfying the condition that
8
¼
P
I
[
P
M
and P
I
\
p
2
P
M
,(
p
¼
1
^j
p
j¼
1)
_
(p
¼
1
^j
p
j¼
1).
2. T is a finite set of transitions;
3. F
(P
T)
[
(T
P) is aflowrelationand P
I
ð
;
T
;
F
Þ
is aWF-net;
4.
has a unique
element, which is the color of the control tokens in P
I
; and
5. C is the color function from P to
S
is a finite set of color sets. Color set E
¼
fg2 S
e
S
, and
8
p
2
P
I
, C(p)
¼
E.
