Publications in Bussiness Process Modeling

Articles in Refereed Journals:

1. Chun Ouyanga, Eric Verbeekb, Wil M.P. van der Aalst, Stephan Breutel, Marlon Dumas, Arthur H.M. ter Hofstede. Formal semantics and analysis of control flow in WS-BPEL. Science of Computer Programming, Vol. 67, Num. 2-3, pages 162-198, April 2007.
   Abstract: Web service composition refers to the creation of new (Web) services by combining functionalities provided by existing ones. A number of domain-specific languages for service composition have been proposed, with consensus being formed around a process-oriented language known as WS-BPEL (or BPEL). The kernel of BPEL consists of simple communication primitives that may be combined using control-flow constructs expressing sequence, branching, parallelism, synchronization, etc. We present a comprehensive and rigorously defined mapping of BPEL constructs onto Petri net structures, and use this for the analysis of various dynamic properties related to unreachable activities, conflicting messages, garbage collection, conformance checking, and deadlocks and lifelocks in interaction processes. We use a mapping onto Petri nets because this allows us to use existing theoretical results and analysis tools. Unlike approaches based on finite state machines, we do not need to construct the state space, and can use structural analysis (e.g., transition invariants) instead. We have implemented a tool that translates BPEL processes into Petri nets and then applies Petri-net-based analysis techniques. This tool has been tested on different examples, and has been used to answer a variety of questions.

2. Roberto Lucchi, Manuel Mazzara. A pi-calculus based semantics for WS-BPEL . Journal of Logic and Algebraic Programming, Vol. 70, Num. 1, pages 96-118, January 2007.
   Abstract: Recently, the term Web services orchestration has been introduced to address some issues related to Web services composition, that is the way of defining a complex service out of simpler ones. Several proposals for describing orchestration for business processes have been presented in the last years and many of these languages make use of concepts as long-running transactions and compensations for coping with error handling. WS-BPEL 2.0, the most credited candidate for becoming a standard, provides three different mechanisms allowing to cope with abnormal situations: exception, event and compensation handling. This complexity makes it difficult to formally define the framework, thus limiting the formal reasoning about the designed applications. In this paper we advocate that three different mechanisms for error handling are not necessary and we formalize a novel orchestration language based on the idea of event notification as the unique error handling mechanism. To this end, we formally define the three BPEL mechanisms in terms of our calculus. It is possible to take advantages of this formal description in two ways. Firstly, this language represents by itself a proposal of simplification for WS-BPEL 2.0 including an unambiguous specification. Secondly, an implementor of an actual WS-BPEL 2.0 orchestration engine could implement simply this single mechanism providing all the remaining ones by compilation. With this attempt we intend to give a concrete contribute towards the improvement of the quality of the BPEL specification, the applicability of BPEL itself and the implementation of real orchestration engines. Finally, as a case study we consider some of the hundreds of open issues met by the WS-BPEL designers and we propose a solution making use of the experience gained developing our algebra.

3. George A. Papadopoulos, Farhad Arbab. Coordination Models and Languages. Advances in Computers, Vol. 46, pages 330-401, 1998.
   Abstract: A new class of models, formalisms and mechanisms has recently evolved for describing concurrent and distributed computations based on the concept of "coordination". The purpose of a coordination model and associated language is to provide a means of integrating a number of possibly heterogeneous components together, by interfacing with each component in such a way that the collective set forms a single application that can execute on and take advantage of parallel and distributed systems. In this chapter we initially define and present in sufficient detail the fundamental concepts of what constitutes a coordination model or language. We then go on to classify these models and languages as either "data-driven" or "control-driven" (also called "process-" or "task-oriented"). Next, the main existing coordination models and languages are described in sufficient detail to let the reader appreciate their features and put them into perspective with respect to each other. The chapter ends with a discussion comparing the various models and some conclusions.

Articles in Refereed Conferences:

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

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

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

4. Florian Rosenberg, Schahram Dustdar. Business Rules Integration in BPEL - A Service-Oriented Approach. CEC, pages 476-479, 2005.
   Abstract: Business rules change quite often. These changes cannot be handled efficiently by representing business rules embedded in the source code of the business logic. Efficient handling of rules that govern ones business is one factor for success. That is where business rules engines play an important role. The service-oriented computing paradigm is becoming more and more popular. Services offered by different providers, are composed to new services by using Web service composition languages such as BPEL. Such process-based composition languages lack the ability to use business rules managed by different business rules engines in the composition process. In this paper, we propose an approach on how to use and integrate business rules in a service-oriented way into BPEL.

5. Wil M. P. van der Aalst, Arthur H. M. ter Hofstede, Mathias Weske. Business Process Management: A Survey . International Conference on Business Process Management (BPM), Lecture Notes in Computer Science, Vol. 2678, Springer Verlag, 2003.
   Abstract: Business Process Management (BPM) includes methods, techniques, and tools to support the design, enactment, management, and analysis of operational business processes. It can be considered as an extension of classical Workflow Management (WFM) systems and approaches. Although the practical relevance of BPM is undisputed, a clear definition of BPM and related acronyms such as BAM, BPA, and STP are missing. Moreover, a clear scientific foundation is missing. In this paper, we try to demystify the acronyms in this domain, describe the state-of-the-art technology, and argue that BPM could benefit from formal methods/languages (cf. Petri nets, process algebras, etc.).