BPEL (Business Process Execution Language)
- Specification, Modelling and Analysis
 

Masters Thesis
Fall 2004- Summer 2006
Department of Computer Science
Univeristy of Illinois at Chicago

Introduction

I am Ramya Chitrakar and I graduated with a Masters degree in Computer Science from the University of Illinois at Chicago (UIC) in the summer of 2006. As part of my thesis, I performed the modeling and analysis of BPEL (Business Process Execution Language) specifications using Petri nets. The purpose of this webpage is to publish the research work of my thesis for the interest of those who wish to learn more about BPEL and its analysis.This webpage will be hosted in future by my advisor Prof. Ugo Buy of the Computer Science department at UIC. I am currently working as a Software Developer in Test with Microsoft Corporation.

I have organized the contents of this site to include a brief description of BPEL, its components and my implementations of BPEL. These are followed by the descriptions of the translation tools from BPEL to Petri nets, description of the analysis tools I used and the results I obtained using the generated Petri nets. I have also documented my experience working with BPEL and these various tools.

Overview

Web-based applications are gaining popularity within the Internet and corporate intranets. Web services are independently developed, modular business process applications. The Web service interaction model, also known as service-oriented architecture paradigm, is a model for communication among these services. The Business Process Execution Language For Web Services (BPEL4WS/ BPEL) is a language for describing business processes and interactions among these services. It extends the Web services interaction model and enables it to support business transactions. Thereby, it is widely used among business process managers.

Though BPEL is an expressive language, it lacks mathematically sound semantics, which hinders the formal verification of business process applications. In my thesis, BPEL specifications for business processes involving concurrency and synchronization were studied and analyzed, by converting them to Petri nets, as Petri nets are mathematical models for distributed and concurrent systems. Tools for translating BPEL specifications into Petri nets and several analysis tools for the Petri nets obtained from the translators were explored. The use, features and limitations of the tools used for BPEL and Petri nets were examined and reported. Finally, several kinds of analysis were performed on the Petri nets corresponding to the synchronization problems written in BPEL and tested for correctness.