Analyzing Web Service Based Business Processes
Axel Martens
Humboldt-Universita¨t zu Berlin,
Department of Computer Sciece, Berlin (Adlershof), Germany
IBM T. J. Watson Research Center,
Component Systems Group, Hawthorne (NY), USA
martens@informatik.hu-berlin.de amarten@us.ibm.com
Abstract. This paper is concerned with the application of Web services
to distributed, cross-organizational business processes. In this scenario,
it is crucial to answer the following questions: Do two Web services fit
together in a way such that the composed system is deadlock-free? –
the question of compatibility. Can one Web service be replaced by an-
other while the remaining components stay untouched? – the question of
equivalence. Can we reason about the soundness of one given Web service
without considering the actual environment it will by used in?
This paper defines the notion of usability – an intuitive and locally prov-
able soundness criterion for a given Web services. Based on this notion,
this paper demonstrates how the other questions could be answered.
The presented method is based on Petri nets, because this formalism is
widely used for modeling and analyzing business processes. Due to the
existing Petri net semantics for BPEL4WS – a language that is in the
very act of becoming the industrial standard for Web service based busi-
ness processes – the results are directly applicable to real world examples.
Keywords: Business Process Modeling, Web Service, BPEL4WS, Tool
based Verification, Petri nets.
1 Introduction
Over the past years, the Internet has evolved from just a communication media
into a platform for B2B integration. Emerging technologies and industrial stan-
dards in the field of Web services enable a much faster and easier cooperation
of distributed partners. This paper is concerned with the application of Web
services to distributed, cross-organizational business processes.
The Scenario. A Web service [1] is a self-describing, self-contained modular
application that can be published, located, and invoked over a network, e. g. the
Internet. A Web service performs an encapsulated function and can be accessed
via a standardized interface. In this paper, each local sub-process of each par-
ticipating company is realized through one Web service. The composition of all
Web services of all participating companies realizes the global business process.
M. Cerioli (Ed.): FASE 2005, LNCS 3442, pp. 19–33, 2005.
c
© Springer-Verlag Berlin Heidelberg 2005

20 A. Martens
Instead of one new specific technology, the Web service approach provides a
stack of closely related technologies [4] to cover heterogeneity and distribution
underneath a homogenous concept of components and composition. Among other
things, the language BPEL4WS [2] belongs to this stack. Due to this layered
architecture, the presented analysis method can be focussed on the Web service’s
BPEL process model without losing generality or practical relevance.
The Goal. The Web service technologies define a technical framework to im-
plement distributed business processes while a minimum of syntactic consistency
is guaranteed. But as this paper will show, there is a need for more advanced
analysis, and there exist effective methods that are able to support the develop-
ment of Web services and Web service based business processes according to the
Service oriented architecture (SOA [9]).
The service oriented architecture describes three roles: The service provider
implements the Web service and publishes its description (the Web service
model) to one or more repositories for potential users to locate. For him, it
is crucial to determine errors and weaknesses of his service prior to publication.
Hence, this paper presents the notion usability – a locally provable soundness
criterion for a given Web service – that prevents publication of erroneous services.
The service requestor is searching for a Web service that he could bind to his
own components. For him, it is crucial to determine whether or not a given Web
service does interact properly with his components. Hence, this paper defines
the criterion of semantic compatibility and provides its verification.
Finally, the service broker manages a repository and allows the service re-
questor to find an adequate service. According to the query-by-example approach,
he compares the actual Web service model (published by provider) with an ab-
stract Web service model submitted by the requestor. Beside other use cases, the
presented equivalence criterion provides a basis for the necessary matchmaking.
The Method. Many of the Web services technologies are still in the standard-
ization process, and therefore some specifications will likely be changed several
times until a consistent status is reached. Hence, the presented method refrains
from the actual syntax of any proposed Web service modeling languages. Instead,
it applies a generic formalism of Petri nets [16] to addresses the core problems
of distributed business processes. This formal method is widely used for mod-
eling and analyzing business processes and Web services [21, 5, 6]. Applying the
rich theory of distributed systems, the presented method is able to define and
verify usability, compatibility and equivalence of Web services. Moreover, the pre-
sented results can easily be adopted to almost any concrete modeling language
(e. g. WS-CDL [7], OWL-S [25] or YAWL [23]). In particular, there exists already
a Petri net semantics for BPEL4WS [18] – a language that is in the very act
of becoming the industrial standard for modeling Web service based business
processes. Hence, the method is directly applicable to real world examples.
The remaining paper is structured as follows: Section 2 gives a short intro-
duction to Petri nets and describes the structure and composition of workflow
modules – the formal model of a Web Sevice. Section 3, discusses and defines the