Sara Houhou
email: sara.houhou@lip6.fr

Souheib Baarir
email: souheib.baarir@lip6.fr

Pascal Poizat
email: pascal.poizat@lip6.fr

Philippe Quéinnec
email: philippe.queinnec@irit.fr

Laïd Kahloud

Laid Kahloul
email: l.kahloul@univ-biskra.dz

A First-Order Logic Verification Framework for Communication-Parametric and Time-Aware BPMN Collaborations

Keywords: BPMN, Formal Semantics, Collaboration, Communication, Time, Verification, First-Order Logic, TLA +, Tool

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

BPMN supports the modelling of the internal processes of organizations and of the way they interact to reach objectives. This modelling can be achieved through the use of process and collaboration diagrams. In the standard [START_REF] Kahloul | Business Process Modeling Notation[END_REF], natural language is used to describe the BPMN execution semantics. This leaves room for interpretation and hampers the formal analyses that would be desirable in order to find defaults at design time rather than when running the processes and collaborations over business process engines. This issue has been addressed in the last decade in different proposals for a formalization of the BPMN execution semantics (see Section 7), some of them being supported with tools. However, these proposals often leave apart features related to communication and time. Meanwhile, BPMN is gaining interest as a modeling language in new areas, such as the Internet of Things (IoT) [START_REF] Casati | Towards business processes orchestrating the physical enterprise with wireless sensor networks[END_REF][START_REF] Meyer | The things of the Internet of Things in BPMN[END_REF]. There, taking into consideration the communication between the nodes of the system, the configuration of different communication modes, and time constraints such as durations and timeouts is a requirement.

Diving into BPMN.

Let us now briefly introduce BPMN before presenting a motivating example in the next part. BPMN (Business Process Model and Notation) is a workflow based notation. It defines a set of element notations (see Fig. 2 for the part of them that we support). These elements can be classified into two types: flow objects (nodes), and connection objects (edges). In BPMN, nodes fall into four categories: events, activities, gateways, and data objects (not supported here). The events denote things that happen while a process is running. They affect the process flow and usually have a trigger or a result. Events may indicate the starting point of a process, identified using a start event or an ending point of a process, identified using an end event. BPMN also defines intermediate events which occur between start and end events. These events affect the process flow in the sense that they must occur for the process to go on. There are different types of intermediate events. In this work we focus on message-related and time-related ones. An intermediate event can be attached to the boundary of an activity, and is then called a boundary event. This is used to interrupt the activity or to launch activities in parallel, based on some condition (e.g., a message reception or the deadline of a timeout). An activity is a unit of work that can be either an atomic task or a compound sub-process. Gateways are used to control the process flow and in particular the activity execution ordering. There are five main types of gateways in BPMN and we are taking into account the main ones [START_REF] Krishna | Checking business process evolution[END_REF]. The exclusive type (XOR in Fig. 2) 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 behaviors. The parallel type (AND in Fig. 2) synchronizes concurrent flows for all its incoming branches and creates concurrent flows for all its outgoing branches. The inclusive type (OR in Fig. 2) states that any number of branches among its incoming or outgoing branches may be taken 1 . These three types of gateways can be merging, splitting, or mixed (both merging and splitting). We support all three cases. Finally, with the event-based gateway (EB in Fig. 2), the process flow is based on which of the events (or message reception tasks) that follow the gateway occurs first. Nodes are connected with edges that can be sequence flows (flows of control), or message flows (flows for message exchange). The sequence flow category can in turn be decomposed into normal sequence flows, conditional sequence flows (expressing the condition for some branch to be activated), and default sequence flows (the default branch to activate if all others, conditional ones, cannot be). BPMN defines three main kinds of models: process diagrams, collaboration diagrams, and choreography diagrams. In this work, we deal with the first two. A process diagram is used to model the activities of a single organization. Collaboration diagrams can be defined with a set of different processes (for different organizations), exchanging messages and cooperating to reach a shared objective. In our work, we abstract away from data (data objects, data stores and message payloads). Therefore, in the sequel, message (resp. event instance) and message type (resp. event type) are used interchangeably. For more information BPMN, see [START_REF] Kahloul | Business Process Modeling Notation[END_REF].

Case study. Let us observe the collaboration model in Figure 1. It involves two participants: a customer and a travel agency. The agency sends offers to the client (loop with an exclusive gateway) in a first sub-process, and, after some time (time boundary event), begins a second sub-process to exchange information (booking, payment, confirmation, ticket) with the customer. The customer may reject some of the offers, and at some point he/she may agree on one (loop using two exclusive gateways). If so, he/she stops accepting offers and he/she sends booking and payment information to the agency and gets the corresponding ticket and confirmation. The agency and the customer rely on interrupting features to deal with the fact that the customer stops accepting offers as soon as he/she has agreed on one, while, as said before, the agency sends offers for some amount of time only. If the customer has not agreed on an offer before the end of this amount of time, the sending of offers by the agency will stop (timer boundary event on the first agency sub-process). The agency will send an interrupting message to the client (message boundary event on the customer offer reception task) which will in turn interrupt the exchange sub-process (message boundary event on the second agency sub-process). If the customer has agreed on an offer before the end of the amount of time, he/she will begin to send information to the agency. The agency will timeout, send an interrupting message to the client (that will not be used), and enter the sub-process which will, this time, not be interrupted.

As one can see, the interplay between communication, interrupting features, and time makes the overall behavior of the collaboration difficult to grasp. Will the collaboration always reach one of its ends? Either that the client and the agency have agreed on an offer (them ending in Transaction Completed and Offer Completed, respectively) or that they have not but they are not waiting for some event to happen (them ending in Transaction Aborted and Offer Aborted, respectively). Will the collaboration reach one of its ends but with pending messages, that have been sent but neither received nor treated? Or, worse, will the collaboration deadlock at some point depending on the choices made by the customer and the agency, and the passage of time?

This corresponds indeed to checking soundness properties (to be further introduced in Sect. 4). One may note the different order in the customer and in the agency for the reception (resp. sending) of the confirmation and of the ticket. As we will see later on (in Section 4), the communication model used between the agency and the customer has an impact on this. With the verification framework we propose, the process designer will be able to check that the collaboration at hand cannot be ensured to be completely sound: for some executions there may be messages left untreated. But the process designer will also be able to check that, given the right choice of communication model (we analyse collaborations for seven possible communication models presented in Sect. 2.2.4), the collaboration is sound if the message treatment constraint is relaxed. The process designer will also see that for some communication models the collaboration even deadlocks, with the client not being able to reach one of its final events. Playing with our counter-example example animator (see Fig. 4) he/she will be able to correct the model. Here this means either changing the chosen communication model or changing the order in which the client or the agency exchanges information.

This case study is just one example of models that can be analyzed using our proposal. The analysis of other examples, including ones from the literature, is presented in Section 5, and models from our example repository are available at [START_REF] Poizat | fbpmn repository[END_REF] under /models.

Contribution. The contribution of this paper is twofold. First, (1.) we provide a formalization of a subset of BPMN execution semantics that supports sub-processes, communication, and time constructs, and is parametric with reference to the properties of the communication. Second, (2.) we support this formalization with tools that automatically perform the verification of correctness properties for BPMN collaboration models, and that animate counter examples when the properties are not satisfied.

As far as (1.) is concerned, we have chosen to define a direct logic semantics for BPMN. We use First-Order Logic (FOL) with natural numbers, sets, and maps. Instead of using an intermediary formal model, e.g., Petri nets or process algebra, this choice of a simple yet expressive framework enables one to get a formal semantics that is amenable to implementation in different formal frameworks while still being close to the semiformal semantics of the standard (hence it can be related to it). Furthermore, with reference to Petri net token based semantics, e.g., [START_REF] Dijkman | Semantics and analysis of business process models in BPMN[END_REF][START_REF] Dechsupa | Transformation of the BPMN design model into a colored Petri net using the partitioning approach[END_REF] as shown in Table 6, our choice to rely on FOL enables us to directly support a non-local semantics for inclusive (OR) gateways, sub-process interruption, and a choice of several communication models. We implement our FOL semantics in TLA + [START_REF] Lamport | Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers[END_REF] as a set of TLA + theories. This corresponds to a pure syntactic transformation of FOL into the corresponding TLA + fragment, as demonstrated in Table 2.

Our semantics supports the seven point-to-point communication models that exist when considering local, causal and global message ordering, and it is easily extensible. As far as the subset of BPMN is concerned, we have first based our choice on the 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], given in [START_REF] Krishna | Checking business process evolution[END_REF]. We have then taken more constructs into account, mainly relative to our focus: creation and termination of processes based on messages or time, message and timerelated intermediary events and boundary events (interrupting or non-interrupting), and event-based gateways. The subset of the notation that we support is given in Figure 2.

With respect to (2.), our approach relies on two steps. First, one uses the fbpmn tool that we have developed to get a TLA + representation of the model to verify. Then, one uses the TLC model checker from the TLA + tool-suite to perform the verification.

The properties of interest are encoded in the TLA + theories we have implemented. They include usual correctness properties for workflows as well as ones (proposed more recently [START_REF] Corradini | A classification of BPMN collaborations based on safeness and soundness notions[END_REF]) that are more specific to BPMN. Termination of verification for some of the properties (see Sect. 5.5) is ensured only for BPMN models with a finite state semantic model. If it is not the case, one can use constraints (see Sect. 6.4.1) to perform verification on a subset of the semantic model.

Both our fbpmn tool and the TLC tool are open source and freely available online.

Furthermore, the models we have used for evaluation in Section 5 are also available online. To get the tools and the models, please see the fbpmn repository [START_REF] Poizat | fbpmn repository[END_REF].

This work is based on the paper "A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations" [START_REF] Houhou | A First-Order Logic semantics for communicationparametric BPMN collaborations[END_REF], extended as follows:

1. We have enriched the subset of BPMN taken into account and the formalization of its execution semantics into first-order logic to support time-related events and (message and time) boundary events, either interrupting or non-interrupting. We propose two different semantics for time and compare their benefits. 2. We have extended the six possible communication models to be used as parameters in the verification of a collaboration with a new one, relative to the causality of message emission. Furthermore, on top of these now seven generic communication models that are applied on a collaboration as a whole, we now support the definition and the use of ad-hoc communication models (a specific model built by assembling micro communication models that provide different constraints on sending and receiving messages).

3. Accordingly, we have extended our verification tool, fbpmn, to support these new elements and communication models. We have also extended fbpmn into a more comprehensive tool suite with a counter-example animator and a containerized Web application where process designers can model and verify BPMN processes or collaborations directly from the browser. This tool suite is now presented, including with reference to its extension as far as verification constraints, new properties, and new communication models are concerned. 4. The presentation is enriched with well-formedness rules, greater details on the semantics rules, the formalization in first-order logic of the communication models and of the properties that are verified, the presentation of the use of fairness for verification in presence of loops and alternatives, and an extended state of the art. 5. We discuss the relation between the FOL semantics and its TLA + implementation. 6. We have a new and more complex and realistic case study, with the new BPMN constructs taken into account.

Overview. The formal part of the paper is developed in Section 2, with Sections 2.1 and 2.2, respectively addressing the presentation of the model underlying the semantics, and then the semantics itself, including seven possible communication models. Section 3 is devoted to taking into account time, with two possible semantics, either nondeterministic abstraction of time or based on explicit time, presented respectively in Sections 3.2 and 3.3. The properties of interest for the process designer are presented in Section 4. The implementation of the semantics in TLA + , verification, and evaluation are presented in Section 5. This section also includes a short introduction to the TLA + language and verification framework, and a discussion on the use of fairness to deal with loops and alternatives in models. Section 6 is devoted to our tool suite, fbpmn, its architecture, general principles, and the way it can be easily extended. Related work is discussed in Section 7, and we end with conclusions and perspectives in Section 8.

Formal Semantics

In this section, we first present the model on which we base the definition of the communication-parametric semantics for BPMN collaborations. This model is used to represent collaborations as typed graphs. In a second step, we present the semantics itself. It follows the "token game" of the standard [1, Ch. 13], with a notion of state that evolves with activation and completion of graph nodes.

A Typed Graph Representation of BPMN Collaborations

In our work, a BPMN model is seen as a typed graph (Def. 2.1), where types corresponding to the BPMN syntax (see Fig. 2) are associated to nodes and edges.

• For Nodes:

-The task type (T ) groups the abstract task (AT ), the receive task (RT ), and the send task (ST ) types. Formally: T = {AT, RT, ST}. -The activity type (A) groups the task and the sub-process (SP ) types. Formally: A = T ∪ {SP}.

-The gateway type (G) groups the parallel (AND), the inclusive (OR), the exclusive (XOR), and the event-based (EB ) gateway types. Formally: G = {AND, OR, XOR, EB}. -The event type (E ) is the set of all event types. Formally:

E = SE ∪ IE ∪ BE ∪ EE.
• For Edges:

-The sequence flow type (SF ) groups the normal sequence flow (NSF ), the conditional sequence flow (CSF ), and the default sequence flow (DSF ) types.

Formally: SF = {NSF, CSF, DSF}. -The message flow type (MF ), is used to denote message flows.

T N odes denotes the set of all node types, with an added type, P, to denote processes. Formally: T N odes = A ∪ G ∪ E ∪ {P}. T Edges denotes the set of all edge types. Formally: T Edges = SF ∪ {MF}. The hierarchical structure of collaborations, with processes P and sub-processes SP is dealt with by using specific types for nodes, and a relation,R, denoting containment. From our example, Figure 1, we would then have two nodes of type P (say n 1 for Customer, n 2 for Travel Agency), two nodes of type SP (say n 3 for Offer SP, n 4 for Exchange SP), n 3 ∈ R(n 2 ), n 4 ∈ R(n 2 ), and n 5 ∈ R(n 3 ) with n 5 being the node of type ST for Make Travel Offer.

Notation (Restriction to types). Given a set of types T , a set X that whose elements can be typed using a function cat X : X → T , and a subset T of T , we note X T = {x ∈ X | cat X (x) ∈ T }. By abuse of notation, we may write X t , for some t in T , instead of X {t} . In the sequel, we are mainly interested into two sets that are typed, N (nodes) typed using T N odes , and E (edges) typed using T Edges . Accordingly, we will use N T (resp. E T ) to denote the subset of nodes (resp. edges) of type T .

Definition 2.1 (BPMN Graph). A BPMN graph is a tuple

G = ( N , E , M, cat N , cat E , source, target, R, msg, attachedTo, isInterrupt) where: • N , is the set of nodes, • E (N ∩ E = ∅), is the set of edges,
• M, is the set of message types,

• cat N : N → T N odes , gives the type of a node,

• cat E : E → T Edges , gives the type of an edge,

• source/target : E → N , give the source/target of an edge,

• R : N {P,SP} → 2 N ∪E , gives the set of nodes and edges which are directly contained in a container (process or sub-process),

• msg : E MF → M gives the message associated to a message flow,

• attachedTo : N BE → N A , gives the activity to which a boundary event node is attached,

• isInterrupt : N BE → Bool, denotes whether a boundary event node is interrupting or not, Notation. We note R + the transitive closure of R.

Auxiliary functions. For a graph G = ( N , E , M, cat N , cat E , source, target, R, msg t , attachedTo, we define the following auxiliary functions:

• in/out : N → 2 E give the incoming/outgoing edges of a node:

in(n) = {e ∈ E | target(e) = n} out(n) = {e ∈ E | source(e) = n}
• a family of functions in T (resp. out T ) : N → 2 E is used to get incoming/outgoing edges of a selected type T , in

T (n) = in(n) ∩ E T and out T (n) = out(n) ∩ E T .
• procOf : N → N P gives the container process of a given node, procOf(n

) = p if and only if n ∈ R + (p).
It is desirable to enforce that models respect some well-formedness rules before performing verification. We therefore define well-formed BPMN graphs using well-formed condition rules.

Well-formed BPMN graph. A well-formed BPMN graph satisfies the following conditions. These rules are extracted from the standard [START_REF] Kahloul | Business Process Modeling Notation[END_REF]:

• (C1) No incoming sequence flow edges for start events: ∀n ∈ N SE , in SF (n) = ∅

• (C2) No outgoing sequence flow edges for end events: ∀n ∈ N EE , out SF (n) = ∅

• (C3) A sub-process contains exactly one None Start Event and no other start event types:

∀n ∈ N SP , |R(n) ∩ N NSE | = 1 ∧ R(n) ∩ N {MSE,TSE} = ∅
• (C4) A sub-process node cannot contain a process node: ∀n ∈ N SP , R(n)∩N P = ∅

• (C5) For each process node, we require that:

it contains at least one initial node:

∀n ∈ N P , R(n) ∩ N SE = ∅;
it contains at least one end node: ∀n ∈ N P , R(n) ∩ N EE = ∅.

• (C6) No looping edges: ∀e ∈ E, source(e) = target(e)

• (C7) No node isolation: ∀n / ∈ N P =⇒ in(n) = ∅ ∨ out(n) = ∅
• (C8) A gateway that has a conditional edge must have a unique default edge: ∀e ∈ E MF , procOf(source(e)) = procOf(target(e))

∀n ∈ N {AND,XOR} , out CSF (n) = ∅ =⇒ |out DSF (n)| = 1
• (C12) An event-based gateway must have two or more outgoing edges:

∀n ∈ N EB , |out SF (n)| ≥ 2
• (C13) Parallel and event-based gateways cannot have an outgoing edge of conditional sequence flow type: ∀n ∈ N {AND,EB} , (out

SF (n) ∩ E CSF = ∅)
• (C14) Elements that follow an event-based gateway can only be catching intermediate message events, receive tasks, or timer intermediate catch events. Additionally, one cannot have both receive tasks and intermediate message events (see for example Fig. 31):

∀n ∈ N EB (∀e ∈ out SF (n), target(e) ∈ N {CMIE,RT,TICE} ) ∧ ({e ∈ out SF (n) | target(e) ∈ N RT } = ∅) ∨ ({e ∈ out SF (n) | target(e) ∈ N CMIE } = ∅)
• (C15) The outgoing edges of an inclusive or an exclusive gateway must be a combination between default sequence flows and conditional sequence flows, or all are of the normal sequence flow type: It should be noted that, but for these rules, we do not require a specific structure of the BPMN graph. For example, we do not require these graphs to be well-balanced (when for each splitting gateway of a given type, there is a corresponding merging gateway of the same type). One can use a splitting exclusive gateway and merge its branches using a parallel gateway. Verification will be able to detect this is a erroneous model.

∀n ∈ N {XOR,

A FOL Semantics for BPMN Collaborations

In order to maintain traceability with the standard, we use a token-based approach to define the semantics. The movement of tokens is based on node types and on two predicates, starting predicate St and completing predicate Ct defined for each node type. These predicates correspond to the enabling of the node to start its execution, and the enabling of the node to complete its execution, respectively. Some nodes only have a start transition (e.g., end events), and others only have a completion transition (e.g., gateways). When a node defines only one of the two predicates, the other one is considered to be false. The semantics (Sect. 2.2.3) relies on a notion of state of the BPMN graph (Sect. 2.2.1) to define the St and Ct predicates. Further, the semantics is parameterized by a type T net that encapsulates the properties of the communication network using an initialization function, initnet, and two predicates, send and receive (see Sect. 2.2.2 for the abstract definition and Sect. 2.2.4 for realizations of T net corresponding to seven communication models).

State

A state of a BPMN graph gives a marking for the nodes and the edges, together with a state of the communication network. Definition 2.2 (State). The state of a BPMN graph is a tuple s = (mn, me, mnet) such that:

• mn : N → N, is a function assigning a natural number marking to each node.

• me : E → N, is a function assigning a natural number marking to each edge.

• mnet : T net , is the state of the communication network.

The set of all states of a BPMN graph is denoted by States. Definition 2.3 (Initial state). The initial state of a BPMN graph, denoted by s o = (mn 0 , me 0 , mnet 0 ), is such that:

• the start nodes of the processes hold a token, all other nodes are unmarked:

∀n ∈ N, mn 0 (n) = 1 if ∃p ∈ N P , n ∈ N SE ∩ R(p) 0 otherwise.
• all edges are unmarked: ∀e ∈ E, me 0 (e) = 0

• the network is empty:

mnet 0 = initnet 2.2.2

. Communication

The properties of communication between two participants (process nodes) for a given type of message are abstracted with an initialization function, initnet, and two transition predicates, send and receive. initnet is used to give the initial state of mnet. send and receive specify when a communication action is enabled and what effect it has on mnet. The value of mnet describes the state of the network in terms of what messages are sent

but not yet received, as the network evolves through time. In essence we are modeling the pool of messages that have been sent but not yet received, possibly using a single universal queue, or by using channel-by-channel queues, or some other structures that carry information to allow and order send and receive events.

Several communication models are formally described in Section 2.

Semantics

We define here the execution semantics of BPMN based on the above-mentioned St and Ct predicates, for each type of node in the BPMN graph, and based on its notion of state. The presentation of time-related constructs is deferred to Section 3 where we present two different semantics for time. In the semantics, let s = (mn, me, mnet) and s = (mn , me , mnet ) denote two states. Additionally, we consider the predicate that denotes marking equality but for nodes and edges given as parameter. Hence, (X) means "nothing changes except for X":

(X) def ≡ ∀n ∈ N \ X, mn (n) = mn(n) ∧ ∀e ∈ E \ X, me (e) = me(e)
Similarly, Ξ denotes that the state of the network does not change:

Ξ def ≡ mnet = mnet.
Start nodes. There are two starting node types for the instantiation of the process: the none start event (NSE ), and the message start event (MSE ).

The behavior of an NSE is defined only by a completing predicate. It consumes its token and generates one token on all of its outgoing sequence flow edges. If it is the initial node of a process p, it activates p by generating a token on it. When an NSE is defined within a sub-process p, its activation is conditioned by the activation of p. Formally.

∀n ∈ N NSE , Ct(n) def ≡ (mn(n) = 1) ∧ (mn (n) = mn(n) -1)
∧ ∀e ∈ out SF (n), (me (e) = me(e) + 1) 3 presents a process p with a none start event (nse), an abstract task (task), and a none end event (nee). It shows that there is a token within nse node which is represented by a green token. nse completes by consuming this token and produces one on P and its outgoing sequence flow (e1). The behavior of a message start event (MSE ) is defined by a completing predicate. An MSE is enabled if it has a token and there is a message offer on one of its incoming sequence flow edges. It completes by consuming the message, generating one token on all of its outgoing sequence flow edges, and activating the process p by generating a token on it. Formally.

∧   (∃p ∈ N P , (n ∈ R(p)) ∧ (mn(p) = 0) ∧ (mn (p) = 1) ∧ ({n, p} ∪ out SF (n)) ∧ Ξ) ∨ (∃p ∈ N SP , (n ∈ R(p)) ∧ ({n} ∪ out SF (n)) ∧ Ξ)   Example. Figure
∀n ∈ N MSE , Ct(n) def ≡ (mn(n) = 1) ∧ (mn (n) = mn(n) -1)
∧ ∀e ∈ out SF (n), (me (e) = me(e) + 1) ∧ ∃em ∈ in MF (n), (me(em) ≥ 1) ∧ (me (em) = me(em) -1) ∧ receive(procOf(source(em)), procOf(n), msg(em))

∧ ∃p ∈ N P , n ∈ R(p) ∧ (mn(p) = 0) ∧ (mn (p) = 1) ∧ ({n, p, em} ∪ out SF (n))
Example. Consider again the example of Figure 3. By modifying the none start event to a message start event (mse), we get the model in Figure 4. It represents the complete execution semantics behavior. The left hand-side of Figure 4 shows that there is a token on the start node and a message offer (m1) on the incoming message flow edge of mse. This latter completes by consuming the message according to the chosen communication model, and producing a token on the process and on all its outgoing edges. Ending nodes. We have three ending node types for the termination of a process: none end event (NEE ), terminate end event (EE ), and message end event (MEE ).

The behavior of a none end event (NEE ) node is defined only by a starting predicate: it is enabled if it has at least one token on one of its incoming edges. It starts by consuming this token and adding one to itself. Formally. A terminate end event (TEE ) node is defined only by a starting predicate: it is enabled if it has at least one token on one of its incoming edges. It behaves like a none end event by consuming a token from one of its incoming sequence flows and generates a token on itself. Besides, it does the additional work of dropping down all the remaining tokens of the process or sub-processes to which it belongs. Formally.

∀n ∈ N NEE , St(n) def ≡ ∃e ∈ in SF (n), (me(e) ≥ 1) ∧ (me (e) = me(e) -1) ∧ (mn (n) = mn(n) + 1) ∧ ({n, e}) ∧ Xi Example.
∀n ∈ N TEE , St(n) def ≡ ∃e ∈ in SF (n), (me(e) ≥ 1) ∧ (mn (n) = 1) ∧ ∃p ∈ N {P,SP } , (n ∈ R(p)) ∧ ∀nn ∈ ((R + (p) ∩ N ) \ {n}), (mn (nn) = 0) ∧ ∀ee ∈ (R + (p) ∩ E), (me (ee) = 0) ∧ (R + (p)) ∧ Ξ
Example. The left-hand side of Figure 6 shows the enabling of a terminate end node (tee) by the presence of a token on its incoming edge (e7). The right-hand side of the figure shows the starting execution of the node. It consumes the token from e7 and generates a token on itself. Besides, it affects all the existing executions in parallel (here e3 and e4) by dropping down all their tokens. A message end event (MEE ) is defined only by a starting predicate. It is enabled to start if it has a token on one of its incoming edges. It starts by moving the token from one of its incoming edges to itself, and sending a message on the network according to the communication model. Formally.

∀n ∈ N MEE , St(n) def ≡ ∃e ∈ in SF (n), (me(e) ≥ 1) ∧ (me (e) = me(e) -1) ∧ (mn (n) = mn(n) + 1) ∧ ∃ee ∈ out MF (n), (me (ee) = me(ee) + 1) ∧ send (procOf(n), procOf(target(ee)), msg(ee)) ∧ ({n, e, ee})
Example. Figure 7 shows the starting behavior of the message end event (mee). It starts by consuming the token from the incoming edge (e2), producing a token on itself, and sending a message m1 on the network. Activity nodes. Two kinds of activity nodes have to be taken into account: the abstract tasks (AT ), and the sub-processes (SP ). The behavior of an abstract task node (AT ) is defined by a starting and a completing predicate. An AT starts if at least one token is present on one of its incoming edges and it does not already own a token. It consumes a token from one of its incoming edges, and produces one on itself. An AT node is completed by consuming one token from itself, and adding one token on each of its outgoing edges. Note that an abstract task may be ended by an interrupting boundary event (see MBE and TBE in pages 20 and 31). Formally.

∀n ∈ N AT , St(n) def ≡ ∃e ∈ in SF (n), (me(e) ≥ 1) ∧ (me (e) = me(e) -1) ∧ (mn(n) = 0) ∧ (mn (n) = mn(n) + 1) ∧ ({n, e}) ∧ Ξ ∀n ∈ N AT , Ct(n) def ≡ (mn(n) = 1) ∧ (mn (n) = mn(n) -1) ∧ ∀e ∈ out SF (n), (me (e) = me(e) + 1) ∧ ({n} ∪ out SF (n)) ∧ Ξ
Example. Figure 8 shows the starting behavior of the abstract task task. It starts by consuming the token from e1 and generating a token on itself. The behavior of a sub-process activity SP node extends the one of an AT node with some additional conditions: when it is enabled, a sub-process adds a token to the start event it contains. It completes when at least one end event it contains has some tokens and none of its edges or non end event nodes are still active (i.e., owning a token). Note that, alike an abstract task, a sub-process may also be ended by an interrupting boundary event (see MBE and TBE in pages 20 and 31). Formally. 10 shows the starting behavior of the sub-process activity (SP ). It starts by consuming a token from its incoming edge (e1) and generating a token on itself 390 and on its start event (nse1). Figure 11 shows that even if there is a token on one of the end events, here nee3, the sub-process can not execute its completing transition: to complete, SP must wait until the token on e5 has given place to one on nee1. Communication. The semantics for MSE and MEE have been presented above. The remaining communicating elements, TMIE, CMIE, MBE, ST and RT require additional conditions for starting and completing due to the presence of sending/reception predicates. All these elements require a token on one of their incoming edges to be enabled.

∀n ∈ N SP , St(n) def ≡ ∃e ∈ in SF (n), (me(e) ≥ 1) ∧ (me (e) = me(e) -1) ∧ (mn(n) = 0) ∧ (mn (n) = mn(n) + 1) ∧ ∀ns ∈ (N NSE ∩ R(n)), (mn (ns) = mn(ns) + 1) ∧ ({e, n} ∪ (N NSE ∩ R(n))) ∧ Ξ ∀n ∈ N SP , Ct(n) def ≡ (mn(n) = 1) ∧ (mn (n) = mn(n) -1) ∧ ∀e ∈ R(n) ∩ E, (me(e) = 0) ∧ ∃n ee ∈ (N EE ∩ R(n)), (mn(n ee ) ≥ 1) ∧ ∀nn ∈ R(n) ∩ N, (mn(nn) ≥ 1 ⇒ nn ∈ N EE ) ∧ ∀nn ∈ (R(n) ∩ N EE ), (mn (nn) = 0) ∧ ∀e ∈ out SF (n), (me (e) = me(e) + 1) ∧ ({n} ∪ (R(n) ∩ N EE ) ∪ out SF (n)) ∧ Ξ Example. Figure
The ST and RT are enabled when they have a token on their incoming edges and they have no token on them. They start executing by moving this token inside. ST completes by sending a message on all its outgoing edges regarding the chosen communication model (which affects the network state) and producing a token on all its outgoing edges.

A ST is not necessarily instantaneous as a send may block, for instance with synchronous communication, RSC or a bounded size network. Another important point is that a boundary event, such as a timeout, can be attached to a receive or send task and not to an event. For all these reasons, we have chosen to make these tasks nonatomic. This allows to distinguish a send task from aThrowMessageIntermediateEvent, and a receive task from a CatchMessageIntermediateEvent. Note that the semantics in the standard is ambiguous, since there are two contradictory aspects: tasks in BPMN are non-atomic while the purpose of a send task is to only send a message, which is intrinsically atomic. Formally.

∀n ∈ N ST , St(n) def ≡ ∃e ∈ in SF (n), (me(e) ≥ 1) ∧ (me (e) = me(e) -1) ∧ (mn(n) = 0) ∧ (mn (n) = mn(n) + 1) ∧ ({n, e}) ∧ Ξ ∀n ∈ N ST , Ct(n) def ≡ (mn(n) = 1) ∧ (mn (n) = mn(n) -1) ∧ ∀e ∈ out SF (n), (me (e) = me(e) + 1) ∧ ∃ee ∈ out MF (n), (me (ee) = me(ee) + 1) ∧ send (procOf(n), procOf(target(ee)), msg(ee)) ∧ ({n, ee} ∪ out SF (n))
Example. Figure 12 presents the starting behavior of a send task activity (task). It shows the same starting behavior as the one presented in Figure 8. Fig. 13 shows the completing behavior, task completes by consuming one token from it and by generating a token on its outgoing edge e2, and producing a message m1 on the network according to the chosen communication model. A receive task (RT ) has a complementary behavior to the send task (ST ). It is enabled to complete only if it is active (i.e., it has a token) and it has a message on one of its incoming message flows. RT completes by consuming the message offer, updating the network state, and producing a token on all its outgoing edges.

420

Formally.

∀n ∈ N RT , St(n) def ≡ ∃e ∈ in SF (n), (me(e) ≥ 1) ∧ (me (e) = me(e) -1) ∧ (mn(n) = 0) ∧ (mn (n) = mn(n) + 1) ∧ ({n, e}) ∧ Ξ ∀n ∈ N RT , Ct(n) def ≡ (mn(n) = 1) ∧ (mn (n) = mn(n) -1) ∧ ∀e ∈ out SF (n), (me (e) = me(e) + 1) ∧ ∃ee ∈ in MF (n), (me(ee) ≥ 1) ∧ (me (ee) = me(ee) -1) ∧ receive(procOf(source(ee)), procOf(n), msg(ee)) ∧ ({n, ee} ∪ out SF (n))
Example. The starting of the receive task activity is similar to the one presented for the abstract task in Figure 8. Fig. 14 shows that the receive task activity (task) can complete if it has a token on itself and a message m1 on its incoming message flow. It completes by consuming its token, receiving the message from the network, and producing a token on its outgoing edge (e2). A throw message intermediate event (TMIE ) defines only the starting behavior. It is enabled to start if it has a token on one of its incoming edges. It starts by consuming the token from this incoming edge, sending a message on the network according to the chosen communication model, and producing a token on all its outgoing edges.

Formally.

∀n ∈ N TMIE , St(n) def ≡ ∃ein ∈ in SF (n), (me(ein) ≥ 1) ∧ (me (ein) = me(ein) -1)
∧ ∀e ∈ out SF (n), (me (e) = me(e) + 1)

∧ ∃eout ∈ out MF (n), (me (eout) = me(eout) + 1) ∧ send (procOf(n), procOf(target(eout)), msg(eout)) ∧ ({ein, eout} ∪ out SF (n))
Example. Figure 15 shows the starting behavior of a throw message intermediate event (Send Notif.). It starts by consuming the token from its incoming edge (e1), producing a token on its outgoing edge (e2), and sending a message m1 on the network. A catching message intermediate event (CMIE ) is an instantaneous event with only a starting transition. It is enabled if it has a message offer on one of its incoming message flow edges and a token on one of its incoming sequential flow edges. It starts by consuming the token from this incoming edge, receiving the message from the incoming message flow according to chosen the communication model, and producing a token on all its outgoing edges. Formally.

∀n ∈ N CMIE , St(n) def ≡ ∃e 1 ∈ in SF (n), (me(e 1 ) ≥ 1) ∧ (me (e 1 ) = me(e 1 ) -1)
∧ ∀e 2 ∈ out SF (n), (me (e 2 ) = me(e 2 ) + 1) ∧ ∃ein ∈ in MF (n), (me(ein) ≥ 1) ∧ (me (ein) = me(ein) -1) ∧ receive(procOf(source(ein)), procOf(n), msg(ein))

∧ ({e 1 , ein} ∪ out SF (n))
Example. Figure 16 shows the starting behavior of a catching message intermediate event (Receive Notif.). It starts by consuming the token from e1, receiving the message m1 from the medium, and producing a token on its outgoing edge, e2. Boundary Events. A message boundary event (MBE ) defines only the starting behavior.

An MBE is ready to start if it has a message offer on one of its incoming message flows, and if the activity on which it is attached has a token. An MBE may have either an interrupting behavior or a non-interrupting one. In the latter case, the MBE starts by receiving a message and generating a token on all its outgoing edges. For an interrupting behavior, the MBE starts also by cancelling the activity to which it is attached, which is possible only if this activity is not a sub-process in a completing step. This is checked using the mayComplete predicate that is formally defined below. Cancelling an activity involves dropping all its tokens. After that, the MBE produces a token on each of its outgoing edges.

Formally.

Auxiliary functions. To formalize the semantics of a message boundary event, we define an auxiliary function.

• mayComplete(n) : N SP → Bool, returns true if the subprocess may complete, i.e., if there are no tokens on its elements except for its end event nodes where there is at least one that holds some tokens.

∀n ∈ N SP , mayComplete(n) def ≡ (mn(n) ≥ 1) ∧ ∀e ∈ (R(n) ∩ E), (me(e) = 0) ∧ ∃nn ∈ R(n) ∩ N EE , (mn(nn) ≥ 1) ∧ ∀x ∈ R(n) ∩ (N \ N EE ), (mn(x) = 0) St interrupting (n, act, ein) def ≡ (act / ∈ N SP ∧ (mn (act) = 0) ∧ ({act, ein} ∪ out SF (n)) ) ∨     act ∈ N SP ∧ ¬mayComplete(act) ∧ (mn (act) = 0) ∧ ∀nn ∈ R(act) ∩ N, (mn (nn) = 0) ∧ ∀ee ∈ R(act) ∩ E, (me (ee) = 0) ∧ ({act, ein} ∪ R(act) ∪ out SF (n))     ∀n ∈ N MBE , St(n) def ≡ ∃act ∈ N A , (act = attachedTo(n)) ∧ (mn(act) = 1) ∧ ∃ein ∈ in MF (n), (me(ein) ≥ 1) ∧ receive(procOf(source(ein)), procOf(n), msg(ein)) ∧ (me (ein) = me(ein) -1) ∧ ∀eo ∈ out SF (n), (me (eo) = me(eo) + 1) ∧ (isInterrupt(n) ∧ St interrupting (n, act, ein)) ∨ (¬isInterrupt(n) ∧ ({ein} ∪ out SF (n)))
Example. Figure 17 presents a part of a process with a none start event nse, an abstract task task1 with an outgoing sequence flow edge e2, an interrupting boundary event (interrupt) with an outgoing sequence flow edge e4, and two abstract tasks task2, and task3. The interrupt boundary node starts by consuming a token from the activity it is attached to, receiving a message m1 from the network, and producing a token on its outgoing edge e4. Figure 18 shows an interrupting boundary event interrupt attached to a sub-process SP. The interrupt event interrupts the execution of SP when it receives a message m1. It cancels the execution of the sub-process by removing all its token (the token on it and the token on node nse1), and generates a token on its outgoing sequence flow edge, e4. Gateways. Gateways are atomic and define only the completing behavior.

465

A parallel gateway (AND) is ready to complete if it has at least one token on all its incoming edges. It completes by removing one token on each of these edges, and producing one on all its outgoing edges. Formally.

∀n ∈ N AND , Ct(n) def ≡ ∀ei ∈ in SF (n), (me(ei) ≥ 1) ∧ (me (ei) = me(ei) -1) ∧ ∀eo ∈ out SF (n), (me (eo) = me(eo) + 1) ∧ (in SF (n) ∪ out SF (n)) ∧ Ξ
Example. Figure 19 shows that the parallel gateway AN D1 completes by consuming a token from its incoming edge (e1) and producing a token on all its outgoing edges (e2 In Figure 20, the parallel gateway AN D2 completes only if all its incoming sequence flows edges (e4 and e5) are synchronized (i.e., own at least a token). An exclusive gateway (XOR) is ready to complete if it has at least one token on one of its incoming edges. It completes by removing this token, and producing one on one 475 of its outgoing edges, depending on conditions. Since we abstract away from data, the concerned edge is non-deterministically chosen. Formally.

∀n ∈ N XOR , Ct(n) def ≡ ∃ei ∈ in SF (n), (me(ei) ≥ 1) ∧ (me (ei) = me(ei) -1) ∧ ∃eo ∈ out SF (n), (me (eo) = me(eo) + 1) ∧ ({ei, eo}) ∧ Ξ
Example. Figure 21 shows that the exclusive gateway (XOR1) completes by consuming a token from its incoming edge (e1), and producing a token on one of its outgoing edges (e2 in the example). As described in the standard [START_REF] Kahloul | Business Process Modeling Notation[END_REF], an event-based gateway (EB ) is always followed by communication elements, either receive tasks (RT ) or intermediate catching message events (CMIE ) 2 . The firing of an event-based gateway relies on the enabling of one of these elements. Hence, an event-based gateway completes by consuming a token from one of its incoming edges, and producing a token on its outgoing edge on which the event is enabled. Formally.

∀n ∈ N EB , Ct(n) def ≡ ∃ei ∈ in SF (n), (me(ei) ≥ 1) ∧ (me (ei) = me(ei) -1) ∧ ∃eo ∈ out SF (n), target(eo) ∈ N {RT,CM IE} ∧ ∃em ∈ in MF (target(eo)), (me(em) ≥ 1) ∧ (me (eo) = me(eo) + 1) ∧ ({ei, eo}) ∧ Ξ Example.
Figure 22 shows a process that contains an event-based gateway (EBG), and two receive tasks (Rec.1 and Rec.2). The left-hand side of the figure shows that the event-based gateway is enabled because it has a token on its incoming edge (e1), and an incoming message for at least one of the two receive tasks. Actually, this is true for both receive tasks here. Hence, EBG completes by consuming the token from e1, and generating a token on one of its two outgoing edges (arbitrarily chosen, here e2). An inclusive gateway (OR) behaves differently from the other gateways. The activation of an OR gateway g is more complex [START_REF] Kahloul | Business Process Modeling Notation[END_REF]Chap. 13]. It can be activated only if:

• ( 1) it has at least one token on one of its incoming edges, and • (2) for each marked node or edge x such that there is a path -that does not pass through g -from x to an unmarked incoming edge of g, there must be also a path -that does not pass through g -from x to a marked incoming edge of g.

The OR gateway completes by adding a token either to the outgoing edges whose conditions are true, otherwise to its default sequence flow edge. Since we abstract from data, we chose non-deterministically to add a token either to a combination (1 or more) of the outgoing non-default edges, or to the default edge. Formally.

Auxiliary functions. To formalize the semantics of an OR gateway, we define some auxiliary functions.

• P re N : N × E → 2 N gives the predecessor nodes of an edge such that n pre is in P re N (n, e) if there is a path from n pre to e that never visits n. Accordingly, P re E : N × E → 2 E gives predecessor edges. These two sets can be structurally computed from the BPMN graph structure, hence can be taken as constants (for a given BPMN model).

• InMinus : N → E gives the unmarked incoming edges of a node:

InMinus(n) = {e ∈ in SF (n) | me(e) = 0}
• InPlus : N → E gives the marked incoming edges of a node:

InPlus(n) = {e ∈ in SF (n) | me(e) ≥ 1}
• ignore E : N → 2 E gives the predecessor edges of the marked incoming edges of a given node:

ignore E (n) def ≡ e∈InPlus (n)
P re E (n, e)

• ignore N : N → 2 N gives the predecessor nodes of the marked incoming edges of a given node:

ignore N (n) = e∈InPlus(n) P re N (n, e) ∀n ∈ N OR , Ct(n) def ≡ (InPlus(n) = ∅) ∧ ∀e ∈ InPlus(n), (me (e) = me(e) -1) ∧ ∀ez ∈ InMinus(n), ∀ee ∈ (P re E (n, ez) \ ignore E (n)), (me(ee) = 0) ∧ (∀nn ∈ (P re N (n, ez) \ ignore N (n)), (mn(nn) = 0)) ∧         ∃Outs ⊂ (out SF (n) ∩ E {NSF,CSF}
), (Outs = ∅) ∧ ∀e ∈ Outs, (me (e) = me(e) + 1)

∧ (InPlus(n) ∪ Outs) ∧ Ξ   ∨ ∃e ∈ out DSF (n), (me (e) = me(e) + 1) ∧ (InPlus(n) ∪ {e}) ∧ Ξ      
Example. Figure 23 illustrates the case when an OR getaway cannot be activated, despite a marked incoming edge, here e3: there is a path from the marked edge e2 to an unmarked incoming edge of OR (e6 or e7) but no path from e2 to a marked incoming edge of OR. If the token on e2 had been on e1, the OR gateway could have been activated.

Communication Models

Generic Communication Models. We define seven communication models which differ in the order the messages can be sent or received, and are all the possible point-topoint models when considering local ordering (per process), causal ordering, and global ordering (absolute time) [START_REF] Chevrou | On the diversity of asynchronous communication[END_REF]. In the following we define the structure of each model as a type called T net where T net ∈ {bag, pair, inbox , outbox, causal, fifoall, RSC}.

The models are formally defined in Table 1 and are explained below. To simplify notation, we include sequences of terms (Seq[T ]) and bags (Bag[T ]) as a part of the usual definition of ground terms in first order logic. We also assume some standard definitions and operations on terms:

Network model Definition

Bag

initnet def ≡ ∅ send (f rom, to, m) def ≡ mnet = mnet ⊕ { f rom, to, m } receive(f rom, to, m) def ≡ f rom, to, m ∈ mnet ∧ mnet = mnet { f rom, to, m } Fifo Pair initnet def ≡ [p, q ∈ N P → ] send (f rom, to, m) def ≡ mnet (f rom, to) = append(mnet(f rom, to), m) receive(f rom, to, m) def ≡ m = head(mnet(f rom, to)) ∧ mnet (f rom, to) = tail(mnet(f rom, to)) Fifo Inbox initnet def ≡ [p ∈ N P → ] send (f rom, to, m) def ≡ mnet (to) = append(mnet(to), f rom, m ) receive(f rom, to, m) def ≡ f rom, m = head(mnet(to)) ∧ mnet (to) = tail(mnet(to)) Fifo Outbox initnet def ≡ [p ∈ N P → ] send (f rom, to, m) def ≡ mnet (f rom) = append(mnet(f rom), to, m ) receive(f rom, to, m) def ≡ to, m = head(mnet(f rom)) ∧ mnet (f rom) = tail(mnet(f rom))
Fifo All Causal

initnet def ≡ ∅ × [p ∈ N P → [q ∈ N P → 0]] send (f rom, to, m) def ≡ mnet [1] = mnet[1] ∪ { f rom, to, m, vc[f rom] } ∧ mnet [2] = vc with vc def ≡ [p ∈ N P → [q ∈ N P → if p = f rom ∧ q = f rom then mnet[2][p][q] + 1 else mnet[2][p][q] ]] receive(f rom, to, m) def ≡ ∃msg ∈ mnet[1], msg[1] = f rom ∧ msg[2] = to ∧ msg[3] = m ∧ ¬(∃msg 2 , msg 2 = msg ∧ msg 2 [2] = to ∧ ∀p ∈ N P , msg 2 [4][p] ≤ msg[4][p]) ∧ mnet [1] = mnet[1] \ {msg} ∧ mnet [2] = [p ∈ N P → if p = to then Sup(mnet[2][p], m[4]) else mnet[2][p]] RSC initnet def ≡ ∅ send (f rom, to, m) def ≡ mnet = ∅ ∧ mnet = { f rom, to, m } receive(f rom, to, m) def ≡ f rom, to, m ∈ mnet ∧ mnet = ∅
• Bag is a multiset of messages. Formally:

bag def ≡ Bag[N P × N P × M]
No order on message reception is imposed. Messages can overtake each other or be arbitrarily delayed. It is usually modeled by a bag, or a set if messages are unique.

• Fifo pair is a queue of messages attached to each couple of processes. Formally:

pair def ≡ N P × N P → Seq[M]
Messages between a couple of processes are received in their send order. Messages from or to different processes are independently received. More precisely, if a process P 1 sends a message m 1 to process P 2 , and later a message m 2 to this same process, then m 2 cannot be received before m 1 .

• Fifo inbox is an input queue attached to each process, where senders put messages. Formally:

inbox def ≡ N P → Seq[N P × M]
Each process has its own unique input queue, and senders add messages to this queue, without blocking. Messages are consumed from this queue in their insertion order. This means that if a process P 1 sends a message m 1 to P 0 , and later (but independently) a process P 2 sends a message m 2 to P 0 , then m 2 cannot be received before m 1 . This model is stricter than Fifo pair as it requires a global order on the emission events.

• Fifo outbox is an output queue attached to each process where messages are retrieved. Formally:

outbox def ≡ N P → Seq[N P × M]
Messages from a same process are received in their send order. If a process P sends a message m 1 and later a message m 2 (to the same process or to another one), then m 2 cannot be received before m 1 , even if the receptions occurs on distinct processes.

• Fifo All is a unique shared queue. Formally:

fifoall def ≡ Seq[N P × N P × M]
Messages are globally ordered, independently of their sender or receiver process, and are received in the global emission order.

• Causal. Messages are received according to the causality of their emission [START_REF] Lamport | Time, clocks and the ordering of events in a distributed system[END_REF]. Formally: Figure 24 presents a model that deadlocks with causal communication. In this example, a scientist writes a proposal, sends the proposal to the client, and sends its description to its financial department. Based on the description, the financial department computes a quote and sends it to the client. Without causal communication, the quote can be received by the client before the proposal; with causal communication, the quote cannot be delivered because it causally depends on the proposal that must be received first. A usual implementation of this model uses causal histories [START_REF] Schwarz | Detecting causal relationships in distributed computations: In search of the holy grail[END_REF][START_REF] Kshemkalyani | Necessary and sufficient conditions on information for causal message ordering and their optimal implementation[END_REF] or vector/matrix logical clocks [START_REF] Raynal | The causal ordering abstraction and a simple way to implement it[END_REF] as presented here 3 . The state of the network mnet holds a couple: the set of messages in transit (with their associated vector clock), and the vector clocks of each process.

V C def ≡ [N P → N] --a vector clock causal ∈ Set[N P × N P × M × V C] × [N P → V C]
• RSC (Realisable with Synchronous Communication) is a shared 1-sized buffer for all processes. Formally:

net RSC def ≡ (N P × N P × M)
Send and receive events strictly alternate. If the couple (send event, reception event) is considered as atomic, this corresponds to synchronous communication [START_REF] Charron-Bost | Synchronous, asynchronous, and causally ordered communication[END_REF].

Ad-hoc Communication Models. The previous communication models are monolithic and are applied on the whole collaboration. In Section 5.4, we show how a modular communication model can be specified.

Transition Relation and Executions

With the previously defined predicates, we are able now to express the complete transition relation (successor relation between states). Definition 2.5 (Transition Relation). Let s and s be two states. We say that s is a successor of s, iff the predicate N ext(s, s ) holds:

N ext(s, s ) def ≡ n∈N (St(n) ∨ Ct(n))
We recall that states, here s and s , correspond to tuples of the form (me, mn, mnet) and (me , mn , mnet ), whose elements are used in the definitions of St and Ct.

An execution of the whole process is defined through the notion of trace.

Definition 2.6 (Trace). A trace is a finite or infinite sequence of states such that σ[0] is the initial state, and ∀i ∈ 0..

Len(σ) -1, N ext(σ[i], σ[i + 1]) (if the trace is finite) or ∀i ∈ N, N ext(σ[i], σ[i + 1]) (if the trace is infinite)
, where σ[i] denotes the i th state of the trace. The set of all the traces of the collaboration is noted T races.

Definition 2.7 (Execution). An execution is a maximal trace, i.e., a trace that goes as far as possible. Formally, an execution σ is either an infinite trace, or a finite trace such that ∃s , N ext(σ[Len(σ)], s ). The set of all the executions of the collaboration is noted Exec.

Fair Executions

A BPMN model can include loops. In that case, an execution defined as a maximal trace can get stuck in a loop, where only this loop progresses, and the rest of the model doesn't progress at all. Moreover, when modeling actual business activities, loops are expected to finish at some point. To prevent these infinite loops, fairness is introduced to restrain the set of executions. We use two kinds of fairness: weak fairness and strong fairness. Informally, weak fairness ensures that a transition cannot be permanently enabled and never done. Strong fairness ensures that a transition cannot be infinitely often enabled and never done. Both are formally defined in Section 5.3.

Thus, fairness is a conjunction of two parts. The first part is the weak fairness on each start (St) and complete (Ct) transitions of every node: ∀n ∈ N ode : weakfair (step(n)). This property ensures that any permanently enabled transition eventually occurs. This means that no process may progress forever while others are never allowed to do so if they can. This also means that if a process contains several loops that are simultaneously live, all loops will progress (not necessarily at the same speed, but no loop can be permanently halted while another run forever).

The second part is the strong fairness on each output edges of XOR, OR, and EB gateways. Strong fairness ensures that no choice is infinitely often ignored: if a XOR, OR, or EB gateway is included in a loop, the fairness forbids the infinite executions that never use some output edges. Either the loop finishes somehow, or all the choices are infinitely often taken. Consider Figure 25, left; as strong fairness is imposed on the two output edges of gateway choice, an execution cannot always ignore the edge (e5) leading to the ending node, and this model is sound. Consider Figure 25, right; as strong fairness is imposed on the output edges of gateway choice, both task1 and task2 are infinitely often chosen.

Temporal Support for BPMN

The goal of our FOL semantics is to give a meaning to the BPMN elements. In a sense, it defines which executions are possible. With regard to time, our semantics is asynchronous: enabled elements are fired at some point, but not necessarily at the instant they have become enabled; message transfer is asynchronous, which means that a message is available for reception at some point after its sending, but there is no time constraint. With these remarks in mind, we present two choices for handling time: in the first one, the semantics does not explicitly handle time constraints, but it reverts to nondeterminism: if a time constraint exists, it may fire; in the second one, the semantics is defined with explicit time to verify duration properties.

BPMN Elements with Time

Events where time occurs are the following:

1. Timer Start Event for Top-level Processes. A process is started when the time constraint allows it.

2. Timer Intermediate Catch Event. The norm states that it acts as a delay.

3. Timer Boundary Event, which can be interrupting or non-interrupting. It can act as a timeout on a long running task (interrupting event) or create a secondary path when the time constraint specifies it (non-interrupting event). 4. An Event-Based Gateway can be followed by a Timer Intermediate Catch Event.

Especially, it can be used as a timeout while waiting for a message amongst several links.

An event with time has an attribute specifying the time constraint. It is one of timeDate (a date and/or time, e.g., 2019-11-27 16:44), timeDuration (a time duration, e.g., PT05:15 for a duration of five hours and fifteen minutes), or timeCycle (a time interval, e.g., a start and end time, or a start time and a duration).

Non-deterministic Abstraction of Time

So far, our FOL semantics is asynchronous (an event or a task is fired at any point of time after it is enabled) and non-deterministic (e.g., for an XOR gateway, any of the output branches can be taken, and the verification ensures that all the cases are covered): the semantics arbitrarily fires an enabled transition. Consequently, time progress can be modeled with non-determinism.

Timer Start Event (TSE ): as the semantics is asynchronous, it is exactly as a None

Start Event (NSE ), where the event will fire at some point.

Timer Intermediate Catch Event (TICE ): it is indistinguishable from a gateway

with one input and one output (it fires at some point).

∀n ∈ N T ICE , Ct(n) def ≡ ∃ei ∈ in SF (n), (me(ei) ≥ 1) ∧ (me (ei) = me(ei) -1) ∧ ∃eo ∈ out SF (n), (
≡ (act / ∈ N SP ∧ (mn (act) = 0) ∧ ({act} ∪ out SF (n))) ∨     act ∈ N SP ∧ ¬mayComplete(act) ∧ (mn (act) = 0) ∧ ∀nn ∈ R(act) ∩ N, (mn (nn) = 0) ∧ ∀ee ∈ R(act) ∩ E, (me (ee) = 0) ∧ ({act} ∪ R(act) ∪ out SF (n))     ∀n ∈ N TBE , St(n) def ≡ ∃act ∈ N A , (act = attachedTo(n)) ∧ (mn(act) = 1) ∧ ∀eo ∈ out SF (n), (me (eo) = me(eo) + 1) ∧ (isInterrupt(n) ∧ St interrupting (n, act)) ∨ (¬isInterrupt(n) ∧ (out SF (n))) ∧ Ξ
4. Event-Based Gateway followed by a Timer Intermediate Catch Event: as the eventbased gateway can be fired at any time after it is enabled, a branch with a TICE is indistinguishable from a Default branch followed by a TICE modelled as above in item 2.

A limitation to non-deterministic time is when a TBE can actually never be fired in BPMN semantics (e.g., a date in the past): the non-deterministic semantics allows it to fire. This gives us an over-approximation: the non-deterministic semantics contains the same executions as with BPMN semantics, plus additional ones. Thus, if the verification states that a property is verified with the non-deterministic semantics, it is necessarily verified with BPMN semantics. The reverse is not true. For instance, in the example of Fig. 26, BPMN semantics states that task task2 should never be activated as its time constraint is always in the past. The non-deterministic semantics defines two executions: one where the timeout is not fired, and one where the timeout is fired and task2 is activated.

Explicit Time

In order to integrate the notion of explicit time, we extend the BPMN graph to deal with some time constraints: here, we treat only the timeDuration type for the different time events (i.e., timeDate and timeCycle types are not handled by our extension).

To simplify our definition, we introduce the set Timer that groups the time start (TSE ), the timer intermediate catch (TICE ) and the timer boundary (TBE ) events: Timer = { TSE, TICE, TBE }. Hence, to express the timeDuration type for each timer node, we add to the graph definition (Def. 2.1) a timing function: G= (N , E, M, cat N , cat E , source, target, R, msg, attachedTo, isInterrupt, timing). timing maps a time duration t to each timer node.

timing : N Timer → N .

We extend the state definition with locals clocks (l c ). Hence, the definitions of state (Def. 2.2) and initial state (Def. 2.3) change as follows.

Definition 3.1 (State). s = (mn, me, mnet, l c ) such that:

• l c : N Timer → N, is the local discrete clock representing the time spent on a given timer node.

Definition 3.2 (Initial state). The initial state of a BPMN graph, denoted by s o = (mn 0 , me 0 , mnet 0 , l c0 ).

• Local clocks are initialized to zero: ∀n ∈ N Timer , l c0 (n) = 0.

• mn 0 , me 0 , and mnet 0 are initialized as above (Def. 2.3).

Based on these changes, we define the execution semantics of the timer event nodes as follows.

• A start timer event (TSE ) is defined by a completing predicate. TSE is enabled to complete only if it has a token and the time of its local clock has elapsed. It completes by consuming its token, producing a token on each of its outgoing edges and on the process, and resetting its local clock. its marked incoming edges, resetting its local clock, and generating a token on its outgoing edges.

∀n ∈ N TSE , Ct(n) def ≡ (l c (n) ≥ T iming(n)) ∧ (l c (n) = 0) ∧ (mn(n) = 1) ∧ (mn (n) = mn(n) -1) ∧ ∀eo ∈ out SF (n), (
Formally.

∀n ∈ N TICE , St(n) def ≡ (l c (n) ≥ T iming(n)) ∧ (l c (n) = 0) ∧ ∃ei ∈ in SF (n), (me(ei) ≥ 1) ∧ (me (ei) = me(ei) -1) ∧ ∀eo ∈ out SF (n), (me (eo) = me(eo) + 1) ∧ ({ei} ∪ out SF (n)) ∧ Ξ Example.
Let us consider a claims process. To support his claim, a client should register and provide some documents. Then, the claim is analysed to take the necessary actions and inform the client. The action to be taken is executed after a certain time. This delay can be modelled by an intermediate catching time event. Figure 28 shows the starting behavior of a timer intermediate catching event (Waiting). The upper part of the figure shows that Waiting is enabled to complete: it has a token on its incoming edge (e4), and its clock meets the deadline. The lower part of the figure shows that Waiting completes by moving the token on its outgoing sequence flow edge (e5), and resetting its local clock. • A timer boundary event (TBE ) is defined by a starting predicate. TBE is ready to start if its local clock meets its deadline and the activity attached to it is active (i.e., owns a token). In this case, we distinguish the interrupting behavior from noninterrupting one. In the latter, a TBE starts by generating a token on its outgoing sequence flow edges and resetting its local clock. In the interrupting behavior, a TBE starts by cancelling the activity which it is attached to if this activity is not a sub-process in its completing step (i.e., it has at least one token on one of its elements other than its end events). If it is the case, the activity is cancelled by dropping all its tokens. The TBE resets then its local clock and produces a token on each of its outgoing edges.

Formally.

St interrupting (n, act) def ≡ (act / ∈ N SP ∧ (mn (act) = 0) ∧ ({act} ∪ out SF (n))) ∨     act ∈ N SP ∧ ¬mayComplete(act) ∧ (mn (act) = 0) ∧ ∀nn ∈ R(act) ∩ N, (mn (nn) = 0) ∧ ∀ee ∈ R(act) ∩ E, (me (ee) = 0) ∧ ({act} ∪ R(act) ∪ out SF (n))     ∀n ∈ N TBE , St(n) def ≡ ∃act ∈ N A , (act = attachedTo(n)) ∧ (mn(act) = 1) ∧ (l c (n) ≥ T iming(n)) ∧ (l c (n) = 0) ∧ ∀eo ∈ out SF (n), (me (eo) = me(eo) + 1) ∧ (isInterrupt(n) ∧ St interrupting (n, act)) ∨ (¬isInterrupt(n) ∧ (out SF (n))) ∧ Ξ Example.
Consider an example of an on-line payment process: when the payment page is opened, the user must enter the credit card number, this task is stopped if a timeout (e.g., 10 minutes) is triggered. Besides, the user receives a notification of the remaining time before the deadline (e.g., at minute 7, to say that it remains 3 minutes). The timeout can be modelled by an interrupting boundary time event (timeOut) and the reminder by a non-interrupting boundary event (timeReminder ). • Event-Based Gateway. Due to the provided semantics for the timer events, the semantics of an event-based gateway must be changed. In the standard, the execution semantics of an event-based gateway is defined as a branching point where exactly one of its outgoing edges is activated, depending on which event is triggered. Then, the path to that event will be used (a token will be sent down the outgoing sequence flows of the event) [START_REF] Kahloul | Business Process Modeling Notation[END_REF].

In a BPMN model, an event-based gateway is followed by a receive task (RT ) or an intermediate catching message event (CMIE ), combined with a timer intermediate catch event (TICE ): the activation of one of the outgoing edges depends on the enabling of these elements (i.e., the reception of a message, or a specific time event is triggered). So, to handle time, we adapt the semantics of an event-based gateway as follows.

An Event-based gateway (EB ) is defined only by a completing predicate. It is ready to complete if one of its incoming edges has a token and one of its target events is enabled (i.e., the target of an outgoing edge is an RT or a CMIE that has an offer on one of its incoming message edges, or the target of an outgoing edge is a timer intermediate event that meets its deadline). The EB completes by consuming the token from one of its incoming edge and producing a token on the outgoing edge on which the event is enabled.

Formally.

∀n ∈ N EB , Ct(n) def ≡ ∃ ei ∈ in SF (n), (me(ei) ≥ 1) ∧ (me (ei) = me(ei) -1) ∧           ∃eo ∈ out SF (n), target(eo) ∈ N {RT,CMIE} ∧ ∃em ∈ in MF (target(eo)), (me(em) ≥ 1) ∧ (me (eo) = me(eo) + 1) ∧ ({ei, eo})   ∨   ∃eo ∈ out SF (n), (target(eo) ∈ N TICE ) ∧ (l c (target(eo)) ≥ timing(target(eo))) ∧ (me (eo) = me(eo) + 1) ∧ ({ei, eo})           ∧ Ξ
Example. Let us consider an extension of the claim process presented in Figure 28.

If the documentation is not provided by the client within a certain period, the claim will fail. This should be included in the diagram (see Fig. 32). After the registration of the claim, an event-based gateway waits for the first event to occur: a Receive document or a TimeOut. The figure shows that after a maximum period 745 of time (defined through the deadline of TimeOut), if the client does not present the documents, TimeOut is activated and then the event-based gateway generates a token on its outgoing edge leading to TimeOut (see lower part of Fig. 32). The lower part of Figure 31 shows the case where the documents are provided in time, and the event-based gateway generates a token on the corresponding outgoing edge 750 (e3). clocks are greater than 0 and they didn't reach their timing limits) as follows:

S def ≡ {n ∈ N TSE | (l c (n) = 0) ∧ (mn(n) = 1)} ∪ {n ∈ N TICE | ∃e ∈ in SF (n), (l c (n) = 0) ∧ (me(e) > 0)} ∪ {n ∈ N TICE | ∃e ∈ in SF (source(in SF (n))), (l c (n) = 0) ∧ (me(e) > 0)} ∪ {n ∈ N TBE | (l c (n) = 0) ∧ (mn(attachedTo(n)) > 0)} ∪ {n ∈ N Timer | timing(n) > l c (n) > 0}
Let Y be the subset of timer nodes in the BPMN graph that are ready to fire:

Y def ≡ {y ∈ N Timer | l c (y) ≥ T iming(y)}
To facilitate the reading of the transition relation, we define the following predicates:

• step defines a step of execution for a given node:

step(n) def ≡ St(n) ∨ Ct(n)
• stepT increases the local clock of each enabled timer node or currently executed:

stepT def ≡ ∀n ∈ S, l c (n) = l c (n) + 1
• f ztime denotes time equality for the local clock of all timer nodes given as parameter:

f ztime(Z) def ≡ ∀z ∈ Z, l c (z) = l c (z)
The transition relation distinguishes two cases. If at least a timer is ready to fire (Y = ∅), then a timer fires (it does a step) or an event-based gateway that precedes a firable timer does a step. Time does not advance, and other timers with the same expiration time can then fire. If no timer is ready to fire, all timers increase (stepT ) and non-deterministically, a step can occur (∃n, step(n)) or no step is done ( (∅) ∧ Ξ).

Definition 3.3 (Transition Relation with time)

. Let s and s be two states. We say that s is a successor of s, iff the predicate N ext(s, s ) holds:

N ext(s, s ) def ≡ (Y = ∅ ∧   (∃n ∈ Y : step(n) ∧ f ztime(N Timer \ {n})) ∨ ∃n ∈ N EB , ∃eo ∈ out SF (n), (target(eo) ∈ Y ) ∧ step(n) ∧ f ztime(N Timer )   ∨ (Y = ∅ ∧ stepT ∧ f ztime(N Timer \ S) ∧ ((∃n ∈ N : step(n)) ∨ ( (∅) ∧ Ξ))

Discussion

The advantage of abstracting time with non-deterministic transitions is its simplicity, and its efficiency in model-checking once translated in TLA + . The first limitation is that it can not recognize impossible-to-meet time constraints, e.g. a time necessarily in the past. As noted above, this is safe with regard to LTL properties, which are the majority of the useful properties in Section 4. The no dead activities property is the only one that cannot be checked, as it translates to a CTL existential property. The second limitation is that we cannot derive any temporal information on a collaboration, for instance how long it takes to complete. With explicit time, on the other hand, it is possible to compute the minimal number of ticks a process or a collaboration need to complete. This requires adding history variables [18, p. 270] to record time information such as the start time of a process, without altering the semantics [START_REF] Abadi | An old-fashioned recipe for real-time[END_REF]. Our semantics use discrete time. As shown in [START_REF] Lamport | Real-time model checking is really simple[END_REF], discrete time allows specifications to be checked with ordinary model checkers, and our semantics do not require continuous time model checkers such as Uppaal.

Verification Properties

Verifying a model involves checking the correctness of its properties. In the context of process modelling, properties are classified into two main classes: structural and behavioural. The structural properties relate to the type of elements and how they are connected. Such properties could be checked using a standard process modelling tool which can enforce that the model is correctly designed. The behavioural properties relate to the sequences of execution as defined by the process model. We further classify the behavioural properties into general and specific ones. The specific properties are unique to business process models, while the general properties are used in other types of models.

General properties. deadlocks and livelocks are common examples of general properties. Fig. 33 shows a simple BPMN model with an XOR and an AND gateway. The XOR gateway produces a token either on its outgoing edge e2 or e3 but not on both. As a consequence, the AND gateway will never be enabled (its incoming edges e4, e5 will never be synchronized). Hence, this model suffers from a deadlock situation. While in a deadlock the involved activities can never be executed and the process can never be completed, in a livelock situation a set of activities are executed indefinitely. Specific properties. Soundness is the main property that can be checked after a process model is executed. Soundness property for business processes was developed by Wil van der Aalst in the context of workflow nets [START_REF] Van Der Aalst | Verification of workflow nets[END_REF]. A workflow net has a unique terminal place and the authors defined the soundness of the WF-net by the satisfaction of the three following requirements: "(1) Option to complete: from any reachable state, it is possible to reach a state with marks on the terminal place, (2) proper completion: if the terminal place is marked, all other places are empty, (3) no dead transitions: it should be possible to execute an arbitrary activity by following an appropriate route through the WF-net". In the case of Petri nets in workflow verification, [START_REF] Van Der Aalst | Soundness of workflow nets: classification, decidability, and analysis[END_REF] and [START_REF] Combi | A modular approach to the specification and management of time duration constraints in BPMN[END_REF] prove that a workflow net is sound if and only if the corresponding short-circuited Petri net is live and bounded. In addition, they define the safeness of a WF-net by ensuring that each place cannot hold multiple tokens at the same time.

In the book [START_REF] Dumas | Fundamentals of Business Process Management[END_REF], [p.186, ch.5], Dumas et.al define informally the soundness of the BPMN process model by the satisfaction of the following three properties: "(1) Option to complete: any running process instance must eventually complete, (2) Proper completion: at the moment of completion, each token of the process instance must be in a different end event, (3) No dead activities: any activity can be executed in at least one process instance".

In [START_REF] Corradini | A classification of BPMN collaborations based on safeness and soundness notions[END_REF], authors address BPMN collaboration models. They introduce a formal definition of safeness and soundness properties by focussing on the specificities of BPMN. "A process is safe if during its execution no more than one token occurs along the same sequence edge". The authors extend the safeness property for processes collaboration which require that "each of all the processes that involved in the overall collaboration execution is safe". On the other hand, they define the soundness of the process as follows:

"A BPMN process is sound, if it can complete its execution without leaving active elements and all the model elements can be activated in at least one of the execution traces".

In addition, they extend the latter to define the soundness of the whole collaboration model. specified as follows. We recall here that a state in our formalisation of BPMN is s = (mn, me, mnet). For an execution σ = s 1 s 2 ... and a node x, we note σ[i].mn(x) the value of the marking of x at step i in σ, and domain(σ) = {1, ..., |σ|}.

Definition 4.1 (Option to complete). Any running process must eventually complete.

A process is complete in a state if markings occur only on end events.

Completed(p, s)

def ≡ ∀n ∈ R(p) ∩ N, (s.mn(n) = 0) ∨ (s.mn(n) = 1 ∧ n ∈ N EE ) ∧ (∀e ∈ R(p) ∩ E, (s.me(e) = 0)) OptionT oComplete def ≡ ∀p ∈ N P , ∀σ ∈ Exec, ∀i ∈ domain(σ), σ[i].mn(p) > 0 ⇒ ∃j ∈ domain(σ), j ≥ i ∧ Completed(p, σ[j])
Definition 4.2 (Proper Completion). At the moment of completion, each token of the process instance must be in a different end event. A process is sound in a state if only its end events hold at most one token, and all the other nodes (ignoring start events) and all the edges are unmarked. Formally, process p ∈ N P is sound in state s if and only if the following predicate is true :

P roperCompletion def ≡ ∀p ∈ N P , ∀σ ∈ Exec, ∀i ∈ domain(σ), Completed(p, σ[i]) ⇒ ∀n ∈ R(p) ∩ N EE , σ[i].mn(n) = 1
soundP r(p, s) def ≡ ∀n ∈ R(p) ∩ N, (s.mn(n) = 0) ∨ (s.mn(n) = 1 ∧ n ∈ (N EE ∪ N SE )) ∧ ∀e ∈ R(p) ∩ E, s.me(e) = 0
Definition 4.8 (Message-relaxed sound collaboration). A collaboration is messagerelaxed sound if eventually all the processes are sound and it is stable:

msgSoundCol def ≡ ∀σ ∈ Exec, ∃i ∈ domain(σ), ∀j ∈ domain(σ), j ≥ i =⇒ ∀p ∈ N P , soundP r(p, σ[j])
Definition 4.9 (Collaboration soundness). A collaboration is sound if and only if, for all executions, eventually, all the processes involved in the collaboration are sound and all the message flow edges are unmarked.

soundCol def ≡ ∀σ ∈ Exec, ∃i ∈ domain(σ), ∀j ∈ domain(σ), j ≥ i =⇒ ∀p ∈ N P , soundP r(p, σ[j]) ∧ ∀e ∈ E MF , (σ[j].me(e) = 0)
With reference to other definitions of soundness [START_REF] Van Der Aalst | Verification of workflow nets[END_REF][START_REF] Dumas | Fundamentals of Business Process Management[END_REF][START_REF] Corradini | A classification of BPMN collaborations based on safeness and soundness notions[END_REF], we consider a form of soundness under fairness assumptions, that could be called fair soundness.

Implementation & Verification

In this section, we present our encoding of the FOL semantics in TLA + . This allows one to easily parameter the properties of the communication, and to benefit from the efficient TLC model checker to automatically verify collaborations.

The TLA + Specification Language and Verification Framework

TLA + [9] is a formal specification language based on untyped Zermelo-Fraenkel set theory for specifying data structures, and on the temporal logic of actions (TLA) for specifying dynamic behaviors. TLA + allows one to specify symbolic transition systems with variables and actions. An action is a transition predicate between a state and a successor state. It is an arbitrary first-order predicate with quantifiers, set and arithmetic operators, and functions. In an action, x denotes the value of a variable x in the origin state, and x denotes its value in the next state. Functions are primitive objects in TLA + . The application of function f to an expression e is written as f [e]. The expression [x ∈ X → e] denotes the function with domain X that maps any x ∈ X to e. The expression [f except ![e 1 ] = e 2 ] is a function that is equal to the function f except at point e 1 , where its value is e 2 . A system specification is usually a disjunction of actions. Fairness, usually expressed as a conjunction of weak or strong fairness on actions, or more generally as an LTL (Linear Temporal Logic) property, ensures progression. Weak fairness on an action states that this action cannot be continuously enabled without being fired, and strong fairness on an action states that this action cannot be infinitely often enabled without being fired. The TLA + toolbox, freely available at http://lamport. azurewebsites.net/tla/tla.html, contains an editor, a pretty-printer, the TLC model checker, and the TLAPS proof assistant.

Encoding of FOL Semantics in TLA +

The expression and action fragment of TLA + contains FOL, and the encoding of the semantics in TLA + is straightforward (459 lines of TLA + formulae). Actually, the given FOL formalisation captures the behavior of each of the components of BPMN (nodes which can be events, activities, and gateways), and thus the behavior of the whole BPMN model. This behavior is defined using the concept of tokens which move from nodes to edges (and vice-versa) when specific conditions are fulfilled. The distribution of those tokens (marking) on the elements of the BPMN model describes its state. Hence, the whole behavior is seen as a set of states reachable when specific transitions are fired.

As extensively described before, the idea here is to associate to each node (n) two predicates4 : a first predicate, St(n), which states if the node can start its execution, and thus changing its current marking before its execution (mn (n)) to another marking after its execution (mn' (n)). The second predicate, Ct(n), that states if the node can finish its execution and so change the current marking (mn (n)) before its termination to another marking (mn' (n)) after its termination.

In this context, the TLA + specification of the semantics of node n is nothing but a direct translation of the St(n) and Ct(n) predicates of node n into the TLA + syntax.

Example.

Let us reconsider the semantics of a "none start event" defined through the predicate Ct(n):

∀n ∈ N NSE , Ct(n) def ≡ (mn(n) = 1) ∧ (mn (n) = mn(n) -1)
∧ ∀e ∈ out SF (n), (me (e) = me(e) + 1)

∧   (∃p ∈ N P , (n ∈ R(p)) ∧ (mn(p) = 0) ∧ (mn (p) = 1) ∧ ({n, p} ∪ out SF (n)) ∧ Ξ) ∨ (∃p ∈ N SP , (n ∈ R(p)) ∧ ({n} ∪ out SF (n)) ∧ Ξ)  
This FOL semantics is translated into a TLA + specification as follows.

nonestart_complete(n) ∧ CatN [n] = N oneStartEvent ∧ nodemarks[n] >= 1 ∧ LET p == ContainRelInv(n) IN ∨ ∧ CatN [p] = P rocess ∧ nodemarks[p] = 0 ∧ nodemarks = [nodemarks except ![n] = @ -1, ![p] = 1] ∨ ∧ CatN [p] = SubP rocess ∧ nodemarks = [nodemarks except ![n] = @ -1] ∧ edgemarks = [e ∈ domain edgemarks → if e ∈ outtype(SeqF lowT ype, n) then edgemarks[e] + 1 else edgemarks[e]] ∧ N etwork!unchanged
Intuitively, the translation is done syntactically as shown in Table 2. Here, we can easily observe that the translation is straightforward, and this holds for all the elements of BPMN.

The resulting theories, for the translation of the whole elements, are available at [START_REF] Poizat | fbpmn repository[END_REF] under theories/tla.

Module PWSTypes defines the abstract constants that correspond to the node and edge types. Module PWSDefs specifies the constants that describe a BPMN graph (Definition 2.1): Node (for N ), Edge (for E), Message (for M), CatN (for cat N ), CatE (for

FOL Expression

TLA

+ expression φ 1 cat N (n) = NSE φ 1 CatN [n] = N oneStartEvent φ 2 mn(n) ≥ 1 φ 2 nodemarks[n] >= 1 φ 3 ∀e ∈ out SF (n), (me (e)
= me(e) + 1)

φ 3 edgemarks = [e ∈ domain edgemarks → if e ∈ outtype(SeqF lowT ype, n) then edgemarks[e] + 1 else edgemarks[e] ] φ 4 ∃p ∈ N P , (n ∈ R(p)) ∧ (mn(p) = 0) ∧ (mn (n) = mn(n) -1) ∧ (mn (p) = 1) φ 4 LET p == ContainRelInv(n) IN ∧ CatN [p] = P rocess ∧ nodemarks[p] = 0 ∧ nodemarks = [nodemarks except ![n] = @ -1, ![p] = 1] φ 5 ∃p ∈ N SP , (n ∈ R(p)) ∧ (mn (n) = mn(n) -1) φ 5 LET p == ContainRelInv(n) IN ∧ CatN [p] = SubP rocess ∧ nodemarks = [nodemarks except ![n] = @ -1] φ 6 Ξ φ 6 N etwork!unchanged cat E ), ContainRel (for R).
. . This module also defines auxiliary functions such as in T , defined in TLA + as the operator intype(type, n) {e ∈ {ee ∈ Edge : target(ee) = n} : CatE[e] ∈ type}.

Module PWSWellFormed encodes the well-formedness predicates for BPMN graphs. For instance, the rule C3 (a sub-process has a unique start event node) becomes: The N ext predicate specifies a possible transition between a starting state and a successor state. It is a disjunction of all the actions. The full specification is then, as usual in TLA + , Init ∧ [N ext] var ∧ Fairness, where Init specifies the initial state (Def. 2.3), and [N ext] specifies that N ext (or stuttering) is verified along all the execution steps.

Fairness in Loops and Alternatives

The restriction to fair executions (Section 2.2.6) is naturally translated in TLA + . TLA + supports weak and strong fairness, defined as below for an action A:

W F e (A) def ≡ ♦¬(ENABLED A e ) ∨ ♦ A e SF e (A) def ≡ ♦ ¬(ENABLED A e ) ∨ ♦ A e
Fairness is then a conjunction of weak fairness on all actions (∀n ∈ N ode : W F var (step(n))), and of strong fairness on XOR, OR and EB transitions.

Communication as a Parameter

One of the objectives of our FOL semantics is to be able to specify the communication behavior as a parameter of the verification. To achieve this, all operations related to communication are isolated in a Network module. This module is a proxy for several implementations that correspond to communication models with different properties, such as their delivery order. Generic Communication Models. We provide seven communication models which differ in the order messages can be sent or received, and are all the possible point-to-point models when considering local ordering (per process), causal ordering, and global ordering (absolute time). Their formal description is provided above in section 2.2.4, and their formal analysis and comparison are in [START_REF] Chevrou | On the diversity of asynchronous communication[END_REF].

The state of the communication model is specified with a variable net, whose content depends on the communication model. The communication actions are two transition predicates send and receive which are true when the action is enabled. These actions take three parameters, the sender process, the destination process and the type of message. Their specification depends on the communication model and is a direct translation in TLA + of the FOL formula of table 1. For instance, NetworkFifo specifies a communication model where the delivery order is globally first-in first-out: messages are delivered in the order they have been sent. Its realization is a queue and the two predicates are:

send (f rom, to, m) net = Append(net, f rom, to, m ) receive(f rom, to, m) net = ∧ f rom, to, m = Head(net) ∧ net = T ail(net)
Ad-hoc Communication Models. The communication models described in 2.2.4 are all monolithic. This means that all the communication interactions are handled by the same communication model, and that it restricts the receptions in the same way for all communication channels. In some cases, one needs to have different properties in different parts of a model. For instance, a set of processes can require Fifo All communication for their interactions, while another set does not have any constraint. Using a modular communication framework based on micromodels [START_REF] Chevrou | A modular framework for verifying versatile distributed systems[END_REF], we offer the possibility to implement the send and receive predicates with a combination of micromodels that are applied to subsets of the channels in the BPMN collaboration. The available micromodels are : the seven ordering model as above, that order the receptions with regard to the emission events; a micromodel where priorities are assigned to channels; a message cap micromodel that limits the number of messages in transit; a bounded micromodel that limits the total number of messages that a set of channels can transport in an execution.

Consider the example in Figure 1. This example has an infinite number of states as the travel agency can send an arbitrary number of offer. Moreover, it is required that the NoMore message is received after all the Offer messages. With the monolithic communication models, this can be handled by using the Fifo Pair (or Fifo All) communication model. However, observe that the Confirmation and Ticket messages are expected by the customer in the reverse order of their emissions. Imposing fifo ordering means that the ticket cannot be delivered before the confirmation, and this collaboration with a Fifo communication model is unsound: the customer process deadlocks without reaching the final state.

Using micromodels, we state that all the channels are point-to-point (micromodel "p2p"), and we impose fifo ordering only on Offer and NoMore (micromodel "fifo11").

Moreover, we limit the overall number of offers by limiting the number of messages sent on Offer (micromodel "voting"). Lastly, we can also bound the number of messages in transit (micromodel "message_cap"). This ad-hoc communication model is described as below:

CHANNELS == {"Offer", "NoMore", "Travel", "Payment", "Abort", "Ticket", "Confirmation"} COMMODELS == {[name → "p2p", params → [chan → CHANNELS ] ],

[name → "fifo11", params → [chan → {"Offer","NoMore

Mechanized Verification

A specific BPMN diagram is described by instantiating the constants in PWSDefs (Node, Edge. . . ) from the BPMN collaboration. This is automated using our fbpmn tool. Regarding the well-formedness of the BPMN diagram, the predicates from PWSWellFormed are assumed in the model. Before checking a model, The TLA + model checker checks these assumptions with the instantiated constants that describe the diagram, and reports an error if an assumption is violated. Otherwise, this proves that the diagram is well-formed.

The TLA + model checker, TLC, is an explicit-state model checker that checks both safety and liveness properties specified in LTL. This logic includes operators and ♦ that respectively denote that, in all executions, a property F must always hold ( F ) or that it must hold at some instant in the future (♦F ). TLC builds and explores the full state space of the diagram to verify if the given properties are verified. These properties are generic properties related to any Business Process diagram, or specific properties for a given diagram. Some generic properties are safe collaboration, sound collaboration and message-relaxed sound collaboration [START_REF] Corradini | A classification of BPMN collaborations based on safeness and soundness notions[END_REF].

A collaboration is safe if no sequence flow holds more than one token:

(∀e ∈ E SF , me(e) ≤ 1) (1)
A collaboration is sound if all the processes are sound and there are no undelivered messages. A process is sound if it is in a stable state where there are no tokens on its inside edges, and no tokens on its nodes, except possibly for start and end events.

SoundP roc(p)

def = ∀e ∈ R(p) ∩ E SF , me(e) = 0 ∧ ∀n ∈ R(p) ∩ N, (mn(n) = 0 ∨ (mn(n) = 1 ∧ n ∈ (N EE ∪ N SE ))) Soundness def = ♦ (∀p ∈ N P , SoundP roc(p) ∧ ∀e ∈ E MF , me(e) = 0) (2)
A collaboration is message-relaxed sound if it is sound when ignoring messages in transit, i.e., when ignoring the Message Flow edges.

M sgRelaxedSoundness def = ♦ (∀p ∈ N P , SoundP roc(p)) (3)
Other generic properties are available, such as the absence of undelivered message or the possible activation which states there does not exist a task node (Abstract Task, Send Task, Receive Task) that is never activated in any execution. From a business process point of view, it means that there are no tasks in the diagram that are never used. This is expressed as ∀n ∈ N T : EF(mn(n) = 0) (TLC can check for the invalidity of the negation of this CTL formula).

Last, the user can also define business model properties concerning a specific diagram. For instance, one can check that the marking of a given node is bounded by a constant (i.e., (nodemarks["Confirm Booking"]) ≤ 1), or that the activation of one node necessarily leads to the activation of another node ( (nodemarks["Book Travel "] = 0 ⇒ ♦(nodemarks["Offer Completed "] = 0)).

Termination of the verification is ensured for a finite state model. When the model checker finds that a property is invalid, it outputs a counter-example trace that we animate on the BPM graphical model to help the user understand it. TLC uses a breadth-first algorithm, and this trace is minimal for safety properties. As any BPMN model is structurally finite, a model with an infinite state space is necessarily unsafe (in the sense of (1): some edges hold more than one tokens). This property is invalidated on a prefix of a trace. TLC incrementally checks invariants during the construction of the state space, and an unsafe model will be detected even if it would yield an infinite state space. TLC cannot check arbitrary properties on an infinite state model. Nevertheless, we can use constraints expressed on states or transitions to limit the state space (see Section 6.4.1).

Experiments

Experiments were conducted on a laptop with a 1.9 GHz (turbo 4.8 GHz) Intel Core i7 processor (quad core) with 32 GB of memory. Results are presented in Table 3. The first column is the reference of the example in our archive. The characteristics of a model are: number of participants, number of nodes (incl. gateways), number of flow edges (sequence or message flows), whether the model is well-balanced (for each gateway with n diverging branches we have a corresponding gateway with n converging branches) and whether it includes a loop. The communication model is asynchronous (bag), fifo-ordered between each couple of processes (fifo pair), globally fifo (fifo all), or synchronous-like (RSC).

The results of the verification then follow. First, data on the resulting transition system are given: number of states, number of transitions, and depth (length of the longest sequence of transitions that the model checker had to explore). For each of the three correctness properties presented above, we indicate if the model satisfies it. Lastly, the accumulated time for the verification of the three properties is given. Our tool supports more verifications (see Table 6) and can be easily extended with new properties. We selected these three ones since they are more BPMN specific [START_REF] Corradini | A classification of BPMN collaborations based on safeness and soundness notions[END_REF].

Table 3 presents the results for a selection from our repository [START_REF] Poizat | fbpmn repository[END_REF] for a variety of gateways and activities. These illustrative examples include realistic business process models (001 and 002 two client-supplier models, 040 from Figure 1, 017 from [START_REF] Krishna | Checking business process evolution[END_REF], and 020 from [START_REF] Corradini | Animating multiple instances in BPMN collaborations: From formal semantics to tool support[END_REF]), and models dedicated to specific concerns: termination end events and sub processes (007-011 from [START_REF] Corradini | A classification of BPMN collaborations based on safeness and soundness notions[END_REF]), inclusive gateways (003, 012, 013 and 018), exclusive and event-based gateways (015 and 016).

A first conclusion is that verification is rather fast: the verification of one property generally takes just a few seconds per model, the longest being for model 020 that takes up to 53s of accumulated time for the three properties (5s for the construction of the state space). Experiments also show the effect of the communication model on property satisfaction (models 1, 2, 6, 20), the use of TLA + fairness to avoid infinite loops [START_REF] Chevrou | On the diversity of asynchronous communication[END_REF][START_REF] Lamport | Time, clocks and the ordering of events in a distributed system[END_REF][START_REF] Abadi | The existence of refinement mappings[END_REF][START_REF] Lamport | Real-time model checking is really simple[END_REF], and the use of terminate end events combined with model constraints (see Section 6.4.1) to deal with unsafety [START_REF] Poizat | fbpmn repository[END_REF].

LTL verification is O(M * 2 F ), where M is the size of the state space, and F is the "size" of the formula (the number of involved temporal operators). F is mainly influenced by the number of fairness constraints. Regarding M , in practice, more than the size of the BPMN schemas, interleaving is the main cause of state explosion. Interleaving is directly linked to the number of processes. Thus, more than the number of nodes (which has a limited impact), the verification time is mainly impacted by the number of processes and the branching in them.

The fbpmn Tool Suite

Our FOL formal semantics for communication parametric BPMN collaboration, and the verification of properties, realized over TLA + and the TLC model checker, as presented in Section 5, are implemented in the fbpmn tool suite. This open source, freely available, suite is made up of :

• the fbpmn program and several accompanying scripts, to perform verification in one's command line and to graphically animate counter examples,

• a Web application version of the above, with a client-side front-end (for BPMN modelling and for giving communication and verification parameters) that runs in one's browser, and a server-side back-end verification engine, built around fbpmn and scripts, for which a Docker version is available.

The URL to get fbpmn is https://github.com/pascalpoizat/fbpmn.

Architecture and General Principles

The fbpmn tool suite is centered around a command, fbpmn, that is available for Linux, OSX, and Windows (binaries are available for the first two, the later requiring, for now, a compilation process). This command is used to transform a BPMN model into a TLA + representation of its BPMN Graph (Def. 2.1). fbpmn is also in charge of the computation of the P re N and P re E sets that are used in the semantics of the OR gateways, since these two sets can be structurally computed from the BPMN graph structure. This generated TLA + module is then passed, together with modules for TLA + implementation of our well-formedness rules (Sect. 2.1) and of semantics (Sect. 2.2), to the TLC model checker, as described in the bottom of Figure 34.

In case verification fails, TLC outputs a counter-example in the form of a trace that includes for each step the state of the markings and the communication network (Def. 2.2). In order to ease the interpretation of this by the process designer, fbpmn can also be used to generate an interactive animation of the counter-example, where one can see the marking over the BPMN model and navigate between the steps of the counter example (Fig. 4). The presentation layer for the counter-example animator has been achieved using the Camunda.io javascript library.

New Communication Models

As stated before, we support the most usual communication models to be used as parameters for the BPMN semantics. Still, one may define new models. In order to achieve this, one has to:

1. define the new communication model semantics, say MyNet, in a NetworkMyNet.tla file in the fbpmn TLA + theories directory 2. copy one of the files in the fbpmn configuration directory to a new file NetworkNN-MyNet.tla in the same directory, with NN being a number different from the existing communication models there 3. in the contents of NetworkNNMyNet.tla, change the line of the network implementation definition to refer to the new communication model as defined in step 1.

Related Work

The formalization of the BPMN execution semantics, and on a wider scale the formal study of business processes, is an active field of research. In this section, we discuss the most significant propositions in formalizing BPMN. We then compare our approach to them. In our selection, we focus on two criteria: (1) the use of BPMN as a modelling language for describing the business process; (2) the existence of tooling support for the developed approach. In Table 5, column Transformation artifact shows the formalism in which the BPMN models are expressed, column Tool for transformation presents the supporting tool for applying the approach, and column Tool for verification presents the tool that is used for the verification. The upper part of the table lists approaches dealing only with process diagrams, while the lower part describes approaches dealing with collaboration diagrams.

In the upper part of the table, the discussed approaches formalize a minimal subset of BPMN 2.0: parallel and exclusive gateways, start and end events, and sequence flows. The inclusive gateway is treated only by a subset of these works. All but two approaches rely on a third-party formalism (i.e., they transform the BPMN models to another language) to conduct the verification. Such an idea has the advantage to reuse Other transformations that have been proposed are those from BPMN to workflow models, e.g., Yet Another Workflow language (YAWL) [START_REF] Ye | Formal semantics of BPMN process models using YAWL[END_REF][START_REF] Ye | Transformation of BPMN diagrams to YAWL nets[END_REF]. YAWL is a language with a strictly defined execution semantics inspired by Petri Nets. In [START_REF] Ye | Formal semantics of BPMN process models using YAWL[END_REF][START_REF] Ye | Transformation of BPMN diagrams to YAWL nets[END_REF], the author provide a formal semantics of BPMN models in terms of a transformation to YAWL nets. They use the ILog BPMN Modeler as a graphical editor tool to create BPMN models. They have implemented an open-source transformer plug-in called, BPMN2YAWL, and integrated it into the ProM platform. This tool transforms a BPMN model into a YAWL one and helps to export the YAWL model as an XML file. This XML file then serves as input to a YAWL-based verification tool. As a proof of concept, the tool has been tested using simple models.

In [START_REF] Van Gorp | A visual token-based formalization of BPMN 2.0 based on in-place transformations[END_REF], the authors propose a formalization of BPMN 2.0 based on a set of in-place graph transformation rules. Then, they provide the implementation of their proposition in a framework called GrGen.

Process algebra have also been considered to formalize and verify BPMN processes [START_REF] Wong | A process semantics for BPMN[END_REF][START_REF] Wong | A relative timed semantics for BPMN[END_REF][START_REF] Wong | Formalisations and applications of BPMN[END_REF]. The authors provide a formal semantic model for BPMN using Communicating Sequential Processes (CSP) followed by a refinement procedure for property checking. Two models are provided: the first one presents an un-timed model to facilitate the verification of safety and liveness properties. The second one, an extension of the first model, introduces relative timing information. This allows the modelling of concurrent activities under temporal constraints. The authors illustrate the advantages of their approach by means of case studies. Translated BPMN models can be checked with CSP checking tools such as FDR.

Another line of work aims at using symbolic encodings. In [START_REF] Lam | A precise execution semantics for BPMN[END_REF] for example, the authors give an execution semantics of BPMN elements expressed using linear temporal logic (LTL). The formalization is defined for a large set of elements of BPMN 1.2. This give an unambiguous definition of the execution semantics of BPMN diagrams, and could serve as a basis for the formal analysis of BPMN diagrams, but no tool is presented.

To overcome some issues related to the mapping of BPMN to other formal languages equipped with their own semantics (e.g., non-local effects of BPMN elements such as termination), several recent works have been proposed for verifying BPMN processes based on a direct formalization of its execution semantics.

Rewriting logic and Maude have been proposed to formalize and analyze BPMN processes. In [START_REF] El-Saber | BPMN formalization and verification using Maude[END_REF], the authors provide a formal semantics for a subset of BPMN models and encode it in Maude for verification purposes. They focus on data objects semantics and their use in database-related decision gateways. Besides, they focus on syntactic issues by introducing the notion of well-formed BPMN processes to avoid them. Unlike this work, we support all process models whether with a structured or non-structured topology.

In [START_REF] Corradini | An operational semantics of BPMN collaboration[END_REF], the authors provide an operational semantics for a subset of BPMN models in terms of Labelled Transition Systems (LTS). The authors focused on the collaboration diagram elements. Then, in [START_REF] Corradini | BProVe: Tool support for business process verification[END_REF], they present a verification tool based on the Eclipse IDE, called Business Process Verifier (BProVe). This tool is based on their proposed operational semantics, implemented using Maude. They use the Maude Linear Temporal Logic (LTL) model-checker to verify properties, and support the verification of safety and soundness properties. In [START_REF] Corradini | Animating multiple instances in BPMN collaborations: From formal semantics to tool support[END_REF], the authors extend their formal framework to include multiple instances and data perspectives. They also provide an associated model animator, called MIDA. It may help the process designers to visualize the behavior of their models and debug them.

From another perspective, the standard [START_REF] Kahloul | Business Process Modeling Notation[END_REF] states that a choreography model can be presented through a collaboration. In [START_REF] Decker | Local enforceability in interaction Petri nets[END_REF], the authors consider the interaction of business process with a choreography perspective. They introduce a new formalism called interaction Petri nets that aims at capturing the interaction in BPMN choreographies. This paper only considers synchronous communication while leaving asynchronous communication as an open question.

Discussion. Unlike the mentioned works, we have defined the execution semantics of BPMN models in terms of First-Order Logic, with the objective of defining a generic formal semantics that can be implemented into different languages and tools. Nevertheless, the above mentioned approaches have mainly focused on verifying the control flow of business process models against a correctness criterion. To the best of our knowledge, these approaches do not support verification of BPMN models under a specific, and parametric, communication model. Table 6 complements Table 5 by looking more into detail the BPMN features and properties of interest that are supported by recent works that provide tool support for the verification of collaboration diagrams and communication features in BPMN. This table divides the approaches between those that rely on an intermediary model, and those that have the benefit of providing a direct link between BPMN constructs and the verification formalism. Our work follows this line. Further, the choice of FOL lets one implement the semantics in different tools, e.g., TLA + as here or SMT solvers. As far as the BPMN coverage criteria is concerned, we can observe that we are among the approaches with a high coverage. The use of FOL to define the semantics, and its implementation in TLA + , made it possible for us to implement quite easily correctness checks as temporal logic properties to be checked against the model.

Conclusion & Future Work

In this paper we have proposed a direct formalization in first-order logic for a subset of BPMN that includes sub-process, communication and time constructs. This semantics is parametric with reference to the properties of the communication model, which is of importance since, as seen for example in Table 3, it has an impact on the properties a BPMN model fulfils or not. Together with time, the support for distinct communication models is useful when it comes to use the BPMN standard in contexts such as the IoT [START_REF] Casati | Towards business processes orchestrating the physical enterprise with wireless sensor networks[END_REF][START_REF] Meyer | The things of the Internet of Things in BPMN[END_REF]. Based on a realization of the first-order logic semantics into TLA + , and the use of the TLC model-checker, we provide business process designers with tool support in order to check domain-specific properties (dedicated either to workflow notations in general, or to BPMN in particular) and animate counter-examples in order to fix erroneous models.

Even if we have provided users with an integrated Web application where one can model, check, and debug business process models, a direct perspective of our work is to integrate it as a plug-in in more general purpose platforms for business processes, such as Apromore [START_REF] Apromore | [END_REF] or ProM [START_REF]Process mining framework (ProM)[END_REF].

An ongoing work is the replacement of parameterization using a global communication model (here one in a choice of seven) by a more fine-grained solution based on the communication framework we have developed in [START_REF] Chevrou | A modular framework for verifying versatile distributed systems[END_REF]. This would support, for example, the definition of communication policies per participant, per couples of communicating participants, or using delivering priorities over the messages in transit.

For now, time is dealt with fixed values in the model (e.g., the duration of task t is 5 units of time, or after a timeout of 15 units of time run some specific subprocess). The extension of parameterization is also interesting as far as time is concerned. This would mean replacing the fixed information about time with intervals (bounded values) or variables (free values). Some collaborations may fulfil properties depending on constraints over the time at which processes are run, or over durations of tasks and timeouts. Retrieving such constraints from the models one verifies, in a synthesis approach, would have an added-value for the business process designers.

Some features that play a role in full-fledged executable collaborations have been discarded here. This is the case of the data (data objects, data stores, assignments, and message payloads) and multi-instance (for activities and pool lanes) constructs.

As far as data are concerned, a direct (and usual) solution is to extend the notion of state with a substitution from variables to values, indexed by process types or process identifiers in case of multi-instance support. This is indeed what we already did for the communication medium (the "substitution" in this case being limited to a single variable, mnet). Lets say that the substitution for data is σ. An assignment such as var := term in a process p would then be supported by adding a clause σ p = σ p var → eval σp (term) in the completion rule for tasks, with σ var → val denoting the update of a substitution σ associating value val to variable var, and eval σ (term) the evaluation of term wrt. σ (that gives values to the free variables in term). Accordingly, the conditions in exclusive and inclusive gateways can also be treated by requiring that their evaluation yields true, i.e., for a condition c, eval σp (c) = true. The treatment for unbound data (e.g., if one wants to verify a process whatever the initialization of the data objects is, or with data stores whose content is unknown), is however much more complicated. This could be tackled using approaches based on symbolic verification techniques [START_REF] Nguyen | A symbolic framework for the conformance checking of valuepassing choreographies[END_REF][START_REF] Li | VERIFAS: A practical verifier for artifact systems[END_REF][START_REF] Durán | Symbolic specification and verification of data-aware BPMN processes using rewriting modulo SMT[END_REF][START_REF] Calvanese | Formal modeling and SMT-based parameterized verification of data-aware BPMN[END_REF][START_REF] Ghilardi | Petri nets with parameterised data -modelling and verification[END_REF].

The support for multi-instance constructs requires also a specific treatment. There, the tokens would have to carry process identifiers and our marking functions (mn and me, yielding a value in N) would have to yield a value in a bag (multi-set) of the type for process identifiers. This would be reflected in the semantic rules for the BPMN constructs, e.g., for a merging parallel gateway, one would no longer require that each input edge has at least one token (me(ei) ≥ 1 in the rule for AND, page 21) but instead that each input edge has at least one token for a process identifier of interest. Further, the support for multi-instance BPMN features not only for processes (pool lanes) but also for activities (sub-processes and tasks) would possibly require that the type for process identifiers has a specific indexed structure.

The interplay between data and multi-instance constructs also adds a degree to the complexity of the semantics, as, e.g., data are used in message payloads and a part of these payloads are used as a correlation mechanism. Few approaches are able to deal with data, multi-instance activities and multi-instance pool lanes [START_REF] Van Gorp | A visual token-based formalization of BPMN 2.0 based on in-place transformations[END_REF][START_REF] Corradini | Animating multiple instances in BPMN collaborations: From formal semantics to tool support[END_REF].

Finally, a last perspective, that goes in the direction of spreading the use of lightweight formal verification for BPMN models, is related to the termination of verification. As we have seen, with our proposal, for some models and some properties, one has to bound the (construction of the) semantic state space using constraints. A perspective would be to identify fragments of the formal model for which termination is ensured, and ones for which changes in the BPMN model or bounding constraints are required. Work in

Figure 1 :

 1 Figure 1: Travel agency case study (extended from an example in [5]).

Figure 2 :

 2 Figure 2: BPMN subset being supported in our work, with types used in the formalization (e.g., MSE stands for Message Start Events and SE for Start Events).

1 Figure 3 :

 13 Figure 3: Completing behavior of a None Start Event. Before (left) and after (right) application of the Ct rule.

1 Figure 4 :

 14 Figure 4: Completing behavior of a Message Start Event. Before (left) and after (right) application of the Ct rule.

Figure 5 1 Figure 5 :

 515 Figure 5: Starting behavior of None End Event. Before (left) and after (right) application of the St rule.

1 Figure 6 :

 16 Figure 6: Starting behavior of a Terminate End Event. Before (left) and after (right) application of the St rule.

1 Figure 7 :

 17 Figure 7: Starting behavior of a Message End Event. Before (left) and after (right) application of the St rule.

1 Figure 8 :

 18 Figure 8: Starting behavior of an Abstract Task activity. Before (left) and after (right) application of the St rule.

Figure 9 1 Figure 9 :

 919 Figure9shows its completing behavior. It consumes the token from itself and generates one on its outgoing edge e2.

Figure 10 :

 10 Figure 10: Starting behavior of a Sub-Process activity. Before (left) and after (right) application of the St rule.

Figure 11 :

 11 Figure11: A Sub-Process activity not ready to complete: a token is still present on one of its edges.

1 m1Figure 12 :

 112 Figure 12: Starting behavior of a Send Task activity. Before (left) and after (right) application of the St rule.

1 Figure 13 :

 113 Figure 13: Completing behavior of a Send Task activity. Before (left) and after (right) application of the Ct rule.

1 m1Figure 14 :

 114 Figure 14: Completing behavior of a Receive Task activity. Before (left) and after (right) application of the Ct rule.

1 Figure 15 :

 115 Figure 15: Starting behavior of a Throw Message Intermediate Event. Before (left) and after (right) application of the St rule.

Figure 16 :

 16 Figure 16: Starting behavior of a Catching Message Intermediate Event. Before (left) and after (right) application of the St rule.

1 Figure 17 :

 117 Figure 17: Starting behavior of an interrupting Message Boundary Event (task case). Before (left) and after (right) application of the St rule.

Figure 18 :

 18 Figure 18: Starting behavior of an interrupting Message Boundary Event (sub-process case). Before (left) and after (right) application of the St rule.

Figure 19 :

 19 Figure 19: Completing behavior of a splitting Parallel Gateway. Before (left) and after (right) application of the Ct rule.

1 Figure 20 :

 120 Figure 20: Completing behavior of a merging Parallel Gateway. Before (left) and after (right) application of the Ct rule.

1 Figure 21 :

 121 Figure 21: Completing behavior of an Exclusive Gateway. Before (left) and after (right) application of the Ct rule.

Figure 22 :

 22 Figure 22: Completing behavior of an Event-Based Gateway. Before (left) and after (right) application of the Ct rule.

1 ORFigure 23 :

 123 Figure 23: Non activable Inclusive Gateway. It has to wait for the token on e2 which is in P re E (OR, e6) and P re E (OR, e7).

• is the empty sequence •

 sequence head : Seq[T ] → T : head of a sequence • tail : Seq[T ] → Seq[T ] : tail of a sequence • append :Seq[T ] × T → Seq[T ] : append an element at the end of a sequence • ⊕, : Bag[T ] × Bag[T ] → Bag[T ] : union and difference of bags

  rom, to, m) def ≡ mnet = append(mnet, f rom, to, m ) receive(f rom, to, m) def ≡ f rom, to, m = head(mnet) ∧ mnet = tail(mnet)

If a message m 1 Figure 24 :

 124 Figure 24: A Non-Causal Execution. The emission of the proposal causally precedes the emission of the description which causally precedes the emission of the quote. Then the quote cannot be consumed before the proposal on the client in the causal communication model.

Figure 25 :

 25 Figure 25: Use of strong fairness to avoid infinite loops (left) and starvation (right).

1 1 5 Figure 27 :

 1527 Figure 27: Completing behavior of a Timer Start Event.

Figure 28 :

 28 Figure 28: Starting behavior of a Timer Intermediate Catch Event.

Figure 29

 29 Figure 29 presents the starting behavior of timeOut. The left-hand side of the figure shows that timeOut is ready to start (i.e., the task CB -payment has a token and the local clock of timeOut meets its deadline). The right-hand side of the figure shows that timeOut starts by cancelling the CB -payment task and generating a token on its outgoing edge (e4).

Figure 29 :

 29 Figure 29: Starting behavior of an interrupting Timer Boundary Event.

Figure 30

 30 Figure 30 presents the starting behavior of timeReminder. The left-hand side of the figure shows that timeReminder is ready to complete (i.e., CB -payment has a token and the local clock of timeReminder meets its deadline). The right-hand 34

Figure 30 :

 30 Figure 30: Starting behavior of a non-interrupting Timer Boundary Event.

Figure 31 :

 31 Figure 31: Completing behavior of an Event-Based Gateway: a message is ready to be received.

Figure 32 :

 32 Figure 32: Completing behavior of an Event-Based Gateway: the timer is ready to fire.

Figure 33 :

 33 Figure 33: BPMN diagram with deadlock.

Definition 4 . 3 (Definition 4 . 4 (Definition 4 . 5 ( 1 ) 4 . 6 (

 434445146 No dead activities). An activity is dead if no execution activates it.N oDeadActivitiesdef ≡ ∀a ∈ N A , ∃σ ∈ Exec, ∃i ∈ domain(σ), σ[i].mn(a) = 0 Undelivered messages). No messages are left in transit. N oU ndeliveredM essages def ≡ ∀σ ∈ Exec, ∃i ∈ domain(σ), ∀j ∈ domain(sigma), j ≥ i =⇒ ∀e ∈ MF, σ[j].me(e) = 0 Safe process). A process is safe if and only if all its sequence flow edges never hold more than one token during their execution. For p ∈ N P , Saf eP r(p) def ≡ ∀σ ∈ Exec, ∀i ∈ domain(σ), ∀e ∈ R(p) ∩ E, (σ[i].me(e) ≤ Definition Safe Collaboration). A collaboration is safe all its processes are safe. Saf e def ≡ ∀p ∈ N P , Saf eP r(p) Definition 4.7 (Process soundness).

  C3_SubP rocessU niqueStart ∀n ∈ N ode : CatN [n] = SubP rocess ⇒ Cardinality(ContainRel[n] ∩ {nn ∈ N ode : CatN [nn] ∈ StartEventT ype}) = 1 Last, module PWSSemantics contains the semantics. It defines the variables for the marking: nodemarks (∈ [N ode → N at]), edgemarks (∈ [Edge → N at]), and net (whose type depends on the selected communication model). Then it contains a translation of the FOL formulas, where each rule yields one TLA + action, translated from the FOL semantics as explained above.

Figure 35 :

 35 Figure 35: fbpmn Web application (modelling and verification panel).

Figure 36 :

 36 Figure 36: fbpmn Web application (verification results).

-

  The start event type (SE ) groups the none start event (NSE ), the message start event (MSE ), and the timer start event (TSE ) types. Formally: SE = {NSE, MSE, TSE}. -The intermediate event type (IE ) groups the catch message intermediate event (CMIE ), the throw message intermediate event (TMIE ), and the timer intermediate catch event (TICE ) types. Formally: IE = {CMIE, TMIE, TICE}. -The boundary event type (BE ) groups the message boundary event (MBE ) and the timer boundary event (TBE ) types. Formally: BE = {MBE, TBE}. Both indeed regroup interrupting and non-interrupting versions. A function, isInterrupt (Def. 2.1), is used to make the difference.

-The end event type (EE ) groups the none end event (NEE ), the terminate end event (TEE ), and the message end event (MEE ) types. Formally: EE = {NEE, TEE, MEE}.

  OR} , (∀e ∈ out SF (n), e ∈ E {CSF,DSF} ) ∨ (∀e ∈ out SF (n), e ∈ E NSF )

	• (C16) Message flows connect the throwing elements (send task, message end event, throw message intermediate event) with catching elements (receive task, message start event, catch message intermediate event, message boundary intermediate event):
	∀e ∈ E MF , source(e) ∈ N {ST,MEE,TMIE} ∧ target(e) ∈ N {RT,MSE,CMIE,MBE}
	• (C17) Message catching elements must have at least one incoming message flow edge: ∀n ∈ N {RT,MSE,CMIE,MBE} , |in MF (n)| ≥ 1
	• (C18) Message throwing elements must have at least one outgoing message flow edge: ∀n ∈ N {ST,MEE,TMIE} , |out MF (n)| ≥ 1

Table 1 :

 1 Encoding of the network models in first-order logic.

  Figure 26: Timer Boundary Event with an impossible timeout. As the timeout on task1 is later than the date imposed by the timer intermediate catch event, this timeout should never fire and task2 should never be activated.3. Timer Boundary Event (TBE ): a TBE is non-deterministically activated, without fairness (it may never fire). Its semantics is close to a Message Boundary Event (MBE), without the constraint on the presence of a message.

	e1	e2	task1	e3
	me (eo) = me(eo) + 1) task2 nee1 nee2 e5 2011-08-14 e4 T 11:00 ∧ ({ei, eo}) ∧ Ξ P nse 2011-08-14 T 12:00 St interrupting (n, act) def

Table 2 :

 2 Translation between FOL and TLA + (NSE example).

Table 3 :

 3 Experimental Results.

Table 5 :

 5 Verification tools in the literature.

	Diagram Features Transformation artifact Process PN Kripke structure Data PN LTL Markov decision process [31], [32] References [27] [28] [29] [30] WF-nets [33] LNT (LOTOS) [34][35] Time Maude source code [36],[37] CPN [38]	Year 2011 2013 2014 2014 2016 2016 2017 2017-2018 2019	BPMN Tool for transformation Tool for verification 1.0 InFlux Woflan , LoLA 2.0 BPMN2SPIN EpiSpin 2.0 BPMN2PN prototype LoLA 2.0 BPVSL -2.0 SBOAT PRISM 2.0 InFlux WFlan 2.0 VBPMN CADP 2.0 BPMN-P Maude Checker 2.0 GROOVE CPN Tool
	Collab.	Time Data Time	PN YAWL CSP LTL Graph rewriting rule Maude source code RECATNets LTS CPN TPN	[39], [7] [40], [41] [42, 43, 44], [45], [46] 2008-2012 2007-2008 2008-2010 [47] 2012 [48], [49] 2010-2013 [50] 2014 [51], [52] 2016-2017 [53], [54] 2017-2018 [8], [55] 2018-2019 [23] 2019	1.0 1.0 2.0 2.0 2.0 2.0 2.0 2.0 2.0 2.0	Transformer BPMN2YAWL BTRANSFORMER Prototype GrGen Prototype BPMNChecker BProve CP4BPMN Transformer	ProM -FDR2 --Maude checker Maude Maude checker CPN Tool -

This is indeed a simplification for this introduction. The semantics as defined in the standard and hence as supported in our work is a bit more complex, see Section

2.2.

We recall that the semantics for time-related constructs is the focus of Section

3, hence we extend the definition of event-based gateways to support time-related events there.

A vector clock is a logical clock that tracks the causal dependencies between send and receive events. They are not to be confused with the clocks used for timing constraints in Section 3.3.

In some cases, the behavior is described using only one of the two predicates.

Table4: Animation of a counter-example (model in Fig.1, for soundness with Fifo Inbox mode) generated with fbpmn.

$ This work was supported by project PARDI funded by the French National Agency for Research under grant ANR-16-CE25-0006.

Desktop Modelling and Verification

Since for a given model one may have different properties of interest (e.g., safety, soundness, and message-relaxed soundness), and since several communication models are possible (e.g., the seven ones presented in Sect. 2.2.4), it would be tedious to run fbpmn for each of the combinations. Hence, we provide the process designer with scripts (only under Linux or OSX) that ease verification.

When the designer launches the fbpmn-check script (upper part of Fig. 34), it reads a configuration directory and runs fbpmn based on the designer preferences. Let us suppose the configuration directory is as follows. This will yield four different properties to be checked for seven different network models, generating at most 28 counter-example traces. Running the fbpmn-logs2html script on a working directory generated by fbpmn-check, finds out these counter-examples and generates an interactive animator for each of them. It is also possible to give fbpmncheck a number of cores to use, this value being passed to the TLC model checker.

Online Modelling and Verification

In order to ease the use of the fbpmn tool suite, we have implemented a Web application for it (Fig. 35). There, the user can import, design, or export a BPMN model (this is achieved using the Camunda.io framework). Then verification parameters can be given: which properties to check, which communication models to check with, possibly model constraints (see below) for nodes and/or edges.

After retrieving the results (Fig. 36) the user has the possibility to see a textual version of counter-examples and/or to animate it on the model as presented in Sect. 6.1.

The fbpmn Web application is available at http://vacs.enseeiht.fr/bpmn/ for demonstration purposes. Yet, if one is interested in it, we advocate the deployment of it on one's own machine or server. For this, we provide a Docker image, downloadable from our Web application.

Extensibility

Our framework can be extended as far as safeness constraints, properties to check, and communication models are concerned.

Model Constraints

Some models are unsafe, i.e., the semantics can yield an infinite marking on some node(s) or edge(s). In such a case, one may rely on model constraints associated to the BPMN model to be verified. Given the model is model.bpmn, one just has to create a file model.constraint of the form:

CONSTANT ConstraintNode <-<ConstraintOnNodes> ConstraintEdge <-<ConstraintOnEdges> Constraint <-<Overall constraint in terms of ConstraintNode and ConstraintEdge> Some node constraints and edge constraints are already defined in our TLA + library, e.g., the one to state that an edge should have at most 2 tokens on it, MaxEdgeMarking2, or the one to limit the number of tokens only on message edges MaxMessageEdgeMarking2.

The most usual constraint combinator is also already defined there, ConstraintNodeEdge, that is the conjunction of the user specified node and edge constraints. Using this, we may verify model 006 (as seen in Sect. 5.6), defined in file e006TravelAgency.bpmn, with a file e006TravelAgency.constraint:

The user is free to extend our constraint library by extending the PWSConstraints.tla TLA + module.

New Properties

We support several properties from the literature. However, it is possible to extend this set. To do so, one has to:

1. define a new property, say MyProperty, at the end of the main TLA + semantic module, PWSSemantics.tla 2. create a new file PropNNMyProperty.cfg in the fbpmn configuration directory, with NN being a number different from the existing properties there 3. in the contents of PropNNMyProperty.cfg refer to the property name given in step 1.

The definition of new properties has some limitations. First it must be possible to define them using LTL since this is the logic that is verified by TLC. Second, these properties must cope with our definition of state (Def. 2.2), i.e., they can be defined in terms of node markings, edge markings, and/or network markings. Properties can also refer to the types of the nodes and edges, as demonstrated in Sect. 5.5 for the soundness property.

the existing results and tools with a minimal effort, but has the main drawback of being very restrictive with respect to the execution semantics of the target formalism.

From a time-related perspective, we consider the approach of [START_REF] Durán | Verifying timed BPMN processes using maude[END_REF][START_REF] Durán | Stochastic analysis of BPMN with time in rewriting logic[END_REF] to be very promising. First, it implements a pure semantics to BPMN without using any transformation. Second, it can deal with time constraints of the model using high level stochastic expressions. However, the approach extends the behavior of the standard BPMN elements (e.g., timeouts for tasks and delays for sequence flow, probabilities to various forms of branching behavior in gateways) to treat the time constraints, and did not stick to the actual behaviors defined in the standard. With respect to our work, we provide a semantics for the timer BPMN elements as they are expressed in the standard.

The bottom part of the table presents work closer to ours with regard to the supported BPMN elements. Some works are based on a transformation approach, while others provide a direct formalization semantics.

Petri nets are used to formalize and verify correctness and soundness properties of BPMN in several works. Among them, the earliest work that we identified is [START_REF] Dijkman | Semantics and analysis of business process models in BPMN[END_REF]. The authors propose a transformation from BPMN 1.2 into Petri nets models. They have chosen the ILog BPMN Modeller as a graphical editor to create BPMN models. The authors apply the defined transformation approach on BPMN models and export the resulting Petri net in the form of a PNML file. Then, they use the resulting files as input for the verification tool to statically check the semantics of BPMN models. With the ProM framework, soundness is verified, as well as other properties such as dead transitions, deadlocks, and livelocks. Even if the work deals with collaboration elements, the formalization as Petri nets suffers from limitation for the presentation of the communication, the hierarchical relation between processes and sub-processes, and the verification of internal activities within them. Recently, the work in [START_REF] Combi | A modular approach to the specification and management of time duration constraints in BPMN[END_REF] has extended the approach of [START_REF] Dijkman | Semantics and analysis of business process models in BPMN[END_REF] to timed Petri nets to be able to express time constraints for activities, process regions, and timer events. Besides, they tackle the detection and management of constraint violations at run-time. The authors propose this formal model to analyze the soundness of the collaboration and of its temporal constraints. However, no formal verification of these properties is given.

In [START_REF] Dechsupa | Transformation of the BPMN design model into a colored Petri net using the partitioning approach[END_REF], the authors present a transformation approach of BPMN models into colored Petri nets (CPN). They have developed a tool called Coloured Petri net for BPMN design (CPN4BPMN) to automatize the transformation. Their approach is defined trough two phases: before applying the transformation, a BPMN design tool (such as the BPMN 2.0 Designer of the Eclipse IDE) is used to partition a BPMN model into sub-models. Then, they use the sub-models as input for the CPN4BPMN tool to generate the corresponding CPN model. Even if their work covers a large set of BPMN elements, (e.g., the boundary events, sub-processes, communication elements), the message exchanges are not specified. Indeed, the partitioning technique does not support unstructured BPMN models.

In [START_REF] Kheldoun | Specification and verification of complex business processes -a high-level Petri net-based approach[END_REF][START_REF] Kheldoun | Formal verification of complex business processes based on high-level Petri nets[END_REF], the authors present a formal verification approach for BPMN based on high-level Petri nets, called RECATNets. The authors provide a prototype to perform the automatic transformation from BPMN to RECATNets. Then the obtained RECATNets are translated into rewriting logic terms, and the Maude model-checker is used to verify proper termination and some other LTL properties. In the papers, no information about the communication model is given, and only a small set of BPMN elements is covered. Besides, no benchmarking is given, and the approach is illustrated through three simple examples. the field of combining control and data perspectives in business process modelling, and performing verification on such expressive models, could be an inspiration here, following what has been done for Data-Aware BPMN [START_REF] Calvanese | Formal modeling and SMT-based parameterized verification of data-aware BPMN[END_REF] and for Catalog Nets [START_REF] Ghilardi | Petri nets with parameterised data -modelling and verification[END_REF].