An Approach Based on Hierarchical Petri Nets for the Verification of Interconnected BPEL Processes

An Approach Based on Hierarchical Petri Nets for the Verification of Interconnected BPEL Processes

Boukhedouma Saida, Alimazighi Zaia
Copyright: © 2018 |Pages: 35
DOI: 10.4018/IJISMD.2018040103
(Individual Articles)
No Current Special Offers


This article describes an MDE approach for transformation from BPEL specifications to WF-nets models for verifying behavioral properties on IOWF (Inter-Organizational Workflow) processes. The authors consider WF processes specified with BPEL and interconnected together according to specific cooperation patterns. They define a specific class of Petri nets called Hierarchical WF-nets (HWN) in order to formally check the “soundness” property on IOWF process models. For that, their verification approach is defined around three main phases: (i) recovery of the BPEL file(s) and generation of process tree(s), (ii) transformation from BPEL to WF-nets (resp. HWN) models using mapping and transformation rules and (iii) verification of the “soundness” property on the models obtained. They particularly define and implement a set of specific transformation rules which are closely linked to the interconnection rules attached to each cooperation pattern. Also, to show the feasibility of their verification method, the authors developed a “WF-Checking” tool which allows the implementation and testing of the proposed approach.
Article Preview


The Workflow technology is widely used to implement and manage both intra and inter-organizational business processes. Specifically, the concept of inter-organizational WF (IOWF) introduced in (Van der Aalst, 99, 2000) was initially used to support the B2B cooperation, particularly suitable to e-commerce applications. An IOWF can be defined as a manager of activities involving two or more workflows autonomous, possibly heterogeneous and interoperable in order to achieve a common business goal. Cooperation between business partners is based on an IOWF process which is obtained by interconnection of two or more WF processes (called WF fragments) provided by different partners. In addition, interconnection of WF processes can be done in different ways. This gives rise to different cooperation patterns (called IOWF-architectures) characterized by different partitioning modes, different modes of execution control and different modes of interaction between WF fragments. In our research, we consider common cooperation patterns fairly widespread in the B2B area, which are the “Capacity sharing”, the “Chained execution”, the “Subcontracting”, the “Case-transfer” and the “Loosely coupled” patterns (Van der Aalst, 2000).

Furthermore, with the advent of the SOA paradigm and Web services standards, the B2B cooperation made considerable progress by taking advantage of the main characteristics of services (loose coupling, interoperability, reuse, adaptation and evolution) (Pessoa et al., 2008). Thus, in order to deal with IOWF process models flexible enough, we proposed in our pervious works (Boukhedouma et al., 2014, 2015), new cooperation patterns based on the SOA paradigm. For that, we introduced a new concept called Service-Based Cooperation Pattern (SBCP) to support the definition of IOWF process models based on services, while meeting the initial IOWF-architectures (Van der Aalst, 2000). Globally, our aim was to redefine and implement a set of structurally well-defined and fairly widespread models for WF interconnection and to provide mechanisms for change support at different levels of the process. In our approach, a WF fragment is defined as an orchestration of elementary and/or composite services; an elementary service encapsulates a single business activity while a composite service encapsulates a set of activities interconnected together.

For implementation aspects, we have considered WF processes specified with the BPEL language. In our cooperation framework, the interconnection of WF fragments is done with respect of a set of interconnection rules and constraints that we have stated for each cooperation pattern (Boukhedouma et al., 2014, 2015). Furthermore, in order to manage changes that can affect the IOWF process models, we defined and implemented a set of adaptation and evolution patterns (Boukhedouma et al., 2017), applied on process models specified with the BPEL language, and interconnected together.

Notice that behavioral properties such as reachability and deadlock-free can be verified on WF fragments but are not necessarily preserved in the IOWF process after interconnection of the fragments. Moreover, such properties are not necessarily preserved in the IOWF process after changes. From there, we have found it necessary to formally check behavioral properties on process models after their interconnection or adaptation/evolution.

In this paper, we focus on the question of checking formally the correctness of interconnected process models specified with BPEL. For that, we particularly focus on the verification of the soundness property defined in (Van der Aalst, 97). This property guarantees minimal behavioral properties to be verified on each process model, mainly the reachability of each activity of the process, proper termination of process instances and deadlock-free.

Complete Article List

Search this Journal:
Volume 14: 1 Issue (2023)
Volume 13: 8 Issues (2022): 7 Released, 1 Forthcoming
Volume 12: 4 Issues (2021)
Volume 11: 4 Issues (2020)
Volume 10: 4 Issues (2019)
Volume 9: 4 Issues (2018)
Volume 8: 4 Issues (2017)
Volume 7: 4 Issues (2016)
Volume 6: 4 Issues (2015)
Volume 5: 4 Issues (2014)
Volume 4: 4 Issues (2013)
Volume 3: 4 Issues (2012)
Volume 2: 4 Issues (2011)
Volume 1: 4 Issues (2010)
View Complete Journal Contents Listing