In a service-oriented architecture, Services are components that interact with each other via well-dened interfaces. Open nets are a special class of Petri nets, designed to model the behavior of open systems. Asynchronous interaction and stateful behavior complicate predicting the combinations of messages that a service can process. We present proles which support the modeler in verifying compliance of the model with given constraints, without knowing its future environment. We explain the computation of proles by static Petri net analysis.
In a service-oriented architecture (SOA) [
Well-developed methods to analyze the behavior of a service S with open
nets, already exist alongside dierent behavioral correctness criteria such as
controllability [
In this paper we present an approach to solve a specic class of behavioral constraints based on well-known static Petri net analysis techniques. Such a constraint species lower and upper bounds for the occurrence of events in the interaction with other services. An event occurs when a message is sent or received. A constraint might e.g. demand the exchange of a single message or 1 Available at http://www.service-technology.org/tools restrict the occurrence of a linear combination of events. A prole for S is a set of constraints that S satises. Since there exists an innite number of linear combinations of events, there also exists an innite number of proles for S, providing dierent levels of precision. But we can inuence this aspect when computing a prole, such that it meets the requirements of the use case. We formally dene the class of constraints, the concept of proles as well as their computation with static Petri net methods in Sec. 3.
Proles can be applied in dierent phases in the lifecycle of a service S. The modeler of S can use proles to prove that the model complies with the specication. Other analysis methods can benet from proles, in this case proles are used as a preprocessor. During implementation of S, proles can be used to generate test cases, since a prole contains constraints that the model satises. After deploying S it will be available in a service repository. A prole can be used to store an abstraction of S that can support behavioral query resolving. A prole, however, does not cover all aspects of S: It is restricted to abstract interaction behavior. We will discuss the application of proles in Sec. 4. We conclude the paper in Sec. 5 with open issues and ideas for further work. 2
CB
C
E TB T
C CB
E T TB
CB
C
TB E T pf (a) N1 pf (b) N2 pf (c) N3
Two services interact by exchanging messages over channels predened in the interface of a service. We assume an asynchronous communication model: Sending and receiving of a message does not occur in the same moment, as opposed to hand-shaking-techniques. Thus, for each exchanged message, two events occur: Sending and receiving. From the viewpoint of one of the involved services however, only one of the two events is observable, namely the event of sending or receiving a message by the service itself. For example, service S sends a message that is later received by service S0, then for S the sending event is observable and from the viewpoint of S0 only the receiving event occurs. Furthermore we assume that a service only communicates unidirectional over a message channel: Either messages are sent or received via this channel.
We use the classical syntax and semantics of Petri nets as in [
Figure 1 shows three open nets with the same interface, graphically emphasized by the dashed line. E, TB and CB are input places, C and T are output places. N1, N2 and N3 are models of simple coee/tea machines that have one button for coee ( CB), one for tea (TB), an input for money (E) and two output slots, one for coee ( C) and one for tea (T). Although the three models have the same interface, they dier obviously in the internal structure.
The modeling of interface places is only the prerequisite for message exchange, message exchange can only occur between a number of open nets that are composed. Two two open nets N and N 0 can be composed if they are syntactically compatible, meaning that they do not share internal places or transitions and have compatible interfaces. Two interfaces A and B are compatible if the output (input) channels of A are not used as output (input) channels in B and vice versa. Composition is done by union of the net elements, composing initial and nal marking and merging identically named interface places that become internal places. 3
In this paper, we approach a specic class of constraints: Lower and upper bounds for event occurrence. Intuitively a constraint of that class species the bounds for legal interaction: An event or a linear combination of several events is only allowed to occur in those bounds. An example for a constraint is 2 a 7, meaning that the event a occurs at least two and at most seven times. A constraint however need not give an integer value for one or both bounds, it can also specify one of the bounds as unbounded, meaning that interaction is not constrained in that direction. For example 2 a _ demands that event a occurs at least two times but might occur innitely often. Dependencies between messages can be expressed easily as well: 1 a + b 1 states that always exactly one of the two events occur. 0 a b 0 demands that a and b occur equally often, since the inequality can easily be transformed to a = b. We can not specify temporal orders between messages, causalities or more complex dependencies. The open nets N1; N2; N3 in Fig. 1 all three comply to the constraints E = 1, 0 C 1, CB + T B = 1. Only N1 and N2 comply with the constraints CB C = 0, T B T = 0, CB + T = 1 and T B + C = 1 that demand that T B (CB) only occurs with T (C). We can not express order restrictions with such constraints, so we can not forbid a behavior as in N2.
Formally, a constraint c is a quadruple hA; ; l; ui, where A is a nite set of events, : A ! ZZ is a linear combination of events and l; u 2 ZZ [ f_g. The semantics of such a constraint is as follows: ; l; u form an inequality of the form l u, with the elements of A as variables. Let N and N 0 be open nets. A run r in N N 0 satises c from the viewpoint of N , written c `N r if and only if the occurrence rate of events in the projection of r to transitions of N is a satisfying assignment for the variables in c. A sequential run is terminating if and only if it starts at the initial marking and ends at the nal marking. N complies with a constraint c if, for an arbitrary N 0 and every terminating sequential run r in N N 0, c `N r holds.
A prole of N species a set of constraints that N complies with. These constraints need not be the strictest ones that apply but might be quite liberal. Computation of a prole for an open net can be done by static analysis, avoiding state space construction. Thus, a prole is an abstraction of the behavior of N with any arbitrary service N 0.
Knowledge of N 0 can not be assumed, therein we nd the rst challenge for computing a prole. We approach the problem by overapproximating every possible N 0 by a canonical open net that has the most liberal interaction behavior, called the unrestricted environment of N , denoted as Nb : An open net, only consisting of exactly one transition for each interface place of N and no internal places. One would not encounter Nb in the practical eld, but it proves to be very helpful in analyzing the service in interaction with Nb and deducing its behavior in an arbitrary environment from the results. The connection between the behavior of N Nb and N N 0 is the following: Fixing any run in N N 0, we can nd a run N Nb , such that the two are equivalent if we just concentrate on N ’s part. We demonstrate this on the example of the open net N1 in Fig. 2(a): Figure 2(b) shows the unrestricted environment for N1 and their composition is depicted in Fig. 2(c).
CB
C pf
However, for computing a prole we do not construct and explore the state space, but use a classical static Petri net method, namely the state equation, a canonical system of linear equations, taking into account two markings ; 0. For every run from to 0, there exists a solution m, such that transitions occur as often in the run as given by m. We construct the state equation of N Nb , setting = and 0 = !. We add an equation for each possible event in N , specifying the transitions of N that let an event occur. The set of all solutions is thus both an overapproximation of all terminating sequential runs r in N Nb and gives the occurrence rates for events in r from the viewpoint of N .
Given a set of linear combinations of events, we can now apply linear programming to nd lower and upper bounds for these combinations. Solutions of these linear programs are constraints that N complies with. Thus we directly construct a prole. The set of linear combinations is the only parameter, the rest is canonical on the net structure. We can distinguish between two general starting points for proles: (1) there exists a specication, given as constraints before computing the prole, (2) we compute the prole in advance. In the rst case, the input for the prole computation can be taken directly from the specication. In the second case, the selection of useful linear combinations has to be done manually, although we can imagine taking into account structural properties like invariants, conict situations and the like.
The computation of proles for a given open net has been implemented in the tool Linda2. It takes a set of constraints as input and computes an according prole, using the lp_solve-library 3 to solve linear problems. Interoperability with other tools is enforced by usage of the same open net format as the other tools in the above mentioned tool chain. 4
Given an open net N and a set of constraints C, we can create a prole to determine compliance of N to the constraints in C. In some cases, however, we are neither able to prove compliance nor non-compliance with this method. We demonstrate the compliance checking process with an example. Let N be cp cy cn cu an arbitrary open net and cy; cn; cu be constraints that restrict the same linear combination. Creating a prole for any of the singleton sets fcyg, fcng and fcug leads to the same result, we denote it as fcpg. Let the bounds given by the constraints cp; cy; cn; cu be as depicted in Fig. 3. We rst check compliance with 2 Available at http://www.service-technology.org/tools/linda 3 Available at http://lpsolve.sourceforge.net cy: N complies with cy since the bounds given by the prole imply those of cy. In contrast to that, N does not comply with cn: The lower bound of cn is greater than the upper bound of cp. In the case of cu however, we can not decide compliance or non-compliance of N with cu by the method of proling.
Given a prole of N , we can also check compliance of N with a constraint c, although the linear combination of c is not directly restricted by any constraint in : We determine a constraint restricting the same linear combination as c that is implied by the constraints in and then do compliance checking as explained above. Finding such an implied constraint can be done by linear programming. 5
We have described a class of constraints for the interaction behavior of a service. Our approach to the solution is the computation of a prole , a set of constraints that a service complies with, using static Petri net analysis methods. We have demonstrated how proling can be used to check compliance, answering with yes, no or unknown.
It is part of further work to determine the inputs of prole computation if they can not be derived from a specication, such that a prole can be stored as an abstraction of an open net. Since a prole is an abstraction, we can think of making use of renement techniques to further explore questions answered with unknown. We will embed proles in dierent tools to analyze services and their composition, so that they benet from preprocessed information or on-the-y checking of constraints.