An Approach to Tackle Livelock-freedom in SOA Christian Stahl1,2,? and Karsten Wolf3,?? 1 Humboldt-Universität zu Berlin, Institut für Informatik Unter den Linden 6, 10099 Berlin, Germany stahl@informatik.hu-berlin.de 2 Department of Mathematics and Computer Science Technische Universiteit Eindhoven P.O. Box 513, 5600 MB Eindhoven, The Netherlands 3 Universität Rostock, Institut für Informatik 18051 Rostock, Germany karsten.wolf@uni-rostock.de Abstract. We calculate a fixed finite set of state space fragments for a service P , where each fragment carries a part of the whole behavior of P . By composing these fragments according to the behavior of a service R we build the state space of their composition P ⊕R which can be checked for deadlocks and livelocks. We show that this approach is applicable to realize a “find” request by a service R with a provided service P in SOA. 1 Introduction In the paradigm of service-oriented computing (SOC) a service serves as a build- ing block for designing flexible business processes by composing multiple services. Service-oriented architectures (SOA) serve as an enabler for publishing services via the Internet such that these services can be automatically found. By dynam- ically binding published services with other services, a composed service that achieves certain business goals can be designed. In SOA, we would like to answer a “find” request by a service R with a provided service P such that P ⊕ R forms a sound, i.e. a deadlock-free and livelock-free system. The apparent approach is to have P (or a public view of P ) stored in the repository and to construct P ⊕R for checking the absence of dead- locks and livelocks upon “find”. This approach is, however, not feasible due to state space explosion, and the necessity to have P (or a formally equivalent pub- lic view) stored in the repository. State space reduction during the construction of P ⊕ R might help a lot but needs to be performed for each “find” request. Another approach is to publish an operating guideline [1] for each service P ; that is, an operational description of all services R such that P ⊕ R is sound. To answer a “find” request by R, one has to check whether R matches with the operating guidelines of P [1]. However, in this approach soundness is restricted to deadlock-freedom so far and hence livelocks in P ⊕ R are possible. ? 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). In this paper, we propose a novel approach. We still build the state space P ⊕ R, but not from operational descriptions of P and R. Instead, we calculate a finite set of state space fragments for a service P . Each fragment carries a part of the whole behavior of P . These fragments are published in a repository. Upon a “find” request by a service R, the state space of P ⊕ R is calculated by composing fragments of P according to the behavior of R. The resulting state space can then be checked for deadlocks and livelocks using a model checker. The approach has two advantages: 1. The construction of fragments and their internal state space reduction is done once for each published service at the “publish” phase. That way, computa- tional efforts are shifted from “find” to “publish”. This is a clear advantage as we expect the number of “find” to be much higher than the number of “publish”. 2. When reducing the size of fragments, we can apply reduction techniques which are different from standard state space reduction techniques used in model checking. In fact, we may reduce the transition system after having computed it. Section 2 formalizes fragments, shows how fragments for a given service P can be computed, and it presents how the state space P ⊕R can be built from the fragments of P . Section 3 sketches several abstractions to condense fragments while preserving deadlocks and livelocks and, finally, Sect. 4 concludes the paper. 2 Calculating State Spaces From Fragments 2.1 Formalizing Fragments In this section, we define fragments and connections between these fragments. A (state space) fragment Frag = (V, E, F ) is a graph that consists of a set V of nodes, a set E ⊆ V × V of (directed) edges, and a set F ⊆ V of final nodes. We assume that different fragments have disjoint sets of nodes. Let x be an element of some fixed set M . An instance Frag(x) of a fragment Frag is built by renaming the constituents as follows: v 7→ [v, x], e = [v1 , v2 ] 7→ [[v1 , x], [v2 , x]] for all v ∈ V and e ∈ E. That way, the structure is preserved but the nodes get previously unused names. To plug different fragments yielding again a state space, we define connections which link states of one fragment to states of another fragment. A connection CFrag 1 ,Frag 2 between fragments Frag 1 and Frag 2 is a subset of VFrag 1 × VFrag 2 . If CFrag 1 ,Frag 2 is a connection between fragments Frag 1 and Frag 2 , then CFrag 1 ,Frag 2 (x, y) = {([v1 , x], [v2 , y]) | (v1 , v2 ) ∈ C} is a connection between Frag 1 (x) and Frag 2 (y). Consider the fragments and the connections depicted in Fig. 1. For instance, we have fragment Frags1 = ({v0 , v1 , v2 }, {(v0 , v1 ), (v0 , v2 ), ∅}) and connection CFrags1 ,Frags3 = {(v1 , v4 )}. Thereby, v0 relabels α, v1 relabels ωa, etc. Given a set of fragments Frag 1 , . . . , Frag n and connections Sn C1 , . . . , Cm , a transitions system TS = (V, E) is defined by V = k=1 VFrag k and E = Example11 Example Frag Frag s1 1 Frag Frag s2 2 Frag Frag s4 4 Frag Frag s5 5 v0: vα0: α v3: vp31: p1 v8: vp81:cp1c v : vp :dp d v1 v1 v4 v4 5 51 1 Frag Frag v2 v2 v3 v3 1: ωa v2: v v1: vωa p21:bp1b v9: vω9: ω s3 3 v6: vp62: p2 v4: vω4: ω v3 v3 v5 v5 v3 v3 v8 v8 v7: vp71:bp1a v7 v7 v3 v3 (a) Fragments (b) Connections Fig. 1. Fragments and connections. Dotted (solid) lines denote fragment internal tran- sitions (connections). Sn Sm i=1 EFrag i ∪ j=1 ECj . Thereby, several instances of one and the same fragment 2 2 or connection may be used to build TS . In the following, we introduce our service model open nets and show how fragments and connections of an open net can be calculated. 2.2 Open Nets and Most Permissive Strategy We use open nets as a service model. An open net N consists of a Petri net together with an interface. The interface is divided into a set of input places and output places. Input places have an empty preset, output places have an empty postset. Furthermore, N has a distinguished initial marking m0 , and a set Ω of final markings such that no transition of N is enabled at any m ∈ Ω. We further require that in the initial and the final markings the interface places are not marked. The behavior of an open net is defined using the standard Petri net seman- tics [2]. With RN (m0 ) we denote the set of reachable markings of N . For example, the open net P depicted in Fig. 2(a) has an initial marking m0P = [α] and the set of final markings is defined by ΩP = {[ω]}. P has two input places c and d and two output places a and b that are depicted on the dashed frame. Example 1 Example 1 α s1 n1 α ?b ?a s1 τ n1 n2 a s2 ?b s3 ?a ?b τ ?a ?b !d !c Fig. n3 2. n2 Open net P and b ?a,?b a s s n4 its most permissive ?b strat- s4 2 ?a,?b 3 ?b ?a!d !c ∗ ω p1 ?b !d ?a,?b ?a,?b ?a egy n5 R . ?x n3 (!x) denotes a b s5 ?a s s6 n4 sending (receiving) message 4 ?a,?b ?b !d c x that?a produces a token on ω p1 p2 s5 ?a,?b n5 input place x (consumes a d ?a s6 token from output place x) c (a) Open net Pp2 (b) Most permissive in P . d strategy R∗ for P 1 1 As a correctness criterion for an open net N we require the absence of dead- locks and livelocks in N . N is deadlock-free and livelock-free if for all reachable markings m ∈ R(m0 ), RN (m) ∩ ΩN 6= ∅. For the composition of two open nets M and N , we require that the input places of M are the output places of N and vice versa. M and N can be composed by merging input places of M with equally labeled output places of N and vice versa. As we are interested in composing open nets such that the composition is deadlock-free and livelock-free we define the notion of a strategy. An open net M is a strategy for an open net N if M ⊕ N is deadlock-free and livelock-free. In [1] it has been proven that there always exists a most permissive strategy R∗ for an open net N that has richer behavior than every other strategy for N . The most permissive strategy for P (of Fig. 2(a)) is depicted in Fig. 2(b). It is an automaton (which can easily be transformed in a state machine and by adding an input (output) place for each ?x (!x) to an open net) with initial state s1 and two final states s3 and s4 . State s6 is depicted for technical purposes only. Every edge to s6 shows a possible set of messages R∗ can receive but that will never occur because P cannot send them. For R∗ we can prove the following useful property. Lemma 1. If R is a strategy of P , then R∗ weakly simulates R. The converse does not hold in general. The automaton R∗ (see Fig. 2(b)) weakly simulates R (see Fig. 3(a)) but P ⊕ R has a livelock (as we will see later on). In fact, R is an example why the operating guideline approach in [1] is not applicable to tackle livelock-freedom. When computing R∗ we have the information needed to calculate the frag- ments and connections of P . Each state s of R∗ is a fragment. In each state s, R∗ has knowledge about the possible markings of P in s. These markings (together with their transitions) are the nodes and the edges of the fragment. Figure 1 shows the fragments and the connections of P . Frags1 is the fragment derived from s1 , Frags2 from s2 and so on. For s6 there is no fragment. We have relabeled the markings of all fragments by v0 , . . . , v9 to make the internals of P anonymous. For each edge of R∗ , we define a connection. The connection is calculated from the edges of R∗ and the markings. Given a service R, the most permissive strategy R∗ for P and the fragments and connections of P , we show in the following how a transition system P ⊕ R can be constructed. 2.3 Fragments and Connections for P From the construction of fragments we know that for each state s of R∗ , its state space is defined by the fragment Frag s . Furthermore, for each pair of fragments Frag 1 6= Frag 2 , the set of edges with source in Frag 1 and sink in Frag 2 is defined by connection CFrag 1 ,Frag 2 . For each fragment Frag, let idFrag denote connection CFrag,Frag . Then, by Lemma 1, R can only be a strategy for P if R∗ (weakly) simulates R. Example 1 Frags1(n1) [v0,n1] Example 1 Frags1(n2) [v0,n2] Fig. 3. Constructing [v1,n1] [v2,n1] the state space P ⊕ R [v1,n2] [v2,n2] from the fragments n1 Frags2(n3) for a given service s1 Frags3(n4) [v3,n3] ?b ?a τ Frags5(n5) R. Note that the ?b [v4,n4] n2 [v5,n5] edge in state n5 yields s2 s3 ?b ?a [n4 , s6 ] ∈ ρ. However, ?b !c !d ?a,?b n3 [v6,n5] as s6 is not reachable, n4 s4 ?a,?b ?b !d there is no fragment ?a [v7,n5] for state s6 and hence ?a,?b n5 s5 ?a s6 there is no transition (a) Requester R (b) TS R from Frag5 to Frag3 . 3 Definition 1 (Construction of TS R ). Let % be simulation relation between R and R∗ . Compose transition system TS R from the following fragments and connections: – FRAG = {Frag s (n) | [n, s] ∈ %}, – CONN = {CFrag s ,Frag s0 (n, n0 ) | [n, s] ∈ %, [n, x, n0 ] ∈ δR (x 6= τ ), [s, x, s0 ] ∈ δR∗ (which implies [n1 0 , s0 ] ∈ %)} ∪ {idFrag s (n, n0 ) | [n, s] ∈ %, [n, τ, n0 ] ∈ δR } The fragment that corresponds to the initial state of R and R∗ is unique and it contains the initial state of the resulting transition system TS R . In our example, (n1 , s1 ), (n2 , s1 ) ∈ %. Thus we add two instances of Frags1 , i.e. Frags1 (n1 ), Frags1 (n2 ). As we have transition [n1 , τ, n2 ] ∈ δR in R we add connection idFrags1 (n1 , n2 ). Furthermore, we add fragment Frags3 (n4 ) because (n4 , s3 ) ∈ %. From transition [n2 , ?a, n4 ] ∈ δR in R and [s1 , ?a, s3 ] ∈ δR∗ we conclude that connection CFrags1 ,Frags3 (n2 , n4 ) for ?a has to be added. Figure 3(b) shows the resulting state space P ⊕ R. TS R contains a livelock (the nodes of Frags2 (n3 ) and Frags5 (n5 ) have no final node), thus R is no strategy for P . The resulting transitions system T SR can be verified for deadlocks and live- locks. Our main result of this paper guarantees that each deadlock and livelock in P ⊕ R is preserved in TS R and vice versa. Theorem 1. Let R be a strategy for P and let TS R be as defined above. Then TS R is bisimilar to the state space P ⊕ R. 3 Deadlock and Livelock-preserving Abstraction To speed up the model checking run when checking TS R , we can apply state- of-the-art reduction techniques such as partial-order and symmetry reduction. Besides this, we statically reduce the fragments. This may lead to a smaller TS R and thus increasing the performance of our approach and, in addition, we need to store smaller fragments in the repository (when publishing P ). All abstractions we sketch in the following preserve both deadlocks and livelocks. For each fragment we compute its strongly connected components (SCCs). It is sufficient to store only SCCs instead of nodes. To condense the state space of each fragment, we adapt state space conden- sation rules from [3]. These rules can be applied to each fragment. For example, we can condense the three SCCs in Frags5 (see Fig. 1(a)) to a single SCC. Finally, we can also minimize R, in particular, its τ transitions. For instance, we can apply minimization rules that preserve branching bisimulation. That way, states n1 and n2 in Fig. 3(a) could be merged. 4 Conclusion We have proposed a technique to realize the “find” operation in SOA in case the composed system is required to be free of deadlocks and livelocks. We suggest that a service provider publishes a set of state space fragments such that each fragment carries a part of the whole behavior of P . Given a requester R, “find” means to construct the state space P ⊕ R from the fragments of P guided by the behavior of R. The resulting state space is checked for deadlocks and livelocks. Although the space complexity is the product of the state spaces of R and P (in worst case), we assume that applying abstraction techniques results in much smaller states spaces. We are currently implementing the proposed approach in our analysis tool Fiona [4]. The computed state space P ⊕ R can then be checked for deadlocks and livelocks using the model checker LoLA [5]. Future work also includes a case study to validate the strength of the abstraction techniques. References 1. Lohmann, N., Massuthe, P., Wolf, K.: Operating guidelines for finite-state services. In Kleijn, J., Yakovlev, A., eds.: 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings. Volume 4546 of Lecture Notes in Computer Science., Springer-Verlag (2007) 321–341 2. Reisig, W.: Petri Nets. EATCS Monographs on Theoretical Computer Science edn. Springer (1985) 3. Juan, E.Y.T., Tsai, J.J.P., Murata, T.: Compositional Verification of Concurrent Systems Using Petri-Net-Based Condensation Rules. ACM Trans. on Programming Languages and Systems 20(5) (1998) 917–979 4. Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing Interacting BPEL Processes. In Dustdar, S., Fiadeiro, J., Sheth, A., eds.: Fourth International Confer- ence on Business Process Management, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings. Volume 4102 of Lecture Notes in Computer Science., Springer- Verlag (2006) 17–32 5. Schmidt, K.: LoLA: A low level analyser. In Nielsen, M., Simpson, D., eds.: 21st International Conference on Application and Theory of Petri Nets, ICATPN 2000, Aarhus, Denmark, June 26-30, 2000, Proceeding. Number 1825 in Lecture Notes in Computer Science, Aarhus, Denmark, Springer-Verlag (2000) 465–474