Information Technology Reference
In-Depth Information
Þ
satisfies a certain property, there
exists a mediator to glue N
1
and N
2
, and in Section 4.4 we give the
method to generate it. We have the following theorem:
We prove that if
Gð
N
1
;
N
2
;
I
Theorem 4.1.
Given an accurate data mapping I, and two SWF-nets N
1
andN
2
, thereexists amediator
M
with respect to I, such thatN
1
andN
2
can
be composed via
M
if
Gð
N
1
;
N
2
;
I
Þ
is well formed, that is,
1.
8
M
2 Rð
M
0
Þ
, there are an edge sequence
s
and a marking M
s
such that M
½
si
M
s
and M
s
M
e
; and
2. Given M
2 Rð
M
0
Þ
with M
M
e
,if
9
p
2
P, M
ð
p
Þ >
M
e
ð
p
Þ
,
then p
2
P
M1
[
P
M2
.
Its proof is given later. The proof shows that the CRG contains all
needed properties in mediator existence checking. Moreover, in our
method to build CRG, state-space exploration is sped up because CRG
is generated as a reduced state space of the composed services,
eliminating some intermediate states that are not relevant
to the
compatibility verification.
We can easily verify that
Gð
Þ
in Figure 4.8 is well formed.
Therefore, we claim that a mediator exists to glue N
1
and N
2
.
Figure 4.9a shows two services with no mediator to glue them.
Service X expects to receive message B and then sends message A in the
next step. Service Y expects to receive message A and then sends
message B in the next step. With data mapping
N
1
;
N
2
;
I
<
X.A, Y.A
>
,
<
X.B,
Y.B
, the CRG (Figure 4.9c) is not well formed. Therefore, X and Y
cannot be composed via mediation. Figure 4.9b shows the composition
of services X and Y with the given data mapping, and the resulting net
contains a deadlock in fact.
>
4.3.4 Proof of Theorem 4.1
The proof of Theorem 4.1 needs the concept of a stubborn set [117].
Intuitively, a set of transitions is called a stubborn set in a given
marking, if each transition in it remains to be stubborn (i.e., enabled)
when a transition outside it fires. This property infers that, in marking
M,ift
M
n
0
, then there is
2
T
S
, t
1
;
t
2
;
...
;
t
n
2
T
S
and Mt
1
t
2
...
t
n
½
i
M
n
t
½
i
a marking M
0
such that Mt
M
0
t
1
t
2
...
t
n
M
n
0
.
½
i
½
i
