Generic and Specific Compatibility Criteria for Web Service Composition: Formal Abstraction and Modular Verification Approach1

Generic and Specific Compatibility Criteria for Web Service Composition: Formal Abstraction and Modular Verification Approach1

Kais Klai (CNRS UMR 5157 SAMOVAR, Sorbonne Paris Cité, University Paris 13, Villetaneuse, France), Samir Tata (CNRS UMR 5157 SAMOVAR, Institute Mines-Telecom, Telecom SudParis, Evry, France) and Hanen Ochi (CNRS UMR 7030 LIPN, Sorbonne Paris Cité, University Paris 13, Villetaneuse, France)
Copyright: © 2012 |Pages: 24
DOI: 10.4018/jwsr.2012100103
OnDemand PDF Download:
No Current Special Offers


For automatically composing Web services in a correct manner, information about their behaviors (an abstract model) has to be published in a repository. This abstract model must be sufficient to decide whether two, or more, services are compatible (the composition is possible) is possible without including any additional information that can be used to disclose the privacy of these services. The compatibility between two Web services can be based either on some generic properties (e.g. deadlock freeness of the composite Web service) or on a specific property expressed with a formal logic. In this paper, the authors address this problem by considering these two kinds of compatibility criteria. The first criterion is defined by different variants of the well-known soundness property on open workflow nets. These properties guarantee the absence of livelocks, deadlocks and other anomalies that can be formulated without domain knowledge. The second criterion is defined by the designer formally by using the Linear Temporal Logic. The proposed approach addresses the automatic abstraction of Web services and the checking of their compatibility using their abstract models only. To abstract Web services, the authors use the symbolic observation graph (SOG) approach that preserves necessary information for service composition and hides private information. The authors show how the SOG can be adapted and used so that the verification of generic and specific compatibility criteria can be performed on the composition of the abstract models of Web services instead of the original composite service.
Article Preview


Service oriented architecture (SOA) has evolved to become a promising technology for the integration of disparate software components using Internet protocols. These components, called Web Services (WS), are available in the distributed environment of the Internet. Organizations attempt to provide their own services through complex tasks, which can be resolved using a combination of several web services. For automatically selecting and composing services in a well-behaved manner, information about the services has to be exposed. Usually, web services are published by giving their public description behavior in a repository, such as Universal Description, Discovery and Integration (UDDI), in order to make possible the collaboration with potential requesters. In particular, this information must be sufficient to decide whether the composition of two services is possible. However, organizations usually want to hide the trade secrets of their services. Thus, for a given service, they need to find a proper abstraction of the process of the service (a.k.a. abstract process) or of its behavior, which should be published instead of the service itself. Therefore, an abstraction should satisfy trade-off between two opposite requirements. On the one hand, it should respect the privacy of the underlying organization. On the other hand, it should enclose enough information to allow the collaboration and the communication with potential partners in a correct way. To compose Web services, in this paper, we address the checking of their compatibility using their abstractions. This mainly raises the following research questions:

  • How to abstract the internal behavior of Web services while preserving necessary information for service composition and hiding private information?

  • How to use abstractions for service composition such that correctness, regarding a given good property, of the composition of Web services (involving internal behavior) is detected from the analysis of the composition of their corresponding abstractions?

  • What are the good properties preserved by abstraction we consider in this paper?

The compatibility of two or more Web services may consider compatibility of parameter (inputs/outputs) at the syntactical level as well as the semantic level. It may also consider the behavioral aspects with several possible behavioral properties. While we believe that the compatibility of parameters is an important issue, the behavioral compatibility discussed here is complex enough in itself to deserve separate treatment.

Different approaches have been proposed to describe the web services’ behavior by proposing an abstraction technique. Among other abstraction approaches, the Symbolic Observation Graph (SOG) approach, initially introduced for model checking of concurrent systems (Haddad, Ilié, & Klai 2004) and then applied to the verification of inter enterprise business (Klai & Ochi, 2012; Klai, Tata et al., 2009), is promising. A SOG is a graph whose construction is guided by a subset of observed actions. The nodes of a SOG are aggregates hiding a set of local states which are connected with non observed actions. The arcs of a SOG are exclusively labeled with observed actions. Thus, we propose to use SOGs as abstraction of web services. By observing the collaborative activities (or actions) of a web service, publishing a SOG as an abstraction allows to hide its internal behavior inside the aggregates. The strength of such an approach is that a SOG associated with a web service represents a reduced abstraction of its reachable state space while preserving its behavioral properties.

To check the compatibility of two web services, which is necessary for their composition, we propose to check the compatibility on the composition of their SOGs instead of the whole composite service (which is unavailable anyway). We formally represent a web services by an oWF-net (Massuthe, Reisig et al., 2005). We define two kinds of compatibility properties between Web services: generic and specific properties. Generic properties are dependent on neither the model of Web service nor the considered business domain. While specific properties are described in terms of precise elements (states, actions, events, etc.) of the Web service.

Complete Article List

Search this Journal:
Volume 19: 4 Issues (2022): 1 Released, 3 Forthcoming
Volume 18: 4 Issues (2021)
Volume 17: 4 Issues (2020)
Volume 16: 4 Issues (2019)
Volume 15: 4 Issues (2018)
Volume 14: 4 Issues (2017)
Volume 13: 4 Issues (2016)
Volume 12: 4 Issues (2015)
Volume 11: 4 Issues (2014)
Volume 10: 4 Issues (2013)
Volume 9: 4 Issues (2012)
Volume 8: 4 Issues (2011)
Volume 7: 4 Issues (2010)
Volume 6: 4 Issues (2009)
Volume 5: 4 Issues (2008)
Volume 4: 4 Issues (2007)
Volume 3: 4 Issues (2006)
Volume 2: 4 Issues (2005)
Volume 1: 4 Issues (2004)
View Complete Journal Contents Listing