Ajay Krishna

Pascal Poizat
email: pascal.poizat@lip6.fr

Gwen Salaün
email: gwen.salaun@inria.fr

Checking Business Process Evolution

Keywords: Business processes, evolution, model transformation, automated verification, tool, BPMN, LNT, LTS

Business processes support the design and implementation of software as workflows of local and inter-organization activities. Tools provide the business process designer with modelling and execution facilities, but they barely provide formal analysis techniques. When one makes a process evolve, for example by refactoring it or by adding new features in it, it is important to be able to check whether, and how, this process has changed, and possibly correct evolution flaws. To reach this objective, we first present a model transformation from the BPMN standard notation to the LNT process algebra and LTS formal models. We then propose a set of relations for comparing business processes at the formal model level. With reference to related work, we propose a richer set of comparison primitives supporting renaming, refinement, property and context-awareness. We also support BPMN processes containing unbalanced structures among gateways. In order to make the checking of evolution convenient for business process designers, we have implemented tool support for our approach as a web application.

Introduction

Business processes describe the production of goods or services as a set of local tasks and inter-organization exchanges. The main business process modelling notations, BPMN 2.0, UML Activity Diagrams, and Eventdriven Process Chains, have a workflow perspective of business processes. BPMN 2.0 (BPMN for short in the sequel) is an ISO standardized notation for modelling business processes. Numerous tools support the design or execution of BPMN models, e.g., Activity, Bonita BPMN, or the Eclipse BPMN Designer. They can be used to set up the first version of a process model, and then to make it evolve by refactoring parts of it (to optimize it or better suit partner organizations) or by adding new features in it.

Motivations. The BPMN modelling tools support basic activities on the models but performing formal analyses on them is barely found in these. Further, evolution needs a special treatment. It can be supported by a form of non-regression verification where the whole set of formal verifications (e.g. relative to the descriptions of expected behaviours) that has been checked on a version of a process is checked again on its evolution. It would also be interesting to have a more global vision of the process behaviour by being able to specify what evolution should / should not be in terms of observable behaviours. Our objectives are to propose to process designers a variety of formally grounded (behavioural) evolution relations between process models, and, given two process models, to support this designer with automated techniques for checking these evolution relations and more generally behavioural properties. These automated techniques should enable the designer to understand the impact of evolution and, if necessary, support the refinement of an incorrect evolution into a correct one.

Approach. To reach these objectives we develop an approach, as shown in Figure 1, based on model transformation, and on property and behavioural equivalence checking. We start with BPMN models that may have been defined in any business process IDE that can output BPMN files that conform to the standard. The process designer uses our Web application, VBPMN, to input the (one or two depending on the verification to perform) process models and the verification parameters. We then have to transform these models into formal models that can support formal analysis. This is achieved in three steps. First we transform the business processes into an intermediate process meta model and format that we propose, the Process Intermediate Format (PIF). PIF gathers a subset of the main common concepts found in business process Domain Specific Modelling Languages (DSMLs). Using PIF as an intermediate model enables one to accept in the future UML Activity Diagrams or Event-driven Process Chains as inputs as soon as model transformations from these DSMLs to PIF are defined. Once we have PIF models, we perform a second transformation into the LNT process algebra. This is an expressive formal language that is at the core of the CADP verification toolbox and that has an operational semantics defined in terms of Labelled Transition Systems (LTSs). We also generate automatically verification scripts in the CADP SVL script language [START_REF] Garavel | SVL: A Scripting Language for Compositional Verification[END_REF]. Their content depends on the verification to be performed (checking for the absence of deadlock, for the satisfaction of a temporal property, or for the correctness of evolution). The CADP toolbox is then finally used to perform the verifications on the LTS semantics of the LNT processes and in case there is an error, a counter-example is returned to the user.

Contributions. The contributions of the work presented here are as follows:

• We present a model transformation from business processes defined in the BPMN standard to LTS formal models. This transformation supports the main gateways found in BPMN and is able to deal with unbalanced workflow models.

• We define a set of evolution relations for business processes that are grounded on formal behavioural relations.

• We propose an abstract intermediate meta model and format for busi-ness processes, PIF. It contains common process workflow concepts found in different business process DSMLs, thus opening the possibility to apply our approach to several of these DSMLs.

• We introduce VBPMN, a freely available tool [START_REF]VBPMN Framework[END_REF] that implements the model transformation and that enables, through a Web application, to check for the evolution of business process and get informative feedback in case of an error.

Outline. Section 2 introduces the BPMN business process modelling language and the running example we will use for illustration purposes. The transformation from BPMN models to the formal models we use for checking evolution is presented in Section 3, together with PIF, a business process meta model that plays an intermediate role between business process modelling languages (such as BPMN) and verification models (such as LTS). In Section 4 we then formally define several behavioural relations that can be used to compare business processes and, accordingly, to check business process evolution. Section 5 addresses the implementation of the outcomes of the previous sections. We present there VBPMN, our Web application for business process verification and some experimental data on the use of its core verification module. Finally, Section 6 reviews related work and Section 7 concludes the article.

BPMN

In this section, we give a short introduction on BPMN. We then present the running example we will use for illustration purposes in the rest of this paper.

BPMN is a workflow-based graphical notation (Fig. 2) for modeling business processes that can be made executable either using process engines (e.g., Activiti, Bonita BPM, or jBPM) or using model transformations into executable languages (e.g., BPEL). BPMN is an ISO/IEC standard since 2013 but its semantics is only described informally in official documents [START_REF] Omg | Business Process Model and Notation (BPMN) -Version 2[END_REF][START_REF]ISO/IEC, International Standard 19510, Information technology -Business Process Model and Notation[END_REF]. Therefore, several attempts have been made for providing BPMN with a formal semantics, e.g., [START_REF] Dijkman | Semantics and Analysis of Business Process Models in BPMN[END_REF][START_REF] Wong | A Process Semantics for BPMN[END_REF][START_REF] Kossak | A Rigorous Semantics for BPMN 2.0 Process Diagrams[END_REF][START_REF] Mateescu | Quantifying the Parallelism in BPMN Processes using Model Checking[END_REF][START_REF] Güdemann | VerChor: A Framework for the Design and Verification of Choreographies[END_REF]. In this paper, we abstract the features of BPMN related to data and we focus on the core features of BPMN, i.e., its control flow constructs, which is the subset of interest with respect to the properties we propose to formally analyse in this paper. More precisely, we consider the following categories of workflow nodes: start and end event, tasks, and gateways.

Start and end events are used to denote respectively the starting and the ending point of a process. A task is an abstraction of some activity and corresponds in practice, e.g., to manual tasks, scripted tasks, or inter-process message-based communication. In our context, we use a unique general concept of task for all these possibilities. Start (end, resp.) events must have only one outgoing (incoming, resp.) flow, and tasks must have exactly one incoming and one outgoing flow.

Gateways are used, along with sequence flows, to represent the control flow of the whole process and in particular the task execution ordering. There are five types of gateways in BPMN: exclusive, inclusive, parallel, event-based and complex gateways. An exclusive gateway is used to choose one out of a set of mutually exclusive alternative incoming or outgoing branches. It can also be used to represent looping behaviours. For an inclusive gateway, any number of branches among all its incoming or outgoing branches may be taken. A parallel gateway creates concurrent flows for all its outgoing branches or synchronizes concurrent flows for all its incoming branches. For an event-based gateway, it takes one of its outgoing branches based on events (message reception). Finally, complex gateways are used to model complex synchronization behaviours especially based on data control. If a gateway has one incoming branch and multiple outgoing branches, it is called a split (gateway). Otherwise, it should have one outgoing branch and multi- We support workflows that exhibit an unbalanced structure between splitmerge gateways. More precisely, this means that any merge gateway does not have necessarily a corresponding split gateway, that is, with the same type and with the same number of branches. We require that BPMN processes are syntactically correct, which is checked by ensuring that the BPMN model conforms to BPMN 2.0 specification. Moreover, although specific processes are syntactically correct, they may be semantically flawed. Those erroneous models are usually refered as anti-patterns [START_REF] Koehler | Process Anti-patterns: How to Avoid the Common Traps of Business Process Modeling[END_REF]. This is the case for instance when a process exhibits a looping behaviour coming back in-between a parallel/inclusive split and merge gateway. In that case, the semantical model will be infinite. This problem is well-known in process algebra, which usually forbids recursive agent calls through parallel composition operators (referred as finite control property [START_REF] Dam | Model Checking Mobile Processes[END_REF]). In our work, this case is detected by applying a pre-processing check and then discarded before model transformation and analysis. The pre-processing traverses the process and, for each parallel or inclusive merge gateway involved in an unbalanced structure, checks whether that gateway is inside a cycle.

Limitations. BPMN has three main kinds of models: processes, collaborations, and choreographies. In this work we deal with the first kind, and the other two are perspectives for a future release of VBPMN (see Section 7). Different subsets of the notation, called process modeling conformance sub-classes, are defined in the BPMN standard. In order to select a sufficient one, we did an analysis of the 825 BPMN processes available in the BIT process library, release 2009 [START_REF] Fahland | Instantaneous soundness checking of industrial business process models[END_REF]. These processes are industrial process models taken from different business domains such as finance or telecommunications. Table 1 presents the outcomes of this analysis, with the number of occurrences for each BPMN element (in the whole set of processes) and the number of processes in which at least one occurrence of the element is found. In our approach we are able to deal with all the BPMN elements we found in this analysis, but for sub-processes. This subset of BPMN that we support corresponds to what is defined as the descriptive conformance sub-class in the BPMN standard, without sub-processes and data, but with inclusive gateways. Sub-processes are a structuring mechanism in BPMN and they could possibly be removed by flattening the processes. Supporting data is of real interest, however, in the descriptive conformance sub-class, its role is unclear. There are no conditions on sequence flows going out of exclusive gateways in this sub-class for example. In the presence of conditional constructs and assignment activities, the support for data would require either to bound the data domains (which could be done using our approach) or to rely on symbolic approaches like in [START_REF] Nguyen | A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies[END_REF].

Example. We use the online shopping system depicted in Figure 3 as a running example. This process starts by searching items, logging in, and initiating payment (exclusive gateways, top part). Then, once the payment is completed, the availability of the ordered items is tackled (inclusive gateways, bottom part). Finally, items are shipped and delivered (exclusive gateways, bottom right part). If some item is unavailable or if the delivery fails (e.g., nobody is present to receive the parcel), a refund is processed provided the payment is made using voucher or card. We can see that this workflow is unbalanced (top right and bottom part) and includes a loop (bottom right part).

Models and Transformations

Process Intermediate Format

Business processes may be modelled using different DSMLs. BPMN is possibly the main one but one may also consider the use of UML Activity Diagrams (UML AD) or Event-driven Process Chains (EPC) for this. The formal approach for the verification of business process evolution advocated by our framework, could indeed apply not only to BPMN, but also to UML AD and EPC, and possibly others, as soon as one is able to retrieve two operational semantic models for the two processes to be compared defined in terms of LTSs. Provided one LTS gives the semantics of an EPC business process, and another LTS gives the semantics of a refactoring of this process in BPMN, our approach would apply.

LTS is a classic model to perform formal analysis. However, they are also quite low-level and do not make explicit the common concepts of business process DSMLs such as the workflow structure and split-join gateway patterns. Therefore, we propose to rely on a pivot meta model, the Process Intermediate Format (PIF), as an intermediate between business process DSMLs and LTS. As presented in Figure 4, PIF contains a subset of concepts found in existing workflow-based DSMLs. The Workflow Patterns Initiative, see e.g., [START_REF] Van Der Aalst | Workflow Patterns[END_REF], has shown that the whole set of concepts in workflow-based DSMLs is larger1 but we believe that the subset supported by PIF in its cur- rent version is sufficient for most process models. It is worth observing that PIF was used recently for validation of Mangrove models [START_REF] Cornax | Automated Analysis of Industrial Workflow-based Models[END_REF] and that a new transformation to Maude was developed for verification of timed business processes [START_REF] Durán | Verifying Timed BPMN Processes using Maude[END_REF].

3.2.

From BPMN to PIF BPMN process models are specified using XML documents conforming to the BPMN schema. A typical BPMN model contains BPMN Diagram Definition (DD) information in addition to BPMN Model information. However, from the verification point of view, DD information is not useful. Thus, model transformation from BPMN to PIF, extracts relevant data from a BPMN model and transforms it into PIF. The Workflow element in PIF is composed of a process, WorkflowNodes and SequenceFlows. WorkflowNodes can be of five different types: InitialEvent, Task, Communication, Gateway and EndEvent. PIF assumes that there is exactly one InitialEvent and one or more EndEvent in the Workflow. Gateway element is further classified into SplitGateway and JoinGateway. Gateways can follow Or, Xor or And pattern to control the process flows. BPMN to PIF transformation patterns are described in Table 2.

As one may have noticed in Table 2, PIF has elements similar to BPMN. So, the transformation is more like a mapping of BPMN model elements to parts in DSMLs, and the BPMN 2.0 standard refers to these workflow patterns when presenting the elements of its modelling notation.

PIF elements.

From PIF to LTS

We present here our transformation from PIF to LTS, obtained through a transformation from PIF to the LNT process algebra, LNT having an LTS semantics. We gave a semantics to each PIF construct based on the informal semantics given in the standard for the corresponding BPMN construct. Hence, using our BPMN to PIF mapping and our PIF to LNT transformation, one gets an LTS semantics for BPMN business processes. It is worth noting that the generated LTS is finite (the number of states is finite) because the BPMN/PIF process is syntactically correct and free of flawed patterns that may generate infinite models.

LNT. LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator[END_REF] is an extension of LOTOS [START_REF] Iso | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF], an ISO standardized process algebra, which allows the definition of data types, functions, and processes. Table 3 provides an overview of the behavioural fragment of LNT syntax and semantics. B stands for a LNT term, G for a gate or action, E for a Boolean expression, T for a type, and P for a process name. The syntax fragment presented in this table contains the termination construct (stop) and gates or actions (G) that may come with offers (send an expression E or receive in a variable x). LNT processes are then built using several operators: sequential composition (;), conditional statement (if), assignment (:=) where the variable should be defined beforehand, hiding (hide) that hides some action in a behaviour, nondeterministic choice (select), parallel composition (par) where the communication between the process participants is carried out by rendezvous on a list of synchronized actions, looping behaviours described using process calls or explicit operators (loop, while).

We also present in Table 3 some examples of rules defining the operational semantics of LNT (action prefix, sequential composition, conditional construct, variable assignment, hiding operator, and choice). An action or gate G can come with offers (send offer '!' or receive offer '?'). The value received in the variable x must be of the type of x (checked with the 'type' function). Note that the received value v substitutes x in B. The conditional statement if executes when the corresponding condition is evaluated to true (expressed using [[.]]). If the condition expression evaluates to false, it results in termination of the block without executing the condition block. Sequential composition consists of two rules. The first one corresponds to normal evolution of the B 1 behaviour. The second rule executes when the first behaviour terminates correctly (δ action). In that case, the second behaviour (B 2 ) starts executing. The operational rule for variable assignment shows how the fresh variable x is substituted by the evaluated expression E in the whole behaviour B. There are two rules for the hiding operator. The first one results in a normal execution if the gate does not belong to the set of gates to be hidden. The second rule, contrarily, involves a gate that is part of the gates to be hidden and the gate transforms into an unobservable τ action. Finally, the select operator triggers nondeterministically one of the choice branches. The reader interested in more details about the syntax and semantics of LNT should refer to [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator[END_REF].

The use of LNT is preferred over the direct use of LTS since this yields a simpler, high-level and more declarative transformation. Thanks to the LTS semantics of LNT, one can use thereafter a rich set of existing tools for LTS-based verification. The choice of LNT over other process algebras has been guided by the existence of the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], which comes with a very comprehensive set of verification tools, including ones supporting the implementation of the various checks presented in the sequel.

Overview. The idea is to encode as LNT processes all PIF elements involved in a process definition, that is, the nodes (tasks, gateways), which correspond to the behaviour of the business process, initial/end events, and sequence flows, which encode the execution semantics of this process. Finally, all these independent LNT processes are composed in parallel and synchronized in order to respect the business process execution semantics. For instance, after execution of a node, the corresponding LNT process synchronizes with the process encoding the outgoing flow, which then synchronizes with the process encoding the node appearing at the end of this flow, and so on.

The encoding patterns for the main PIF constructs are described in Table 4 except for Or gateways, which are tackled separately in Tables 5 and6. The actions corresponding to the flows ( incf, outf, etc.) will be used as synchronization points between the different workflow elements. The begin and finish actions in the initial/end events are just used to trigger and terminate, respectively, these events. The actions used in task constructs (e.g., task) will be the only ones to appear in the final LTS. All other synchronizations actions will be hidden because they do not make sense from an observational point of view. We do not present the encoding of communication/interaction messages in Table 4 because they are translated similarly to tasks. And gateways are encoded using the par LNT operator, which corresponds in this case to an interleaving of all flows. Xor gateways are encoded using the Table 3: LNT Syntax and Semantics (Behaviour Part) [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator[END_REF].

B ::= stop | G(!E, ?x) | B 1 ; B 2 | if E then B end if | var x:T in x := E; B end var | hide G 1 , ..., G m in B end hide | select B 1 []...[]B n end select | par G 1 , ..., G m in B 1 ||...||B n end par | P [G 1 , ..., G m ](E 1 , ..., E n ) | loop B end loop | while E loop B end loop Act v ∈ type(x) G(!E, ?x) ; B G ![[E]] !v → B{v /x} Seq-1 B 1 β → B 1 B 1 ; B 2 β → B 1 ; B 2 Seq-2 B 1 δ → B 1 B 2 β → B 2 B 1 ; B 2 β → B 2 If-1 [[E]] = true B β → B if E then B end if β → B If-2 [[E]] = false if E then B end if δ → stop Var B{[[E]]/x} β → B var x:T in x := E; B end var β → B Hid-1 B β → B gate(β) ∈ {G 1 , ..., G m } hide G 1 , ..., G m in B end hide β → hide G 1 , ..., G m in B end hide Hid-2 B β → B gate(β) ∈ {G 1 , ..., G m } hide G 1 , ..., G m in B end hide τ → hide G 1 , ..., G m in B end hide Sel i ∈ [1, n] B i β → B i select B 1 []...[]B n end select β → B i
loop incf ; select outf1 [] outf2 [] outf3 end select end loop XorJoin loop select incf1 [] incf2 [] incf3 end select ; outf end loop
select LNT operator, which corresponds to a nondeterministic choice among all flows. All constructs (sequence flows, tasks, gateways) are enclosed within an LNT loop operator since these elements can be repeated several times if the business process exhibits looping behaviours. However, the decision to repeat is not taken at this local level, but it depends of the overall workflow structure whose encoding will be presented in the rest of this section.

Composition. Once all workflow elements are encoded into LNT, the next step is to compose them in order to obtain the behaviour of the whole business process. To do so, we compose in parallel all the flows with all the other constructs. All flows are interleaved because they do not interact one with another. All events and nodes (start/end events, tasks, gateways) are interleaved as well for the same reason. Then both sets are synchronized on flow sequences (actions denoted by sequence flow IDs). These additional actions are finally hidden because they should not appear as observable actions and will be transformed into internal transitions in the resulting LTS. Each process call is accompanied with its alphabet, that is, the list of actions used in that process. For instance, each call of a flow process comes with a couple of actions corresponding to the initiation and termination of the flow.

Balanced Or gateways. The Or gateways in PIF correspond to the BPMN inclusive gateways. The semantics of the inclusive gateways is quite intricate in the original version of BPMN [START_REF] Christiansen | Formal Semantics and Implementation of BPMN 2.0 Inclusive Gateways[END_REF]. BPMN 2.0 simplifies the semantics of the inclusive merge gateway by allowing the merge to execute whenever a token arrives at the merge level. From the process algebra point of view, this can be simply encoded as an XorJoin gateway as already presented beforehand in this section. In the rest of this section, we assume that the OrJoin gateways correspond to a real synchronization point as described in the execution semantics of the first version of BPMN. We support both semantics in the tool support we will present in Section 5.

As a first step, we also assume here that each OrJoin gateway has a corresponding OrSplit gateway with the same number of branches. This is what we call balanced gateway that can be generalized to balanced workflows / processes if all gateways in the process exhibit a balanced structure. The encoding of the Or gateways use the select and par operators to allow all possible combinations of the outgoing branches. Table 5 describes the translation patterns in LNT. Note the introduction of synchronization points (s i ), which are necessary to indicate to the OrJoin gateway the behaviour that was executed at the OrSplit level. Without such synchronization points, an OrJoin gateway does not know whether it is supposed to wait for one or several branches (and which branches in this second case).

Unbalanced Or gateways. In case of an unbalanced structure of the workflow, we cannot use the synchronization points solution we used for balanced Or gateways. Therefore, the only solution we have is to use a global process in charge of keeping track of all active tokens and of deciding if a certain OrJoin gateway can be triggered or not. To do so, we use an additional process called scheduler. The scheduler runs in parallel with all the other LNT processes encoding the aforementioned workflow constructs and synchronizes with them to keep track of active flows in the whole PIF process. Each time a synchronization occurs between the scheduler and a flow process, the scheduler updates a local set of flow identifiers corresponding to the set of active flows. This means that at any moment during the process exploration, the scheduler exactly knows all tokens currently active.

Table 6 describes the translation patterns in LNT for unbalanced Or gateways. Note that synchronization points (s i ) are still necessary at the OrSplit level to indicate to the scheduler how many branches have been fired and to enable it to capture the exact number of active tokens. One can also see that each flow action has as parameter the identifier of the flow, which is required at the scheduler level to keep track of active tokens. The process encoding the OrJoin gateway is different in case of unbalanced structure. First of all, the process is activated when a first token arrives at this level of the workflow. Concretely speaking, this corresponds to a synchronization between the OrJoin process and one of the incoming flows. Then, the OrJoin process can either accumulate tokens or can receive a message from the scheduler indicating that the merge is possible (no more tokens are to be awaiting). In that case, the scheduler moves on and synchronizes with the outgoing flow, which means that a token is generated for that flow. Note that the synchronization between the OrJoin process and the scheduler is effective only when the scheduler decides so, we will see how it works in practice in the next paragraph.

The scheduler runs in parallel to all other LNT processes and can synchronize (Sync) on all actions as described in Figure 5. The scheduler is passive in the sense that it does not impact the execution of the workflow, but for OrJoin gateways. In that latter case, the scheduler decides whether to trigger a specific OrJoin gateway. For all other workflow elements, the scheduler synchronizes on flows and keeps track of all active tokens in a local set. To do so, the scheduler is encoded in LNT using a select construct. It is worth noting that in order to catch tokens without "losing" them during the execution, the scheduler has to reproduce faithfully the business process execution. As an example, when a token arrives at a task, the scheduler synchronizes in sequence with the flow incoming that task followed by the flow outgoing the task. This behaviour appears in the same choice of the select mentioned before. If it were to be encoded differently, the token would disappear during the task execution, generating erroneous computation of the scheduler at the OrJoin gateway level. If we put it differently, the scheduler implements task execution in an atomic manner.

Figure 6 shows an excerpt of the scheduler process for our running example. Here, we can note that the scheduler keeps track of the tokens by adding and removing the identifiers in the activeflows set. Consider flow37 begin which refers to the initial event, in this case the scheduler does not remove any identifier from the active flow set as there is no incoming flow. Similarly, for flow30 finish which is an end event, the scheduler does not add any identifier to the active flow set. As mentioned earlier, the scheduler mimics the workflow behaviour. This is illustrated in flow39 finish, which refers to an Xor gateway. Since Xor is a choice, we see the select operator with two choices corresponding to the outgoing flows (flow2, flow3). It is also worth noting that the scheduler removes ident1 from the active flows and adds the identifier corresponding to the begin flow (ident2 or ident3) in order to keep track of the tokens. Let us now focus on the active part of the scheduler, that is, the part of its behaviour where it decides whether an activated OrJoin gateway can be triggered or not. Note that the scheduler process is equipped with four parameters corresponding to: (i) the set of active tokens (IDS is a set of identifiers), (ii) the structure of the business process, (iii) the set of tokens accumulated at the OrJoin level, and (iv) the set of currently activated OrJoin gateways. The scheduler triggers a merge behaviour if there is an active merge (an OrJoin gateway) waiting to happen. If there are several activated OrJoin gateways, there is an enumeration on all their identifiers. Given an OrJoin gateway identifier, we check whether the merge is possible (is merge possible). In case of no token being present upstream of the OrJoin gateway, all tokens have arrived, hence the merge is possible. But we also have to check if the scheduler has consumed all arrived tokens (is sync done). If both conditions are satisfied, we synchronize with the process encoding the concerned OrJoin gateway indicating it that the merge can be triggered (MoveOn). The entire LNT code for those functions (is merge possible and is sync done) is given in appendix. Finally, we synchronize on the flow outgoing of that OrJoin gateway and we recursively call the scheduler process updating all parameters. If the merge is not possible, we have a simple recursive call to the scheduler process without changing any parameter. synchronizes on flow actions as well as on the MoveOn action which is used by the scheduler to submit messages to the processes encoding OrJoin gateways. The process is encoded in two parts, flows on the one hand and nodes on the other hand. The LNT processes for flows and nodes synchronize on flow actions. Last but not least, from an external point of view, all flow actions are hidden to let visible only task names. One can see the corresponding LTS (56 states and 119 transitions) shown in Figure 8 where we removed all internal transitions for readability reasons. The top part of the LTS is quite dense because the use of inclusive gateways in BPMN (Or gateways in PIF) induce many possible combinations in the order of task executions.

| | f i n a l [ f l o w 3 0 f i n i s h , f i n i s h ] | | f i n a l [ f l o w 3 4 f i n i s h , f i n i s h ] | | . . . | | | | x o

Evolution Notions

In this section, we formally define several kinds of comparisons between BPMN processes. Their analysis allows one to ensure that the evolution of one process into another one is satisfactory.

Notation. LNT processes are denoted in italics, e.g., p, and BPMN processes are denoted using a bold font, e.g., b. In the sequel, we denote with ||p|| the semantic model of an LNT process p, that is the LTS for p. Further,

Preliminaries

The following definitions are taken from [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF]. They are relative to the LTS-level relations that we ground on to define our evolution relations.

Definition 1 (Branching bisimulation). Two graphs g and h are branch-ing bisimilar if there exists a symmetric relation R [...] (called branching bisimulation) between the nodes of g and h such that:

(i) The roots are related by R;

(ii) If R(r, s) and r → a r , then either a = τ and R(r , s) or there exists a path s ⇒ s 1 → a s 2 ⇒ s such that R(r, s 1 ), R(r , s 2 ) and R(r , s ).

The original definition (given above) refers to (process) graphs that are "connected, rooted, edge-labelled and direct graphs" [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF]. LTSs are such graphs, with the roots corresponding to initial states. In the definition, r → a r denotes an edge (= LTS transition) from node (= LTS state) r to node r labelled by a. Further, s ⇒ s 1 denotes a sequence (path) of zero or more silent (τ ) transitions from s to s 1 (s can be s 1 ). In the sequel we also refer to branching bisimulation as branching equivalence, and when g and h are branching bisimilar we may use g br ≡ h. If we remove the symmetric constraint on R in the previous definition we get a branching simulation or branching preorder between g and h, denoted with g br < h, and we say that h simulates g.

Conservative Evolution

Our first comparison criterion is strong. Given an evolution b b , it ensures that the observable behaviour of b is exactly preserved in b . It supports very constrained refactorings of BPMN processes such as grouping or splitting parallel or exclusive branches (e.g., ( (a, b), c) (a, b, c) where (x 1 , . . . , x n ) denotes a balanced exclusive split-merge). At the semantic level, several behavioural equivalences could be used. We have to deal with internal transitions introduced by hiding (see Section 3). Hence, we chose to use branching equivalence, introduced in Section 4.1, since it is the finest equivalence notion in presence of such internal transitions.

Inclusive and Exclusive Evolution

In most cases, one does not want to replace a business process by another one having exactly the same behaviour. Rather, one wants to be able to add new functionalities in the process, without interfering with the existing ones. The duality between inclusive and exclusive evolution is usual when one formalizes the fact that some abstract specification a is correctly implemented into a more concrete system c. For some people, this means that at least all the behaviours expected from a should be available in c. Taking the well-known "coffee machine" example, if a specification requires that the machine is able to deliver coffee, an implementation delivering either coffee or tea (depending on the people interacting with it) is correct. For others, e.g., in the testing community, an implementation should not expose more behaviours than what was specified.

Selective Evolution

Up to now, we have supposed that all tasks in the original process were of interest. Still, one could choose to focus on a subset of them, called tasks of interest. This gives freedom to change parts of the processes as soon as the behaviours stay the same for the tasks of interest. For this, we define selective evolution up to a set of tasks T . Tasks that are not in this set will be hidden in the comparison process. Formally, this is achieved with an operation [T ] on LTSs, which, given an LTS l, hides any transition whose label is not in T by changing this label to τ (it becomes an internal transition). Again, here we can rely on branching equivalence to deal with these internal transitions. A specific interesting case of selective evolution is when the set of tasks of interest corresponds exactly to the tasks of the original process. This lets the designer add new behaviours not only in a separate way (as with inclusive evolution) but also within the behaviours of the original process. For example, a; b (a, log); b, that is a way to log some each time a is done, is not an inclusive evolution but is a selective conservative evolution with reference to {a, b}. Accordingly to selective conservative evolution, we can define selective inclusive evolution (respectively selective exclusive evolution) by using the branching preorder, br <, instead of br ≡.

Renaming and Refinement

One may also want to take into account renaming when checking an evolution b b . For this we use a relabelling relation R ⊆ T b × T b , where T b (respectively T b ) denotes the set of tasks in b (respectively b ). We require that for every t in T b , if we have (t, t 1 ) and (t, t 2 ) in R then t 1 = t 2 , i.e., R is a (possibly partial) function. Applying a relabelling relation R to an LTS l, which is denoted by l R, consists in replacing in l any transition labelled by some t in the domain of R by a transition labelled by R(t).

To take into account task renaming in any of the above-mentioned evolutions, we just have to perform the equivalence (or preorder) checking up to relabelling in the formal model for b. Sometimes renaming is not sufficient, e.g., when evolution corresponds to the refinement of a task by a workflow. We define a refinement rule as a couple (t, W ), noted t W 2 , where t is a task and W a workflow. A set of refinement rules, or refinement set, R = i∈1...n t i W i is valid if there are no multiple refinements of the same task (∀i, j ∈ 1 . . . n, i = j ⇒ t i = t j ) and if no refinement rule has in its right-hand part a task that has to be refined (∀i, j ∈ 1 . . . n, t i ∈ W j ). These constraints enforce that refinements do not depend on the application ordering of refinement rules, i.e., they are deterministic.

To take into account refinement in evolution, a pre-processing has to be performed on the source process. For example, given that b R denotes the replacement in b of t i by W i for each

t i W i in R, b b is a conservative evolution up to a refinement set R iff || Θ(b R) || br ≡ || Θ(b ) ||.

Property-Aware Evolution

A desirable feature when checking evolution is to be able to focus on properties of interest and avoid in-depth analysis of the workflows. This gives the freedom to perform changes (including some not possible with the previous evolution relations) as long as the properties of interest are preserved. Typical properties are deadlock freedom or safety and liveness properties defined over the alphabet of process tasks and focusing on the functionalities expected from the process under analysis. Such properties are written in a temporal logic supporting actions and, to make the property writing easier, the developer can rely on well-known patterns as those presented in [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF].

Context-Aware Evolution

A process is often used in the context of a collaboration, which in BPMN takes the form of a set of processes ("pool lanes") communicating via messages. When evolving a process b, one may safely make changes as soon as they do not have an impact on the overall system made up of b and these processes. To ensure this, we have to compute the semantics of b communicating on a set of interactions I (a subset of its tasks) with the other processes that constitute the context of b. We support two communication modes: synchronous or asynchronous. For each mode m we have an operation × I is the LTS synchronous product [START_REF] Arnold | Finite Transition Systems -Semantics of Communicating Systems[END_REF]. For asynchronous communication, m × I is achieved by adding a buffer to each process [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. Here, to keep things simple, we will suppose without loss of generality, that a context is a single process c. Accordingly, we may define context-aware inclusive and exclusive evolution, or combine them with renaming and refinement.

Example. We introduce in Figure 9 a revised version of the online shopping process presented in Figure 3. In this new process, when the client decides to choose and buy items, (s)he can sign in/up in parallel with its decision to purchase specific items. In the new process, it is achieved by adding an additional parallel gateway.

The two versions of the online shopping process are not conservative because the Choose Items task can appear before Sign In/Up tasks in the new version of the process. However, both versions are related with respect to the inclusive/exclusive evolution notions. The new version includes all possible executions of the former one (the opposite is false) while incorporating new traces (those including Choose Items and Sign In/Up in sequence for instance).

As far as property-aware evolution is concerned, one can check for instance whether any Choose Items task eventually leads to a Deliver Items task. Following [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF], this corresponds to the pattern:

REQUIREMENT: The choice of items will eventually lead to items being delivered. PATTERN: Response, between Choose Items and Deliver Items SCOPE: Global

In [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF], the patterns are related to the LTL and CTL temporal logics, and to quantified regular expressions. Since we target the CADP verification toolbox, we use MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF] instead. The pattern can be formalized in MCL using box modalities ([..]) and fix points (mu X . (..)) as follows:

[true* . "CHOOSEITEMS"] mu X . ( true true and [not ("DELIVERITEMS")] X)

The property specifies that each Choose Items transition in the LTS denoted by [true* . "CHOOSEITEMS"], would inevitably lead to the delivery of items, which is specified by the formula: mu X . ( true true and [not ("DE-LIVERITEMS")] X). This property is actually not satisfied for any version of the process because some item may be unavailable or because the delivery may abort after several attempts. If using the same pattern we check that the Choose Items task eventually leads to the Check Inventory task, this property is satisfied by both versions of the online shopping process.

Tool Support

In this section, we focus on the implementation of our approach. We will present first the Web application that can be used to access and use the VBPMN analysis functionalities. Then, we will focus on the verification of BPMN processes using the CADP toolbox, and we will particularly present some experimental results to show how our approach scales.

Web Application

Business processes are usually designed by business analysts that may not be familiar with formal verification techniques and tools. Our goal is to enable one to benefit from formal verification without having to deal with a steep learning curve. The VBPMN Web Application has been developed in this direction. It hides the underlying transformation and verification process, it provides the users with simple interaction mechanisms, and it generates analysis results that are easily relatable to the input process model(s). There are numerous IDEs supporting the modelling of business processes. Extending a specific one, e.g. the Eclipse BPMN designer, would limit the community that could use VBPMN. Hence, we have decided to architect it as a Web application. However, the integration as a plug-in of a platform for business processes that goes beyond modelling, such as ProM [START_REF]ProM Framework[END_REF], would be a relevant and complementary approach as far as broadening the audience of our verification techniques is concerned.

The VBPMN Web application is hosted on a Tomcat application server. Its responsive UI invokes a RESTful API to trigger the transformation from BPMN to PIF and the verification of the process models. The use of such an API makes the platform more extensible -other people could build custom UIs using them. Internally, the API is built using the Jersey JAX-RS implementation. The model-to-model transformation from BPMN to PIF is realized at the XML level (both BPMN and PIF have XML representations) using a combination of JAXB and of the Woodstox Streaming XML API (StAX), which implements a pull parsing technique and offers better performance for large XML models. The model-to-text transformation from PIF to LNT and SVL [START_REF] Garavel | SVL: A Scripting Language for Compositional Verification[END_REF] is achieved using a Python script that can also be used independently from the Web application as a command-line interface tool.

As far as the user interface is concerned, one can choose either to verify some property or to check process evolution correctness. In the first case (Fig. 10), one has to upload the BPMN process model and specify the temporal logic formula for the property.

In the later case (Fig. 11), one has to upload two BPMN processes, specify the evolution relation, and optionally give tasks to hide or to rename in the comparison. As a result one can visualize the LTS models that have been generated for the BPMN processes. Further, in case the verification fails, i.e., either the property does not yield or the evolution is not correct, one gets a counter-example model.

Analysis with CADP

The operational semantics of the LNT process algebra enables us to generate LTSs corresponding to the BPMN process model given in the VBPMN UI. These LTSs may then be analyzed using CADP. VBPMN currently provides two kinds of formal analysis: functional verification using model checking and process comparison using equivalence checking.

Functional verification. One can for example use model checking techniques to search for deadlocks or livelocks. Another option is to use the CADP model checker for verifying the satisfaction of process-specific safety and liveness properties. In this case, since the properties depend on the process, they have to be provided by the analyst. The use of patterns for properties is a perspective (see Section 7).

One can also be interested in checking soundness of the process. Soundness as defined in [START_REF] Van Der Aalst | The Application of Petri Nets to Workflow Management[END_REF] requires three conditions:

• C1, from the initial state it is always possible to reach the final state,

• C2, from the moment the final state is reached, there are no remaining tokens in the process,

• C3, there is no dead transition from the initial state.

All three conditions can be checked using MCL formulas and model checking techniques. C3 can be checked using, for any task t, the following formula: true * . "t" true C1 requires to let visible (it is hidden for now, see Fig. 7) the finish action used to encode end events in LNT (Tab. 4) and to check the reachability on all paths of those actions: mu X . ( true true and [not ("finish")] X) C2 requires in addition to make appear as parameter to this finish action the number of current tokens remaining in the process, and then to check that when such actions are reached, the number of tokens is zero.

Process comparison. It takes as input two process models, an evolution relation and possibly additional parameters for the relation. Several evolution relations are proposed. Conservative evolution ensures that the observational behaviour is strictly preserved. Inclusive evolution ensures that a subset of a process behaviour is preserved in a new version of it. Selective evolution (that is compatible with both conservative and inclusive evolution) allows one to focus on a subset of the process tasks. It is also possible to have VBPMN work up-to a renaming relation over tasks. If the two input process models do not fulfil the constraints of the chosen evolution relation, a counter-example that indicates the source of the violation is returned by VBPMN in the UI. This helps the process analyst in understanding the impact of evolution and supports the refinement into a correct evolved version of a process model. All the evolution relations are checked using the CADP equivalence checker and SVL scripts for hiding and renaming as demonstrated with the SVL patterns in Figure 12.

Experiments

We used a Mac OS laptop running on a 2.3 GHz Intel Core i7 processor with 16 GB of Memory. We carried out experiments on many examples taken from the literature or hand-crafted, and we present in Table 7 some of these results. ..} → in the tool: mode=conservative, options=hide/rename + hide T with expose mode -expose mode is a shortcut to hide all tasks but for the ones given "b.bcg" = total hide all but t1, ... in "b.bcg" "b'.bcg" = total hide all but t1, ... in "b'.bcg" bcg open "b.bcg" bisimulator -equal -branching -diag "b'.bcg" checking conservative evolution of b b up to a relabelling R={(t 1 , t 1 ), . . .} → in the tool: mode=conservative, options=hide/rename + rename R with rename first -rename first is an option to rename in the first process only -it is also possible to rename in the second process or in both "b.bcg" = total rename t1 -> t1', ... in "b.bcg" bcg open "b.bcg" bisimulator -equal -branching -diag "b'.bcg"

Each example consists of two versions of the process (original and revised).

For each version, we first characterize the workflow by giving the number of tasks, sequence flows, and gateways. We also indicate whether the workflow exhibits balanced structure especially for inclusive gateways (B) 3 and if there is looping behaviour in the process (L). We show then the size (states and transitions) of the resulting LTS before and after minimization. Minimization is useful for automatically removing unnecessary internal transitions, which were introduced during the process algebra encoding but do not make sense from an observational point of view. We use branching reduction [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF], which is the finest equivalence notion in presence of internal transitions and removes most internal transitions in an efficient way. Finally, the last column gives the results when comparing the LTSs for the two versions of the process using conservative, inclusive, and exclusive evolution, resp., and the overall computation time.

Examples 8 and 8' correspond to the first and second versions of the online shopping process we used in this paper as running example. Medium-size examples (e.g., example 7) can result in quite huge LTSs involving millions of states and transitions. This is due to our choice to show processes in the table containing several parallel and inclusive gateways, in most cases nested, which result in many possible interleaved executions in the corresponding LTSs. In contrast, example 10/10' involves about 200 tasks but exhibits a quite sequential structure, and then the generated LTSs are very small (less than a thousand states and transitions). Another comment concerns the considerable drop in size of the LTSs before and after minimization. Example 3' for example goes from about 2,000 states/5,000 transitions to about 30 states/60 transitions. This drastic reduction is due to all sequence flow actions encoded in LNT for respecting the BPMN original semantics. They do not have any special meaning per se, and are therefore hidden and removed by reduction.

As far as computation times are concerned, we observe that the final column of Table 7 gives the overall time, that is, the time for generating both LTSs, minimizing and comparing them. The comparison time is negligible. It takes 568 seconds (9 minutes and 28 seconds) for instance for generating and minimizing both LTSs for examples 11 and 11', and only 3 seconds for comparing both LTSs wrt. the three evolution notions considered in the table. Note that for processes involving unbalanced inclusive gateways, the time importantly increases for generating corresponding LTSs compared to balanced workflows. This is the case between example 12/12' which takes more than 10 minutes for generating an LTS consisting of about 1 million of states/transitions whereas example 11/11' results in less than 10 minutes to obtain an LTS containing about 4 millions of states and 26 millions of transitions. This drastic fall-down in performance comes from the LNT encoding for unbalanced workflows, which induces extra-computations during the LTS generation process. On a wider scale, computation times remain reasonable (about half an hour for all the examples shown in Table 7) even for LTSs containing millions of states and transitions.

Related Work

The absence of a single accepted modelling notation for business processes, raised the need to find ways to relate models written using different notations. The Workflow Pattern Initiative, see, e.g, [START_REF] Van Der Aalst | Workflow Patterns[END_REF], has addressed this issue by caracterizing the atomic patterns one may find in business processes. A correspondence between these patterns and some workflow languages, in-cluding BPMN, UML AD, and EPC, can be found on their Web site. Further, the BPMN standard itself refers to workflow patterns for its notational elements. Several general ontologies for business process modelling have also been proposed, a comprehensive one being BPMO [START_REF] Yan | Semantic Business Process Modeling and WSMO Extension[END_REF] 4 . PIF is simpler than BPMO. It originates from a previous intermediate format we had defined, CIF [START_REF] Güdemann | VerChor: A Framework for the Design and Verification of Choreographies[END_REF]. Its objective is neither to be a comprehensive set of all concepts found in workflows, nor to support automated mapping between notations in their whole. Rather, it is focused on a subset of common concepts found in the three main business process notations that support a formal treatment in order to achieve different formal analyses of business processes.

Several works have focused on providing formal semantics and verification techniques for business processes using Petri nets, process algebras, abstract state machines, or rewriting logic. There was a significant effort aimed at providing formal semantics and verification techniques for business processes using Petri nets, see, e.g., [START_REF] Martens | Analyzing Web Service Based Business Processes[END_REF][START_REF] Decker | Interaction-centric Modeling of Process Choreographies[END_REF][START_REF] Dijkman | Semantics and Analysis of Business Process Models in BPMN[END_REF][START_REF] Raedts | Transformation of BPMN Models for Behaviour Analysis[END_REF][START_REF] Corradini | An Operational Semantics of BPMN Collaboration[END_REF]. To the best of our knowledge, none of these works focus on the formal comparison and evolution of processes. As far as rewriting logic is concerned, in [START_REF] El-Saber | BPMN Formalization and Verification using Maude[END_REF], the authors propose a translation of BPMN into rewriting logic with a special focus on data objects and data-based decision gateways. They provide new mechanisms to avoid structural issues in workflows such as flow divergence by introducing the notion of well-formed BPMN process. Their approach aims at avoiding incorrect syntactic patterns whereas we propose automated analysis at the semantic level. Rewriting logic is also used in [START_REF] Durán | Verifying Timed BPMN Processes using Maude[END_REF] for analyzing BPMN processes with time using simulation, reachability analysis, and model checking to evaluate timing properties such as degree of parallelism and minimum/maximum processing times. We focus on behavioural and not on time analysis here.

Let us now concentrate on those using process algebras for formalizing and verifying BPMN processes, which are the most related to the approach presented in this paper. The authors of [START_REF] Wong | A Process Semantics for BPMN[END_REF] present a formal semantics for BPMN by encoding it into the CSP process algebra. They show in [START_REF] Wong | Verifying Business Process Compatibility[END_REF] how this semantic model can be used to verify compatibility between business participants in a collaboration. This work was extended in [START_REF] Wong | A Relative Timed Semantics for BPMN[END_REF] to propose a timed semantics of BPMN with delays. [START_REF] Capel | Automating the Transformation from BPMN Models to CSP+T Specifications[END_REF][START_REF] Mendoza-Morales | Conceptual Framework for Business Processes Compositional Verification[END_REF] focus on the semantics proposed in [START_REF] Wong | A Process Semantics for BPMN[END_REF][START_REF] Wong | A Relative Timed Semantics for BPMN[END_REF] and propose an automated transformation from BPMN to timed CSP. In a previous work [START_REF] Güdemann | VerChor: A Framework for the Design and Verification of Choreographies[END_REF], we have proposed a first transformation from BPMN to LNT, targeted at checking the realizability of a BPMN choreography. We followed a state machine pattern for representing workflows, while we here encode them in a way close to Petri net firing semantics, which favours compositionality and is more natural for a workflow-based language such as BPMN. In [START_REF] Corradini | An Operational Semantics of BPMN Collaboration[END_REF], the authors propose a new operational semantics of a subset of BPMN focusing on collaboration diagrams and message exchange. The BPMN subset is quite restricted (no support of the inclusive merge gateway for instance) and no tool support is provided yet. Compared to the approaches above, our encoding also gives a semantics to the considered BPMN subset by translation to LNT, although it was not our primary goal. The main difference with respect to these related works is our focus on the evolution of processes and its automated analysis.

In the rest of this section, we present existing approaches for comparing several BPMN processes (or workflows). In [START_REF] Lam | Foundation for Equivalences of BPMN Models[END_REF], the author proposes a theoretical framework for comparing BPMN processes. His main focus is substitutability and therefore he explores various sorts of behavioural equivalences in order to replace equals for equals. This work applies at the BPMN level and aims at detecting equivalent patterns in processes. In a related line of works, [START_REF] Kluza | Overview of BPMN Model Equivalences. Towards Normalization of BPMN Diagrams[END_REF] studies BPMN behaviours from a semantic point of view. It presents several BPMN patterns and structures that are syntactically different but semantically equivalent. This work is not theoretically grounded and is not complete in the sense that only a few patterns are tackled. The notion of equivalence is similar to the one used in [START_REF] Lam | Foundation for Equivalences of BPMN Models[END_REF]. The authors of [START_REF] Kluza | Overview of BPMN Model Equivalences. Towards Normalization of BPMN Diagrams[END_REF] also overview best practices that can be used as guidelines by modelers for avoiding syntactic discrepancies in equivalent process models. Compared to our approach, this work only studies strong notions of equivalence where the behaviour is preserved in an identical manner. We consider a similar notion here, but we also propose weaker notions because one can make deeper changes (e.g., by introducing new tasks) and in these cases such strong equivalences cannot be preserved.

In Chapter 9 of [START_REF] Reichert | Enabling Flexibility in Process-Aware Information Systems -Challenges[END_REF], the authors study the evolution of processes from a migration point of view. They define several notions of evolution, migration, and refactoring. Our goal here is rather complementary since we have studied the impact of modifying a workflow wrt. a former version of this workflow on low-level formal models, but we do not propose any solutions for applying these changes on a running instance of that initial workflow. In [START_REF] Weidlich | Behaviour Equivalence and Compatibility of Business Process Models with Complex Correspondences[END_REF], the authors address the equivalence or alignment of two process models. To do so, they check whether correspondences exist between a set of activities in one model and a set of activities in the other model. They consider Petri net systems as input and process graphs as low-level formalism for analysis purposes. Their approach resides in the identification of regions (set of activities) in each graph that can coincide with respect to an equivalence notion. They particularly study two equivalence notions, namely trace and branching equivalences. The main limit of this approach is that it does not work in the presence of overlapping correspondences, meaning that in some cases, the input models cannot be analyzed. This work shares similarities with our approach, in particular the use of low-level graph models, hiding techniques and behavioural equivalences for comparing models. Still, our approach always provides a result and considers new notions of model correspondence such as property-aware evolution.

It is worth mentioning another line of work aiming at measuring the degree of similarity of business process models, see, e.g., [START_REF] Van Dongen | Measuring Similarity between Business Process Models[END_REF][START_REF] De Medeiros | Quantifying Process Equivalence Based on Observed Behavior[END_REF]. As an example, [START_REF] Van Dongen | Measuring Similarity between Business Process Models[END_REF] achieves this goal first using causal footprints as an abstract representation of the behaviour captured by a process model. Then, given two footprints, the similarity is computed using the vector space model approach from information filtering and retrieval. In this paper, we chose a different angle of this question by studying qualitative aspects of processes instead of quantitative aspects.

This article is an extended version of a conference paper published in [START_REF] Poizat | Checking Business Process Evolution[END_REF]. The key additions of this journal version are as follows: (i) an improvement of our process algebra encoding to support unbalanced workflows, (ii) the extension of our tool support, and particularly of the Web application, to support comparison analysis as well as model checking of business processes, (iii) the extensive validation of our approach on a large set of case studies, most of them taken from the literature on this topic, and (iv) a refined review and comparison with related work.

Conclusion

We have introduced our approach for checking the evolution of BPMN processes. To promote its adoption by business process designers, we have implemented it in a tool, VBPMN [START_REF]VBPMN Framework[END_REF], that can be used through a Web application. We have presented different kinds of atomic evolutions that can be combined and formally verified. We have defined a BPMN to LNT model transformation, which, using the LTS operational semantics of LNT enables us to automate our approach using existing LTS-based verification tools. This translation to LNT supports exclusive, inclusive and parallel gateways (including different semantics of inclusive merge gateways), looping behaviours, and unbalanced structure of workflows. We have applied our approach to many examples for evaluation purposes. The experimental results shown in this paper confirm that our tool is rather efficient since it can handle quite large examples within a reasonable amount of time.

As far as perspectives are concerned, let us mention the main ones. Larger subset of the BPMN standard. BPMN has three main kinds of models: processes, collaborations, and choreographies. In this work we support the first ones, at the descriptive conformance sub-class level, without sub-processes and data, but with inclusive gateways. We plan to extend our support to sub-processes (with boundary events to deal with errors and compensations) and data (to deal with conditional flows). As far as other kinds of models are concerned, collaborations where only one process evolves can be supported using context-aware evolution, one of the evolution relations we propose. The extension to full-fledged collaborations could be possible through the transformation of each process in the collaboration and by relating communication tasks (synchronously or using buffers for asynchronous communication). The extension to choreography is possible by adding choreography tasks in PIF and treating them as basic observable atoms in the behavioural equivalences and inclusion relations. However, based on our past experience on choreography verification [START_REF] Güdemann | VerChor: A Framework for the Design and Verification of Choreographies[END_REF], we believe that specific evolutions relations could be defined for choreographies. Patterns of properties. When the analyst wants to check model-specific properties on the processes, they have to be input directly using the MCL temporal logic. The reuse of well-known patterns for properties such as those presented in [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF], and the automation of a translation from such patterns to the MCL temporal logic would clearly help there. Enhanced feed-back. Diagnoses are returned to the designers in the form of low-level counter-examples (LTSs). This could be enhanced by presenting this information directly on the BPMN models, e.g. using animation. New front-and back-ends. In the implementation of our BPMN to LNT transformation, we rely on an intermediate format including the main workflow-based constructs. This paves the way for new front-end DSLs and other back-end verification techniques. Another perspective of this work is to propose quantitative analysis for comparing business processes as studied in [START_REF] Van Dongen | Measuring Similarity between Business Process Models[END_REF][START_REF] De Medeiros | Quantifying Process Equivalence Based on Observed Behavior[END_REF]. Our goal is thus to consider non-functional requirements in BPMN processes, such as the throughput and latency of tasks, which can be modelled by extending LTSs with Markovian information and computed using steady-state analysis [START_REF] Coste | Ten Years of Performance Evaluation for Concurrent Systems using CADP[END_REF].

A. LNT Types and Functions for the Scheduler Process

The following code block provides LNT specification of BPMN types and functions used in the scheduler process. It also shows how to check for the merge using BPMN 1.0 semantics. BPMN 2.0 merge semantics is simpler (which is not shown here) and it is checked in a similar manner.

module bpmntypes ( i d ) with " g e t " i s ( * s e t o f i d e n t i f i e r s * ) type IDS i s set of ID with "= =" , " !=" , " i n t e r " , " l e n g t h " , "empty" , "member" , " i n s e r t " , " union " , " remove " , " d i f f " end type

(

Figure 1 :

 1 Figure 1: Framework Overview.

Figure 2 :

 2 Figure 2: BPMN Notation (part of).

Figure 3 :

 3 Figure 3: Online Shopping Process in BPMN (element identifiers in italics).

Figure 4 :

 4 Figure 4: PIF Meta Model (abstract concepts are shown in grey).

Figure 5 :

 5 Figure 5: Scheduler Composition with PIF Elements (Sync denotes synchronization and INT denotes interleaving. F, G and T denote flows, gateways and tasks respectively).

Example.

  The translation of the online shopping process in LNT results type NODE i s i ( i n i t i a l : INITIAL ) , f ( f i n a l s : FINALS ) , g ( gateways : GATEWAYS ) , t ( t a s k s : TASKS ) end type type NODES i s set of NODE end type type BPROCESS i s p r o c ( name : ID , nodes : NODES, f l o w s : FLOWS ) end type process s c h e d u l e r [ . . . ] ( a c t i v e f l o w s : IDS , bpmn : BPROCESS, s y n c s t o r e : IDS , m e r g e s t o r e : IDS ) i s s e l e c t f l o w 3 7 b e g i n ( ? i d e n t 1 of ID ) ; s c h e d u l e r [ . . . ] ( union ( { i d e n t 1 } , r e m o v e i d s f r o m s e t ( { } , a c t i v e f l o w s ) ) , bpmn , s y n c s t o r e , m e r g e s t o r e ) [ ] f l o w 3 9 f i n i s h ( ? i d e n t 1 of ID ) ; s e l e c t f l o w 2 b e g i n ( ? i d e n t 2 of ID ) ; s c h e d u l e r [ . . . ] ( union ( { i d e n t 2 } , r e m o v e i d s f r o m s e t ( { i d e n t 1 } , a c t i v e f l o w s ) ) , bpmn , s y n c s t o r e , m e r g e s t o r e ) [ ] f l o w 3 b e g i n ( ? i d e n t 3 of ID ) ; s c h e d u l e r . . . end s e l e c t [ ] f l o w 3 0 f i n i s h ( ? i d e n t 1 of ID ) ; s c h e d u l e r [ . . . ] ( union ( { } , r e m o v e i d s f r o m s e t ( { i d e n t 1 } , a c t i v e f l o w s ) ) , bpmn , s y n c s t o r e , m e r g e s t o r e ) [ ] m e r g e i d := any ID where member ( mergeid , m e r g e s t o r e ) ; i f ( i s m e r g e p o s s i b l e (bpmn , a c t i v e f l o w s , m e r g e i d ) and i s s y n c d o n e (bpmn , a c t i v e f l o w s , s y n c s t o r e , m e r g e i d ) ) then MoveOn( ! m e r g e i d ) ; o u t f ( ? i d e n t 1 of ID ) ; s c h e d u l e r [ . . . ] ( union ( { i d e n t 1 } , r e m o v e i n c f (bpmn , a c t i v e f l o w s , m e r g e i d ) ) , bpmn , r e m o v e s y n c (bpmn , s y n c s t o r e , m e r g e i d ) , remove ( mergeid , m e r g e s t o r e ) ) e l s e s c h e d u l e r [ . . . ] ( a c t i v e f l o w s , bpmn , s y n c s t o r e , m e r g e s t o r e ) end i f end s e l e c t end process

Figure 6 :

 6 Figure 6: Excerpt of the LNT Scheduler Process for the Online Shopping Process.

  r s p l i t e x c l u s i v e g a t e w a y 1 [ f l o w 3 9 f i n i s h , f l o w 2 b e g i n , f l o w 3 b e g i n ] | | t a s k 1 1 [ f l o w 6 f i n i s h , c h o o s e I t e m s , f l o w 8 b e g i n ] | | . . . end par end par end par end hide end process

Figure 7 :

 7 Figure 7: Main LNT Process for the Online Shopping Process.

Figure 8 :

 8 Figure 8: LTS Formal Model for the Online Shopping Process.

Definition 1 .

 1 (Conservative Evolution) Let b and b be two processes, b b is a conservative evolution iff || Θ(b) || br ≡ || Θ(b ) ||.

A

  typical example is adding new paths, e.g., (a, b) (a, b, c), or evolving an existing one, e.g., (a, b) (a, (b, c)). So here, we ground on a preorder relation rather than on an equivalence one, ensuring that, given b b , all observable behaviours that were in b are still in b . For this we rely on the branching preorder, introduced in Section 4.1. Definition 2. (Inclusive Evolution) Let b and b be two processes, b b is an inclusive evolution iff || Θ(b) || br < || Θ(b ) ||. Similarly, one may refine a process by implementing only a part of it. Here, in b b , one does not want that b exposes any additional behaviour that is outside what is specified in b. This is a reversed form of inclusive evolution. Definition 3. (Exclusive Evolution) Let b and b be two processes, b b is an exclusive evolution iff || Θ(b ) || br < || Θ(b) ||.

Definition 4 .

 4 (Selective Conservative Evolution) Let b and b be two processes, and T be a set of tasks, b b is a selective conservative evolution with reference to T iff || Θ(b ) || [T ] br ≡ || Θ(b) || [T ].

  For example, b b is a conservative evolution up to a relabelling relation R for b and b iff || Θ(b) || R br ≡ || Θ(b ) ||.

Definition 5 .

 5 (Property-Aware Evolution) Let b and b be two processes, T be a set of tasks, and φ be a formula defined over T , b b is a propertyaware evolution with respect to φ iff || Θ(b) || |= φ ⇒ || Θ(b ) || |= φ.

m×

  I , where || Θ(b) || m × I || Θ(c) || denotes the LTS representing the communication on a set of interactions I between b and c. For synchronous communication, m

Figure 9 :

 9 Figure 9: Online Shopping Process in BPMN (v2).

Figure 10 :

 10 Figure 10: VBPMN Web Application in Use: Property Verification.

Figure 11 :

 11 Figure 11: VBPMN Web Application in Use: Model Comparison.

  checking conservative evolution of b b → in the tool: mode=conservative, options=none bcg open "b.bcg" bisimulator -equal -branching -diag "b'.bcg" checking inclusive evolution of b b → in the tool: mode=inclusive, options=none bcg open "b.bcg" bisimulator -smaller -branching -diag "b'.bcg" checking exclusive evolution of b b → in the tool: mode=exclusive, options=none bcg open "b.bcg" bisimulator -greater -branching -diag "b'.bcg" checking selective conservative evolution of b b wrt. a set of tasks T={t 1 , .

Figure 12 :

 12 Figure 12: SVL Patterns for the Verification of the Evolution Notions.

(

  * bpmn-p r o c * ) type BPROCESS i s p r o c ( name : ID , nodes : NODES, f l o w s : FLOWS ) end type ( * Check f o r merge w i t h BPMN 1 . x s e m a n t i c s * ) function i s m e r g e p o s s i b l e ( p : BPROCESS, a c t i v e f l o w s : IDS , m e r g e i d : ID ) : Bool i s var i n c f : IDS , i n a c t i v e i n c f : IDS , a c t i v e m e r g e : Nat , v i s i t e d : IDS , r e s u l t : Bool in v i s i t e d := n i l ; ( * j u s t i t e r a t e t h r o u g h g a t e w a y s * ) i n c f := f i n d i n c f ( p , m e r g e i d ) ; a c t i v e m e r g e := f i n d a c t i v e t o k e n s ( a c t i v e f l o w s , i n c f ) ; ( * --c h e c k i f a l l t h e i n c f have t o k e n s -- * ) i f ( a c t i v e m e r g e = = length ( i n c f ) ) then return True e l s e ( * f i r s t remove i n c f w i t h a c t i v e t o k e n s * ) i n a c t i v e i n c f := r e m o v e i d s f r o m s e t ( a c t i v e f l o w s , i n c f ) ; ( * t h e n c h e c k upstream f o r r e m a i n i n g f l o w s * ) eval r e s u l t := c h e c k a f u p s t r e a m ( ! ? v i s i t e d , p , a c t i v e f l o w s , i n a c t i v e i n c f ) ; return r e s u l t end i f end var end function function i s s y n c d o n e ( p : BPROCESS, a c t i v e f l o w s : IDS , s y n c s t o r e : IDS , m e r g e i d : ID ) : Bool i s var i n c f : IDS , a c t i v e s y n c : IDS in i n c f := f i n d i n c f ( p , m e r g e i d ) ; a c t i v e s y n c := i n t e r ( a c t i v e f l o w s , i n c f ) ; i f ( empty ( a c t i v e s y n c ) ) then return F a l s e e l s i f ( i n t e r ( a c t i v e s y n c , s y n c s t o r e ) = = a c t i v e s y n c ) then return True e l s e return F a l s e end i f end var end function ( * Merge c h e c k f o r p a r a l l e l g a t e w a y s * ) function i s m e r g e p o s s i b l e p a r ( p : BPROCESS, s y n c s t o r e : IDS , m e r g e i d : ID ) : Bool i s var i n c f : IDS , a c t i v e s y n c : IDS in i n c f := f i n d i n c f ( p , m e r g e i d ) ; i f ( i n t e r ( i n c f , s y n c s t o r e ) = = i n c f ) then return True e l s e return F a l s e end i f end var end function ( * f i n d s a l l t h e upstream f l o w s and c h e c k s f o r t o k e n s * ) function c h e c k a f u p s t r e a m ( in out v i s i t e d : IDS , p : BPROCESS, a c t i v e f l o w s : IDS , i n c f : IDS ) : Bool i s var count : Nat , r e s u l t : Bool , r e s u l t 2 : Bool in case i n c f in var hd : ID , t l : IDS , u p f l o w : IDS , s o u r c e : ID in c o n s ( hd , t l ) -> s o u r c e := f i n d f l o w s o u r c e ( p , hd ) ; i f ( s o u r c e = = DummyId) then return True e l s i f ( member ( s o u r c e , v i s i t e d ) ) then eval r e s u l t := c h e c k a f u p s t r e a m ( ! ? v i s i t e d , p , a c t i v e f l o w s , t l ) ; return r e s u l t e l s e v i s i t e d := i n s e r t ( s o u r c e , v i s i t e d ) ; u p f l o w := g e t i n c f b y i d ( p , s o u r c e ) ; i f ( u p f l o w = = n i l ) then return True end i f ; count := f i n d a c t i v e t o k e n s ( a c t i v e f l o w s , u p f l o w ) ; i f ( count = = 0 of Nat ) then eval r e s u l t := c h e c k a f u p s t r e a m ( ! ? v i s i t e d , p , a c t i v e f l o w s , u p f l o w ) ; eval r e s u l t 2 := c h e c k a f u p s t r e a m ( ! ? v i s i t e d , p , a c t i v e f l o w s , t l ) ; return r e s u l t and r e s u l t 2 e l s e return F a l s e end i f end i f | n i l -> return True

Table 1 :

 1 Analysis of the BPMN elements found in the BIT process library, release 2009.

	category element	occurences present in files
	flow	sequence flow	35.082	825/825
	gateway parallel gateway	11.175	715/825
	task	task	7.759	825/825
	event	end event	3.533	825/825
	event	start event	3.027	825/825
	gateway exclusive gateway	1.956	478/825
	structure sub-process	883	58/825
	structure definitions	825	825/825
	structure process	825	825/825
	gateway inclusive gateway	135	47/825

ple incoming branches, and it is called a merge (gateway).

Table 2 :

 2 Mapping from BPMN to PIF.

	BPMN	PIF
	Start event	InitialEvent	BPMN gateway PIF gateway
	End event	EndEvent	Parallel split	AndSplit
	Tasks (several)	Task	Parallel merge	AndJoin
	Sequence flow	SequenceFlow	Exclusive split	XorSplit
	sourceRef (Seq flow)	source	Exclusive merge	XorJoin
	targetRef (Seq flow)	target	Inclusive split	OrSplit
	sourceRef (Flow node) incomingFlows	Inclusive merge	OrJoin
	targetRef (Flow node) outgoingFlows

Table 4 :

 4 Encoding PIF into LNT (part of, continued below).

	PIF Construct	BPMN Notation	LNT Encoding
	InitialEvent		begin ; outf
	EndEvent		incf ; finish
	SequenceFlow		loop begin ; finish end loop
	Task		loop incf ; task ; outf end loop
			loop incf ;
	AndSplit		par outf1 || outf2 || outf3
			end par end loop
			loop par
	AndJoin		incf1 || incf2 || incf3 end par ;
			outf end loop
	XorSplit

Table 5 :

 5 Encoding PIF into LNT (balanced Or gateways).

	PIF Gateway	BPMN Notation	LNT Encoding
		loop incf ;
		select (*s i if one matching merge*)
	OrSplit	outf1 ; s1 [] outf2 ; s2
		[] par outf1 || outf2 end par ; s3
		end select end loop
		loop select (* s i if one matching split *)
		s1 ; incf1
	OrJoin	[] s2 ; incf2
		[] s3 ; par incf1 || incf2 end par
		end select ; outf end loop

Table 6 :

 6 Encoding PIF into LNT (unbalanced Or gateways).

	PIF Gateway	BPMN Notation	LNT Encoding
		loop incf (?ident of ID) ;
		select (* s i if one matching merge *)
		s1 ; outf1 (?ident of ID)
	OrSplit	[] s2 ; outf2 (?ident of ID) [] s3 ; par outf1 (?id1 of ID)
			|| outf2 (?id2 of ID)
			end par
		end select end loop
		mergestatus := False ;
		while mergestatus == False loop
		select
		incf1 (?ident of ID)
	OrJoin	[] incf2 (?ident of ID)
		[] MoveOn(!mergeid) ;
		mergestatus := True
		end select
		end loop ; outf (?ident of ID)

Table 7 :

 7 Experimental Results.

	BPMN			Characteristics			LTS (states/transitions)		Evol.
	Proc.	Tasks Flows		Gateways	B L	Raw	Minimized	≡ < >
	1 1'	6 7	11 15		2	2 + 2	√ √	× ×	29/29 78/118	8/9 11/14	×	√ 15s	×
	2 2'	4 8	7 14			1 2		√ √	× ×	70/105 36/38	7/9 10/12	√ √ √ 15s
	3 3'	7 8	14 16		2	+ 2 4	√ √	× ×	62/87 1,786/5,346	10/11 28/56	× × × 15s
	4 4'	15 16	29 33	3 5	+ 2 + 2	+ 2 + 2	× × × √	469/1,002 479/1,013	24/34 26/37	×	√ 15s	×
	5 5'	12 12	32 33	7 7	+ 2 + 2	+ 2 + 2	√ √ √ √	3,038/9,785 3,039/9,787	32/63 32/64	×	√ 16s	×
	6 6'	22 23	46 52	10	10 + 4 + 4 + 2	√ √ √ √	179/248 570/1,295	32/41 38/57	×	√ 16s	×
	7 7'	12 12	24 24		4	6 + 2	√ √	× ×	742,234/3,937,158 6,394/21,762	148/574 60/152	× × 31s	√
	8 8'	22 22	41 44	8	8 + 2 + 2 + 2	× ×	√ √	1,818/2,236 1,889/2,327	149/210 158/223	×	√ 1m13s	×
	9	12	26	4	+ 2	+ 2	× ×	11,990/17,949	289/453	× ×	√
	9'	8	20		4	+ 2	× ×	1,003/1,274	53/77		1m2s
	10	192	210		12		+ 6	× ×	791/988	201/218	×	√	×
	10'	193	214		14		+ 6	× ×	799/997	203/221		2m48s
	11 11'	20 20	43 39		6	+ 6 8	√ √	× 4,488,843/26,533,828 × 4,504,775/26,586,197	347/1,450 348/1,481	×	√ 9m31s	×
	12 12'	16 18	34 40	3 5	+ 6 + 6	+ 2 + 2	× × × √	797,335/1,549,764 867,055/1,659,930	1,498/2,537 × 2,007/3,374 22m15s √ ×

  * f l o w * ) type FLOW i s f l o w ( i d e n t : ID , s o u r c e : ID , t a r g e t : ID ) end type ( * s e t o f f l o w s * )

	( * gateway p a t t e r n * )
	type GPATTERN i s
	s p l i t , merge
	end type
	( * gateway * )
	type GATEWAY i s
	gateway ( i d e n t : ID , p a t t e r n : GPATTERN, s o r t : GSORT, i n c f : IDS , o u t f : IDS )
	end type
	( * s e t o f g a t e w a y s * )
	type GATEWAYS i s
	set of GATEWAY
	end type
	( * node * )
	type NODE i s
	i ( i n i t i a l : INITIAL ) ,
	f ( f i n a l s : FINALS ) ,
	g ( gateways : GATEWAYS ) ,
	t ( t a s k s : TASKS )
	end type
	type FLOWS i s ( * s e t o f nodes * )
	set of FLOW type NODES i s
	end type set of NODE
	end type
	( * t a s k * )
	type TASK i s
	t a s k ( i d e n t : ID , i n c f : IDS , o u t f : IDS )
	end type
	( * s e t o f t a s k s * )
	type TASKS i s
	set of TASK
	end type
	( * i n i t i a l e v e n t * )
	type INITIAL i s
	i n i t i a l ( i d e n t : ID , o u t f : ID )
	end type
	( * f i n a l e v e n t * )
	type FINAL i s
	f i n a l ( i d e n t : ID , i n c f : IDS )
	end type
	( * s e t o f f i n a l e v e n t s * )
	type FINALS i s
	set of FINAL
	end type
	( * t y p e o f gateway * )
	type GSORT i s
	xor , and , or
	end type

One may find a correspondence at http://www.workflowpatterns.com/ evaluations/standard/ between abstract workflow concepts and their counter-

The symbol is overloaded since a refinement rule is an evolution at the task level.

The table shows a √ if there are no inclusive gateways or if there are balanced inclusive gateways, and a × if there are unbalanced inclusive gateways

Indeed (a quite old) one of these ontologies is named PIF[START_REF] Lee | the PIF Working Group, The PIF process interchange format and framework[END_REF]. We were not aware of it when we began working on (our) PIF.