A Finite Representation of all Substitutable Services and its Applications

Abstract

We present a finite representation of all substitutable services P 0 of a given service P . We show that our approach can be used for at least two applications: (1) given a finite set of services P = {P1, ..., Pn}, we provide a representation of all services P 0 that can substitute every Pi ∈ P, and (2) given a service P 00 that cannot substitute a service P , we find the most similar service P ∗ to P 00 that can substitute P .

Introduction

? Funded by the DFG-Graduiertenkolleg 1324 “METRIK”.

?? Funded by the DFG project “Substitutability of Services” (RE 834/16-1). ? ? ? Supported by the DFG project “Operating Guidelines for Services” (WO 1466/8-1).

The remainder of this paper is organized as followed. Section 2 recalls some formalisms and substitutability notion. Section 3 presents a finite representation of all services P 0 that can substitute a given service P . Section 4 outlines a method to compute a finite representation of all services P 0 that can substitute all services Pi ∈ {P1, ..., Pn} that are given. Section 5 shows how to correct errors in a non-substitutable service P 00 with respect to a given service P . Finally, Section 6 concludes the paper. 2

Background

We model the behavior of a service P with a service automaton. A service automaton is a finite state automaton with a set Q of states, a set F ⊆ Q of final states, an initial state q0 ∈ Q, a set I of input interfaces, a set O of output interfaces (I and O are pairwise disjoint), and a non-deterministic transition relation δ ⊆ Q × {I ∪ O ∪ {τ }} × Q. The edges are labeled with output message x ∈ O sent to (labeled “!x”) the environment, or input message x ∈ I received from (labeled “?x”) the environment, or internal move (label “τ ”). A non-final state with no outgoing transition is called a deadlock.

Given two service automata P and R, their composition P ⊕ R is a service automaton in which its set of states is the cartesian product of QP , QR, and the set of all multisets of pending messages between P and R. We assume that two composable service automata have compatible interfaces (IP = OR and IR = OP ), but all other constituents are pairwise disjoint. The composition P ⊕ R is deadlock-free if P ⊕ R does not contain a deadlock. R is a strategy of P iff P ⊕ R is deadlock-free. The strategy relation is symmetric, that is, R is a strategy of P implies P is also a strategy of R. We write Strat(P ) to denote the set of all strategies of P . See [ 2 ] for further details.

Throughout this paper, we assume a deadlock-free composition, i.e., there always exists at least one strategy for a given service.

An operating guideline OG (P ) of P is a deterministic service automaton Sφ where each state q of S is annotated with a Boolean formula φ(q). A matching relation between states of a service automaton and Sφ are used to characterize a set of service automata. We write Match(Sφ) to denote the set of all service automata S0 that satisfies a matching relation with Sφ. OG (P ) characterizes the (possibly infinite) set of all strategies of P , i.e., Match(OG(P )) = Strat (P ) [ 2 ].

Figure 1(a) depicts a service automaton P1 and Fig. 1(b) depicts an operating guideline of P1.

We define our substitutability notion called accordance. A service P 0 substitutes a service P under accordance (P 0 accords with P ) iff every strategy of P is also a strategy of P 0, i.e., Strat (P ) ⊆ Strat (P 0). We assume that P and P 0 are interface equivalent (IP = IP 0 and OP = OP 0 ) and write Accord (P ) to denote the (possibly infinite) set of all services P 0 that substitute P under accordance.

[ 3 ] presents an algorithm to decide whether P 0 substitutes P under accordance using their operating guidelines.

!A ?C

?D (a) P1 !B ?E ?A !C p1: ?A ∧ ?B

?B p2: !C p3: !D ∨ !E !D

!E p4: final (b) OG(P1) τ ?A

?B τ τ

τ !C !D !D !E !E τ q2: ?C q3: ?D ∧ ?E !A ?C q1: !A ∨ !B

?D q4: final !B

?E (c) MS (P1) (d) OG(MS (P1)) Definition 1 (Maximal Strategy, MS ). Let P be a service automaton and OG (P ) = Sφ be its operating guideline. A maximal strategy of P , denoted MS (P ), is obtained from S by replacing every node q by a non-deterministic internal choice between all the valid combinations of outgoing edges from q w.r.t. satisfying assignment in φ(q).

Proposition 1 ([ 5 ]). Let P be a service automaton such that Match(OG (P )) 6= ∅. Then for all R ∈ Match(OG (P )) holds: Strat (MS (P )) ⊆ Strat (R).

By the help of Proposition 1 we prove that OG(MS (P )) represents the set Accord (P ) of all service automata P 0 that can substitute a service automaton P under accordance.

Theorem 1 (Characterizing all substitutable services). Let P and P 0 be two service automata. Let OG (P ) be an operating guideline of P . Then, P 0 substitutes P under accordance iff P 0 ∈ Match(OG (MS (P ))).

Strat (P ), Accord (P ) = T Strat (P ) : P 0 ∈ Strat (R)} = T

Next, we will show that T

R∈Match(OG(P )) Strat (R) follows.

R∈Strat(P )) Strat (R). Since Match(OG (P )) = R∈Match(OG(P )) Strat (R) = Match(OG (MS (P ))).

Consequently, Accord (P ) = Match(OG (MS (P ))).

T T can conclude that T conclude that T know MS (P ) ∈ Strat (P ) and Strat (P ) = that for all R ∈ Match(OG (P )) holds: Strat (MS (P )) ⊆ Strat (R). Therefore, we R∈Match(OG(P )) Strat (R) ⊆ Strat (MS (P )). Proposition 1 asserts

R∈Match(OG(P )) Strat (R) = Strat (MS (P )). We

Match(OG(P )). Therefore, we can R∈Match(OG(P )) Strat (R) = Strat (MS (P )) immediately follows.

We know Strat (MS (P )) = Match(OG (MS (P ))). Thus, we can conclude that R∈Match(OG(P )) Strat (R) ⊇ Strat (MS (P )). Consequently, tu Proof. We will show that Accord(P ) = Match(OG (MS (P ))). lation is a symmetric relation, we conclude that Accord (P ) = Consider Accord (P ) = {P 0 | Strat (P ) ⊆ Strat (P 0)}. Since the strategy re{P 0 | ∀R ∈

Theorem 1 shows that the operating guideline OG (MS (P )) is a finite representation of all P 0 that can substitute P under accordance.

Our result enables a service designer to effectively derive P 0 from OG (MS (P )). Clearly, P 0 can substitute P under accordance, as it matches with OG (MS (P )). The designer can also use P 0 as a template to tailor a new version P 00 by filling P 0 with some internal actions. This way, it can be decided if P 00 substitutes P under accordance by checking if P 00 ∈ Match(OG (MS (P ))).

With our approach, we can also decide accordance (as presented in [ 3 ]) of two services P 00 and P by checking if P 00 ∈ Match(OG (MS (P ))). 4

Conjoining Substitutable Services

Suppose a service designer would like to design a new service which can support all potential customers of both a hotel booking service and a flight booking service. The representation of all services that can substitute both booking services is helpful for the designer. With this representation, the designer can decide whether such a new service does exist, and in case it does, a well-suited upgrade of a new service can be derived immediately from such a representation.

Pi∈P section T

For a finite set P = {P1, .., Pn} of service automata, we show that the inter

Accord(Pi) of sets of all services that accord with every Pi can be represented by the product of all operating guidelines of maximal strategy MS (Pi) of Pi, where Pi ∈ P

.

The product of two operating guidelines [ 3 ] is defined as an operating guideline that characterizes the intersection of all service automata that match with these two operating guidelines. The product of two operating guidelines assumes that both operating guidelines are interface equivalent.

Match(OG (S2)).

Proposition 2 ([ 3 ]). Let OG

⊗ = OG (S1) ⊗ OG (S2) be the product of operating guidelines OG (S1) and OG (S2), Then, Match(OG ⊗) = Match(OG (S1)) ∩ ?C !A ?D !B ?E ?C !A r1: !A ∨ !B ?D r4: final !B ?E r2: ?C ∧ ?D r3: ?E q2r2: ?C ∧ ?D

q3r3: ?D ∧ ?E ?C !A q1r1: !A ∨ !B ?D q4r4: final

?D (c) OG⊗ !B ?E Corollary 1 (Characterizing intersection of substitutable services). Let P1 and P2 be two service automata. Let OG (P1) be an operating guideline of P1 and OG (P2) be an operating guideline of P2. Then,

Match(OG (MS (P1)) ⊗ OG (MS (P2))) = Accord (P1) ∩ Accord (P2). Proof. Follows from Proposition 2 and Theorem 1. tu

Corollary 1 shows that we can use the product of operating guidelines to compute the finite representation of all services that accords with both P1 and P2. In case the returned product describes an empty set, there is no service automaton P 0 that can substitute both P1 and P2 under accordance.

Since the product ⊗ of operating guidelines is commutative and associative, the result from Corollary 1 can be easily generalized to the product of any finite number n of operating guidelines of MS (Pi), where Pi ∈ {P1, .., Pn}. (a) P2

(b) OG(MS (P2))

⊗ as a finite representation of all services that can substitute both P1 (Fig. 1(a)) and P2 (Fig. 2(a)) under accordance. OG the synchronous product of OG (MS (P1)) and OG (MS (P2)), where each node is annotated with the conjunction of the two Boolean formulas of the corresponding ⊗ is states of OG (MS (P1)) and OG (MS (P2)). For example, the node q2r2 in OG is annotated with φ(q2r2) =?C∧?D, which is the conjunction of φ(q2) =?C in ⊗ 5

Correcting Non-Substitutable Services

Suppose a service designer has designed an ill-suited upgrade of a travel agency service that does not accord with the travel agency service. Synthesizing a new well-suited upgrade of the service using an approach proposed in Section 3 may not be sufficient, as the well-suited upgrade might be very different and totally ignore the structure of its ill-suited upgrade version. The designer might prefer to reuse an ill-suited upgrade of the service instead of synthesizing a new well-suited upgrade of the service.

To reuse an ill-suited upgrade of the service, the errors found in the ill-suited upgrade can be fixed manually. Nevertheless, the manual correction is a tedious and error-prone procedure. This scenario motivates a method to synthesize a well-suited upgrade of the service automatically from its ill-suited upgrade.

Given two service automata P and P 00 where P 00 does not accord with P , we propose a procedure to correct P 00 with respect to P . The errors in P 00 can be detected and corrected automatically using a simulation-based graph edit distance, as introduced in [ 4 ] to fix a faulty service to cooperate deadlock-freely in a choreography. The approach takes P 00 and OG (MS (P )) as its input, computes the most similar service automaton P ∗ to P 00 such that P ∗ ∈ Match(OG (MS (P ))), and returns the edit actions that are necessary to transform P 00 into P ∗. Clearly, P ∗ can substitute P under accordance, as it matches with OG (MS (P )). That is, P ∗ cooperates deadlock-freely with every strategy of P . This way, P 00 can be reused, as P ∗ is most similar to P 00, yet accords with P .

So far the simulation-based graph edit distance approach is applicable only for acyclic and deterministic services [ 4 ]. 6

Conclusion

We have proposed an approach to characterize the set Accord (P ) of all services P 0 that can substitute a service P under accordance. We have shown that a finite representation of Accord (P ) can be computed using the concept of a maximal strategy [ 5 ] and its operating guideline [ 2 ]. With this representation, we can decide accordance of two services and derive from it a new service that accords with a given service.

We have shown two applications of our approach. Given a finite set of services P = {P1, ..., Pn}, we provide a representation of the intersection of Accord (Pi) for all Pi ∈ P with the help of the product of operating guidelines [ 3 ]. For a service P 00 that cannot substitute a service P , we provide an automatic correction procedure to transform P 00 into the most similar P ∗ such that P ∗ accords with P with the help of the simulation-based graph edit distance [ 4 ].

References

1. Papazoglou , M.P. : Web Services: Principles and Technology . Pearson - Prentice Hall , Essex ( 2007 )

2. Lohmann , N. , Massuthe , P. , Wolf , K. : Operating guidelines for finite-state services . In Kleijn, J., Yakovlev , A., eds. : ICATPN 2007 . Volume 4546 of LNCS ., SpringerVerlag ( 2007 ) 321 - 341

3. Stahl , C. , Massuthe , P. , Bretschneider , J.: Deciding substitutability of services with operating guidelines . LNCS ToPNoC II(5460) ( 2008 ) 172 - 191

4. Lohmann , N.: Correcting deadlocking service choreographies using a simulationbased graph edit distance . In Dumas, M. , Reichert , M., eds. : BPM 2008 . Volume 5240 of LNCS ., Springer-Verlag ( 2008 ) 132 - 147

5. Mooij , A.J. , Voorhoeve , M. : Proof techniques for adapter generation . In Bruni, R., Wolf , K., eds. : WS-FM 2008 Milan, Italy, Proc. LNCS , Springer-Verlag ( 2008 )