=Paper=
{{Paper
|id=Vol-501/paper-7
|storemode=property
|title=Profiling Services with Static Analysis
|pdfUrl=https://ceur-ws.org/Vol-501/Paper5.pdf
|volume=Vol-501
}}
==Profiling Services with Static Analysis==
Proling Services with Static Analysis
Jan Sürmeli
Humboldt-Universität zu Berlin, Institut für Informatik
Unter den Linden 6, 10099 Berlin, Germany
suermeli@informatik.hu-berlin.de
Abstract. 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 sys-
tems. Asynchronous interaction and stateful behavior complicate predict-
ing 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 ex-
plain the computation of proles by static Petri net analysis.
1 Introduction
In a service-oriented architecture (SOA) [1], services interact with each other
by exchanging messages over predened channels. Typically, services are under-
stood as software artifacts that oer a functionality over a well-dened interface,
dening those channels a service uses. Control and data ow of services heavily
depend on the interaction with other services. We aim at analyzing the behavior
of a service S and thus model S with open nets (or service nets, open workow
nets) [2]. We will describe this extension to classical Petri nets in Sec. 2.
Well-developed methods to analyze the behavior of a service S with open
nets, already exist alongside dierent behavioral correctness criteria such as con-
trollability [3] and exchangeability [4]. Those criteria can be veried by dynamic
techniques and were implemented in a tool chain1 . Another subject is to check
behavioral constraints on services and their compositions. We can demand orders
on messages, causalities, limits et cetera. Work in this area has been done in [5].
We can think of dierent levels of abstraction as well as extensions of the classical
evaluation of a constraint to true or false, e.g. three valued logics, probabilities
or costs. On top of that, services behave dependent on their environment, so
we are interested in overapproximating the behavior for all or a subclass of all
possible environments. Work on structural analysis on open nets has been done
in [6].
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 re-
ceived. 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 lin-
ear 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 spec-
ication. 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 Modeling with Open Nets
E E CB TB
CB TB C T E
C T CB TB C T
pf pf pf
(a) N1 (b) N2 (c) N3
Fig. 1. Three open nets with the nal marking [pf ]
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 S 0 , then for S the sending
event is observable and from the viewpoint of S 0 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 [7]. We dene
the behavior of a Petri net N as the set of all sequential runs in N . Open nets are
Petri nets that are augmented by a nal marking and an interface for message
exchange, the latter is realized by designating some places as input and some
as output places. These so called interface places are used as connectors for the
composition. Other places are called internal places and the net structure is that
of a classical Petri net.
Figure 1 shows three open nets with the same interface, graphically empha-
sized 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 ex-
change, 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 syntac-
tically 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 Proles for Open Nets
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 ∈ ZZ ∪ {_}. 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 be-
havior, 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).
E
E
CB
CB TB TB
C
C T
pf T pf
(a) N1 (b) N
c1 (c) N1 ⊕ N
c1
Fig. 2. N1 (repeated from Fig. 1), its unrestricted environment N
c1 and N1 ⊕ N
c1 .
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 pro-
gramming 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 start-
ing 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-library3 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 Application of Proles
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
Fig. 3. The bounds given by four constraints cp , cy , cn , cm .
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 {cy }, {cn } and {cu }
leads to the same result, we denote it as {cp }. 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 Conclusion and Further Work
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.
References
1. Gottschalk, K.: Web services architecture overview.
http://www.ibm.com/developerworks/web/library/w-ovr/ (2000)
2. Massuthe, P., Reisig, W., Schmidt, K.: An Operating Guideline Approach to the
SOA. Annals of Mathematics, Computing & Teleinformatics 1(3) (2005) 3543
3. Wolf, K.: Does my service have partners? T. Petri Nets and Other Models of
Concurrency 2 (2009) 152171
4. Stahl, C., Massuthe, P., Bretschneider, J.: Deciding Substitutability of Services with
Operating Guidelines. Transactions on Petri Nets and Other Models of Concurrency
II, Special Issue on Concurrency in Process-Aware Information Systems 2(5460)
(March 2009) 172191
5. Lohmann, N., Massuthe, P., Wolf, K.: Behavioral constraints for services. In
Alonso, G., Dadam, P., Rosemann, M., eds.: Business Process Management, 5th
International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007,
Proceedings. Volume 4714 of Lecture Notes in Computer Science., Springer-Verlag
(September 2007) 271287
6. Oanea, O., Wolf, K.: An ecient necessary condition for compatibility. In Kopp, O.,
Lohmann, N., eds.: ZEUS. Volume 438 of CEUR Workshop Proceedings., CEUR-
WS.org (2009) 8187
7. Reisig, W.: Petri nets: an introduction. Springer-Verlag New York, Inc., New York,
NY, USA (1985)