Publications in 2004

Articles in Refereed Journals:

1. Neal Leavitt. Are Web Services Finally Ready to Deliver?. IEEE Computer, Vol. 37, Num. 11, pages 14-18, November 2004.
   Abstract: Web services, in brief, are a framework of software technologies designed to support interoperable machine-to-machine interaction over a network. Companies on different systems can use Web services to exchange information online with business partners, customers, and suppliers. Various standards organizations and industry consortia are developing Web services specifications without a unifying authority. Organizations such as the World Wide Web Consortium (W3C), the Organization for the Advancement of Structured Information Standards (OASIS), the Liberty Alliance Project, and the Web Services Interoperability Organization (WS-I) have developed or reviewed numerous standards. A primary goal of Web services is to unlock a new generation of e-commerce applications.

2. Xiulan Yu, Long Zhang, Ying Li, Ying Chen. WSCE: a flexible Web Service Composition Environment. Web Services, 2004. Proceedings. IEEE International Conference on, To Appear, July 2004.
   Abstract: In this paper, we propose the concepts of virtual partner and inspector into the Web services composition. Virtual partner, as an IT level concept, is a Web service (pseudo Web service) using the same interface with the actual partner but different binding message. A virtual partner can be invoked directly by a business process described by BPEL, so that the BPEL programmer can test both application's functionality and non functionality performance early in the development cycle to avoid any problems in the final runtime, or test the selection of their partners in business level design. The IT virtual partners provide developers with a range of the techniques which let them explore every aspect of their program. Inspector is proposed when using the third-party process engine. An inspector itself is also a Web service. The programmer can register any required output information in it. The IT virtual partner and the inspector concepts have been integrated in our WSCE, a flexible Web Services Composition Environment for a business process. WSCE is a prototype of autonomic modeling and simulation environment. With the help of a third-party BPEL engine, it provides programmer with concepts and tools to facilitate business process programming.

3. Liangzhao Zeng, Benatallah, B., Ngu, A.H.H., Dumas, M., Kalagnanam, J., Chang, H.. QoS-aware middleware for Web services composition. Software Engineering, IEEE Transactions on, Vol. 30, Num. 5, pages 311-327, May 2004.
   Abstract: The paradigmatic shift from a Web of manual interactions to a Web of programmatic interactions driven by Web services is creating unprecedented opportunities for the formation of online business-to-business (B2B) collaborations. In particular, the creation of value-added services by composition of existing ones is gaining a significant momentum. Since many available Web services provide overlapping or identical functionality, albeit with different quality of service (QoS), a choice needs to be made to determine which services are to participate in a given composite service. This paper presents a middleware platform which addresses the issue of selecting Web services for the purpose of their composition in a way that maximizes user satisfaction expressed as utility functions over QoS attributes, while satisfying the constraints set by the user and by the structure of the composite service. Two selection approaches are described and compared: one based on local (task-level) selection of services and the other based on global allocation of tasks to services using integer programming.

4. Andrew W. Cooke, Alasdair J. G. Gray, Werner Nutt, James Magowan, Manfred Oevers, Paul Taylor, Roney Cordenonsi, Rob Byrom, Linda Cornwall, Abdeslem Djaoui, Laurence Field, Steve Fisher, Steve Hicks, Jason Leake, Robin Middleton, Antony J. Wilson, Xiaomei Zhu, Norbert Podhorszki, Brian A. Coghlan, Stuart Kenny, David O'Callaghan, John Ryan. The Relational Grid Monitoring Architecture: Mediating Information about the Grid. J. Grid Comput., Vol. 2, Num. 4, pages 323-339, 2004.
   Abstract: We have developed and implemented the Relational Grid Monitoring Architecture (R-GMA) as part of the DataGrid project, to provide a flexible information and monitoring service for use by other middleware components and applications. R-GMA presents users with a virtual database and mediates queries posed at this database: users pose queries against a global schema and R-GMA takes responsibility for locating relevant sources and returning an answer. R-GMAs architecture and mechanisms are general and can be used wherever there is a need for publishing and querying information in a distributed environment. We discuss the requirements, design and implementation of R-GMA as deployed on the DataGrid testbed. We also describe some of the ways in which R-GMA is being used.

5. Mariya Koshkina, Franck van Breugel. Modelling and verifying web service orchestration by means of the concurrency workbench. SIGSOFT Softw. Eng. Notes, Vol. 29, Num. 5, pages 1-10, ACM, 2004.
   Abstract: Verification techniques like model checking, preorder checking and equivalence checking are shown to be relevant to web service orchestration. The Concurrency Workbench of the New Century (CWB) is a verification tool that supports these verification techniques. By means of the Process Algebra Compiler (PAC), the CWB is modified to support the BPE-calculus. The BPE-calculus is a small language, based on BPEL4WS, to express web service orchestration. Both the syntax and the semantics of the BPE-calculus are formally defined. These are subsequently used as input for the PAC. As output, the PAC produces modules that are incorporated into the CWB so that it supports the BPE-calculus and, hence, provides a verification tool for web service orchestration.

6. Milanovic, N., Malek, M.. Current solutions for Web service composition. Internet Computing, IEEE, Vol. 8, Num. 6, pages 51-59, November/December 2004.
   Abstract: Web service composition lets developers create applications on top of service-oriented computing's native description, discovery, and communication capabilities. Such applications are rapidly deployable and offer developers reuse possibilities and users seamless access to a variety of complex services. There are many existing approaches to service composition, ranging from abstract methods to those aiming to be industry standards. The authors describe four key issues for Web service composition.

7. Marco Pistore, Marco Roveri, Paolo Busetta. Requirements-Driven Verification of Web Services. Electr. Notes Theor. Comput. Sci., Vol. 105, pages 95-108, 2004.
   Abstract: We propose a requirements-driven approach to the design and verification of Web services. The proposed methodology starts from a requirements model, which defines a business domain at a "strategic" level, describing the participating actors, their mutual dependencies, goals, requirements, and expectations. This business requirements model is then refined into a business process model. In this refinement, definitions of the processes carried out by the actors of the domain are added to the model in the form of BPEL4WS code. We show how to exploit model checking techniques for the verification of the specification, both at the requirements and at the process level. At the requirements level, model checking is used to validate the specification against a set of queries specified by the designer; at the process level, it is used to verify if the BPEL4WS processes satisfy the constraints described in the requirements model.

Articles in Refereed Conferences:

1. Foster, H., Uchitel, S., Magee, J., Kramer, J.. Compatibility verification for Web service choreography. pages 738-741, July 2004.
   Abstract: In this paper we discuss a model-based approach to verifying process interactions for coordinated Web service compositions. The approach uses finite state machine representations of Web service orchestrations and assigns semantics to the distributed process interactions. The move towards implementing Web service compositions by multiple interested parties as a form of distributed system architecture motivates the need for supporting compatibility verification of activities and transactions in all the processes. The described approach is supported by a suite of cooperating tools for specification, formal modeling and providing verification results from orchestrated Web service interactions.

2. Rohit Aggarwal, Kunal Verma, John A. Miller, William Milnor. Constraint Driven Web Service Composition in METEOR-S. IEEE SCC, pages 23-30, 2004.
   Abstract: Creating Web processes using Web service technology gives us the opportunity for selecting new services which best suit our need at the moment. Doing this automatically would require us to quantify our criteria for selection. In addition, there are challenging issues of correctness and optimality. We present a Constraint Driven Web Service Composition tool in METEOR-S, which allows the process designers to bind Web Services to an abstract process, based on business and process constraints and generate an executable process. Our approach is to reduce much of the service composition problem to a constraint satisfaction problem. It uses a multi-phase approach for constraint analysis. This work was done as part of the METEOR-S framework, which aims to support the complete lifecycle of semantic Web processes.

3. Jesus Arias-Fisteus, Luis Sanchez Fernandez, Carlos Delgado Kloos. Formal Verification of BPEL4WS Business Collaborations. E-Commerce and Web Technologies, 5th International Conference, EC-Web 2004, Proceedings, Lecture Notes in Computer Science, Vol. 3182, pages 76-85, Springer Verlag, 2004.
   Abstract: Web services are a very appropriate communication mechanism to perform distributed business processes among several organisations. These processes should be reliable, because a failure in them can cause high economic losses. To increase their reliability at design time, we have developed VERBUS, a framework for the formal verification of business processes. VERBUS can automatically translate business process definitions to specifications verifiable in several available tools. It is based on a modular and extensible architecture: new process definition languages and verification tools can be added easily to the framework. The prototype of VERBUS presented in this work can verify BPEL4WS process specifications, by translating them to Promela. The Promela specifications are verified with the well known model checker Spin. In this paper we describe the general architecture of VERBUS and how BPEL4WS specifications are translated and verified. The explanation is completed by describing what types of properties can be verified and providing an overview of the implementation.

4. Tevfik Bultan, Xiang Fu, Jianwen Su. Tools for Automated Verification of Web Services. ATVA, pages 8-10, 2004.

5. Vikas Deora, Jianhua Shao, Gareth Shercliff, Patrick J. Stockreisser, W. A. Gray, N. J. Fiddian. Incorporating QoS Specifications in Service Discovery. WISE Workshops, pages 252-263, 2004.
   Abstract: In this paper, we extend the current approaches to service discovery in a service oriented computing environment, such as Web Services and Grid, by allowing service providers and consumers to express their promises and requirements for quality of service (QoS). More specifically, we allow service providers to advertise their services in an extended DAML-S that supports quality specifications, and we allow service consumers to request services by stating required quality levels. We propose a model here for incorporating QoS specifications and requirements in service discovery, and describe how matchmaking between advertised and requested services based on functional as well as quality requirements is supported in our model.

6. Roozbeh Farahbod, Uwe Glässer, Mona Vajihollahi. Specification and Validation of the Business Process Execution Language for Web Services. Abstract State Machines, pages 78-94, 2004.
   Abstract: We formally define an abstract executable semantics for the Business Process Execution Language for Web Services in terms of a distributed ASM. The goal of this work is to support the design and standardization of the language. There is a need for formalism. It will allow us to not only reason about the current specification and related issues, but also uncover issues that would otherwise go unnoticed. Empirical deduction is not sufficient. - Issue 42, OASIS WSBPEL TC. The language definition assumes an infrastructure for running Web services on some asynchronous communication architecture. A business process is built on top of a collection of Web services performing continuous interactions with the outside world by sending and receiving messages over a communication network. The underlying execution model is characterized by its concurrent and reactive behavior making it particularly difficult to predict dynamic system properties with a sufficient degree of detail and precision under all circumstances.

7. Xiang Fu, Tevfik Bultan, Jianwen Su. Analysis of Interacting BPEL Web Services. WWW'04: Proceedings of the 13th International Conference on World Wide Web, pages 621-630, ACM Press, 2004.
   Abstract: This paper presents a set of tools and techniques for analyzing interactions of composite web services which are specified in BPEL and communicate through asynchronous XML messages. We model the interactions of composite web services as conversations, the global sequence of messages ex- changed by the web services. As opposed to earlier work, our tool-set handles rich data manipulation via XPath expressions. This allows us to verify designs at a more detailed level and check properties about message content. We present a framework where BPEL specifications of web ser- vices are translated to an intermediate representation, followed by the translation of the intermediate representation to a verification language. As an intermediate representation we use guarded automata augmented with unbounded queues for incoming messages, where the guards are expressed as XPath expressions. As the target verification language we use Promela, input language of the model checker SPIN. Since SPIN model checker is a finite-state verification tool we can only achieve partial verification by fixing the sizes of the input queues in the translation. We propose the concept of synchronizability to address this problem. We show that if a composite web service is synchronizable, then its conversation set remains same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite web services with unbounded input queues can be completely verified using a finite state model checker such as SPIN.

8. Xiang Fu, Tevfik Bultan, Jianwen Su. Realizability of Conversation Protocols With Message Contents. ICWS, 2004.
   Abstract: A conversation protocol is a top-down specification framework which specifies desired global behaviors of a web service composition. In our earlier work [A formalism for specification and verification of reactive electronic services] we studied the problem of realizability, i.e., given a conversation protocol, can a web service composition be synthesized to generate behaviors as specified by the protocol. Several sufficient realizability conditions were proposed in [A formalism for specification and verification of reactive electronic services] to ensure realizability. Conversation protocols studied in [A formalism for specification and verification of reactive electronic services], however, are essentially abstract control flows without data semantics. This paper extends the work in [A formalism for specification and verification of reactive electronic services] and achieves more accurate analysis by considering data semantics. To overcome the state-space explosion caused by the data content, we propose a symbolic analysis technique for each realizability condition. In addition, we show that the analysis of the autonomy condition can be done using an iterative refinement approach.

9. Xiang Fu, Tevfik Bultan, Jianwen Su. Model checking XML manipulating software. ISSTA, pages 252-262, 2004.
   Abstract: The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, and the expressive XML query languages (such as XPath) make formal specification and verification of software systems that manipulate XML data a challenge. In this paper, we present our initial efforts in automated verification of XML data manipulation operations using the SPIN model checker. We present algorithms for translating (bounded) XML data and XPath expressions to Promela, the input language of SPIN. The techniques presented in this paper constitute the basis of our Web Service Analysis Tool (WSAT) which verifies LTL properties of composite web services.

10. Gang Huang, Meng Wang, Liya Ma, Ling Lan, Tiancheng Liu, Hong Mei. Towards Architecture Model based Deployment for Dynamic Grid Services. IEEE International Conference on E-Commerce Technology for Dynamic E-Business (CEC-East'04), 2004.
    Abstract: The deployment of grid services should make the services, including those to be deployed and those already deployed, operate with desired functionalities and qualities. The critical challenge in the deployment is that many technical and nontechnical factors have to be taken into account, such as performance, reliability, utilization, operating cost, incomes, and so on. Since the factors change continuously, some deployed services may have to be redeployed for guaranteeing their functionalities and qualities. This position paper presents an approach to the deployment and redeployment of grid services based on software architecture models. In this approach, all services in a grid consist in a software architecture, which represents the services, their relationships and other factors in a global, understandable and easy-to-use way. To demonstrate the approach, a visual tool for deploying services onto a set of popular grid infrastructures, including J2EE application servers and BPEL engines, with the help of software architectures is developed.

11. Michael C. Jaeger, Gregor Rojec-Goldmann, Gero Mühl. QoS Aggregation for Web Service Composition using Workflow Patterns. EDOC, pages 149-159, 2004.
    Abstract: Contributions in the field of Web services have identified that (a) finding matches between semantic descriptions of advertised and requested services and (b) nonfunctional characteristics - the quality of service (QoS) - are the most crucial criteria for composition of Web services. A mechanism is introduced that determines the QoS of a Web service composition by aggregating the QoS dimensions of the individual services. This allows to verify whether a set of services selected for composition satisfies the QoS requirements for the whole composition. The aggregation performed builds upon abstract composition patterns, which represent basic structural elements of a composition, like sequence, loop, or parallel execution. This work focusses on workflow management environments. We define composition patterns that are derived from Van der Aalst's et al. comprehensive collection of workflow patterns. The resulting aggregation schema supports the same structural elements as found in workflows. Furthermore, the aggregation of several QoS dimensions is discussed.

12. Jinghai Rao, Xiaomeng Su. A Survey of Automated Web Service Composition Methods. SWSWPC, pages 43-54, 2004.
    Abstract: In todays Web, Web services are created and updated on the fly. Its already beyond the human ability to analysis them and generate the composition plan manually. A number of approaches have been proposed to tackle that problem. Most of them are inspired by the researches in cross-enterprise workflow and AI planning. This paper gives an overview of recent research efforts of automatic Web service composition both from the workflow and AI planning research community.

13. Gwen Salaün, Lucas Bordeaux, Marco Schaerf. Describing and Reasoning on Web Services using Process Algebra. ICWS, 2004.
    Abstract: We argue that essential facets of web services, and especially those useful to understand their interaction, can be described using process-algebraic notations. Web service description and execution languages such as BPEL are essentially process description languages; they are based on primitives for behaviour description and message exchange which can also be found in more abstract process algebras. One legitimate question is therefore whether the formal approach and the sophisticated tools introduced for process algebra can be used to improve the effectiveness and the reliability of web service development. Our investigations suggest a positive answer, and we claim that process algebras provide a very complete and satisfactory assistance to the whole process of web service development. We show on a case study that readily available tools based on process algebra are effective at verifying that web services conform their requirements and respect properties. We advocate their use both at the design stage and for reverse engineering issues. More prospectively, we discuss how they can be helpful to tackle choreography issues.

14. James Skene, D. Davide Lamanna, Wolfgang Emmerich. Precise Service Level Agreements. ICSE, pages 179-188, 2004.
    Abstract: SLAng is an XML language for defining service level agreements, the part of a contract between the client and provider of an Internet service that describes the quality attributes that the service is required to possess. We define the semantics of SLAng precisely by modelling the syntax of the language in UML, then relating the language model to a model that describes the structure and behaviour of services. The presence of SLAng elements imposes behavioural constraints on service elements, and the precise definition of these constraints using OCL constitutes the semantic description of the language. We use the semantics to define a notion of SLA compatibility, and an extension to UML that enables the modelling of service situations as a precursor to analysis, implementation and provisioning activities.

15. Andreas Wombacher, Peter Fankhauser, Erich J. Neuhold. Transforming BPEL into Annotated Deterministic Finite State Automata for Service Discovery. ICWS, pages 316-323, 2004.
    Abstract: Web services advocate loosely coupled systems, although current loosely coupled applications are limited to stateless services. The reason for this limitation is the lack of a method supporting matchmaking of state dependent services exemplarily specified in BPEL. In particular, the sender's requirement that the receiver must support all possible messages sent at a certain state are not captured by models currently used for service discovery. Annotated deterministic finite state automata provide this expressiveness. In this paper the transformation of a local process specification given in BPEL to annotated deterministic finite state automata is presented.

16. Tao Yu, Kwei-Jay Lin. Service Selection Algorithms for Web Services with End-to-End QoS Constraints. CEC, pages 129-136, 2004.
    Abstract: Web services are new forms of Internet software that can be universally deployed and invoked using standard protocol. Services from different providers can be integrated to provide composite services. In this paper, we study the end-to-end QoS issues of composite service by utilizing a QoS broker that is responsible for coordinating the individual service component to meet the quality constraint. We design the service selection algorithms used by QoS brokers to meet end-to-end QoS constraints. The objective of the algorithms is to maximize the user-defined utility while meeting the end-to-end delay constraint. We model the problem as the Multiple Choice Knapsack Problem (MCKP) and provide efficient solutions. The algorithms are tested for their performance.