The field of Semantic Web services marries the technology of delivering services over the Web with the Semantic Web. This brings up a variety of issues, which range from service-specific and domain ontologies to service discovery, service choreography (i.e., specification of how autonomous client agents interact with services), automated contracting for services, service enactment, execution monitoring, and others. A number of past and ongoing projects proposed solutions to some of these problems. These include OWL-S,SWSL,WSMO,and WSCDL.WSMO is one of the more comprehensive approaches to Semantic Web Services, as it covers virtually all of the aforementioned areas. In this paper, we focus on one particular aspect of WSMO—its support for service choreography,which is based on the formalism of Abstract State Machines (ASMs) [3].
Although ASMs have been used to design and verify software in the past, this
formalism is too general and leaves Web service designers to their own sevices.To the best of our knowledge, there has been little work to help guide Web service designers through the process of actual building of ASM-based choreographies. Our first contribution is to show that control flow graphs, which are commonly used to design workflows (and thus can be used as visual design tools for choreographies), have a modular translation into ASMs and can be used to specify WSMO choreography interfaces.
Next, we discuss some of the drawbacks of using ASMs in WSMO. We argue that the problem of choreography is inextricably related to the problem of contracting for Web services. We define one very useful instance of the problem of contracting and show that ASMs are inadequate to deal with this problem. We then propose a solution grounded in Concurrent Transaction Logic (CTR) [2]. Based on our previous results [15], we show that both service choreography and service contracts have natural representation in CTR: the former as deductive rules and the latter as constraints. In addition, CTR enables us to reason about consistency of the contracts with the choreographies, about service enactment,and other issues. In this way, CTR-based WSMO choreography can be seen as a natural extension of the ASM-based WSMO choreography.
An introduction to WSMO choreography is given in Section 2. Section 3 pro poses a more intuitive, visual language for specifying service interactions, and develops a methodology for automatic generation of WSMO choreography transition rules. Section 4 defines the problem of service contracting as choreography under the constraints specified as service policies and customers requirements and highlights the limitations of the current WSMO choreography in this area. It then proposes CTR as a formalism that overcomes those problems. Section 5 presents related work, and Section 6 concludes this paper.
Download
PDF Ebook WSMO Choreography: From Abstract State Machines to Concurrent Transaction Logic
