Publications in 2006

Articles in Refereed Journals:

1. Wenhui Sun, Jinyu Zhang, Feng Liu. WS-SLA: A Framework for Web Services Oriented Service Level Agreements. Computer Supported Cooperative Work in Design, 2006. CSCWD '06. 10th International Conference on, To Appear, May 2006.
   Abstract: Service level agreements (SLA) becomes the prevailing business model for delivery of a large number of products and services in telecommunication and IT arenas. We presents an integrated service level agreement model applied to operating supporting system (OSS), on the basis of WfMC workflow reference model and service oriented architecture (SOA). And an application scenario instance of SLA system architecture is described by a set of operations models by Business Process Execution Language (BPEL)

2. Christel Baier, Marjan Sirjani, Farhad Arbab, Jan J. M. M. Rutten. Modeling component connectors in Reo by constraint automata. Sci. Comput. Program., Vol. 61, Num. 2, pages 75-113, 2006.
   Abstract: In this paper we introduce constraint automata and propose them as an operational model for Reo, an exogenous coordination language for compositional construction of component connectors based on a calculus of channels. By providing composition operators for constraint automata and defining notions of equivalence and refinement relations for them, this paper covers the foundations for building tools to address concerns such as the automated construction of the automaton for a given component connector, equivalence checking or containment checking of the behavior of two given connectors, and verification of coordination mechanisms.

3. Mike P. Papazoglou, Willem-Jan van den Heuvel. Service-oriented design and development methodology. Int. J. Web Eng. Technol., Vol. 2, Num. 4, pages 412-442, 2006.
   Abstract: Service Oriented Architectures (SOA) are rapidly emerging as the premier integration and architectural approach in contemporary, complex, heterogeneous computing environments. SOA is not simply about deploying software: it also requires that organisations evaluate their business models, come up with service-oriented analysis and design techniques, deployment and support plans, and carefully evaluate partner/customer/supplier relationships. Since SOA is based on open standards and is frequently realised using Web Services (WS), developing meaningful WS and business process specifications is an important requirement for SOA applications that leverage WS. Designers and developers cannot be expected to oversee a complex service-oriented development project without relying on a sound design and development methodology. This paper provides an overview of the methods and techniques used in service-oriented design and development. The aim of this paper is to examine a service development methodology from the point of view of both service producers and requesters and review the range of elements in this methodology that are available to them.

Articles in Refereed Conferences:

1. Dmytro Rud, Andreas Schmietendorf, Reiner Dumke. Performance Modeling of WS-BPEL-Based Web Service Compositions. Services Computing Workshops, pages 140-147, September 2006.
   Abstract: This paper addresses quality of service aspects of Web service orchestrations created using WS-BPEL from the standpoint of a Web service integrator. A mathematical model based on operations research techniques and formal semantics of WS-BPEL is proposed to estimate and forecast the influence of the execution of orchestrated processes on utilization and throughput of individual involved nodes and of the whole system. This model is applied to the optimization of service levels agreement process between the involved parties

2. A. Rozinat, W.M.P. van der Aalst. Conformance Testing: Measuring the Fit and Appropriateness of Event Logs and Process Models. Business Process Management Workshops, Lecture Notes in Computer Science, Vol. 3812, pages 163-176, February 2006.
   Abstract: Most information systems log events (e.g., transaction logs, audit trails) to audit and monitor the processes they support. At the same time, many of these processes have been explicitly modeled. For example, SAP R/3 logs events in transaction logs and there are EPCs (Event-driven Process Chains) describing the so-called reference models. These reference models describe how the system should be used. The coexistence of event logs and process models raises an interesting question: "Does the event log conform to the process model and vice versa?". This paper demonstrates that there is not a simple answer to this question. To tackle the problem, we distinguish two dimensions of conformance: fitness (the event log may be the result of the process modeled) and appropriateness (the model is a likely candidate from a structural and behavioral point of view). Different metrics have been defined and a Conformance Checker has been implemented within the ProM Framework.

3. Wil M. P. van der Aalst, Marlon Dumas, Chun Ouyang, Anne Rozinat, H. M. W. Verbeek. Choreography Conformance Checking: An Approach based on BPEL and Petri Nets. The Role of Business Processes in Service Oriented Architectures, 2006.
   Abstract: Recently, languages such as BPEL and CDL have been proposed to describe the way services can interact from a behavioral perspective. The emergence of these languages heralds an era where richer service descriptions, going beyond WSDL-like interfaces, will be available. However, what can these richer service descriptions serve for? This paper investigates a possible usage of behavioral service descriptions, namely as input for conformance checking. Conformance checking is the act of verifying whether one or more parties stick to the agreed-upon behavior by observing the actual behavior, e.g., the exchange of messages between all parties. This paper shows that it is possible to translate BPEL business protocols to Petri nets and to relate SOAP messages to transitions in the Petri net. As a result, Petri net-based conformance checking techniques can be used to quantify fitness (whether the observed behavior is possible in the business protocol) and appropriateness (whether the observed behavior "overfits" or "underfits" the business protocol). Moreover, non-conformance can be visualized to pinpoint deviations. The approach has been implemented in the context of the ProM n framework.

4. Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, Sergio Storari, Paolo Torroni. Computational Logic for Run-Time Verification of Web Services Choreographies: Exploiting the OCS-SI Tool. WS-FM, pages 58-72, 2006.
   Abstract: In this work, we investigate the feasibility of using a framework based on computational logic, and mainly defined in the context of Multi-Agent Systems for Global Computing (SOCS UE Project), for modeling choreographies of Web Services with respect to the conversational aspect. One of the fundamental motivations of using computational logic, beside its declarative and highly expressive nature, is given by its operational counterpart, that can provide a proof-theoretic framework able to verify the consistency of services designed in a cooperative and incremental manner. In particular, in this paper we show that suitable "Social Integrity Constraints", introduced in the SOCS social model, can be used for specifying global protocols at the choreography level. In this way, we can use a suitable tool, derived from the proof-procedure defined in the context of the SOCS project, to check at run-time whether a set of existing services behave in a conformant manner w.r.t. the defined choreography.

5. Fabio Barbon, Paolo Traverso, Marco Pistore, Michele Trainotti. Run-Time Monitoring of Instances and Classes of Web Service Compositions. ICWS, pages 63-71, 2006.
   Abstract: The run-time monitoring of web service compositions has been widely acknowledged as a significant and challenging problem. In this paper, we propose a novel solution to the problem of monitoring web services implemented in BPEL. We devise an architecture that clearly separates the business logic of a web service from its monitoring functionality. The architecture supports both "instance monitors" that deal with the execution of a single instance of BPEL process, as well as "class monitors" that report aggregated information about all the instances of a BPEL process. We also define a language for the specification of instance and class monitors. The language allows for specifying boolean, statistic, and time-related properties. Finally, we devise a technique for the automatic translation of all these kinds of monitors to Java programs.

6. Patricia Bouyer, Pierre-Alain Reynier, Serge Haddad. Extended Timed Automata and Time Petri Nets. ACSD, pages 91-100, 2006.
   Abstract: Timed Automata (TA) and Time Petri Nets (TPN) are two well-established formal models for real-time systems. Recently, a linear transformation of TA to TPNs preserving reachability properties and timed languages has been proposed, which does however not extend to larger classes of TA which would allow diagonal constraints or more general resets of clocks. Though these features do not add expressiveness, they yield exponentially more concise models. In this work, we propose two translations: one from extended TA to TPNs whose size is either linear or quadratic in the size of the original TA, depending on the features which are allowed; another one from a parallel composition of TA to TPNs, which is also linear. As a consequence, we get that TPNs are exponentially more concise than TA.

7. Yan-ping Chen, Zeng-zhi Li, Qin-xue Jin, Chuang Wang. Study on QoS Driven Web Services Composition. Frontiers of WWW Research and Development - APWeb 2006, Lecture Notes on Computer Science, Vol. 3841, pages 702-707, Springer Verlag, 2006.
   Abstract: Providing composed Web Services based on the QoS requirements of clients is still an urgent problem to be solved. In this paper, we try to solve this problem. Firstly, we enhanced the current WSDL to describe the QoS of services, and then gave a way to choose the proper pre-exist services based on their QoS.

8. Mohan Baruwal Chhetri, Jian Lin, SukKeong Goh, Jian Ying Zhang, Ryszard Kowalczyk, Jun Yan. A Coordinated Architecture for the Agent-based Service Level Agreement Negotiation ofWeb Service Composition. ASWEC, pages 90-99, 2006.
   Abstract: Recent progress in the field of Web services has made it possible to integrate inter-organizational and heterogeneous services on the Web at runtime. If a user request cannot be satisfied by a single Web service, it is (or should be) possible to combine existing services in order to fulfill the request. However, there are several challenging issues that need to be addressed before this can be realized in the true sense. One of them is the ability to ensure end-to-end QoS of a Web service composition. There is a need for a SLA negotiation system which can ensure the autonomous QoS negotiation of Web service compositions irrespective of the application domain. In this paper we propose agent-based coordinated-negotiation architecture to ensure collective functionality, end-to-end QoS and the stateful coordination of complex services. We describe a prototype implementation to demonstrate how this architecture can be used in different application domains. We have also demonstrated how the negotiation system on the service provider's side can be implemented both as an agent based negotiation system and as a Web service based negotiation system.

9. Gero Decker, Johannes Maria Zaha, Marlon Dumas. Execution Semantics for Service Choreographies. WS-FM, pages 163-177, 2006.
   Abstract: A service choreography is a model of interactions in which a set of services engage to achieve a goal, seen from the perspective of an ideal observer that records all messages exchanged between these services. Choreographies have been put forward as a starting point for building service-oriented systems since they provide a global picture of the system's behavior. In previous work we presented a language for service choreography modeling targeting the early phases of the development lifecycle. This paper provides an execution semantics for this language in terms of a mapping to PI-calculus. This formal semantics provides a basis for analyzing choreographies. The paper reports on experiences using the semantics to detect unreachable interactions.

10. Howard Foster, Sebastian Uchitel, Jeff Magee, Jeff Kramer. LTSA-WS: a tool for model-based verification of web service compositions and choreography. ICSE '06: Proceedings of the 28th international conference on Software engineering, pages 771-774, ACM, 2006.
    Abstract: In this paper we describe a tool for a model-based approach to verifying compositions of web service implementations. The tool supports verification of properties created from design specifications and implementation models to confirm expected results from the viewpoints of both the designer and implementer. Scenarios are modeled in UML, in the form of Message Sequence Charts (MSCs), and then compiled into the Finite State Process (FSP) process algebra to concisely model the required behavior. BPEL4WS implementations are mechanically translated to FSP to allow an equivalence trace verification process to be performed. By providing early design verification and validation, the implementation, testing and deployment of web service compositions can be eased through the understanding of the behavior exhibited by the composition. The approach is implemented as a plug-in for the Eclipse development environment providing cooperating tools for specification, formal modeling, verification and validation of the composition process.

11. Raman Kazhamiakin, Paritosh K. Pandya, Marco Pistore. Representation, Verification, and Computation of Timed Properties in Web Service Compositions. ICWS, pages 497-504, 2006.
    Abstract: In this paper we address the problem of qualitative and quantitative analysis of timing aspects of Web service compositions defined as a set of BPEL4WS processes. We introduce a formalism, called Web Service Timed State Transition Systems (WSTTS), to capture the timed behavior of the composite web services. We also exploit an interval temporal logic to express complex timed assumptions and requirements on the system's behavior. Building on top of this formalization, we provide techniques and tools for modelchecking BPEL4WS compositions against time-related requirements. We also present a symbolic algorithm that can be used to compute duration bounds of behavioral intervals that satisfy such requirements. We perform a preliminary experimental evaluation of our approach and tools with the help of an e-Government case study.

12. Kyriakos Kritikos, Dimitris Plexousakis. Semantic QoS Metric Matching. ECOWS, pages 265-274, 2006.
    Abstract: As the Web Service paradigm gains popularity for its promise to transform the way business is conducted, the number of deployed Web Services grows with a fast rate. While sophisticated semantic discovery mechanisms have been invented to overcome the UDDI's syntactic discovery solution in order to provide more recallable and precise results, the amount of functionally equivalent Web Services returned is still large. The solution to this problem is the description of the QoS non-functional aspect of Web Services. QoS encompasses the performance of Web Services and can be used as a discriminator factor for refining Web Service advertisement result lists. However, most scientific efforts presented so far are purely syntactic and are not capturing all aspects of QoS-based Web Service description leading to imprecise syntactic discovery mechanisms. This paper presents a novel, rich and extensible ontology-based approach for describing QoS of Web Services that complements OWL-S. It is shown that, by using this approach and by introducing the concept of semantic QoS metric matching, QoS-based syntactic matchmaking and selection algorithms are transformed to semantic ones leading to better results.

13. Marina Mongiello, Daniela Castelluccia. Modelling and verification of BPEL business processes. Fourth Workshop on Model-Based Development of Computer-Based Systems, 2006.
    Abstract: A business process is a complex Web service with functions provided by different Web services, which are already existing in Web and are dynamically integrated for granting a more complex business task. For this reason, business processes have become more and more diffuse in B2B and B2C domains, so that the importance of their activities asks for a high-level of reliability. Methods and tools for supporting automatic system verification and validation could be useful. Among the techniques of automatic verification, we choose model checking method, because we applied it efficiently for verification of a single Web service and in this paper we extend the area of application also in business processes. Descriptions of the behavior of a business process are coded using a standard language, BPEL4WS, that has broadly spread because it is able to describe a business process as both an executable process and an abstract process. Therefore, we model a BPEL description of a generic business process with a formal model and we formalize correctness properties about the reliability of the business process design. Also, we build a framework that performs automatic verification of formal models of business processes through NuSMV model checker. If there is a violation of correctness specifications, NuSMV provides counter-examples, so we can locate errors and effect right changes for correcting business process design.

14. Nicole Oldham, Kunal Verma, Amit Sheth, Farshad Hakimpour. Semantic WS-agreement partner selection. WWW '06: Proceedings of the 15th international conference on World Wide Web, pages 697-706, ACM, 2006.
    Abstract: In a dynamic service oriented environment it is desirable for service consumers and providers to offer and obtain guarantees regarding their capabilities and requirements. WS-Agreement defines a language and protocol for establishing agreements between two parties. The agreements are complex and expressive to the extent that the manual matching of these agreements would be expensive both in time and resources. It is essential to develop a method for matching agreements automatically. This work presents the framework and implementation of an innovative tool for the matching providers and consumers based on WS-Agreements. The approach utilizes Semantic Web technologies to achieve rich and accurate matches. A key feature is the novel and flexible approach for achieving user personalized matches.

15. Mohsen Rouached, Olivier Perrin, Claude Godart. Towards Formal Verification of Web Service Composition. Business Process Management, pages 257-273, 2006.
    Abstract: Web services composition is an emerging paradigm for enabling application integration within and across organizational boundaries. Current Web services composition proposals, such as BPML, WSBPEL, WSCI, and OWL-S, provide solutions for describing the control and data flows in Web service composition. However, such proposals remain at the descriptive level, without providing any kind of mechanisms or tool support for analysis and verification. Therefore, there is a growing interest for the verification techniques which enable designers to test and repair design errors even before actual running of the service, or allow designers to detect erroneous properties and formally verify whether the service process design does have certain desired properties. In this paper, we propose to verify Web services composition using an event driven approach. We assume Web services that are coordinated by a composition process expressed in WSBPEL and we use Event Calculus to specify the properties and requirements to be monitored.

16. Yuan Yuan, Zhongjie Li, Wei Sun. A Graph-Search Based Approach to BPEL4WS Test Generation. ICSEA, 14 pages, 2006.
    Abstract: Business Process Execution Language for Web Services (BPEL4WS) is a kind of concurrent programming languages with several special features that raise special challenges for verification and testing. This paper proposes a graph-search based approach to BPEL test case generation, which effectively deals with BPEL concurrency semantics. This approach defines an extension of CFG (Control Flow Graph) - BPEL Flow Graph (BFG) - to represent a BPEL program in a graphical model. Then concurrent test paths can be generated by traversing the BFG model, and test data for each path can be generated using a constraint solving method. Finally test paths and data are combined into complete test cases.

17. Johannes Maria Zaha, Alistair P. Barros, Marlon Dumas, Arthur H. M. ter Hofstede. Let's Dance: A Language for Service Behavior Modeling. OTM Conferences (1), pages 145-162, 2006.
    Abstract: In Service-Oriented Architectures (SOAs), software systems are decomposed into independent units, namely services, that interact with one another through message exchanges. To promote reuse and evolvability, these interactions are explicitly described right from the early phases of the development lifecycle. Up to now, emphasis has been placed on capturing structural aspects of service interactions. Gradually though, the description of behavioral dependencies between service interactions is gaining increasing attention as a means to push forward the SOA vision. This paper deals with the description of these behavioral dependencies during the analysis and design phases. The paper outlines a set of requirements that a language for modeling service interactions at this level should fulfill, and proposes a language whose design is driven by these requirements.

Technical Reports and Manuals:

1. Siddharth Bajaj, Don Box, Dave Chappell, Francisco Curbera, Glen Daniels, Phillip Hallam-Baker, Maryann Hondo, Chris Kaler, Dave Langworthy, Anthony Nadalin, Nataraj Nagaratnam, Hemma Prafullchandra, Claus von Riegen, Daniel Roth, Jeffrey Schlimmer, Chris Sharp, John Shewchuk, Asir Vedamuthu, Ümit Yalcinalp, David Orchard . Web Services Policy Framework (WS- Policy). IBM, March 2006.
   Abstract: The Web Services Policy Framework (WS-Policy) provides a general purpose model and corresponding syntax to describe the policies of a Web Service. WS-Policy defines a base set of constructs that can be used and extended by other Web services specifications to describe a broad range of service requirements and capabilities.