Formal Abstraction and Compatibility Checking of Web Services

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 property 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. In this paper we address the automatic abstraction of Web services and the checking of their compatibility using their abstract models only. To abstract Web services, we use the symbolic observation graph (SOG) approach that preserves necessary information for service composition and hides private information. We show how the SOG can be adapted and used so that the verification of different variants of compatibility can be performed on the composition of the abstract models (SOGs) of Web services instead of the original composite service.