Article Preview
TopIntroduction
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.