Publications in Program Analysis

Articles in Refereed Journals:

1. J. Cardoso. Complexity analysis of BPEL Web processes. Software Process: Improvement and Practice, Vol. 12, Num. 1, pages 35-49, Whiley-Interscience, 2007.
   Abstract: Several organizations have already realized the potential of using WS-BEPL, the Process Execution Language for Web Services, to model the behavior of Web services in business processes. WS-BPEL provides a model for describing simple or complex interactions between business partners. In some cases, WS-BPEL process designs can be highly complex, due, for example, to the vast number of Web services carried out in global markets. High complexity in a process has several undesirable drawbacks; it may result in poor understandability, more errors, defects, and exceptions, leading to processes requiring more time to be developed, tested, and maintained. Therefore, excessive complexity should be avoided. Processes that are highly complex tend be less flexible, since it is more complicated to make changes to the process. The major goal of this article is to present two metrics to analyze the control-flow complexity (CFC) of WS-BPEL Web processes. The metrics are to be used at design-time to evaluate the complexity of a process design before implementation actually takes place.

Articles in Refereed Conferences:

1. Moreno Marzolla, Raffaela Mirandola. Performance Prediction of Web Service Workflows. Software Architectures, Components, and Applications, Lecture Notes in Computer Science, Vol. 4880, pages 127-144, January 2008.
   Abstract: Web Services play an important role in the SOA paradigm, as they allow services to be selected on-the-fly to build applications out of existing components. In this scenario, the BPEL notation can be used as an orchestration language which allows the user to describe interactions with Web Services in a standard way. The performance of a BPEL workflow is a very important factor for deciding which components must be selected, or to choose whether a given sequence of interactions can provide the requested quality of service. Due to its very dynamic nature, workflow performance evaluation can not be accomplished using traditional, heavy-weight techniques. In this paper we present a multi-view approach for the performance prediction of service-based applications encompassing both users and service provider(s) perspectives. As a first step towards the realization of this integrated framework we present an efficient approach for performance assessment of Web Service workflows described using the BPEL notation. Starting from annotated BPEL and WSDL specifications, we derive performance bounds on response time and throughput. In such a way users are able to assess the efficiency of a BPEL workflow, while service provider(s) can perform sizing studies or estimate performance gains of alternative upgrades to existing systems. To bring this approach to fruition we developed a prototype tool called bpel2qnbound, using which we analyze a simple case study.

2. 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

3. Jorge Cardoso. About the Data-Flow Complexity of Web Processes. 6th International Workshop on Business Process Modeling, Development, and Support: Business Processes and Support Systems: Design for Flexibility, pages 67-74, 2005.
   Abstract: Abstract. Organizations are increasingly faced with the challenge of managing e-commerce and e-business applications involving Web services and Web processes. In some cases, Web processes’ design can be highly complex, due, for example, to the vast number of services carried out in global markets. High complexity in a process has several undesirable drawbacks, it may result in bad understandability, more errors, defects, and exceptions leading processes to need more time to develop, test, and maintain. Therefore, excessive complexity should be avoided. Flexibility and complexity are guiding principles in the design of business processes. In most business processes, flexibility and complexity are related inversely. Processes with a high complexity tend be less flexible, since it is more complicated to make changes to the process. In our previous work we have defined a metric to measure the control-flow complexity of Web processes. The major goal of this paper is to study the issues and establish the requirements for the development of a metric to analyze the data-flow complexity of Web processes.

4. 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.

Technical Reports and Manuals:

1. Oliver Kopp, Rania Khalaf, Frank Leymann. Reaching Definitions Analysis Respecting Dead Path Elimination Semantics in BPEL Processes. Num. 2007/04, Institut für Architektur von Anwendungssystemen, November 2007.
   Abstract: The Business Process Execution Language for Web Services (BPEL) is a workflow language geared towards Service Oriented Computing. BPEL provides basic workflow capabilities, such as the ability to impose control on a set of activities via explicit links, as well as advanced features such as recovery and event handling. The area of workflow often requires understanding the data dependencies as well as the control dependencies between activities. This aids in business process design as well as in analysis and rengineering. BPEL, however, uses shared variables to model data. Activities read and write data to these variables, i.e. there is no explicit data link construct. In order to draw out the flow of data between the activities of a BPEL process, one must therefore perform data-flow analysis on that process. To address this problem, we present an algorithm that statically determines such data dependencies. "Statically" means, that we do not determine the dependencies per process instance at runtime, but on the process model without creating any instances. Mainstream data-flow analysis techniques are presented in [ALSU06, Muc97, NNH04]. However, these techniques cannot be directly applied to a BPEL process, since BPEL supports both parallelism and dead path elimination (DPE, [CDG+ 03, OAS07, CKLW03, BK05, LR00]). DPE is a technique used in BPEL to propagate activity disablement down paths that can no longer be executed. The algorithm in this paper consists of reaching definitions analysis dealing with DPE, enabling it to reduce the number of data dependencies when compared to approaches not dealing with DPE.