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.
? 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, computational 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 2.1
Calculating State Spaces From 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 CFrag1,Frag2 between fragments Frag1 and Frag2 is a subset of VFrag1 × VFrag2 .
If CFrag1,Frag2 is a connection between fragments Frag1 and Frag2, then CFrag1,Frag2 (x, y) = {([v1, x], [v2, y]) | (v1, v2) ∈ C} is a connection between Frag1(x) and Frag2(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 Frag1, . . . , Fragn and connections C1, . . . , Cm, a transitions system TS = (V, E) is defined by V = Skn=1 VFragk and E =
v0:vα0: α
v3:vp31: p1
v8:vp81:cp1c
FraFgrsa5g5 v1:vω1a:ωa v2:vp21:bp1b FraFgrsa3g3 v4:vω4: ω v9:vω9: ω v5:vp51:dp1d v6:vp62: p2 v7:vp71:bp1a (a) Fragments
Sin=1 EFragi ∪ Sm
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. 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
semantics [
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 output1places a and b that are depicted on the dashed frame. EExxamampleple 1 a b c d a b c ω d α ω α
p1 p1
p2 (a) Open net Pp2 ?b s1 s?a 1 s3 ?a s2 ?b ?b !d !c
s4s2!?ca,?b ?a,?bs3 s?5b ?a!?da,?sb4 ?as,6?b
s5 ?a?a,?b s6 (b) Most permissive strategy R∗ for P ?a,?b ?a n4 n1τ n2
n1 ?b τ Fig. 2. Open net P and
n3 n ?bi?tas!d mo2st p?bermissive strat?a egn5y R∗. ?xn3 (!x) denotes a sne4nding?(brec!deiving) message x th?aat produces a token on
n input place5 x (consumes a token from output place x) in P .
As a correctness criterion for an open net N we require the absence of deadlocks 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 [
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 [
When computing R∗ we have the information needed to calculate the fragments 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
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 CFrag1,Frag2 . 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 ?b
Fig. 3. Constructing the state space P ⊕ R from the fragments for a given service R. Note that the ?b edge in state n5 yields [n4, s6] ∈ ρ. However, as s6 is not reachable, there is no fragment for state s6 and hence there is no transition from Frag5 to Frag3. (a) Requester R (b) TS R 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 = {CFrags,Frags0 (n, n0) | [n, s] ∈ %, [n, x, n0] ∈ δR (x 6= τ ), [s, x, s0] ∈ δR∗ (which implies [n1 0, s0] ∈ %)} ∪ {idFrags (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 livelocks. 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 stateof-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
condensation rules from [
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
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 [