In a service-oriented architecture, a provider publishes its service in a service repository. A requester approaches a broker which returns a service S matching the requester's service R. Then, S and R are coupled. The provider of S may require a specific relation between the expenses and rewards for an execution of S, summarized in a policy ϕ. The control flow of S may contain both internal and external decisions: By sending messages, R may trigger a certain execution path. Based on models of S and R, the broker may decide if R violates ϕ before coupling. If so, the broker may not couple S and R. In this paper, we provide a formal framework to model policies, and introduce a decision procedure for policy violation based on open net models of the services.
We understand a service as a component with an inner control flow and an interface to exchange messages asynchronously with other services. Thereby, it provides a certain functionality which may be used by other services. A provider publishes its service in a repository. A requester approaches a broker for accessing a previously published service. The provider earns a reward for providing its service. This reward may manifest as a usage fee, or a provision from the repository owner, or from any third party. Usually, a provider desires some beneficial relation between this reward and the expenses for providing its service. As an example, a provider might want the expenses to be covered by the reward. We specify such requirements as policies. A partner either violates a policy or not. The provider aims at its service being coupled only with non-violating partners. Both reward and expenses may have fixed and variable components. This is a quite usual problem in economics and solutions for this problem are known for a long time. However, in our case, we encounter another difficulty: We consider stateful services. A stateful service has its own control flow which is influenced by internal and external decisions. External decisions are made through asynchronous message exchange. Therefore, reward and expenses for providing a service vary from requester to requester.
As a running example, consider a vending machine which sells coffee and tea,
modeled as an open net [
ω 1 !coffee !tea 2 !tea !coffee 3 !quit 4 !quit
!quit (c) V(ϕ) three messages: Either an order for coffee, an order for tea, or a quit message. To receive an order it executes the respective transition c or t. Subsequently, it serves the beverage by executing b. A quit message may be consumed by executing q, resulting in a final state ω. The machine may serve up to three beverages, as indicated by the three tokens in the place in the bottom. The provider of the vending machine may have fixed expenses of 10 units for providing its service and variable expenses for each served beverage depending on the type: 20 units for coffee and 10 units for tea. As a reward, the provider collects a fixed amount of 5 units and additionally 25 units per served beverage. Assume the provider desires the expenses to be fully covered by the reward, specified in a policy ϕV. We find that a customer ordering at least one beverage is a good customer, whereas a customer ordering nothing and simply quitting is not. However, asynchronous message exchange induces a subtle problem: A customer ordering a beverage and then sending the quit message before receiving the beverage is a bad customer: The vending machine might receive the quit message first. A simple partner for V is shown in Fig. 1(b): D orders either a tea or a coffee, receives the beverage, and sends a quit message. Obviously, D does not violate ϕV.
There exists work on quality of service (QoS), e.g. [
5 !quit coffee
tea beverage
quit (a) Service V
(b) Service D 1 !coffee !tea 2 3 ?beverage ?beverage 4 !quit
5
(d) A(D)
which reach a specific goal in the least expensive way, e.g. [
We sketch our solution. Upon publishing, the provider states its requirements
in form of a policy ϕ. Upon requesting, the broker decides whether the requester
violates the policy or not. This procedure is similar to that of Operating
Guidelines [
We illustrate our approach on the running example: Figure 1(c) shows automaton V(ϕV) which finitely represents violating partner behavior. For instance, the sequence !tea!quit (read: send tea, send quit) may result in expenses that are not covered by the reward and therefore violates ϕV. By comparing V(ϕV) with an abstract model of a requester, the broker may decide policy violation. For example, automaton A(D) in Fig. 1(d) is an abstract model of open net D in Fig. 1(b). Comparing V(ϕ) and A(D), we find no common path to a final state. Therefore, D does not violate ϕV. As a consequence, the broker may return V.
The rest of the paper is structured as follows: Section 2 shortly recalls basic formal concepts, especially open nets. We introduce a framework for policies in Sect. 3. We sketch our approach to compute a finite representation of violating behavior in Sect. 4. Finally, we conclude our paper and present ideas for future work in Sect. 5. 2
As usual, Z denotes the set of all integers. We write Σ∗ for the set of all finite sequences over an alphabet Σ. For σ ∈ Σ∗, we write σ(i) for the i-th character in σ. We denote the restriction of σ to Σ0 ⊆ Σ with σ|Σ0 . We recall the basic notions of Petri nets: A Petri net is a tuple N = hP, T, F, m0i of places P , transitions T , arcs F and initial marking m0. We denote the set of all markings of N with MN . We denote the preset and postset of x ∈ P ∪ T with •x and x•, respectively. We canonically extend these notions to sets of net elements by union. We call a sequence σ ∈ T ∗ firing sequence if the transitions in σ may be fired subsequently starting in m0. We write beh(N, m) for the set of all firing sequences resulting in a marking m.
Open nets are Petri nets with an interface declaration and a set of final markings: We define an open net as a tuple N = hP, T, F, m0, I, O, Ωi where hP, T, F, m0i forms a Petri net, I, O are disjoint subsets of P with •I ∪ O• = ∅, called input and output places, respectively, and Ω ⊆ MN is a set of final markings. We call the Petri net ip(N ) = hP 0, T, F 0, m00i the inner process of N where P 0 = P \ (I ∪ O), F 0 = F ∩ ((P 0 × T ) ∪ (T × P 0)), and m00(p) = m0(p) for all p ∈ P 0. We call two open nets N1, N2 partners if their inner processes are component-wise disjoint, I1 = O2, and O1 = I2. We compose two partners N1, N2 by accordingly merging the interface places, yielding N1 ⊕ N2. Example 1. Figure 1(a) shows an open net V with input places quit, coffee and tea, and output place beverage. The set ΩV of final markings cannot be seen from the figure. We define ΩV = {m | m ∈ MV ∧ m(ω) > 0}. The open net D in Fig. 1(b) and V are partners. 3
A policy specifies the allowed behavior of a provided service N in composition with an arbitrary partner Q. The main building blocks of a policy are cost functions and constraints. For the following definitions, we assume a given open net N with transitions TN .
Cost functions. There are different approaches to define cost functions based on behavior. The most general is to define a cost function as a mapping from transition sequences to some value domain. Throughout this paper, we use the set of integers Z for this purpose. In our approach, we specify the costs for executing a single transition after having executed a (finite) history. This covers varying costs for executing a single transition based on the knowledge which transitions have been fired. A cyclic service usually has infinitely many and arbitary long (finite) runs. To ease up analysis, we encode histories into hash values.
A hashing from a set A into a set B is a function f : A → B. Usually, the idea is that the elements of B, called hash values, are more lightweight than those of A. Thus, a hash function may be used for efficient table lookups and the like. Typically, a hash function is required to fulfill a number of properties ensuring its usability. In this paper, we use finite histories as input: a finite sequence of transitions. We define a history hashing h as a hashing from TN∗ into some set H having two properties: Continuity and Finiteness.
Definition 1 (Continuity, finiteness, history hashing). We define two properties for functions h : TN∗ → H: 1. Continuity. Let σ, σ0, σ00 ∈ TN∗ . If h(σ) = h(σ0), then h(σσ00) = h(σ0σ00). 2. Finiteness. H is finite.
We call h a history hashing if h has both properties continuity and finiteness.
Intuitively, continuity demands that, given two histories with the same hash value, each equal continuation of the two results in the same hash value again. Finiteness restricts history hashings to finite sets of hash values. We elaborate on the value of these properties for analysis in Sect. 4. For the definitions of this section, we assume a given history hashing h into a set of hash values H.
As mentioned above, we define cost functions for executing single transitions based on the hash values. Thus, the domain of such a function is the cross product of the set of transitions and the set of hash values. Induction yields the semantics of the cost function: The costs for a complete transition sequence. Definition 2 (Cost functions). We call a function f : TN × H → Z cost function. We define the semantics of f as the function kf k : TN∗ → Z with – kf k ( ) = 0, and – kf k (σt) = f (t, h(σ)) + kf k (σ) if t ∈ TN , σ ∈ TN∗ .
Example 2. We define the cost functions mentioned in Sect. 1 for open net V in Fig. 1(a). For both functions, we need to know whether a coffee or a tea order has been received last. We cover those two cases by the hash values coffee and tea. For totality, we introduce a third hash value, other. We define a hash function h : TV∗ → H with TV = {c, t, b, q} and H = {coffee, tea, other}. We define the sets of occurrences of c and t in σ ∈ TV∗: OCσ = {i | σ(i) = c} and OTσ = {i | σ(i) = t}.
other h(σ) =
if OCσ = OTσ = ∅, coffee if OCσ 6= ∅ ∧ (OTσ 6= ∅ ⇒ max(OCσ) > max(OTσ)), tea otherwise.
Based on this hashing, we define the cost functions f and g over TV with hashing h to specify the expenses and the reward for the provider to execute V: – ∀t ∈ TV \ {b}, a ∈ H : f(t, a) = g(t, a) = 0, – f(b, coffee) = 20, f(b, tea) = 10, f(b, other) = 0, and – g(b, coffee) = g(b, tea) = 25, g(b, other) = 0.
The choice of the history hashing determines the class of cost functions that may be build. We propose to make use of deterministic finite automata (DFA). A history may be interpreted as a word. Using a history σ as input for a DFA, the resulting state q may be understood as a hash value for σ. Such a history hashing obviously satisfies continuity as a DFA is deterministic and total. Additionally, since its set of states is finite, finiteness holds. Utilizing such a hashing, we can express any cost function where conditions consist of checking membership of the history in regular languages.
Constraints. We introduce constraints as restrictions on behavior by specifying conditional bounds for cost functions. As conditions, we use markings. As bounds, we use integer intervals. Intuitively, a transition sequence meeting the condition satisfies a constraint if its costs are inside given bounds. If the transition sequence results in a different marking or cannot be fired, it trivially satisfies the constraint. Definition 3 (Constraints). We call a pair p = hm, τ i constraint over a set G of cost functions, iff m ∈ Mip(N) is a marking of the inner process of N and τ maps each cost function f to an integer interval.
A transition sequence σ ∈ TN∗ satisfies p = hm, τ i, written σ |= p, iff σ ∈ beh(ip(N ), m) ⇒ ∀f ∈ G : kf k (σ) ∈ τ (f ).
Example 3. We model the constraint informally described in Sect. 1: Upon reaching a final marking, all expenses should be covered by the reward. We define this as one constraint pm per final marking m ∈ ΩV. Each pm is defined over cost function (g − f) as defined in Example 2. At first glance, the acceptance interval for this cost function is [0, ∞). However, we did not model the fix costs yet. We thus shift the acceptance interval by the difference of the fix costs yielding i = [5, ∞). We inspect some example firing sequences and decide constraint satisfaction for each. The firing sequence cb trivially satisfies each pm since it does not result in a final marking. The firing sequences σ = cbq and σ0 = q result in a final marking. While σ satisfies each pm, σ0 does not: (g − f)(σ) = 5 ∈ i, (g − f)(σ0) = 0 6∈ i.
Policies. A policy is basically a collection of constraints over a given set of cost functions. Policy violation requires a change of the viewpoint: Policies are defined over the behavior of a fixed open net N . However, policy violation is not a property of N but of a partner Q of N . By sending messages to N , Q may influence the control flow of N . Intuitively, Q violates a policy ϕ, if it sends messages, such that N may choose a firing sequence which does not satisfy all constraints in ϕ. Formally, we define policy satisfaction for a transition sequence of N and based thereon policy violation.
Definition 4 (Policies). We define a policy as a tuple ϕ = hN, h, G, Ci where G is a set of cost functions and C is a set of constraints over G. A transition sequence σ ∈ TN∗ satisfies ϕ, written σ |= ϕ, iff ∀p ∈ C : σ |= p. A partner Q of N violates ϕ iff there exists a firing sequence σ of N ⊕ Q, such that σ|TN 6|= ϕ. Example 4. We combine the open net V from Fig. 1(a), the hashing h from Example 2, the cost functions f, g from Example 2, and the constraints pm (m ∈ ΩV) from Example 3 to policy ϕV = hV, h, {(g − f)}, {pm | m ∈ ΩV}i. We find cbq |= ϕV and q 6|= ϕV. Consider open net D from Fig. 1(b) as a partner for V. We answer the question if D violates ϕV or not: There are two firing sequences σ, σ0 of V ⊕ D which result in a final marking of V: σ|TV = cbq, and σ|0TV = tbq.
To decide whether D violates ϕV, we need to decide σ|TV |= ϕV ∧ σ|0TV |= ϕV which boils down to deciding ∀m ∈ ΩV : σ|TV |= pm ∧ σ|0TV |= pm. D does not violate ϕV because {(g − f)(σ|TV ), (g − f)(σ|0TV )} = {5, 15} ⊆ [5, ∞). 4
In this section, let N be an open net and ϕ = hN, h, G, Ci be a policy. Our approach follows three steps: (1) Compute the ϕ-state space S(ϕ). (2) Finitely represent all ϕ-violating behavior, yielding V(ϕ). (3) Decide policy violation utilizing V(ϕ).
The ϕ-state space. The state space of a system is usually a directed graph where each vertex represents a state of the system and each edge stands for a transition from the source state to the target state. In case of a Petri net, a state is a marking and an edge is a transition. Many properties may be decided on the state space by exploring the set of all states or their order.
Our property of interest is the following: Which firing sequences satisfy the given policy? The problem is that even a finite state space generally may represent infinitely many firing sequence due to cyclic behavior. This can be easily overcome if it is possible to transform the property into a state property, i.e. if it is sufficient to inspect a state to conclude if the firing sequences resulting in this state have the property or not.
We intend to do the same trick for our property of interest. In a first step, we enrich states with the so far incurred costs for each cost function. However, this is not sufficient: Let σ, σ0 be firing sequences resulting in the same costs and marking. Let σ00 be a transition sequence, such that σσ00 and σ0σ00 are firing sequences again. Then, σσ00 and σ0σ00 do not necessarily result in the same costs again.
Example 5. Consider the firing sequences σ1 = cbc and σ2 = cbt of the inner process of open net V from Fig. 1(a). According to cost function f from Example 2, both σ1 and σ2 result in the same state: Firing yields obviously the same marking and the same costs of 20 units. However, continuing with b, we find that f (cbcb) = 40 6= f (cbtb) = 30.
We thus add the hash value of the history. Formally, we define a ϕ-state as a triple q = hm, x, τqi consisting of a marking m, a hash value x, and a mapping τq : G → Z.
Example 6. We continue Example 6. According to the history hashing h from Example 2, the hash values for σ1 and σ2 are different: h(σ1) = coffee 6= h(σ1) = tea. We can distinguish the resulting states of σ1 and σ2 by their hash values.
Given a ϕ-state q, it is trivial to decide if the firing sequences resulting in
q satisfy the policy or not: We check membership of the current values given
by τq with the intervals given by τ for each constraint hm, τ i. Additionally, if
the ϕ-state space S(ϕ) is finite, we may compute it with a depth first search,
thereby exploiting property Continuity. Property Finiteness ensures that the set
S of reachable states is finite iff {hm, τqi | hm, x, τqi ∈ S} is. Given S(ϕ), we may
compute V(ϕ), similarly as in [
Deciding ϕ-violation. We finitely represent the ϕ-violating partner behavior as a finite automaton V(ϕ). Thereby, a word represents partner behavior: ?a!b?c stands for receiving a, followed by sending b and receiving c. We can represent the set of traces of the inner process of any open net Q as a finite automaton A(Q), if it is finite state. By setting the set of final states to the complete state set, policy violation may be decided by comparing the languages of V(ϕ) and A(Q). If their intersection is non-empty, Q violates ϕ.
Example 7. Figure 1(c) shows V(ϕV) of ϕV from Example 4, Fig. 1(d) shows A(D) of D from Fig. 1(b). V(ϕV) and A(D) do not share an accepting run, ϕV is not violated.
Similarly, we believe that V(ϕ) may be used as a constraint automaton as
introduced in [
We provided a formal framework to specify policies ϕ, describing acceptable behavior of a partner based on cost functions and constraints. We explained how a ϕ-state space may be computed and processed if it is finite. We sketched a decision procedure based on this representation. In the future, we aim at solving the problem that the ϕ-state space is not necessarily finite. We intend to apply techniques similar to the coverability graph for Petri nets. We plan to extend our proof of concept implementation to evaluate the practical usability of our approach with a case study.