Rim Saddem-Yagoubi

Pascal Poizat
email: pascal.poizat@lip6.fr

Sara Houhou
email: sara.houhou@lip6.fr

Business Processes Meet Spatial Concerns: the sBPMN Verification Framework

Keywords: Business Processes, Spatial Concerns, Formal Semantics, Verification, Tool, BPMN, First-Order Logic, TLA +

BPMN is the standard for business process modeling. It includes a rich set of constructs for control-flow, inter-process communication, and time-related concerns. However, spatial concerns are left apart while being essential to several application domains. We propose a comprehensive extension of BPMN to deal with this. Our proposal includes an integrated notation, a first-order logic semantics of the extension, and tool-supported verification means through the implementation of the semantics in TLA + . Our tool support and our model database are open source and freely available online.

Introduction

The Business Process Model and Notation (BPMN) [START_REF]Business Process Modeling Notation[END_REF] is the de facto standard notation for the modeling of business processes. This rich notation includes features to support different aspects to be taken into account when designing a process model. This includes, among others, specifying the control flow, the inter-process communication, and time-related concerns.

Yet, a conventional process model may suit one's needs in a given context and not in other ones (think of rules for allowing, or not, attendance to conferences based on the COVID-related status of the hosting country). A context sensitive approach to business process modeling also offers the ability to adapt the process behaviours to changing contexts [START_REF] Saidani | Towards context aware business process modelling[END_REF]. Coined by Schilit and Theimer [START_REF] Schilit | Disseminating active map information to mobile hosts[END_REF] in 1994, the term "context" has been given a generic definition by Dey [START_REF] Dey | Understanding and using context[END_REF] in 2001 as "any information that can be used to characterize the situation of an entity".

Transferring this definition to the business process management domain, a useful definition of a business process context could be "the minimum set of variables containing all relevant information that impact the design and execution of a business process" [START_REF] Rosemann | Context-aware process design exploring the extrinsic drivers for process flexibility[END_REF]. Saidani and Nurcan further identify in [START_REF] Saidani | Towards context aware business process modelling[END_REF] four important kinds of contexts: location, time, resource, and organisation-related contexts. As a contextual factor, location is widely discussed as part of research related to mobile applications and it has wider implications for process management [START_REF] Rosemann | Context-aware process design exploring the extrinsic drivers for process flexibility[END_REF].

Without a first-class treatment for the location context in process modelling, one would have to rely on an abstraction of it, e.g., using non-determinism to model conditional branching based on the current state of this context. This is known to yield over-approximation issues. For illustration purposes, let us suppose a process where a robot has to treat rooms in a power-plant or fields in a farm. For this, one relies on a looping workflow pattern, where the robot performs several tasks while there is still at least a place to deal with. Our case study, below, is an instance of this. With support for the location context, it is possible, first, to represent the state of the world (the power-plant rooms or the fields, and their status) and, second, to exit the loop when all places have been treated. Without this support, the fact that there is still, or not, a place to deal with would be modelled using non-determinism. One would then have a possible infinite run, where there is always a place left to treat, making it impossible to perform verification without using bounded analysis (up to some length of runs) or fairness constraints. In line with this, we focus here on the impact of the location-related context in the design and the execution of business processes.

Contributions. Our contributions in this direction are threefold. First, (1.) we propose an extension of the BPMN standard notation in order to take into account location-related (which we call spatial) concerns, (2.) we define a formal execution semantics for this extension, and (3.) we provide the process designers with tools for the automated verification of their extended process models.

With respect to (1.), we support the modeling of control flows based on location constraints, of process mobility, and of the action of processes on their environment. In this work we assume that only the processes at hand have the possibility to change this environment (i.e, the environment cannot independently evolve). We made the choice to extract the specification of the location-related context into a specific structure that is then attached to the process model for verification. This makes the modelling of processes more generic, maintainable, and extensible as one can very simply change the context of use of a process to see the impact on its correctness. This structure, that we call space structure, describes all components of a location context: places (called basic locations), possible moves between places, and logical groups of places (called group locations) that can evolve over time and with the action of the processes. All our extensions rely on the standard BPMN extension mechanisms. The usual process design tools can hence be used to model extended processes (in practice, we use Camunda for this). Our extensions can be "forgotten" by verification or execution tools not supporting them. But using our own tooling (see below, 3.) Fig. 1: BPMN subset being supported. Extension points are colored in green.

the process designers will be able to go beyond standard BPMN verification and check also models in presence of location extensions.

With respect to (2.), we follow the approach in [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF] and extend its first-order logic execution semantics for BPMN6 towards taking into account our extensions. This is achieved structurally on the different extension constructs (space structure initial configuration, processes initial locations, extended inclusive and exclusive gateways, tasks for process mobility or for acting on the context).

With respect to (3.), our approach is based on two steps. An extended process model is first transformed into a TLA + representation of it. Then, given this representation and the TLA + implementation of the (2.) semantics, the modelchecker from the TLA + tool-suite is used to perform verification of both standard process properties (safety, soundness) and location-related ones. Our tools and the models we use for evaluation are open source and available online [START_REF] Poizat | fbpmn repository[END_REF].

BPMN Primer. The subset of BPMN that we support is given in Figure 1. The main instrument to control the flow in processes are gateways. Parallel gateways (AND) require that all incoming flows are active and give control to all outgoing flows. Exclusive (XOR) and event-based (EB) gateways only require one of the incoming flows to be active and activate only one of the outgoing flows based either on a condition (for XOR) or some event (for EB, here message reception). The inclusive gateway (OR) has a more complex semantics. First, several outgoing flows can be activated at a time, based on conditions. Second, it requires that the maximum possible number of incoming flows are active (this may require waiting for some time before more incoming flows are activated, even if one is already active). Inter-process message-based communication can be achieved using send tasks (ST) or message throwing events (MEE at the end of a process, TMIE otherwise), and receive tasks (RT) or message catching events (MSE at the start of a process, CMIE otherwise). Activities are subject to boundary events either interrupting or not (the former interrupt the activity, the latter activate some flow branch without interrupting the activity). We refer the reader to [START_REF]Business Process Modeling Notation[END_REF] for more detailed information on the BPMN notation and to [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF] for more discussion on the, complex, inclusive gateway.

Case study. Figures 2 and3 present the case study we use to illustrate our proposal and to perform verification. The outcomes of verification on more examples are synthesized in Section 3. This model is a simplified version of a collaborative process model where a controller (Controller), a crop planting robot (Planter), and a watering robot (Sprayer, not taken into account here) have to plant crops and water several fields spread over both banks of a river. The context of the collaboration is the river and its banks, with three different instances given in Figures 2a-2c. Places (basic locations) are either fields (F1 to F6), river (R1 and R2), bridge (B), or mountain (M). There is also the base (base) from which our collaboration peers will operate and move. Over these places we may define logical groups of locations (of simply, group locations) for the places where to plant crops (toPlant), the places to water (toWater), the places with crops (planted), and the watered places (watered). Finally, we have possible moves around the location context, based on roads and bridge. All together, basic locations, group locations, and possible moves, make up possible space structures to be associated to location-aware processes. Please note that in practice the location structures are of course not denoted using pictures but rather as a set of information extending the BPMN element for the process collaboration: <bpmn:collaboration id="s006Robots2"><bpmn:extensionElements> <camunda:properties> <camunda:property name="base-locations" value="[base,F1,F2,F3,F4,F5,F6,R1,R2,B,M]" /> <camunda:property name="group-locations"

value="[toPlant,planted,toWater,watered]" /> <camunda:property name="transitions"

value="[(base,F1),(F1,base),(F1,F2),(F2,F1),(F2,F3),...,(M,F6)]" /> <camunda:property name="initial-space" value="{toPlant:[F1,F2,F3,F4,F5,F6], planted:[], toWater:[], watered:[]}" /> </camunda:properties> </bpmn:extensionElements></bpmn:collaboration> Fig. 3: Crop planting collaboration.

In Figure 3 we have a BPMN collaboration that has been extended with the extensions we propose. In green we show which elements are extended (in addition to the whole collaboration, as seen before, and the processes' pool lanes extended to denote where the processes start). In blue we use notes to give, as comments, extensions that are indeed also stored as extension elements in the XML source BPMN file. We remind that since we use BPMN extension mechanisms, these extensions can be directly entered in BPMN design tools. The whole model (diagram and source file, with extensions) is available from [START_REF] Poizat | fbpmn repository[END_REF].

The controller starts by activating the planter. It then checks if there are still some places where to plant crops. If so it sets znc to be any of these. In our extension checking some location-related constraint and setting accordingly a location variable is done at once using a space condition, znc: any toPlant (set znc to be any of the places in group toPlant). Then the controller sends a message to the planter ordering it to get there and waits to receive either an acknowledgement or the information that there is some problem. In the first case the controller registers that the place is now planted using an update action, removing znc from group toPlant and adding it to groups planted and toWater. If there is a problem, then the controller interrupts the planter and stops.

On its side, the planter starts upon activation by the controller and, after starting its engine, it enters the in operation sub-process. In this sub-process, it loops on receiving an order to move (it has then access to the shared znc information), checking if znc can be reached from its current location (using reachable, denoting places that are reachable, in the space condition _: any znc and reachable), and accordingly either moving to znc using a move action and sending an acknowledgement to the controller, or signalling a problem. Upon interruption by the controller, the loop stops and the planter tries to get back to the base (again, using a space condition to check if this is possible).

We were able to model spatial concerns in our collaboration. But what about correctness? Can the collaboration processes reach termination (black circles in the rightmost part of Fig. 3)? Are all fields planted at the end? Let us consider the contexts. If the planter starts on the right bank then the left one cannot be planted due to the one-way bridge (Fig. 2a). If the planter starts on the left bank (Fig. 2b) or if the bridge is two-way (Fig. 2c) then all fields can be planted.

This case study illustrates several points. First, a process model can operate on (or be adapted to) different space structures. Conversely, a space structure can be used with many processes (we have used one with several variants of the crop planting collaboration). This is made possible by separating the specifications of the context and of the processes, and then integrating them. Further, we have seen that, switch two variants of a process or two variants of a space structure and correctness may no longer hold. In the sequel we will see how to give a formal semantics to our extensions and support their verification using tools.

Outline. The formal part of the paper is developed in Section 2, addressing the presentation of the models underlying the semantics, and then the semantics itself. The implementation of the semantics in TLA + , verification, and evaluation are then presented in Section 3. This section also includes a short introduction to the TLA + language and verification framework. Related work is given in Section 4, and we end with conclusions and perspectives in Section 5.

Formal Semantics

In this section, we first give the formal models for extended BPMN diagrams. Then, we present their formal semantics. It follows the "token game" given (in natural language) in chapter 13 of the standard [START_REF]Business Process Modeling Notation[END_REF] and builds on the semantics for basic BPMN given in [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF]. Hence, we will focus on points of extensions only.

Formal Models for Space BPMN

As we have seen earlier, space structures represent contexts with base locations, group locations, and possible moves. Hence the following definition. Notation. In the sequel, definitions are taken given a space structure S = (B, G, →) and a set of variables V such that V ∩ L = ∅.

Space formulas are used to denote a subset of the base locations (see their interpretation in Def. 10). They are central to our extension as they are used both in conditions on conditional sequence flows (CSF) and in mobility actions.

Definition 2 (Space Formula). The set of (space) formulas over S and V, denoted by F orm, is the smallest set generated by {true, v, b, g, not f ,

f 1 or f 2 , here, reachable} for v ∈ V, b ∈ B, g ∈ G, and f, f 1 , f 2 ∈ F orm. Further, f 1 and f 2 is defined as not (not f 1 or not f 2 ).
Space actions are extensions of BPMN (abstract) tasks that can represent either a move or the update of the context by some process. Additionally, we use a specific pass action for tasks that are not related to the spatial concerns.

Definition 3 (Space Action). The set of (space) actions over S and V, denoted by Action, is the smallest set generated by {move(f

), update(u, G -, G + ), pass} for f ∈ F orm, u ∈ V, G -⊆ G, G + ⊆ G, and G -∩ G + = ∅.
Informally (the formal semantics is given in Def. 11), move(f ) denotes that the process of interest moves to a location satisfying f and update(u, G -, G + ) denotes the update of the context by removing some locations (retrieved by evaluating u) from all groups in G -and adding them to all groups in G + .

We may now give definitions for processes, which are represented using graphs with typed nodes and edges. Types correspond to the BPMN elements (see Fig. 1, e.g., XOR for exclusive gateways): T N odes = {AT , RT , ST , N SE, M SE, T SE, CM IE, T M IE, T ICE, M BE, T BE, N EE, T EE, M EE, AN D, OR, XOR, EB, SP , P } and T Edges = {N SF , CSF , DSF , M F }. Definitions 4 and 5 are taken (and restructured) from [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF]. Definition 6 integrates our extensions.

Definition 4 (Graph).

A graph is a tuple ρ = (N, E, source, target) where N is the set of nodes, E (with N ∩ E = ∅) is the set of edges, and source/target : E → N denote the source/target of an edge.

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

ρ = (ρ, cat N , cat E , R, M, msg t ) where ρ is a graph, cat N : N → T N odes gives the type of a node (N T denoting the set {n ∈ N | cat N (n) ∈ T }), cat E : E → T Edges gives the type of an edge (E T denoting the set {e ∈ E | cat E (e) ∈ T }), R : N {SP,P } → 2 N ∪E
gives the set of nodes and edges which are directly contained in a container (process or sub-process), M is the set of message types, and msg t : E {M F } → M gives the message associated to a message flow.

Definition 6 (Space BPMN Graph).

A space BPMN graph is a tuple ρ • = ( ρ, S, V, cvar, ckind, ccond, ≺, act) where ρ is a BPMN graph, S is a space structure, V is a set of variables, cvar : E {CSF } → V, ckind : E {CSF } → {any, all}, and ccond : E {CSF } → F orm are total functions that assign respectively a variable, a kind (denoting how to associate the interpretation of a space formula to a condition variable), and a space formula to each conditional edge, ≺⊆ E {CSF } × E {CSF } , is a relation ordering the conditional sequence flows outgoing from a conditional gateway, and act : N {AT } → Action is a total function that assigns an action to each abstract task.

Semantics for Space BPMN: States and Initial State

The semantics relies on the notion of state of the space BPMN graph, which is defined in terms of state markings, edge markings, and space configuration.

Notation. In the sequel, definitions are taken given a space BPMN graph ρ • = ( ρ, S, V, cvar, ckind, ccond, ≺, act) with S = (B, G, →) and L = B ∪ G.

Definition 7 (Space Configuration). A (space) configuration c is a couple of substitutions (σ, subs), σ being a variable to base locations substitution (σ : V → 2 B ) and subs being a group to base locations substitution (subs : G → 2 B ).

The set of all configurations (of a space BPMN graph ρ • ) is denoted by Conf igs. We note σ ⊥ the empty variable configuration (∀v

∈ V, σ ⊥ (v) = ∅). Given a configuration c = (σ, subs), σ[v → B], denotes the update of σ by associating B to v (i.e., σ[v → B] is σ(v ) for each v in V \ {v} and B for v).
Accordingly, subs[g → B], denotes the update of subs by associating B to g.

Among the variables, we have process locations, i.e., we have a variable loc p ∈ V for each p in N {P } , and σ(loc p ) gives the location of a process p. A configuration encompasses (in σ) the current values of variables -including the location of processes -and (in subs) the state of the relation between group and base locations. To become a state, a configuration is completed with the current marking of the BPMN graph nodes and edges.

Note that here we assume a model of shared variables (e.g. the znc variable in our example). This is driven by formalization convenience. Local variables with values exchanged using communication (messages) is part of our perspectives.

Definition 8 (State).

A state is a triple s = (mn, me, c) where mn : N → N (node marking), me : E → N (edge marking), and c is a configuration.

The set of all states (of a space BPMN graph ρ • ) is denoted by States. One of them is the state in which the graph starts its execution: its initial state.

Definition 9 (Initial state). The initial state of a space BPMN Graph ρ • is a state s o = (mn 0 , me 0 , c 0 = (σ 0 , subs 0 )) such that only processes and their start events are marked (∀n ∈ N, mn 0

(n) = 1 if ∃p ∈ N {P } , n ∈ N {N SE,M SE,T SE} ∩ R(p)
, and 0 otherwise), no edge is marked (∀e ∈ E, me 0 (e) = 0), and σ 0 is set only for the start locations of processes (∀v

∈ V, either ∃p ∈ N {P } , ∃loc p,0 ∈ B, v = loc p ∧ σ 0 (v) = {loc p,0 } or σ 0 (v) = ∅).
The initial locations for processes (the loc p,0 ) and subs 0 are parameters of the model and, hence, of its verification. In our example, for the context in Figure 2b, we had all fields to plant and the planter starting in F1 (or in base, with base → F1). This means that the configuration in the initial state is such that σ 0 (loc Planter ) = {F1} (or {base}) and subs 0 (toPlant) = {F1, . . . , F6}.

Semantics for Space BPMN: Formulas and Actions

Having defined configurations, it is now possible to give a semantics to formulas and actions. Let us begin with the former.

Definition 10 (Formula Interpretation). The interpretation of a formula f with reference to a configuration c = (σ, subs) and a process p, is denoted by In our example we use formula znc and reachable in the planter. Its interpretation is the intersection of σ{znc} and of the locations that are reachable from the planter location. This is not empty only if znc is reachable, which is what we want to express. Let us now come to the actions.

||f || p c (|| _ || _ _ : F orm × N {P } × Conf igs → 2 B )
Definition 11 (Actions Evaluation). The evaluation of an action a over a configuration c = (σ, subs) and a process p is denoted by

[[a]] p c ([[ _ ]] _ _ : Action× N {P } × Conf igs → Conf igs)
and defined as follows:

-

[[move(f )]] p c = c where c is c if ||f and reachable|| p c = ∅ and c is (σ[loc p → {b}], subs) with {b ∈ ||f and reachable|| p c } otherwise. -[[update(u, G -, G + )]] p c = (σ, subs ) where subs (g) is subs(g)\σ(u) if g ∈ G -, subs(g) ∪ σ(u) if g ∈ G + , and subs(g) otherwise (remind that G -∩ G + = ∅) -[[pass]] p c = c
Action move(f ) does nothing if f corresponds to no reachable locations satisfying it, otherwise one of the locations is chosen and the process location is updated accordingly. Action update(u, G -, G + ) updates groups in G -and G + respectively adding/removing locations in u. Action pass does nothing.

In our example the planter tries to move to its base at the end. Using condition _: base and reachable, it checks before that this is indeed possible. Without checking this (suppose there is no exclusive gateway) trying move(base) if the base is not reachable would make the process block on this task.

Semantics for Space BPMN: Execution Semantics

In order to maintain traceability with the standard [START_REF]Business Process Modeling Notation[END_REF], we use a token-based approach. The movement of tokens is based on node types. We define an execution model based on two predicates (St, Ct) for each node type which correspond to, respectively, the enabling of the node to start its execution, and the enabling of the node to complete its execution. When not specified, the predicate is true.

The formal execution semantics is given in Table 1. The semantics of the elements in Figure 1 and not in Table 1 is kept from [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF]. We consider that mn and mn (resp. me and me ) denote two successive markings of a node (resp. edge) Table 1: Space BPMN semantics (extensions to [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF]).

n ∈ N {XOR} Ct(n) def ≡ ∃ei ∈ in SF (n), me(ei) ≥ 1 ∧ me (ei) = me(ei) -1 ∧ ∃eo1 ∈ out {CSF } (n), ||ccond(eo1)|| procOf (n) c = ∅ ∧ ∀eo2 ∈ out {CSF } (n), eo2 ≺ eo1 ⇒ ||ccond(eo2)|| procOf (n) c = ∅ ∧ me (eo1) = me(eo1) + 1 ∧ ∃v ∈ V, v = cvar(eo1) ∧ ckind(v) = all ⇒ σ = σ[v → ||ccond(eo1)|| procOf (n) c ] ∧ ckind(v) = any ⇒ ∃x ∈ ||ccond(eo1)|| procOf (n) c , σ = σ[v → x] ∧ ({ei, eo1}) ∧ Ξ subs ∨ ∧ ∀eo1 ∈ out {CSF } (n), ||ccond(eo1)|| procOf (n) c = ∅ ∧ ∃eo2 ∈ out {DSF } (n), me (eo2) = me(eo2) + 1 ∧ ({ei, eo2}) ∧ Ξ σ subs n ∈ N {OR} Ct(n) def ≡ In + (n) = ∅ ∧ ∀ei ∈ In + (n), me (ei) = me(ei) -1 ∧ ∀ez ∈ In -(n), ∀ee ∈ (P reE(n, ez) \ ignoreE(n)), me(ee) = 0 ∧ ∀nn ∈ (P reN (n, ez) \ ignoreN (n)), mn(nn) = 0 ∧ ∃es ⊆ out {CSF } (n) ∧ es = ∅ ∧ ∃eo ∈ out {CSF } (n) \ es, ||ccond(eo)|| procOf (n) c = ∅ ∧ ∀eo ∈ es, ||ccond(eo)|| procOf (n) c = ∅ ∧ me (eo) = me(eo) + 1 ∧ ∃v ∈ V, v = cvar(eo) ∧ ckind(v)= all ⇒ σ = σ[v → ||ccond(eo)|| procOf (n) c ] ∧ ckind(v)= any ⇒ ∃x ∈ ||ccond(eo)|| procOf (n) c , σ = σ[v → x] ∧ (In + (n) ∪ es) ∧ Ξ subs ∨ ∧ ∀eo1 ∈ out {CSF } (n), ||ccond(eo1)|| procOf (n) c = ∅ ∧ ∃eo2 ∈ out {DSF } (n), me (eo2) = me(eo2) + 1 ∧ (In + (n) ∪ {eo2}) ∧ Ξ σ subs n ∈ N {AT } St(n) def ≡ ∃ei ∈ in SF (n), me(ei) ≥ 1 ∧ me (ei) = me(ei) -1 ∧ mn (n) = mn(n) + 1 ∧ ({n, ei}) ∧ Ξ σ subs Ct(n) def ≡ mn(n) ≥ 1 ∧ mn (n) = mn(n) -1 ∧ ∀eo ∈ out SF (n), me (eo) = me(eo) + 1 ∧ c = [[act(n)]] procOf (n) c ∧ act(n) = move(f ) ⇒ ||f and reachable|| procOf (n) c = ∅ ∧ act(n) = pass ∧ ({n} ∪ out SF (n)) ∧ Ξ σ subs ∨ act(n) = move(f ) ∧ ({n} ∪ out SF (n)) ∧ Ξ subs ∨ act(n) = update(u, G -, G + ) ∧ ({n} ∪ out SF (n)) ∧ Ξ σ
in the execution semantics. Accordingly c = (σ, subs) and c = (σ , subs ) denote two successive configurations. is a predicate that denotes marking equality but for nodes and edges given as parameter, (X) means "nothing changes but for X": (X) ≡ ∀n ∈ N \ X, mn (n) = mn(n) ∧ ∀e ∈ E \ X, me (e) = me(e). In the same way, we define Ξ σ ≡ σ = σ, Ξ subs ≡ subs = subs, and Ξ σ subs ≡ Ξ σ ∧Ξ subs . In the semantics we use helper functions: in/out : N → 2 E give the incoming/outgoing edges of a node, in(n

) = {e ∈ E | target(e) = n} and out(n) = {e ∈ E | source(e) = n}. A family of functions in T (resp. out T ) : N → 2 E is used to combine in (resp. out) with E T , in T (n) = in(n) ∩ E T and out T (n) = out(n) ∩ E T .
The type set for sequence flows, SF , is defined as {N SF, CSF, DSF }. procOf : N → N {P } gives the container process of a given node, procOf (n) = p if and only if n ∈ R + (p), with R + being the transitive closure of R. Further, to deal with the complex semantics of the OR gateway, and formalize in a correct way its definition in [START_REF]Business Process Modeling Notation[END_REF], we use some more functions: In -: N → E gives the unmarked incoming edges of a node:

In -(n) = {e ∈ in SF (n) | me(e) = 0}.
In + : N → E gives the marked incoming edges of a node:

In + (n) def = {e ∈ in SF (n) | me(e) ≥ 1}. 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. ignore E : N → 2 E gives the predecessor edges of the marked incoming edges of a given node: ignore Let us now describe Table 1.

E (n) = e + ∈In + (n) P re E (n, e + ).
Space Formulas and Gateways. Gateways are atomic hence define only the Ct predicate. A XOR gateway may complete by choosing one of its outgoing conditional flows eo 1 whose formula is satisfied (its interpretation, Def. 10, is not empty). In case there are several such transitions, we follow the BPMN standard and use ordering (≺) so that only the first one is activated. If there is no such flow, the default sequence flow outgoing from the gateway (if it exists) is activated. When a conditional flow is activated, its variable is updated at the same time. Depending on the condition kind (any or all), either a single location from the formula interpretation or all of them are taken to update σ(v).

An OR gateway has some differences wrt. a XOR gateway. First it requires that no more ongoing flow ez can be activated before completing (lines 3-5 of Ct). Second, all outgoing conditional flows whose conditions are satisfied are activated (lines 6-8 of Ct are used to get the maximal set es of such flows).

Space Actions and Abstract tasks. Actions are associated to abstract tasks which can start if at least one of their incoming flows is active. The completion of these tasks depends on the evaluation of their action (Def. 11) in order to change the configuration (c to c ), either σ for moves or subs for updates. For move(f ), we require that there is at least one reachable location in the interpretation of f .

Implementation & Verification

In this section, we present the implementation of our approach in a tool suite, sBPMN, enabling the verification of extended BPMN models and the animation of counter-examples. sBPMN is a part in a more general project about BPMN verification [START_REF] Poizat | fbpmn repository[END_REF]. It works as presented in Figure 4.

The user first designs an extended BPMN model using any modeler with support for BPMN extension mechanisms (we use Camunda). This model corresponds to Definition 5 with extensions information for Definition 6 (extensions to BPMN) and Definition 9 (initial state parameter). In practice, the space structure and the initial value of the subs relation are associated to the process diagram (as shown in page 5), initial locations are associated to processes, and conditional information and actions are associated respectively to conditional flows and to abstract tasks. A TLA + representation of this model is retrieved using the fbpmn command with option sbpmn2tla. Given this representation, the TLA + implementation of the semantics, and the TLA + encoding of generic and user given model-specific properties, the TLC model checker from the TLA + tool box (freely available at http://lamport.azurewebsites.net/tla/tla.html) is used to perform verification. If some properties are not satisfied, TLC outputs a counter-example trace that is then transformed using the fbpmn command with option log2html into an HTML+JS page enabling the user to animate the counter example on the BPMN model, step by step, to understand the error(s). We provide users with a script, sfbpmn-check, that performs all steps in Figure 4 in a transparent way (see [START_REF] Poizat | fbpmn repository[END_REF], under scripts/).

Implementing the semantics and encoding models in TLA +

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, and where quoting denotes the value of variables in the successor state. This is in phase with our St and Ct predicates. Further, the expression and action fragment of TLA + contains first-order logic, that we use to express the semantics. Hence, the encoding of the semantics in TLA + is straightforward (up to the TLA + concrete syntax of course). For example, the TLA + implementation for the semantics of XOR nodes is given in Figure 5. The comprehensive TLA + theories for the semantics is available at [START_REF] Poizat | fbpmn repository[END_REF] under theories/stla.

Properties and Verification

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 ). In our framework, properties are either properties that are generic to all process models, or user given properties specific to a given process model (see Fig. 6).

For the former, we reuse the TLA + implementation given in [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF] for the properties defined by [START_REF] Corradini | A classification of BPMN collaborations based on safeness and soundness notions[END_REF]: (1) safety, (2) soundness and (3) message-relaxed soundness. A collaboration is safe if no sequence flow holds more than one token. A collaboration is sound if all processes are sound and there are no undelivered messages, a process being sound if it can reach a state where nothing but its events are active. Finally, message-relaxed soundness is soundness without taking into account undelivered messages (tokens on message flows). For the model-specific properties, the user can rely on the elements in states (Def. 8), namely node and edge markings, variable substitution (including process locations) and group substitution. Examples of such properties are given in Figure 6.

Experiments

Experiments were conducted on a 3.5 GHz Intel Core i7 processor (dual core) laptop with 16 GB of memory and running MacOS. Results for a selection of Fig. 6: Generic and model-specific properties in TLA + . models from our model database (available from [START_REF] Poizat | fbpmn repository[END_REF], under models/) are presented in Table 2. The first column is the reference of the example in our model database. The characteristics of a model are: number of participants, number of nodes (incl. gateways), number of flow edges (sequence or message flows). When there is communication, we use a bag communication asynchronous model [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF]. 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 correctness properties presented above, we indicate if the model satisfies it. Lastly, the accumulated time for the verification of the properties is given (the time to transform BPMN models to TLA + transformation is negligible). We selected these five properties since they include BPMN specific generic ones [START_REF] Corradini | A classification of BPMN collaborations based on safeness and soundness notions[END_REF], model-specific ones, and cover the safety vs liveness spectrum.

The first model, s004, is a single crop planting process with a loop (find a zone to be planted, move to it, plant it, and mark it to be sprayed) that exits when there are no such zones. Model s006 is our example given in Figure 3. In this model (and other ones), the id of the end at base TEE is PlanterEndInBase and is used in verification (see property U ser1 in Fig. 6). Model s007 is a variant of model s006 where the context is updated in the planter rather than in the controller. Further, the planter uses the here space formula in the update action rather than znc. Model s008 is the full model (with processes inspired by s007), with both robots and two parallel robot-specific sub-processes in the controller. Finally, s009 is a variant of model s006 where the system does not stop upon an unreachable zone to plant, rather the zone is moved to a notTreated group. Experiments show that our tool supports the verification of BPMN models with the different extensions we propose and is rather fast, even in presence of loops. Verification takes less than a few seconds for most models. It should be noted that property (1) being a safety property, it requires the whole state space to be constructed when the model satisfies the formula. With model s008 we can see the impact of non-determinism in the model, as we have both intra-process concurrency (two parallel sub-processes in the controller), inter-process concurrency (three peers with message communication), and existential quantification over the movements of the processes (planter and sprayer can move to several places each time). Still, verification is achieved in reasonable time.

Related Work

Context awareness and context modelling is widely studied in different domains such as Web systems, mobile applications, ubiquitous computing, and business process engineering [START_REF] Saidani | Towards a generic context model for BPM[END_REF]. Most approaches that support context awareness for Business Process Management (BPM) provide a categorization of contextual information [START_REF] Born | Context-driven business process modelling[END_REF][START_REF] Rosemann | Context-aware process design exploring the extrinsic drivers for process flexibility[END_REF][START_REF] Saidani | Towards context aware business process modelling[END_REF][START_REF] Saidani | Towards a generic context model for BPM[END_REF]. Location is there stressed as an essential element.

A classification of contextual information into categories, that include geographical ones, is proposed in [START_REF] Born | Context-driven business process modelling[END_REF], with each category referring to multiple context values. The location model, in our work, is represented by the space structure. Many information reported in [START_REF] Bettini | A survey of context modelling and reasoning techniques[END_REF] were useful to identify its elements. Two kinds of coordinate systems, geometric and symbolic coordinates, are mentioned in [START_REF] Bettini | A survey of context modelling and reasoning techniques[END_REF]. Our space structure relies on the latter, with basic locations. According to [START_REF] Bettini | A survey of context modelling and reasoning techniques[END_REF], for symbolic coordinates and in order to allow spatial reasoning, explicit information about the spatial relations between pairs of symbolic coordinates has to be provided. This led in our approach to two instances of such relations: a static one, the → relation, and a dynamic one, the subs relation in configurations.

A survey on spatial models of context information is given in [START_REF] Bettini | A survey of context modelling and reasoning techniques[END_REF], yet without an appropriate model for locations in BPM. The only context modeling approach for BPM we are aware of is [START_REF] Saidani | Towards a generic context model for BPM[END_REF]. It includes location as a context entity with two attributes, zipcode and city. This is subsumed by our approach as these attributes, and their relations, can be represented using the → and subs relations.

Our space structure could be implemented with the data-related constructs of BPMN. Still, this would be cumbersome in comparison to a domain-specific extension like ours. This would also harm the separate reuse of contexts and process models which is made possible by our integration. While there are tools to animate BPMN models with data [START_REF] Corradini | MIDA: Multiple instances and data animator[END_REF], there is a lack of tools for their verification. Choosing an intermediary expressiveness level, with just the data required for spatial concerns, made verification amenable in our approach. The approach presented in [START_REF] Calvanese | Formal modeling and SMT-based parameterized verification of data-aware BPMN[END_REF] presents interesting perspectives in terms of verification. This approach operates with to distinct databases: a static one (catalog) and an evolving one (repository). Since we deal with environments evolving as a result of the action of processes, we would have to study whether group locations could be treated as part of the catalog and the subs relation as part of the repository.

Conclusion and Perspectives

We have proposed a BPMN extension for spatial concerns. Its principles are indeed applicable to other notations such as UML activity diagrams. This widens the use of this family of notations to systems where mobile processes act on their environment. Through the definition of a first-order semantics, its implementation in TLA + , and an automated model transformation, we made it possible to check both the usual process properties (safety, soundness) and contextspecific properties. When properties are not satisfied by models, our tools generate counter-examples that are animated on the BPMN models. Our tools and model database are open source and available online at [START_REF] Poizat | fbpmn repository[END_REF].

A first perspective of this work is to consider that the actions of processes can modify the possible moves in the spatial context. We already partially support this through the definition and updates of group locations, but modifying the → relation itself would add more expressiveness. By now, processes share the variables set by the evaluation of conditional flows. An extension would be to have also a local perspective of variables, and use message payloads to share them. Taking into account that the environment can evolve by itself (or under the action of processes not being modelled) is also an interesting perspective. This could be achieved, for example, with a specification of possible evolutions to be taken into account at verification time in conjunction with the properties of interest. Indeed, while we use here LTL (with TLA+ extensions to address model-specific properties), we could also study the use of LTL extensions to spatial concerns [START_REF] Haghighi | Spatel: a novel spatial-temporal logic and its applications to networked systems[END_REF][START_REF] Nenzi | Qualitative and quantitative monitoring of spatio-temporal properties with SSTL[END_REF]. In this work, we base on the BPMN execution semantics given in [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF] with the non-deterministic treatment for time-related elements given there. Another perspective concerns taking into account the second semantics for time given in [START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF], and study the interplay between time and space. A last perspective is to integrate an optimization aspect to the models, enabling processes to choose their path based on more complex, optimizing strategies, rather than on space formulas only.

Fig. 2 :

 2 Fig. 2: Case study -location contexts.

Definition 1 (

 1 Space Structure). A space structure is a tuple S = (B, G, →) where B is the set of base locations, G is the set of group locations, and →⊆ B × B denotes all possible moves between base locations. Further, we require that B ∩ G = ∅ and (b, b) ∈→ for every b in B. Space structures may represent different kinds of location-based contexts such as countries and administrative or epidemiological statuses, offices and security levels, or agricultural environments as in our case study where, B = {F1, . . . , M}, G = {toPlant, toWater, planted, watered}, and {(F2, F2), (F2, F5)} ⊂→. The set of all locations is denoted by L = B ∪ G, → * denotes the transitive closure of →, and b 1 → b 2 denotes that (b 1 , b 2 ) ∈→.

  and defined as: ||true|| p c = B (all base locations), ||v|| p c = σ(v) (value of a variable), ||b|| p c = {b} (base location), ||g|| p c = subs(g) (current locations of a group), ||not f || p c = B \ ||f || p c (difference), ||f 1 or f 2 || p c = ||f 1 || p c ∪ ||f 2 || p c (union), ||here|| p c = σ(loc p ), and ||reachable|| p c = {b ∈ B | σ(loc p ) → * b} (reachable locations).

ignore N : N → 2 N

 2 gives the predecessor nodes of the marked incoming edges of a given node: ignore N (n) = e + ∈In + (n) P re N (n, e + ).

Fig. 4 :

 4 Fig. 4: Tool support (blue: model-specific, green: non model-specific).

Fig. 5 :

 5 Fig. 5: Semantics of XOR nodes in TLA + (part of).

Table 2 :

 2 Experimental results (the space structure is the one in Fig.2b).

	ref.	Characteristics	Com.		LTS size		validity	total
	proc. nodes (gw.) SF/MF model states trans. depth (1) (2) (3) (4) (5) time
	s004 1	6 (1)	5/0	none	34	34	34		<1s
	s006 2	32 (7)	30/5	bag	276 437 118	×	2s
	s007 2	31 (7)	29/5	bag	67	104	31		1s
	s008 3	67 (16)	74/10 bag 4898 16263 53		8m31s
	s009 2	33 (7)	31/5	bag	296 472 123	×	3s

As far as time-related elements are concerned, we take the first, non-deterministic, semantics given in[START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaboration[END_REF].

Acknowledgements. The authors would like to thank Markus Alexander Kuppe and Philippe Quéinnec for their help with TLA + and the TLA + Toolbox.

This work was supported by project PARDI ANR-16-CE25-0006. contact author


Arnaud Lenoble
email: arnaud.lenoble@u-bordeaux.fr

Monica Gala

Véronique Laroulandie

The Past and Future of the University of Bordeaux's Bird Skeleton Reference Collection

Keywords: Archaeozoology, Birds, Osteology, Palaeoecology, Taphonomy Archéozoologie, Oiseaux, Ostéologie, Paléoécologie, Taphonomie

The PACEA laboratory at the University of Bordeaux houses a collection of a little over a thousand of bird skeletons, including specimens from Europe and the French West Indies. The collection started in the 1950s to support the lab's various research projects. In recent years, the rhythm of acquisitions has accelerated due to the development of new research topics and a collective investment in managing the collection. Since its creation, the priorities of collection have shifted from a pure focus on osteology to the recording of detailed biological and contextual information for each specimen. This evolution reflects the succession of various research topics carried out in the lab: determining the paleoenvironmental context of fossil specimens, avian zooarcheozoology, and more recently, changes in Caribbean bird communities through time. over the next few years, our aim is to publish the collection in biodiversity databases, such as VertNet and gBIF, include virtual specimens (digital models based on high-resolution X-Ray tomography) in the collection, and expand interinstitutional exchanges.

The European Bird Curator Congress in Paris provided a unique opportunity to present the PACEA reference collection of bird skeletons to researchers working on paleo-ornithology. This collection comprises over a thousand osteological specimens and documents avifauna from France and its overseas territories (i.e. Guadeloupe, Martinique, etc.). Here we present an assessment of the collection designed to identify the motives that led the PACEA research laboratory to devote what were sometimes relatively considerable resources to maintain and develop an osteological collection of birds.

Considering the age-old separation between regional museums and universities in France, it should come of no surprise that the collection lacks any specific mission statement concerning its accessibility to the public or heritage preservation. In this respect, the objectives of this collection differ from those typical of museum collections, meaning that the most appropriate way to present our laboratory's unique approach to this substantial avian reference collection is to trace its evolution over time.

The inception of the collection parallels the development of French universities following the Second World War. Built over a period of about sixty years, which is a relatively short span of time compared to most museum collections, the collection represents a significant investment for a research laboratory. The emergence of new research objectives over this period inevitably enlarged the scope of the collection. The development of the PACEA avian collection can be divided into three distinct stages:

-an initial focus on palaeontology and paleoenvironments, -followed by the investigation of processes influencing the preservation of avifauna accumulations in archaeological sites and the role of birds in the prehistoric diet, -and current work devoted to West Indian avian communities and their evolution. This distinction is somewhat artificial in the sense that, while rapid changes in the way the collection was built or managed certainly existed, new research objectives nevertheless drew upon previous results. With that said, a clear link is evident between the development of new research objectives, policies concerning the acquisition of new specimens, and the overall management of the collection. In fact, each of the three periods in the development of the collection arrived at a different solution to this equation.

Here we investigate the influence of rainfall regime and differing forested habitats on the demographic patterns of this invasive rodent on Guadeloupe during the wet and dry seasons based on data collected from trapped black rats. We hypothesize that forested habitats with marked hydric seasonality should support more variable black rat populations whose size varies seasonally compared with the climatically more stable forested habitats.

The 1950s to 1980s: Creation of the osteological collection

The avifauna collection of the Bordeaux University is rooted in the teaching of prehistory, which began with the creation of a university degree in Prehistory and Anthropology by G. Malvesin-Favre in 1951, followed by the founding of the Laboratory of Anthropology and Prehistory a few years later in 1954. Malvesin-Favre, a lecturer in botany, was also a passionate archaeologist and a member of the Bordeaux Archaeological Society since 1918. The laboratory he established was successively known as the Prehistory Laboratory (1956), the Laboratory of Prehistory and Quaternary Geology (1959), the Quaternary Institute (1968), the Institute of Prehistory and Quaternary Geology (1993) before becoming the PACEA (de la Préhistoire à l'Actuel, Culture, Environnements, Anthropologie) laboratory in 2003.

The beginning of the collection coincided with the founding of the laboratory, and initially comprised specimens purchased from French naturalia shops (Boubée et cie, Auzoux, Deyrolle, Schluter) with the aim of supporting teaching. Details of the original collection resembled a Prévert-style inventory -eagle (Aquila sp.) and hawk (Accipiter sp.) leg bones and skulls are recorded alongside a series of prehistoric human skulls and two fossil Orangutan teeth.

As members of the laboratory began to undertake numerous excavations at sites in southwestern France, particularly in the Les Eyzies region, the priorities of the collection changed direction. These field projects, particularity the famous work of F. Bordes from the 1950s to the 1970s, in no small part helped forge the laboratory's reputation. This work also helped establish the Palaeolithic cultural succession in south-western France over the past 100,000 years [START_REF] Delpech | Avian biodiversity on Guadeloupe Islands (F.W.I.): environmental adaptation and extinction from the Late Pleistocene to pre-Columbian and modern times[END_REF].

These excavations produced rich assemblages of flint artefacts as well as abundant faunal remains, highlighting the necessity of developing an osteological reference collection for faunal analyses. This collection included the skeletons of large and small mammals, a few amphibians and reptiles, and birds.

Moreover, since its creation and due to it being part of the Faculty of Sciences, the laboratory developed a multidisciplinary research project combining prehistory, geology, palaeobotany and palaeontology in order to trace the trajectory of human evolution and its environmental backdrop. The reconstruction of ancient fauna and their evolution was itself a major research topic for the laboratory (e.g. Prat, 1966a, b, c), with osteology playing an essential role in this research (e.g. [START_REF] Prat | Sur la discrimination des phalanges antérieures et postérieures d'Équidés[END_REF]. Thus, from the 1950s to about the 1990s, faunal analysis carried out at the laboratory primarily concerned regional prehistoric sites and focused on aspects of paleontology and the reconstruction of paleoenvironments. This research focused on documenting the biological evolution of animals, reconstructing past animal communities, establishing a relative chronology of sites, and determining the environmental conditions in which prehistoric hunter-gatherers lived.

From this point onwards, birds regularly figured on published fauna lists, such as for the Late Glacial fauna from the site of Gare de Couze in the Dordogne, where F. [START_REF] Prat | La faune du gisement de la Gare de Couze[END_REF] initially identified Snowy Owl Bubo scandiacus and Willow Ptarmigan Lagopus lagopus, and F. [START_REF] Delpech | Recherches paléontologiques concernant quelques gisements du Magdalénien VI : stations de la Gare de Couze (Dordogne), du Morin (Gironde) et de Duruthy[END_REF] added a curlew (Numenius sp.), Blackbird Turdus merula, Redwing Turdus iliacus and Eurasian Nuthatch Sitta europaea. The identifications of these species aided in reconstructing palaeoenvironmental conditions that prevailed during the formation of the site. For example, the predominance of Snowy Owls in the bird assemblage indicated the occupation of the site to have coincided with cold climatic conditions (Arctic tundra). This example equally illustrates the necessity of determining as many species as possible, from passerines to large raptors, when reconstructing paleoenvironments.

During this period, the first evidence for human modification of bird bones also emerged in the form of the intentionally sawn-off ends of a tibiotarsus from the large Pleistocene Crane Grus primigenia at the site of Duruthy in the Les Landes department [START_REF] Delpech | Faunes du Magdalénien VI et de l'Azilien du gisement de Duruthy, commune de Sorde-l'Abbaye (Landes)[END_REF]. However, traces of human modifications on bird bones were not systematically investigated, as it will become the case with the development of zooarchaeology.

In addition to the purchase of specimens, the growth of the collection was largely due to accidental discoveries by members of the laboratory, mainly F. Prat and F. Delpech, as well as the donations of old collections, such as the one from the Bordeaux Zoological Institute [START_REF] Armand | Les collections scientifiques de l'Université de Bordeaux[END_REF]. The re-use of stuffed specimens and the recycling of waste from taxidermists were also largely responsible for increasing the taxonomic diversity of the collection. Consequently, a significant portion of the collection from this period consists of incomplete skeletons (Fig. 1). By the mid-1990s, the osteological collection comprised nearly 400 complete and incomplete individuals, the large majority of which remained European specimens (Fig. 2). It is important to note that the constitution of this "initial" collection essentially took place prior to the development of legislation targeting wildlife conservation. As a result, no specific procedures were followed to trace the origin of skeletons and, although a typewritten inventory exists for the purpose of managing the collection, it does not establish the legal origin of the specimens. Moreover, information concerning the geographical origin and biological characteristics (maturity, sex) of the specimens are not provided. The overall lack of archival information accompanying the acquisitions means that very little documentation is available for this older collection.

1990s to 2010s: Zooarchaeology and Taphonomy

In the 1990s, the development of zooarchaeological (e.g. [START_REF] Chaix | Éléments d'archéozoologie[END_REF][START_REF] Kenneth | Zooarchaeology: Past, Present and Future[END_REF] and taphonomic approaches (e.g. [START_REF] Behrensmeyer | Fossils in the making: vertebrate taphonomy and paleoecology[END_REF]Lyman, 1994) underlay the emergence of new research themes. During this period, several of the laboratory's projects focused explicitly on avian remains, with the related goals of investigating site formation processes (i.e. distinguishing the role of humans and natural processes in the accumulation of faunal assemblages) and documenting the relationship between humans and birds. This latter aspect concerned both determining the species exploited by prehistoric groups and for what ends (food, the creation of tools or personal ornaments).

This new period is equally reflected in the completion of university dissertations focusing on avian remains [START_REF] Laroulandie | Taphonomie et archéozoologie des oiseaux en grotte : Applications aux sites paléolithiques du Bois-Ragot (Vienne), de Combe Saunière (Dordogne) et de la Vache (Ariège)[END_REF] and the subsequent recruitment of an ornitho-zooarchaeologist who supervises master's theses on the taphonomy and archaeozoology of bird remains (e.g. [START_REF] Bail | L'exploitation de la chouette harfang (Nyctea scandiaca) au Magdalénien récent : étude des gisements du Faustin et de Gare de Couze[END_REF][START_REF] Bouchard | L'avifaune du site tardiglaciaire de Rhodes II (Ariège) : Approche taphonomique, archéozoologique et paléoenvironnementale[END_REF]. This work primarily concerns the Palaeolithic of southern France.

Western palearctic avifauna, particularly boreal taxa well represented in prehistoric sites, remained poorly documented in the bird skeleton collection of this period. This period prioritized the acquisition of complete skeletons, which are particularly important, as zooarchaeological and taphonomic studies require the largest possible sample of bones collected during excavations to be identified [START_REF] Peres | Methodological Issues in Zooarchaeology[END_REF][START_REF] Lefebvre | Contemporary Challenges in Zooarchaeological Specimen Identification[END_REF]. A recent study of Snowy Owl bones (B. scandiacus) from the Gare de Couze is an instructive example. The anatomical representation of the skeletal elements of this taxon reveals an over-representation of the terminal and penultimate phalanx. This data, combined with the presence of cut-marks referable to disarticulation, not only supports a human origin for the accumulation but also makes it possible explore why and how Late Glacial huntergatherers used these elements [START_REF] Bail | L'exploitation de la chouette harfang (Nyctea scandiaca) au Magdalénien récent : étude des gisements du Faustin et de Gare de Couze[END_REF][START_REF] Laroulandie | De la plume à l'oeuf : exploitation des ressources aviaires au Magdalénien dans le Sud de la France[END_REF].

The general improvement of the osteological collection was not the only motivation for acquiring new bird specimens. There was equally the need to (a) build taphonomic reference collections documenting bone damage produced by different agents involved in the formation of fossil assemblages (e.g. [START_REF] Laroulandie | Damage to Pigeon long bones in pellets of the Eagle Owl Bubo bubo and food remains of Peregrine Falcon Falco peregrinus: zooarchaeological implications[END_REF] and (b) carry out butchery and disarticulation experiments designed to aide zooarchaeological interpretations (Fig. 3, see also [START_REF] Laroulandie | Anthropogenic versus nonanthropogenic bird bone assemblages: new criteria for their distinction[END_REF].

This period also saw the development of legislation to protect and preserve wild species (CITES and French laws for the protection of wildlife). The acquisition of several specimens missing from the collection required authorizations that involved a substantial time investment and legal expertise. As it stands, obtaining these authorizations somewhat hindered the ambitious goals for growing the avifauna collections. However, a ministerial authorization obtained in 1998 allowed the transport and possession of protected wild specimens from animal welfare centres to the laboratory.

Despite these issues, about a hundred new specimens were added to the collection (Anatidae, Columbids, Tytonids, Passerines), mainly species recovered from France. However, species that may have been present during glacial periods remained poorly represented, meaning that the analysis of avifaunal assemblages from Palaeolithic sites in Western Europe could only be carried out by consulting comparative material housed at the French National Museum in Paris.

The 2010s: Palaecological issues

New research topics have been addressed at PACEA over the past decade, including the evolution and structure of bird communities in relation to natural or human-induced environmental changes, temporal variations in the distribution of taxa, and morphological modifications of these species. The emergence of a more ecology-based approach is highlighted by the Bivaag (2013-2015: Biodiversité insulaire vertébrée ancienne de l'archipel de Guadeloupe) and ECSIT (2016-2020: Écosystèmes insulaires tropicaux, réponse de la biocénose vertébrée terrestre à 6 000 ans d'anthropisation du milieu) projects that focus on the French West Indies.

These projects have produced evidence for a high number of extinct reptile [START_REF] Bailon | New data on Pleistocene and Holocene herpetofauna of Marie Galante (Blanchard cave, Guadeloupe Islands, French West Indies): insular faunal turnover and human impact[END_REF], mammal [START_REF] Stoetzel | Late Quaternary changes in bat palaeobiodiversity and palaeobiogeography under climatic and anthropogenic pressure: new insights from Marie-Galante, Lesser Antilles[END_REF] and bird species from several contexts in the West Indies. A preliminary analysis of the bird bones collected from palaeontological and archaeological sites on the Guadeloupe islands documented two extinct species, the Macaw (Ara cf. guadeloupensis) and a Barn Owl (Tyto sp.), and 11 species extirpated from one or more islands: the Black-capped Petrel Pterodroma hasitata, three Rallidae (Porphyrio martinica; Porzana flaviventer, Laterallus cf. jamaicensis), the Burrowing Owl Athene cunicularia, the Swainson's Hawk Buteo swainsoni, a nighthawk of the genus Anthrostomus, two Turdidae (Turdus lherminieri and Turdus cf. nudigensis), and two mimids (Cinclocerthia ruficauda, Mimus gundlachii). Moreover, these now-extinct taxa suggest a significant turnover of island birds over the past 15,000 years. The presence of several fossilbearing caves on Marie-Galante currently makes it the best documented context. On this island, nearly 30% of the avian taxa represented in fossil or archaeological sites are extirpated or extinct species (Gala et al., 2016).

The determination of bird bones is thus at the core of a doctoral research currently being carried out at the laboratory by one of the co-authors of this paper (M.G.). However, this research requires a comprehensive comparative collection of West Indian birds, as illustrated by a previous study that demonstrated the presence of an indigenous macaw on the Guadeloupe archipelago. This was based on an ungual claw bone recovered from a Pleistocene layer preserved in one of the caves of Marie-Galante (Gala & Lenoble, 2015). The association of this extinct taxon with Ara guadeloupensis Clark 1905 is consistent with Clark's original description based on accounts from the European colonial period. This demonstration required substantial comparative work based on the fossil specimen itself and Ara and Amazona skeletons from the Paris Museum and the PACEA collection. For this study, about fifteen additional psittacids specimens were added to the PACEA bird skeleton collection, all of which were donated by breeders and taxidermists.

Caribbean bird specimens are currently poorly or very partially represented in European museum collections, which meant that research in this area required the development of a dedicated osteological collection. This was made possible through financial support from associated research projects, with the improved reference collection continuing to benefit all of the laboratory's projects. The development of the reference collection first involved drawing up a list of desired taxa and contacting appropriate organisations (i.e. animal welfare centres, wildlife management structures, zoos or museums) susceptible to furnish the specimens. The procedures for acquiring, processing and best exploiting the new osteological material was reorganised, and laboratory staff were trained in the legal requirements for obtaining the necessary acquisition/transport/possession permits for protected specimens. To date, approximately thirty permits have been obtained for the acquisition of new specimens. In addition, the preparation of the specimens has been improved; a more rapid enzymatic maceration process has been introduced [START_REF] Simonsen | A fast preparation of skeletal materials using enzyme maceration[END_REF], and the preparation area has been standardized and certified by the relevant health authorities.

Contextual information has also been improved and now systematically includes the geographical origin and biology of the specimens, supplemented, if necessary, by photographic evidence to document the bird's plumage. This progress emerged in parallel with the development of zooarchaeology and taphonomic analysis and reinforces the shift from an emphasis on osteological or paleontological specimens, which prevailed during the early years of the collection, to a focus on a biological specimen concept. The recording of biological information has also been enhanced; necropsies are commonly carried out, and, in the case of wild specimens and when interested research institutions have been identified, tissue samples are taken. Since 2014, some two hundred tissue samples from Caribbean birds, as well as those from the European Atlantic coast, have been sent to the Paris Museum. Finally, the collection catalog has been made entirely accessible to lab members via the laboratory's server, which allows interested researchers to contribute to the management of the catalog. A simplified version is also available to the international research community via the laboratory's website (http://www.pacea.u-bordeaux.fr/Collection-d-anatomie-comparee.html).

This new organization significantly increased the avifauna collection (Fig. 2). Currently, the collection consists of a little over 1,100 specimens from 25 orders dominated by passerines and Charadriiformes, followed by Columbiformes, Anseriformes and Accipitriformes, with approximately four hundred specimens, or 35% of the total collection, comprising Caribbean avifauna. As West Indian specimens are also poorly represented in Caribbean osteological collections, a portion of the collection, around a hundred bird skeletons, has been donated to the Guadeloupe Departmental Museum of Archaeology to help develop zooarchaeological and palaeobiological research.

The acquisition of West Indian specimens has thus been an important focus of the PACEA laboratory in recent years, and has resulted in a substantial collection of bird skeletons. This is particularly true for Guadeloupe, where the majority of the studied palaeontological and archaeological sites are located. Thanks to the support of governmental or public structures in the French West Indies, it has been possible to collect specimens that were poorly represented in museum collections. Of the 248 species on the list of birds from the islands of Guadeloupe, excluding introduced species, 118 are mentioned as "uncommon", "common" or "very common" in the list [START_REF] Levesque | Liste des oiseaux de la Guadeloupe (Grande-Terre, Basse-Terre, Marie-Galante, les Saintes[END_REF]. Three-quarters of these 118 species were acquired by the PACEA laboratory (Fig. 4). Représentation de l'avifaune de Guadeloupe dans la collection ostéologique d'oiseaux de l'Université de Bordeaux.

Moreover, the Guadeloupe avifauna includes sixteen so-called "patrimonial species" that group together the endemic species of Guadeloupe with endemic species of the Eastern Caribbean. These taxa are occasionally represented in osteological collections, mainly in North America (e.g. the Smithsonian Institute, the Florida Museum or the Royal Ontario Museum). Fourteen of these sixteen species are represented in the PACEA reference collection, and, according to VertNet, skeletons of three species exists only in this collection: The Guadeloupe Woodpecker Melanerpes herminieri, the Forest Thrush Turdus lherminieri, and the Plumbeous Warbler Setophaga plumbea. Several species are, however, still missing from the collection, including both rare species and species currently absent from Guadeloupe but which may have been in the past, such as the Lesser Antilles Owl Tyto insularis, which is currently present only in Dominica and Saint Vincent, or the White-breasted Thrasher Ramphocinclus brachyurus, an endangered species represented by small populations on the islands of Saint Lucia and Martinique.

As the identification of extinct species involves comparing fossil remains with all specimens from a given family, or at least its Caribbean representatives, the list of essential specimens was expanded to include birds from other Caribbean islands. Overcoming this limitation required innovative solutions, for example inter-museum loans of specimens or 3D models rendered from CTscans of specimens preserved in other establishments. This allowed the morphologies of loaned specimens to be recorded or obtain 3D models of bones from specimens that are too rare to be loaned or represented only by specimens preserved in alcohol. To date, 50 specimens from the Caribbean avifauna have been microscanned. The continuation and development of these two approaches, however, implies that the PACEA collection and studies carried out at the lab are made available to the broader community of avian collection curators

The future of the collection

The future objectives of the collection can succinctly be summed up as "accessibility, donation, and exchange". While a web-accessible catalog, tissue donations, and the lending or exchange of specimens with other research institutions is, of course, a promising start, much remains to be done. Improving the accessibility of the collection remains at the forefront of future objectives and includes plans for a web-based research engine as well as integrating our database in international databases, such as Vertnet or GBIF. In addition, obtaining permanent permits for the possession of protected species should entitle PACEA to a CITES exemption procedure and facilitate the loan or exchange of specimens.

A more long-term objective is the integration of the PACEA CT-scanned specimens within a national, European or international network of virtual specimens. The PACEA laboratory currently has a large sample of 'virtual' specimens that can be made available to other institutions; with the inclusion of 3D models of numerous specimens missing from our collection would be of great help to the research conducted in the laboratory. However, such an exchange network or structure is yet to be developed.

Figure 1 .

 1 Figure 1. Partial specimens recovered from taxidermists. Left: partial skeleton (wings and skull) of Short-toed Snake-Eagle, Circaetus gallicus (PACEA-O-46) obtained by recycling a stuffed specimen. Right: postcranial axial skeleton of an individual of the same species (PACEA-O-246) obtained by recovering naturalization by-products. Caractère partiel des spécimens issus de la taxidermie. Gauche : squelette partiel de Circaète Jean-le-Blanc, Circaetus gallicus (PACEA-O-46) obtenu par recyclage d'un spécimen naturalisé et documentant les membres et le crâne de l'oiseau. Droite : squelette partiel d'un individu de la même espèce (PACEA-O-246), obtenu par récupération des sous-produits de naturalisation et documentant le squelette axial post-crânien.

Figure 2 .

 2 Figure 2. Growth of the bird skeleton collection since the founding of the PACEA laboratory in 1954. The three periods of the collection constitution are shown on the graph: 1 = 1950s to 1980s; 2 = 1990s to 2010s; 3 = 2010s to present. Accroissement de la collection d'ostéologie aviaire au cours du temps, depuis la constitution du laboratoire PACEA (1954) jusqu'à aujourd'hui. Les trois périodes de constitution de la collection sont identifiées sur la figure : 1 = années 50 à 80, 2 = années 90 à 2010, 3 = années 2010 à aujourd'hui.

Figure 3 .

 3 Figure 3. Human and non-human modifications on bird humerus; a) fracturation and bilateral beak impacts on a pigeon humerus observed in modern Bubo bubo pellets, b) beak impact on a pigeon humerus in modern food remains of Falco peregrinus; c) experimental crushing, notching and tearing on Perdrix perdix produced during the disarticulation of the elbow; d) archaeological crushing, notching and tearing on Lagopus sp. from the Magdalenian site of La Vache (France). Modifications humaines et naturelles d'humérus d'oiseau ; a) impact bilatéral de bec et fracturation d'humérus de pigeon issu de pelotes de régurgitation de Bubo bubo, b) impact de bec sur humérus de pigeon dans des restes alimentaires actuels de Falco peregrinus ; c) écrasement experimental, arrachement et encoches obtenus expérimentalement par désarticulation d'aile de Perdrix perdix ; d) écrasement, arrachement et encoches observés sur des restes archéologiques de Lagopus sp. du site magdalénien de La Vache (France).

Figure 4 .

 4 Figure 4. Representation of the Guadeloupe bird fauna in the skeleton collection of the Bordeaux University.Représentation de l'avifaune de Guadeloupe dans la collection ostéologique d'oiseaux de l'Université de Bordeaux.

Acknowledgements

This paper forms part of the ECSIT Project: "Écosystèmes insulaires tropicaux, réponse de la faune indigène terrestre de Guadeloupe à 6 000 ans d'anthropisation du milieu", conducted by the CNRS with financial support from the European PO-FEDER program (grant n° 2016-FED-503), the Guadeloupe Regional Council, and the DAC of Guadeloupe. We would also like to thank D. Armand and B. Maureille, who provided historical information concerning the PACEA lab, J. Fuchs and C. Lefèvre from the MNHN, the staff of the ROM, NHMUK, UMMZ, AMHN, the ornithologists of Guadeloupe, as well as all the individuals who helped improve the PACEA bird skeleton collection and its management.