Francisco Durán

Camilo Rocha

Gwen Salaün

Symbolic Specification and Verification of Data-aware BPMN Processes using Rewriting Modulo SMT

The Business Process Model and Notation (BPMN) is the standard notation for modeling business processes. It relies on a workflow-based language that allows for the modeling of the control-flow graph of an entire process. In this paper, the main focus is on an extension of BPMN with data, which is convenient for describing real-world processes involving complex behavior and data descriptions. By considering this level of expressiveness due to the new features, challenging questions arise regarding the choice of the semantic framework for specifying such an extension of BPMN, as well as how to carry out the symbolic simulation, validation, and assess the correctness of the process models. These issues are addressed first by providing a symbolic executable rewriting logic semantics of BPMN using the rewriting modulo SMT framework, where the execution is driven by rewriting modulo axioms and by querying SMT decision procedures for data conditions. Second, reachability properties, such as deadlock freedom and detection of unreachable states with data exhibiting certain values, can be specified and automatically checked with the help of Maude, thanks to its support for rewriting modulo SMT. The approach presented in this paper has been validated on realistic processes and it is illustrated with a running example.

Introduction

Business processes are omnipresent in companies all around the world. A business process is a collection of structured activities or tasks that produce a specific product and fulfil a specific organizational goal for a customer or market. A process aims at modeling activities, their causal and temporal relationships, and specific business rules that process executions have to comply with. In this context, business process modeling is of prime importance to analyze and control business processes.

Business processes are usually described using workflow-based notations. BPMN is one of these notations. It was normalized by ISO/IEC in 2013 [START_REF]International Standard 19510, Information technology -Business Process Model and Notation[END_REF] and has become the de facto standard for modeling business processes. BPMN is a quite expressive notation that describes the order in which a set of activities is executed. Beyond basic operators (e.g., beginning, end, sequence), the notion of gateways allows designers to specify different evolutions of the process control flow (e.g., choice, parallel, messagebased). In this work, there is the particular interest on data descriptions, which take two different forms in BPMN processes, namely: (i) as variables that are initialized and modified during the process execution, and (ii) as conditions that may be used in gateways to decide the branches to be triggered at runtime. Representing data and conditions in BPMN is crucial for enabling the modeling of real-world processes, where data is pervasive and comes from different sources. BPMN tools such as the Activiti or Bonita platforms provide support for the definition of data-aware workflows. However, as it can be seen in the related work section of this paper, just a few formal specification and verification approaches consider this level of expressiveness.

The research presented in this paper takes a step farther by supporting the symbolic specification, execution, and analysis of data-aware processes with an external and nondeterministic environment (e.g., interaction with user input or sensor probing). This basically means that process variables can be initialized using assignments or by means of lookup operations, so that their values are non-deterministically provided by the environment. The consideration of such open systems, however, poses new challenges that include the potential infinitely-branching nondeterminism due to the environment. Queries over such systems are, in general, beyond the reach of ground rewriting and would require, for instance, inductive techniques over the rewrite relation.

Given such a general and symbolic modeling language for BPMN processes, there are several questions that arise from a correctness point of view. For example, is it possible to verify that a given process is deadlock free for any possible input and interaction with the environment? Are there parts of the workflow that are never reached or cannot be reached during execution under some initial conditions? Are there possible executions of the process leading to a state where the variables have specific values? It can be difficult to answer these questions when considering data ranging over possibly infinite domains. Indeed, most approaches on the analysis and verification of workflows are based on process over-approximation in which data is abstracted, either just by removing it or by replacing it with stochastic information. Although these approaches are useful in the formal analysis of workflows, they can miss important information hidden in the data. E.g., they can miss deadlocks due to data-based conditions that are removed or identify false livelocks since all loops in a process without data are always nonterminating.

The main contributions of this paper are a formal rewriting-based symbolic semantics for BPMN with data support and automated verification techniques for checking properties of interest, such as the ones abovementioned. The encoding of BPMN is made using the rewriting logic framework and is fully executable in the Maude system [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF]. It comprises BPMN operators such as end/start events, sequence flows, and gateways annotated with data constraints, and support for looping behavior and unbalanced split/join composition (i.e., no systematic correspondence between split and join gateway patterns). Although some important BPMN features, such as events or exceptions, are not considered, the current supported subset is quite expressive.

The symbolic analysis and verification techniques focus on the behavioral aspect of the BPMN processes, which is described as a control-flow graph with data annotations. Data variables and data-based conditions are supported with the help of the recently developed rewriting modulo SMT approach [START_REF] Rocha | Rewriting Modulo SMT and Open System Analysis[END_REF], which is well suited to model and analyze reachability properties of infinite-state open systems that exhibit both internal and external nondeterminism due to the environment. In particular, data variables are logical variables under the control of an SMT-solver and data conditions are constraints over these variables that can be checked for satisfiability with SMT-based decision procedures. This approach ultimately enables the automatic verification of existential reachability properties of BPMN processes with a potential infinite number of initial states. They include deadlock freedom, detection of unreachable states, and reachability of certain states based on data analysis relative to an initial constraint on the data variables. The Maude specification presented here and several examples are available at http://maude.lcc.uma.es/BPMN-SMT.

The organization of the rest of this paper is as follows. Section 2 introduces BPMN with data and the running example. The example has design issues on purpose, with the intention of identifying them with the help of the proposed formal analysis approach. Section 3 gives some background about rewriting logic and rewriting modulo SMT. Section 4 introduces the Maude encoding of the considered subset of BPMN, with emphasis on the handling of data. In Section 5, analysis techniques for automatically verifying properties on data-aware BPMN processes are presented and illustrated with the help of the running example; it ends with a proposal to correct such an example. Section 6 surveys related work and Section 7 concludes the paper.

BPMN with Data

BPMN is a workflow-based notation for modeling business processes as collections of tasks that produce specific services or products for particular clients. BPMN is an ISO/IEC standard [START_REF]International Standard 19510, Information technology -Business Process Model and Notation[END_REF], and can be executed by using different process interpretation engines (e.g., Activiti, Bonita BPM, or jBPM).

In this paper, our goal is not to consider the whole expressiveness of the BPMN language, but to concentrate on its main elements related to control-flow modeling and on data aspects that can be represented in BPMN constructs (variables and conditional flows). By focusing on these aspects, we show how automated analysis is possible for them. Specifically, we consider the node types event, task, and gateway, and the edge type sequence flow. Figure 1 illustrates the syntax of BPMN supported in this work, including examples of data assignments and conditions at exclusive/inclusive split gateways.

Start and end events are used, respectively, to initialize and terminate processes. A task represents an atomic activity that has exactly one incoming and one outgoing flow. A gateway is used to control the divergence and convergence of the execution flow. A sequence flow describes two nodes executed one after the other, i.e., imposing the execution order.

In BPMN, variables are global to the process. Their initialization and modification is possible at the task level using assignment (:=). Values from the environment can be read using a lookup operator. In this paper, we consider basic datatypes (integer, real and Boolean) with usual functions on them. As an example, integers can be manipulated using functions +, -, *, etc. These variables are also used to define conditions in gateways.

Gateways are crucial since they are used to model control flow branching and therefore influence the overall process execution. In this paper, we support the three main types of gateways, namely, exclusive, inclusive and parallel gateways. Gateways with Fig. 1. BPMN syntax augmented with data variables and conditions one incoming branch and multiple outgoing branches are called splits, e.g., inclusive split gateway. Gateways with one outgoing branch and multiple incoming branches are called merges, e.g., parallel merge gateway. An exclusive gateway chooses one out of a set of mutually exclusive alternative incoming or outgoing branches depending on the evaluation of conditions on their outgoing flows. For an inclusive gateway, any number of branches among its incoming or outgoing branches may be taken depending on the evaluation of flow conditions. A parallel gateway creates concurrent flows for its outgoing branches or synchronizes concurrent flows for its incoming branches. In this work, we support unbalanced workflows, meaning that each merge gateway does not necessarily have a corresponding split gateway with a correspondence of the branches among outgoing and incoming flows. We also support workflows with looping behaviors.

We assume that BPMN processes are syntactically correct. This can be enforced using existing works, e.g., [START_REF] El-Saber | BPMN Formalization and Verification using Maude[END_REF], or using a BPMN engine, as the Activiti or Bonita platforms. Note that any well-typed expression may be used in assignments, using variables, literal and operators, any valid Boolean expression may be used in conditions, and split (resp. merge) gateways may have any positive number of outgoing (resp. incoming) branches.

The semantics of BPMN is described informally in official documents [START_REF]International Standard 19510, Information technology -Business Process Model and Notation[END_REF][START_REF]Object Management Group. Business Process Model and Notation (BPMN) -V. 2.0[END_REF], and several attempts have been made for giving a formal semantics to subsets of BPMN (see Section 6). The semantics of BPMN is usually described using tokens representing the evolution of a process execution. A token can enter and leave a task by following the incoming and outgoing flows associated to that task. Tokens are created and consumed at gateways. When a token arrives at a parallel split gateway, it is consumed and one token is generated for every outgoing flow of the split gateway. When a token is consumed at an exclusive split gateway, only one token is created and assigned to the outgoing flow whose condition is evaluated to true. In the case of an inclusive split gateway, when a token is consumed, some new tokens are generated and assigned to the outgoing flows (one for each outgoing flow whose corresponding condition is evaluated to true). We assume that a process starts its execution with exactly one token located at its start event, and finishes its execution when all tokens are at end events. In the following, we will Fig. 2. Running example: e-visa application process say that a task or flow (or branch) is active if it has a token associated with it. E.g., the branches a gateway follows during an execution will be called the active branches.

Running example. We use as running example an online e-visa service described as a BPMN process shown in Figure 2. The workflow models the on-line application for a visa, in which the user has to fulfil several forms, provide an electronic copy of her passport and pay the corresponding fees. The process starts with the client initiating the application by filling some basic information. A scanned version of the passport must then be provided. The calculation of the size and quality of the uploaded file is modeled as reading from the environment its size and quality using the lookup operator. If the size of the uploaded file does not respect the size limit (2MB), the user may try again to submit another file. Once the file size is within the size limit, the application checks for image quality. Here, again, if the quality is not good enough, the user can upload another scanned version of her passport. The user has up to three attempts to upload the scanned copy of her passport with valid file size and quality. When both the size limit and scan quality respect the imposed thresholds, the request is evaluated and a result is notified to the user (accept or reject). The evaluation is performed by a human agent, which provides her response as an input to the system. In case of acceptance, the user has to pay for fees and the bureau in charge of visa delivery prepares the requested document. Both activities are achieved in parallel because they are independent. Finally, an electronic version of the visa is delivered by email.

In addition to classic BPMN elements, data are used at different places of the process, e.g., for keeping track of the number of attempts or for storing the size and quality of the uploaded files. In those usages, the case study includes several interesting data-related features: different variable types (integer, real and Boolean), variable manipulation (assignments, arithmetic expressions and predicates), data-based decisions (depending on input data file size and quality), and external decisions (application evaluation by agent).

As the careful reader has already possibly noticed, and as we will see in Section 5, the process in Figure 2 has several design problems, e.g., the number of attempts for uploading the passport is not correctly handled and checked. The remaining sections of this paper will show how the proposed analysis techniques can detect these issues.

Rewriting Logic and Rewriting Modulo SMT in a Nutshell

This section briefly explains order-sorted rewriting logic and rewriting modulo SMT, summarizing Sections 2-5 in [START_REF] Rocha | Rewriting Modulo SMT and Open System Analysis[END_REF]. Rewriting logic [START_REF] Meseguer | Conditional Rewriting Logic as a Unified Model of Concurrency[END_REF] is a semantic framework that unifies a wide range of models of concurrency. Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF] is a language and tool to support the formal specification and analysis of concurrent systems in rewriting logic. Notation on terms, term algebras, and equational theories is used as in, e.g., [START_REF] Baader | Term Rewriting and All That[END_REF][START_REF] Goguen | Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations[END_REF].

An order-sorted signature Σ is a tuple Σ=(S , ≤, F) with a finite poset of sorts (S , ≤) and a set of function symbols F typed with sorts in S . The binary relation ≡ ≤ denotes the equivalence relation (≤ ∪ ≥) + generated by ≤ on S and its point-wise extension to strings in S * . For any sort s ∈ S , the expression

[s] denotes the connected component of s, that is, [s] = [s] ≡ ≤ . A top sort in Σ is a sort s ∈ S such that for all s ∈ [s], s ≤ s. Let X = {X s } s∈S
denote an S -indexed family of disjoint variable sets with each X s countably infinite. The set of terms of sort s and the set of ground terms of sort s are denoted, respectively, by T Σ (X) s and T Σ,s ; similarly, T Σ (X) and T Σ denote, respectively, the set of terms and the set of ground terms. T Σ (X) and T Σ denote the corresponding order-sorted Σ-term algebras. A substitution is an S -indexed mapping θ : X -→ T Σ (X) that is different from the identity only for a finite subset of X and such that θ(x) ∈ T Σ (X) s if x ∈ X s , for any x ∈ X and s ∈ S . Substitutions extend homomorphically to terms in the natural way. A substitution θ is called ground if and only if ran(θ) = ∅. The application of a substitution θ to a term t is denoted by tθ.

An equational theory is a tuple (Σ, E), with Σ an order-sorted signature and E a finite collection of (possibly conditional) Σ-equations. An equational theory E = (Σ, E) induces the congruence relation = E on T Σ (X) defined for t, u ∈ T Σ (X) by t = E u if and only if E t = u, where E t = u denotes E-provability by the deduction rules for order-sorted equational logic in [START_REF] Meseguer | Membership Algebra as a Logical Framework for Equational Specification[END_REF]. The expressions T E (X) and T E (also written T Σ/E (X) and T Σ/E ) denote the quotient algebras induced by = E on the term algebras T Σ (X) and T Σ , respectively. T Σ/E is called the initial algebra of (Σ, E).

A rewrite theory is a tuple R = (Σ, E, R) with (Σ, E) an order-sorted equational theory and R a finite set of Σ-rules. R = (Σ, E, R) is called a topmost rewrite theory if it has a top sort Conf such that no operator in Σ has Conf as argument sort and each rule

l → r if φ ∈ R satisfies l, r ∈ T Σ (X) Conf and l X. A rewrite theory R induces a rewrite relation → R on T Σ (X) defined for every t, u ∈ T Σ (X) by t → R u if and only if there is a rule (l → r if φ) ∈ R and a substitution θ : X -→ T Σ (X) satisfying t = E lθ, u = E rθ, and E φθ. The tuple T R = (T Σ/E , → * R ) is called the initial reachability model of R [3]
. Appropriate requirements are needed to make an equational theory E admissible, i.e., executable in rewriting languages such as Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF]. In this paper, it is assumed that the equations of E can be decomposed into a disjoint union E B, with B a collection of regular and linear structural axioms (such as associativity, and/or commutativity, and/or identity) for which there exists a matching algorithm modulo B producing a finite number of B-matching solutions, or failing otherwise. Furthermore, it is assumed that the equations E can be oriented into a set of (possibly conditional) sort-decreasing, operationally terminating, confluent rewrite rules -→ E modulo B. . Under sort-decreasingness, operational termination, and confluence, the term t ↓ E/B is unique up to B-equality. For a rewrite theory R, the rewrite relation → R is undecidable in general, even if its underlying equational theory is admissible, unless conditions such as coherence [START_REF] Viry | Equational Rules for Rewriting Logic[END_REF] are given (i.e, whenever rewriting with → R/E∪B can be decomposed into rewriting with → E/B and → R/B ).

A rewrite theory R = (Σ, E B, R) modulo a built-in subtheory E 0 = (Σ 0 , E 0 B 0 ) ⊆ (Σ, E B
) is a topmost rewrite theory with a signature of built-ins Σ 0 = (S 0 , ≤ 0 , F 0 ). The ground rewrite relation → R induced by a rewrite theory with built-ins R is the topmost rewrite relation defined for any t, u ∈ T Σ,Conf as follows: t → R u if and only if there is a rule l → r if φ in R and a ground substitution σ : X -→ T Σ such that t = E B lσ, u = E B rσ, and

T E 0 | = φσ.
The symbolic rewrite relation induced by a rewrite theory with built-ins R operates over pairs (t ; ϕ), called constrained terms, where t ∈ T Σ (X 0 ) Conf is a term, ϕ ∈ QF Σ 0 (X 0 ) is a constraint of built-ins, and X 0 ⊆ X are the variables with sorts in S 0 . Each formula in QF Σ 0 (X 0 ) is a Boolean combination of atoms, where an atom is a Σ 0 -equation with variables in X 0 . For any term t ∈ T Σ (X) Conf and constraint ϕ, the denotation t ϕ is defined as

t ϕ = {t ∈T Σ,Conf | (∃σ : X-→T Σ ) t = E tσ ∧ T E 0 | = ϕσ}. Given a rewrite rule ((l ; φ l ) → (r ; φ r ) if φ) ∈ R, with l, r ∈ T Σ (X) Conf and φ ∈ QF Σ 0 (X 0 ), a con- strained term (t ; φ t ) ∈ T Σ (X 0 ) Conf × QF Σ 0 (X 0 ) symbolically rewrites to a constrained term (u ; φ u ) ∈ T Σ (X 0 ) Conf ×QF Σ 0 (X 0 ) (denoted by (t ; φ t ) R (u ; φ u )) if and only if there is a substitution θ such that: (a) lθ = E B t and rθ = E B u, (b) T Σ/E B | = (φ l ∧ φ t θ) ⇔ φ u , and (c) φ u is T Σ/E B -satisfiable. Condition (a)
can be solved by matching as in the definition of → R above. Condition (b) can be met by setting φ u to be φ l ∧ φ t θ. Condition (c) is checked with the help of decision procedures available from an SMT solver via the function check-sat. Observe that, up to the choice of the semantically equivalent ϕ u , the symbolic relation R is deterministic in the sense of being determined by the rule and the substitution θ (here it is assumed that variables in the rules are disjoint from the ones in the target terms). The reader is referred to [START_REF] Rocha | Rewriting Modulo SMT and Open System Analysis[END_REF] for details about rewriting modulo SMT and the correspondence between → R and R . ( flow ( sf1 ) , flow ( sf2 ) , . . . , flow ( sf24 ) , flow ( sf25 ) ) > Fig. 3. Running example: representation in Maude of the e-visa application process

Symbolic Specification

The symbolic semantics of BPMN is defined as a rewrite theory R, with built-ins E 0 and topsort Conf. A symbolic state is a constrained term (t ; ϕ), where t is a configuration of objects and ϕ a constraint. The objects in t represent the set of nodes and flows of a process, and keep information of the execution of the process. The constraint ϕ ranges over the built-in sorts Boolean, Integer, and Real, of Booleans, integers, and reals, respectively, and it maintains the bookkeeping of constraints accumulated during execution. For example, a constraint ϕ can encode the possible values for an integer variable that are possible after the process is executed. Figure 3 includes a representation in Maude of the e-visa application process as a Process object. This object represents the static part of the process, and identifies its nodes (attribute nodes) and flows (attribute flows). The process pid is parametric on 4 built-in variables, namely, OK (of sort Boolean), try and filesize (of sort Integer), and quality (of sort Real). Thus the constraints accumulated during the execution of this process range over these 4 variables.

The initial node of the process is represented as the term start(initial, sf1) specifying that the initial node has outgoing flow sf1. Task nodes are specified by an identifier, a label, an input flow, an output flow, and a list of assignments. An assignment has the form x := E, where x is a variable, and E an expression over the variables with the same sort of x. In this particular example, x is a variable in the set {OK, try, filesize, quality} and E an expression over the same set of variables. For in-

< sim : Simulation | tokens : token ( sf1 ) , constr : true , varidx : ( v ( OK ) | -> 0 , v ( try ) | -> 0 , v ( filesize ) | -> 0 , v ( quality ) | -> 0 ) >
Fig. 4. Running example: simulation in Maude of the e-visa application process stance, the assignment try := try + 1 in task t4 indicates that the value represented by the variable try is to be incremented in one unit. For the reading of external variables we use the lookup operator. E.g., variables filesize and quality are read in tasks t3 and t5, respectively. Split nodes are specified by an identifier, a type (exclusive, inclusive, or parallel), an incoming flow, and a nonempty list of outgoing flows.

Exclusive and inclusive gateways are equipped with constraints associated to the outgoing flows: these represent conditions over the data of the process. For instance, in the exclusive split gateway s2, the list (sf10, quality < 9/10) (sf11, quality >= 9/10) specifies that the flow sf10 is triggered when the quality of the picture is below 90% and that the flow sf11 is taken otherwise. Merge nodes are specified by an identifier, a type (the same types of split gateways), a set of incoming flows, and an outgoing flow. End nodes are specified by an identifier and an incoming flow. Flows are specified just by an identifier. Figure 4 shows a representation in Maude of an execution state of the process as the object sim. This object gathers the dynamic information used along execution, and has attributes identifying the set of tokens (attribute tokens), the constraint accumulated during execution (attribute constr), and a map (of sort Map{SymbVar, Nat}) for indexing the built-in variables present in the state (attribute varidx). In this example, the token to be processed next is at flow sf1, the constraint is true (i.e., the empty one), and all variables in the process are indexed at 0.

The index of a variable can increase during execution, which is key because an expression over the built-ins is evaluated with respect to a given variable indexing. Since the variables in a process are "mathematical" variables, they need to be treated with a predicate-transformer approach (opposed to the imperative programming-like approach). For example, given the variable indexing v(try) |-> 4, the expression try + 1 is interpreted as try#4 + 1, meaning that the interpretation of the increment of try by one unit is to be done with respect to the 'latest' version of the variable. When an assignment such as try := try + 1 is evaluated, it creates a constraint that is added to the global constraint and depends on the given variable indexing. For example, with the variable indexing v(try) |-> 4, the evaluation of try := try + 1 results in the constraint try#5 === try#4 + 1, meaning that the "new" value of try corresponds to its previous value incremented by one. The lookup operator works similarly, although in this case there is no restriction on the new value.

The concurrent transitions of R are specified by rewrite rules that update the simulation object sim. Specifically, there are 12 rewrite rules that model the different actions Fig. 5. Execution of a task with a list of assignments that may happen in the system, e.g., start or end the execution of a process, handle the arrival of a token to split and merge gateways, tasks, and flows. For illustration purposes, we explain in the rest of this section two of these rules.

Figure 5 shows the rewrite rule that handles execution of a task. Intuitively, executing a task results in a new symbolic state in which the constraint is updated by accumulating the constraints that result from the list of assignments associated to the task, if possible. Since handling an assignment changes the variable indexing kept in the object sim, a new version of the variable indexing term needs to be computed. Both the constraint resulting from a list of assignments and the new variable indexing are computed with the help of the auxiliary function prepare-update. For example, the evaluation of the term prepare-update((X := X + 1)

(Y := Y + X), (v(X) |-> 4, v(Y) |-> 0))
returns the pair

((v(X) |-> 5, v(Y) |-> 1), X#5 === X#4 + 1 and Y#1 === Y#0 + X#5)
where the index of both variables X and Y is incremented, and the constraint chains the sequential assignment performed on these variables. Note that this rule does not check the satisfiability of the constraint B1 resulting from the assignment in conjunction with the constraint B from the state; this is because if the latter is satisfiable, so is their conjunction since the newly constrained variables in B1 are fresh with respect to B.

One interesting case for symbolic specification can be observed in the semantics of inclusive gateways, axiomatized by the rule in Figure 6. In a version without data, when a token arrives at a split gateway, any number of outgoing flows are selected and assigned newly created tokens that start executing right away. However, in a symbolic version with data, the situation is more complex because all possible flow selections Fig. 6. Arrival of a token to an inclusive split gateway need to be considered and checked for satisfiability relative to the global constraint. E.g, if there are n outgoing flows, then there are at most 2 n -1 possible selections satisfiable relative to the global constraint. Each one of these scenarios, computed by the auxiliary function gen, can be identified by the set of the m constraints (0 < m ≤ n) associated to the selected outgoing flows, say Γ, and the set of the nm constraints associated to the outgoing flows that are not selected, say ∆. Then, the constraint B1 associated to such selection is logically equivalent to the following conjunction of constraints:

γ∈Γ γ ∧ δ∈∆ ¬δ.
Such a constraint needs to be interpreted with respect to the current variable indexing, resulting in a new constraint, say B2; this is done with the help of the auxiliary function process-expression. Finally, a split is possible if the constraint representing the symbolic split is compatible with the constraint B accumulated in the state, i.e., if check-sat(B and B2) evaluates to true.

Symbolic Execution and Reachability Analysis

Symbolic execution and reachability analysis can be useful for exploring infinitely many system executions at once. In the rewriting modulo SMT implementation available from Maude, symbolic execution of the rewrite theory R presented in Section 4 uses a combination of term rewriting, matching modulo axioms, and SMT solving. This consists in applying equations and rewrite rules from an initial term (e.g., from an initial state such as the one in Figure 3) and querying the SMT solver for checking satisfiability of constraints at each rewrite step, when necessary. The full potential of rewriting modulo SMT can be exploited for solving existential reachability queries in the initial model T R of a rewrite theory R modulo built-ins E 0 . The type of existential reachability question that rewriting modulo SMT can answer can be formulated as follows: are there states in t φ that can reach a state in u ψ ?

This question is especially useful for symbolically proving or disproving safety properties, such as inductive invariants and deadlock freedom of T R : when u ψ is a set of bad states, the goal is to check whether reaching a state in u ψ is possible.

In the rest of this section, we show how to use symbolic rewriting and symbolic reachability analysis for verifying properties of interest on data-aware processes encoded into Maude's rewriting logic. This is illustrated using the e-visa application process introduced in Section 2. Note that, beyond toy examples and the e-visa application process we use as running example in this paper, we have also applied our approach to two other examples we found in the literature: a drug store process [START_REF] Herbert | Using Stochastic Model Checking to Provision Complex Business Services[END_REF] and a DMN process on application file handling [25, Section 11.2].

Symbolic Rewriting

As for regular rewrite theories, rewriting may be useful for gathering a first understanding of the whereabouts of our systems. Consider the running example in Figure 2. For the initial state corresponding to the terms in Figures 3 and4, the following rewrite command in Maude symbolically executes the process for ten consecutive rewrite steps:

rew [ 1 0 ] initSystem ( v ( OK : Boolean ) v ( TRY : Integer ) v ( FSIZE : Integer ) v ( QUAL : Real ) ) .
The initSystem operator generates the initial state depending on the specified list of variables. Maude's output to this command corresponds to one of the possible states reached after ten rewrite steps; in this case, the output is the following term:

Integer + 1 , varidx : ( v ( OK ) | -> 0 , v ( TRY ) | -> 2 , v ( FSIZE ) | -> 1 , v ( QUAL ) | -> 0 ) >
In this state, there is exactly one token, at task t2, the "Upload scanned passport" task. The constraint indicates that the TRY variable has value 1 and that FSIZE#1 is at least 2. After a first upload of an oversized file, task "Alert size error" was executed, where the TRY variable got increased, and then moved to the task t2. Note that the index of variable TRY is set to 2 because of the initial assignment on this variable in the "Apply online" task, and its update in "Alert size error". The index for FSIZE is 1.

A constraint like the one in this final state can also be interpreted as the conditions on the initial state and interactions to lead us to such state. Although a symbolic state may represent an infinite number of concrete states, as a symbolic path may represent an infinite number of concrete executions, in this case, we can say that any execution in which we upload an oversized file will lead to this state in ten rewriting steps.

Symbolic Reachability Analysis

Beyond symbolic rewriting, symbolic reachability is useful in order to answer a number of interesting questions such as the following ones:

-What are the reachable states after execution of n rewrite steps? Notice that each rewrite represent an infinite number of possible executions. -Is it possible for an input variable to be assigned a certain value? As an example, can we check whether our running example can reach a state in which the TRY variable takes a value greater than 3? -Are there deadlocks in the process? -Does a process have unreachable flows or tasks?

In the rest of this section, we will see how reachability analysis can be used to answer these questions. Consider the following existential query, where R is the rewrite theory presented in Section 4 corresponding to the running example in Figure 2:

T R | = (∃OK:Boolean, TRY:Integer, FSIZE:Integer, QUAL:Real, St:Conf) initSystem(v(OK) v(TRY) v(FSIZE) v(QUAL)) * → R St ∧ "St is → R -irreducible" ∧ "TRY = 3 in St".
This query asks whether we can reach from our initial state an irreducible state (w.r.t. the rewrite relation) in which the value of the TRY variable can be 3. Observe that infinitely many states need to be considered in the query because some of the variables range over infinite domains (e.g., integer and real numbers). This means that such a query, in general, is beyond the reach of ground rewriting and would require, for instance, inductive techniques over the rewrite relation. However, the following search command can be issued in Maude to find a proof (or a counterexample) of the reachability query for → R using the symbolic rewrite relation R :

s e a r c h [ 1 ] initSystem ( v ( OK ) v ( TRY ) v ( FSIZE ) v ( QUAL ) ) =>! St such that check-sat ( get-constr ( St ) and process-expression ( get-varidx ( St ) , try === 3 ) ) .
Note the use of [START_REF] Baader | Term Rewriting and All That[END_REF] and =>! to indicate, respectively, our interest in finding exactly one witness to the existential reachability query and that such a witness needs to be irreducible (i.e., no rule can be applied to it). The function calls get-constr(St) and get-varidx(St) return, respectively, the constraint and the variable indexing from any execution state St. The satisfiability of the constraint TRY === 3 needs to be checked against the variable indexing at each corresponding execution state; this is achieved by invoking the auxiliary function process-expression. The above search command generates the following output:

Integer === 3 ) , varidx : ( v ( OK ) | -> 0 , v ( TRY ) | -> 4 , v ( FSIZE ) | -> 3 , v ( QUAL ) | -> 1 ) >
This means that there is at least one ground execution from an initial state that reaches an irreducible state where the value of the TRY variable is 3. Indeed, the constraint tells us how to reach such a state: three files must be uploaded, the first two with size over 2 MB and the third with a quality under the threshold. Observe that this solution is actually a final state because all tokens have been processed. Note also the ellipses for brevity. The process does not change along the execution. The indication of requesting only one solution is important. Without it, Maude would have kept giving more and more solutions, in which any number of oversized passport files are uploaded due to the unguarded loop. This clearly points out a design error. A corrected version of the process is given below.

As mentioned earlier, the symbolic specification R presented in Section 4 can be used to automatically check for other safety properties such as deadlock freedom. In general, a reachability query associated to having a deadlock in T R can be cast as the following satisfaction relation:

T R | = (∃ - → x , St:Conf) initSystem( - → x ) * → R St ∧ "St is → R -irreducible" ∧ "St is not final".
In this formula, -→ x denotes the list of variables input to the process specified by R. The condition on the irreducibility of the state St is the same one appearing in the previous reachability goal. In the symbolic semantics R, a state is considered final whenever all tokens in the state have been consumed. This is of practical importance because checking for final states can be decided by checking the contents of the token set, namely, by checking if the set is empty. The following search command in Maude can be used to find deadlocks in the running example process:

Maude> s e a r c h [START_REF] Baader | Term Rewriting and All That[END_REF] in RUN :

initSystem ( v ( OK ) v ( TRY ) v ( FSIZE ) v ( QUAL ) ) =>!
Integer + 1 ) , varidx : ( v ( OK )| -> 0 , v ( TRY )| -> 5 , v ( FSIZE )| -> 4 , v ( QUAL )| -> 1 ) >
The witness provided shows that a deadlock can actually be reached. The constraint in the deadlock state tells us that by uploading a file with poor quality after three oversized files, we reach a state in which there is a token at the flow sf12, the outgoing flow of task "Alert quality error". Note that in that state the variable TRY has value 4, and none of the alternative branches of the following exclusive split can be triggered.

Let us now illustrate the check of whether certain flows or tasks are reachable. The following command proves that the task "Pay for fees" cannot be reached with an oversized file. In this section we have included the results provided by Maude on the number of executions and time obtained when executing all the rewrite and search commands. If we look at the last search command above, we can see that the exploration of 500 states took around 8 seconds. This number is rather low for Maude, if compared to standard rewriting/search. Notice however that symbolic rewriting/search involves additional satisfiability checks during the rewriting process, which are handled by invocation to back end SMT solvers.

Last but not least, let us give a corrected version of the running example (Figure 7) where the problem coming from an erroneous handling of the number of attempts has been resolved. This was achieved using an exclusive split gateway before the scanned passport upload, which checks for the number of attempts. If this number is greater than three, the process terminates. Note that all the properties mentioned beforehand in this section are satisfied by this new version of the process as we will show in the final part of this section.

There are now only eight possible ways to reach a final state with the variable TRY with value 3, showing the different combinations for uploading an invalid file at most 3 times:

s e a r c h initSystem ( v ( OK ) v ( TRY ) v ( FSIZE ) v ( QUAL ) )
=>! St such that check-sat ( get-constr ( St ) and process-expression ( get-varidx ( St ) , gen-intvar ( " TRY " ) === 3 ) ) .

Integer >= 3 ) , varidx : ( v ( OK ) | -> 0 , v ( TRY ) | -> 4 , v ( FSIZE ) | -> 3 , v ( QUAL ) | -> 0 ) > . . .
Integer >= 3 ) , varidx : ( v ( OK ) | -> 0 , v ( TRY ) | -> 4 , v ( FSIZE ) | -> 3 , v ( QUAL ) | -> 3 ) >
The new version of the process is deadlock free: Finally, as for the previous version, there is no way to reach the "Pay for fees" task (t9) with an oversized file:

s e a r c h [ 1 , 5 0 0 ] initSystem ( v ( OK ) v ( TRY ) v ( FSIZE ) v ( QUAL ) ) =>! St such that get-tokens ( St ) =/=
s e a r c h [ 1 , 5 0 0 ] initSystem ( v ( OK ) v ( TRY ) v ( FSIZE ) v ( QUAL ) ) =>!

Related Work

Several works have focused on providing rigorous definitions and formal semantics for business processes using Petri nets, process algebras, or abstract state machines, see, e.g., [7, 8, 14, 18-20, 26, 29, 33, 34]. The main differences with respect to these related works are our focus on data-aware workflow models and the fact that our encoding gives a symbolic semantics to BPMN by translation to Maude. As far as data-based analysis is concerned, Decision Model and Notation (DMN) is a recent OMG standard for modeling decisions in an interchangeable format. DMN can be used into workflow-based notations for representing conditions. [START_REF] Calvanese | Semantics and Analysis of DMN Decision Tables[END_REF] proposes a formal semantics of DMN decision tables, a notion of DMN table correctness, and algorithms that check the detection of overlapping rules and missing rules. These algorithms have been implemented in the DMN toolkit and validated through empirical evaluation.

Our modeling language provides the same expressiveness as decision tables existing in DMN, but our analysis techniques go further since they allow to verify properties of interest on the whole flow of control taking data and conditions into account.

Herbert and Sharp [START_REF] Herbert | Using Stochastic Model Checking to Provision Complex Business Services[END_REF] choose to simplify the modeling of exclusive/inclusive split gateways by considering probabilities instead of conditions. They propose an algorithm for translating a BPMN subset extended with probabilistic information into the guarded command language used by PRISM. This enables model checking of quantitative properties of business processes such as transient probabilities, occurrence of events, and best-/worst-case scenarios. [START_REF] Herbert | Using Stochastic Model Checking to Provision Complex Business Services[END_REF] uses the notion of rewards, from Markov Models [START_REF] White | Markov Decision Processes[END_REF], as annotated values that can be used to keep track of quantities of interest (e.g., execution times, number of iterations, etc.) in processes.

In [START_REF] Prandi | Formal Analysis of BPMN via a Translation into COWS[END_REF], Prandi et al. propose a formalization for BPMN models which supports rewards and probabilistic elements. They propose a conversion of BPMN models into a model expressed in the Calculus for Orchestration of Web Services (COWS) [START_REF] Pugliese | A Calculus for Orchestration of Web Services[END_REF], which can then be analyzed by using model checking. [START_REF] Nguyen | A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies[END_REF] focuses on the analysis of choreography models. The main property of interest in that context is called conformance and aims at checking whether the distributed implementation and the choreography behave identically. The authors mainly focus on data description. Their approach supports choreographies extended with conditions and relies on SMT solving for conformance checking.

Several authors have used rewriting logic and Maude to model and analyze BPMN processes. El-Saber and Boronat [START_REF] El-Saber | BPMN Formalization and Verification using Maude[END_REF] propose a translation of BPMN into rewriting logic with a special focus on data-based decision gateways. They provide mechanisms to avoid structural issues in workflows such as flow divergence by introducing the notion of "well-formed" BPMN process. Their approach aims at avoiding incorrect syntactic patterns whereas we propose automated analysis at the semantic level. Kheldoun et al. [START_REF] Kheldoun | Specification and Verification of Complex Business Processes -A High-Level Petri Net-Based Approach[END_REF] propose high-level Petri nets and to use Maude's LTL model checker for, respectively, specifying BPMN processes and analyzing behavioral properties. They also focus on handling exceptions and activity cancellation. Durán and Salaün used Maude to represent BPMN processes enriched with time features in [START_REF] Durán | Verifying Timed BPMN Processes using Maude[END_REF]. In this paper, they show how real-time analysis of such BPMN processes could be performed. Specifically, they used simulations, reachability analysis and model checking, and calculate certain properties such as minimum and maximum expected response times, maximum degree of parallelism, and synchronization times. Corradini et al. present in [START_REF] Corradini | BProVe: A Formal Verification Framework for Business Process Models[END_REF] their tool BProVe, a friendly tool for the verification of business processes modeled in BPMN. The tool accepts BPMN processes in standard notation and can perform checks of soundness and safeness on them, as defined in [START_REF] Wynn | Business Process Verification -Finally a Reality![END_REF] and [START_REF] Dijkman | Semantics and analysis of business process models in BPMN[END_REF], respectively, using Maude's LTL model checker.

Concluding Remarks

This paper focused on the BPMN modeling language enhanced with constructs for supporting data (variables and conditions). A a symbolic semantics for BPMN with data was proposed using Maude's rewriting logic framework. The transformation to Maude enables the verification of process models, including properties such as deadlock freedom and reachability of certain states based on data constraints. The verification task can be automated by using rewriting modulo SMT techniques. The approach was used on several use cases, including an online e-visa application process.

As far as future work is concerned, a first perspective is to increase the number of properties to verify. A first step in this direction is the verification of livelock absence. As initially proposed in [START_REF] Rocha | Rewriting Modulo SMT and Open System Analysis[END_REF], the approach presented in this work can also benefit of LTL model checking based on rewriting modulo SMT. The challenge here is in implementing effective mechanisms for dealing with the state explosion problem, such as the ones presented in [START_REF] Bae | Guarded terms for rewriting modulo SMT[END_REF]. The authors are also considering equational abstractions for rewriting modulo SMT. A second perspective aims at combining some previous work on timed BPMN [11] with the approach for data-based process models presented here. This will certainly result in a richer language for process modeling and the likely need of new verification techniques, useful both for timing and data-based analysis.

  c r l [ execTask ] : < PId : Process | nodes : ( task ( NId , TaskName , FId1 , FId2 , AsgL ) , Nodes ) , flows : ( flow ( FId2 ) , Flows ) , Atts > < SId : Simulation | tokens : ( token ( NId ) , Tks ) , constr : B , varidx : VMp , Atts1 > => < PId : Process | nodes : ( task ( NId , TaskName , FId1 , FId2 , AsgL ) , Nodes ) , flows : ( flow ( FId2 ) , Flows ) , Atts > < SId : Simulation | tokens : ( token ( FId2 ) , Tks ) , constr : ( B and B1 ) , varidx : VMp1 , Atts1 > i f ( VMp1 , B1 ) := prepare-update ( AsgL , VMp ) .

  c r l [ splitGatewayInclusive ] : < PId : Process | nodes : ( split ( NId , inclusive , FId , LTIB ) , Nodes ) , flows : Flows , Atts > < SId : Simulation | tokens : ( token ( FId ) , Tks ) , constr : B , varidx : VMp , Atts1 > => < PId : Process | nodes : ( split ( NId , inclusive , FId , LTIB ) , Nodes ) , flows : Flows , Atts > < SId : Simulation | tokens : ( tokens ( IL ) , Tks ) , constr : ( B and B2 ) , varidx : VMp , Atts1 > i f ILL1 . IL . ILL2 := gen ( project1 ( LTIB ) ) / \ B1 := get-constr ( IL , LTIB ) / \ B2 := process-expression ( VMp , B1 ) / \ check-sat ( B and B2 ) .

<

  p : Process | nodes : . . . , flows : . . . > < s : Simulation | tokens : token ( t2 ) , constr : ( TRY # 1 : Integer === 0 and FSIZE # 1 : Integer >= 2 and TRY # 2 : Integer === TRY # 1 :

Solution 1 ( 1 : 2 : 2 : 3 : 4 :

 112234 state 1 5 5 ) states : 171 rewrites : 2111 in 68 ms cpu ( 7 0 ms real ) ( 3 0 8 7 4 rewrites / second ) St --> < p : Process | nodes : . . . , flows : . . . > < s : Simulation | tokens : empty , constr : ( TRY # 1 : Integer === 0 and FSIZE # Integer >= 2 and TRY # Integer === TRY # 1 : Integer + 1 and FSIZE # Integer >= 2 and TRY # Integer === TRY # 2 : Integer + 1 and FSIZE # 3 : Integer < 2 and QUAL # 1 : Real < 9 / 1 0 and TRY # Integer === TRY # 3 : Integer + 1 and TRY # 4 :

1 : 2 : 2 : 3 : 3 : 4 : 4 : 1 : 5 :

 122334415 St such that get-tokens ( St ) =/= empty . Solution 1 ( state 2 4 9 ) states : 265 rewrites : 2852 in 97 ms cpu ( 9 9 ms real ) ( 2 9 1 8 3 rewrites / second ) St --> < p : Process | nodes : . . . , flows : . . . > < s : Simulation | tokens : token ( sf12 , 0 ) , constr : ( TRY # 1 : Integer === 0 and FSIZE # Integer >= 2 and TRY # Integer === TRY # 1 : Integer + 1 and FSIZE # Integer >= 2 and TRY # Integer === TRY # 2 : Integer + 1 and FSIZE # Integer >= 2 and TRY # Integer === TRY # 3 : Integer + 1 and FSIZE # Integer < 2 and QUAL # Real < 9 / 1 0 and TRY # Integer === TRY # 4 :

  s e a r c h [ 1 , 5 0 0 ] initSystem ( v ( OK ) v ( TRY ) v ( FSIZE ) v ( QUAL ) ) =>!St such that token-at ( " Pay for fees " , St ) and check-sat ( get-constr ( St ) and process-expression ( get-varidx ( St ) , gen-intvar ( " FSIZE " ) > 2 ) ) . No solution . states : 8846 rewrites : 117728 in 7818 ms cpu ( 8 1 5 1 ms real ) ( 1 5 0 5 7 rewrites / second )

Fig. 7 .TRY # 3 : 4 :

 734 Fig. 7. Running example: e-visa application process (V2)

Solution 8 ( 3 : 3 : 4 :

 8334 state 2 5 9 ) states : 267 rewrites : 3457 in 134 ms cpu ( 1 3 6 ms real ) ( 2 5 7 3 9 rewrites / second ) St --> < p : Process | nodes : . . . , flows : . . . > < s : Simulation | tokens : empty , gtime : 0 , constr : ( TRY # 1 : Integer === 0 and TRY # 1 : Integer < 3 and FSIZE # 1 : Integer < 2 and QUAL # 1 : Real < ( 9 / 1 0 ) . Real and TRY # 2 : Integer === TRY # 1 : Integer + 1 and TRY # 2 : Integer < 3 and FSIZE # 2 : Integer < 2 and QUAL # 2 : Real < ( 9 / 1 0 ) . Real and TRY # Integer === TRY # 2 : Integer + 1 and TRY # 3 : Integer < 3 and FSIZE # 3 : Integer < 2 and QUAL # Real < ( 9 / 1 0 ) . Real and TRY # Integer === TRY # 3 : Integer + 1 and TRY # 4 :

  E is confluent modulo B if and only if for all t, t 1 , t 2 ∈ T Σ (X), if t → * E/B t 1 and t → * E/B t 2 , then there is u ∈ T Σ (X) such that t 1 → * E/B u and t 2 → * E/B u. The term t ↓ E/B ∈ T Σ (X) denotes the E-canonical form of t modulo B so that t → * E/B t ↓ E/B and t ↓ E/B cannot be further reduced by → E/B

	The rewrite system is sort decreasing modulo B if and only if for each (t → u if γ) ∈ -→ E and substitution -→ E θ, ls(tθ) ≥ ls(uθ) if (Σ, B, -→ E ) γθ. The system -→ E is operationally terminating modulo B [10] if and only if there is no infinite well-formed proof tree in (Σ, B, -→ E ). Furthermore, -→

  empty .

	No solution .
	states : 293 rewrites : 3333 in 123 ms cpu ( 1 2 6 ms real ) ( 2 6 8 8 2 rewrites / second )

  St ) , gen-intvar ( " FSIZE " ) > 2 ) ) .

	St
	such that token-at ( " Pay for fees " , St )
	and
	check-sat (
	get-constr ( St )
	and
	process-expression ( get-varidx ( No solution .
	states : 293 rewrites : 3530 in 133 ms cpu ( 1 3 5 ms real ) ( 2 6 5 1 8 rewrites / second )
	s e a r c h [ 1 , 5 0 0 ] initSystem ( v ( OK ) v ( TRY ) v ( FSIZE ) v ( QUAL ) )
	=>! St
	such that token-at ( t9 , St )
	and
	check-sat (
	No solution .

get-constr ( St ) and process-expression ( get-varidx ( St ) , gen-intvar ( " FSIZE " ) > 2 ) ) . states : 293 rewrites : 3490 in 132 ms cpu ( 1 3 4 ms real ) ( 2 6 3 9 0 rewrites / second )

Acknowledgments. The authors would like to thank the anonymous reviewers for their valuable comments on an earlier draft of this paper. F. Durán has been partially supported by Spanish MINECO/FEDER project TIN2014-52034-R and Univ. Málaga, Campus de Excelencia Internacional Andalucía Tech. The work of C. Rocha was partially supported by CAPES, Colciencias, and INRIA via the STIC AmSud project "EPIC: EPistemic Interactive Concurrency" (Proc. No 88881.117603/2016-01), and by Capital Semilla 2017, project "SCORES: Stochastic Concurrency in Rewrite-based Probabilistic Models" (Proj. No. 020100610).


Paco Bustamante

Yves Cherel

Florence Caurant

P Miramand

Cadmium, copper and zinc in octopuses from Kerguelen Islands, Southern Indian Ocean

Keywords: Cephalopods, Octopus, Sub-Antarctic, Heavy metals, Cadmium, Digestive gland, Detoxification processes

come

Cadmium, copper and zinc in octopuses from Kerguelen

Islands, Southern Indian Ocean

INTRODUCTION

Recent studies have shown elevated concentrations of Cd in several marine invertebrates from Antarctic areas, mostly in crustaceans [START_REF] Hennig | Metal concentrations in Antarctic zooplankton species[END_REF][START_REF] Mauri | Heavy metals in the Antarctic scallop Adamussium colbecki[END_REF]Petri & Zauke 1993;Zauke & Petri 1993;[START_REF] Ahn | Baseline heavy metal concentrations in the antarctic clam, Laternula elliptica in Maxwell Bay, King George Island, Antarctica[END_REF][START_REF] Bargagli | Elevated cadmium accumulation in marine organisms from Terra Nova Bay (Antarctica)[END_REF]. Data on Cd levels in mollusks from this area are few. Especially, there are no data available regarding cephalopods. First, cephalopods occupy a predominant niche in the trophic chains [START_REF] Rodhouse | Role as consummers[END_REF], particularly in the Antarctic Polar Frontal Zone in the South Atlantic Ocean, where they, especially the ommastrephid Martialia hyadesi, occupy the ecological niche of epipelagic fish [START_REF] Rodhouse | Cephalopods occupy the ecological niche of epipelagic fish in the Antarctic Polar Front Zone[END_REF]. Cephalopods are predominant in the trophic system, because they are eaten by many oceanic animals like marine mammals [START_REF] Clarke | Cephalopods in the diet of cetaceans and seals[END_REF][START_REF] Clarke | Cephalopods as prey. III. Cetaceans[END_REF], and seabirds [START_REF] Croxall | Cephalopods as prey. I. Seabirds[END_REF][START_REF] Cherel | A review of the food of albatrosses[END_REF]. In the Southern Ocean, benthic octopuses were found in the food of Rockhopper and Gentoo penguins [START_REF] Brown | Seasonal and annual variation in diets of macaroni (Eudyptes chrysolophus) and southern rockhopper (E. Chrysocome chrysocome) penguins at sub-Antarctic Marion Island[END_REF][START_REF] Adams | Temporal variation in the diet of the gentoo penguin Pygoscelis papua at sub-Antarctic Marion Island[END_REF], royal albatrosses [START_REF] Imber | Feeding ecology of Antarctic and sub-Antarctic Procellariiformes[END_REF] and Weddell seals (Clarke & McLeod 1982). They were also reported as minor but regular prey of southern elephant seals [START_REF] Rodhouse | Cephalopod prey of the southern elephant seal, Mirounga leonina[END_REF]) and albatrosses [START_REF] Cherel | A review of the food of albatrosses[END_REF]. In Kerguelen waters, octopuses are common items of black-browed albatrosses during the chick-rearing period (Y. Cherel and H. Weimerskirch, unpublished data) and they were found in the diet of gentoo penguins [START_REF] Bost | Variation spatio-temporelle des ressources marines et stratégies adaptatives des oiseaux côtiers : le cas du Manchot papou (Psygoscelis papua)[END_REF]. Second, some studies on elemental bioaccumulation show that cephalopods accumulate high levels of trace elements, particularly Cd and Cu (Ghiretti-Magaldi et al. 1958;[START_REF] Rocca | Copper distribution in Octopus vulgaris Lam. hepatopancreas[END_REF][START_REF] Renzoni | Mercury concentration in the water, sediments and fauna of an area of the Tyrrhenian coast[END_REF][START_REF] Martin | High copper concentrations in squid livers in association with elevated levels of silver, cadmium, and zinc[END_REF][START_REF] Smith | Concentrations of the elements Ag, Al, Ca, Cd, Cu, Fe, Mg, Pb and Zn, and the radionuclides 210 Pb and 210 Po in the digestive gland of the squid Nototodarus gouldi[END_REF][START_REF] Miramand | High concentrations of some heavy metals in tissues of the Mediterranean octopus[END_REF][START_REF] Miramand | Concentration and distribution of heavy metals in tissues of two cephalopods, Eledone cirrhosa and Sepia officinalis, from the French coast of the English Channel[END_REF]. Thus, cephalopods represent important species for studying the transfer of Cd into marine food webs in Antarctic and sub-Antarctic areas.

This paper describes the bioaccumulation and tissue distribution of Cd, Cu and Zn in two octopus species living in the Kerguelen shelf waters: Graneledone sp. and Benthoctopus thielei. The Kerguelen Islands constitute a small archipelago in the South Indian Ocean, at the Antarctic Polar Frontal Zone (Fig. 1), where release of heavy metals is presumably negligible or non-existent. Moreover, the Kerguelen Islands are of special interest because there is no information available on heavy metal levels in invertebrates from sub-Antarctic areas.

MATERIALS AND METHODS

Octopuses were collected from catches of a trawling fishery for Patagonian toothfish Dissostichus eleginoides in the upper slope (400-600 m) of the northern Kerguelen shelf, located between 47°00' and 47°20'S, and 69°00' and 69°20' E. They were immediately frozen aboard and kept at -20°C. Two groups of cephalopods were used: some were collected in February 1994, the others in May/June 1995. In order to calculate allometric equations between body mass, body length, hood, and crest lengths of beaks (Y. Cherel, unpublished data), the first group was thawed one time and re-frozen before heavy metal analysis. Thus, due to possible metal diffusion during a thawing/freezing cycle [START_REF] Martin | High copper concentrations in squid livers in association with elevated levels of silver, cadmium, and zinc[END_REF], the distribution of heavy metals in various tissues was only measured in the latter group.

Digestive gland, branchial hearts, gills, digestive tract, genital tract and ink sac were totally removed from the dissected individuals. In addition, pieces of mantle muscle and of the skin were sampled to determine metal concentrations. This implies that the remains of the animal were composed of arms, the rest of the mantle, muscle and skin. For all animals, stomach contents were removed before metal analysis. Our laboratory participate to European intercalibration exercises which allowed to quantify the internal analytical variability about 12.5 %.

For the nomenclature of the two octopus species commonly found in Kerguelen waters, i.e.

Benthoctopus thielei and Graneledone sp. (a still undescribed species closely related to G. antarctica) we followed [START_REF] Nesis | Cephalopods of the world. Squids, Cuttlefishes, Octopuses, and Allies[END_REF]. Seventeen individuals of each species were used: 11 females (mean wet wt = 123 ± 89 g) and 6 males (mean wet wt = 121 ± 75 g) of Benthoctopus thielei and 11 females (mean wet wt = 85 ± 93 g) and 6 males (mean wet wt = 208 ± 98 g) of Graneledone sp. Each individual has been weighted and measured (mantle length, total length).

Tissue samples (whole individual regarding 1994 samples and the different organs regarding 1995 samples) were dried for several days at 80°C until constant weight. Two aliquots of approximately 300 mg of each homogenised dry sample were digested with 4 ml of 65 % HNO 3 and 1 ml of HClO 4 70 % during 24 hours at 80°C. After evaporation, the residues were dissolved in nitric acid 0.3 N. Blank were carried through the procedure in the same way as the sample. Cu and Zn were determined by flame and Cd by flameless atomic absorption spectrophotometry using a Varian spectrophotometer Vectra 250 Plus with Deuterium background correction.

All glassware and plastic was cleaned with HNO 3 / HCl 1N and rinsed with deionized water.

Reference material, Orchard-Leaves standard (NBS) and MA-A-2 fish-flesh standard (IAEA) were treated and analysed in the same way. The results for standards are shown in Table 1.

All the results are given in micrograms of metal per gram of the dry weight tissue (µg/g dry wt). For each element, the mean ± standard deviation and the coefficient of variation are given. Distribution percentages of metals are given in percent of the total fresh weight of the individual.

RESULTS

Our sampling included males and females and represented a large range of size and weight: between 14 g and 279 g for Benthoctopus thielei and between 6 g and 343 g for Graneledone sp. Metal concentrations (µg/g dry wt) in Benthoctopus thielei and Graneledone sp. from the Kerguelen Island waters are reported in Table 2. In both species, Cd, Cu and Zn were concentrated in similar amounts. Mean Cd concentrations were 39.1 ± 5.3 µg/g in Graneledone sp. and 38.2 ± 7.6 µg/g in Benthoctopus thielei. Mean Cu concentrations were 68 ± 30 µg/g and 68 ± 29 µg/g and corresponding Zn concentrations 131 ± 19 µg/g in Graneledone sp. and 166 ± 39 µg/g in Benthoctopus thielei.

For both species, heavy metal concentrations were similar in small and large individuals. The analytical results for males and females were compared. ANOVA test have shown no significant differences between metals concentrations by sex (p<0.05). For both elements, no correlation were found for Graneledone sp. while in Benthoctopus thielei, Cd and Zn were correlated positively (p<0.05) and Cu and Zn were correlated negatively (p<0.05). Figure 2 show relationships between metal concentrations and mantle length by sex. Correlation coefficients were significant in Graneledone sp. for Cu and Zn in females and in Benthoctopus thielei for Cd in males and Zn in females. The coefficients of variation (CV) were less than 25 % for Cd and Zn, and near to 40 % for Cu (Table 2).

The distribution of heavy metals in one individual of each species are reported in Table 3.

Most of the Cd (91 % and 89 %, respectively in Graneledone sp. and Benthoctopus thielei) was accumulated in the digestive gland with concentrations as high as 369 and 245 µg/g in Graneledone sp. and Benthoctopus thielei, respectively. Zn concentration was higher in Benthoctopus thielei digestive gland (416 µg/g) and represented 53 % of the total amount, whereas in Graneledone sp. it was close to the concentrations found in the other organs (102 µg/g), and represented only 16 % of the total amount. In both species, the remains contained high percentages of Zn with 67 % for Graneledone sp. and 44 % for Benthoctopus thielei.

Total Cu concentrations (165 µg/g for Graneledone sp. and 25 µg/g for Benthoctopus thielei) as well as distribution were quite different between both individuals. The digestive gland of Graneledone sp. exhibited high Cu concentration (1092 µg/g) and corresponded to the major site of Cu storage with 79 % of the total body burden. In contrast, the digestive gland of Benthoctopus thielei contained only 25 % of the total Cu body burden and displayed a very low concentration (42 µg/g).

DISCUSSION

Metal Levels

Despite the analysis of males and females over a large range of size and weight, the variability of the metal concentrations was relatively small. The most striking feature was the higher values for the coefficient of variation for Cu compared to that of Cd and Zn.

The homogeneity of metal concentrations found in the 34 individuals was particularly remarkable. We hypothesise that the concentrations measured in this study were a relatively good representation of the concentrations encountered in specimens subject to similar ambient water composition and probably similar diets. Nevertheless, the coefficient of variation of Cu was particularly interesting. This coefficient was higher in both species sampled from the Kerguelen waters than in other octopuses species: 27 % in Octopus vulgaris [START_REF] Miramand | High concentrations of some heavy metals in tissues of the Mediterranean octopus[END_REF] and 11 % for Eledone cirrhosa [START_REF] Miramand | Concentration and distribution of heavy metals in tissues of two cephalopods, Eledone cirrhosa and Sepia officinalis, from the French coast of the English Channel[END_REF]. Moreover the Cu variability was higher than Cd variability. This was surprising when one considers that Cu and Zn (unlike Cd) are essential elements which implies that they are maintained at a fairly constant concentration. The high Cd concentration might disrupt Cu homeostasis.

In order to compare the concentration of trace elements with other cephalopod species, Table 4 shows Cd, Cu and Zn concentrations in the digestive gland and in whole individuals of cephalopods from the European waters where industrial releases of pollutants occur. In both species from Kerguelen waters, Zn concentrations were in the same range than those found in other species (Table 4).

In contrast, Cd and Cu concentrations found in octopuses caught from Kerguelen waters were noteworthy. Cu concentrations were low except for one individual for Graneledone sp. (165 µg/g) and two individuals of Benthoctopus thielei (114 and 149 µg/g) (Table 2 andTable 4).

Cd concentrations in both species were very high (Table 2). These concentrations in Kerguelen Islands octopuses were one order of magnitude greater than those found in others cephalopods (Table 4).

Such high Cd concentrations were unexpected for mollusks coming from a presumably unpolluted area far from any anthropogenic source of contaminants. Recently, [START_REF] Bargagli | Elevated cadmium accumulation in marine organisms from Terra Nova Bay (Antarctica)[END_REF] have measured Cd concentrations in various organisms caught in Terra Nova Bay (Antarctica). All organisms collected in this area showed relatively elevated concentrations, but in most groups, concentrations were lower than 10 µg/g dry wt or close to 15 µg/g dry wt.

Only some samples of the sponge Porifera exhibited higher Cd concentrations (i.e. 10-80 µg/g dry wt). In Antarctic areas, such high Cd concentrations only occurred in the scallop Adamussium colbecki [START_REF] Berkman | Trace metal concentrations in scallops around Antartica: extending the Mussel Watch Programme to the Southern Ocean[END_REF], and in some zooplanktonic crustaceans, particularly in the hyperiid amphipod Themisto gaudichaudii. These species accumulated Cd to levels similar or greater than Kerguelen octopuses [START_REF] Hennig | Metal concentrations in Antarctic zooplankton species[END_REF]. Compared with Cd concentrations in other mollusk species, these concentrations were also remarkable. Thus, most of the mollusks species (bivalves and gastropods) caught in unpolluted areas contained Cd concentrations lower than 5 µg/g dry wt [START_REF] Eisler | Trace metal concentrations in marine organisms[END_REF][START_REF] Bryan | Pollution due to heavy metals and their compounds[END_REF]. Only some Pectinidae species which are well known for their ability to accumulate Cd, exhibited concentrations nearer to those found in the Kerguelen octopuses [START_REF] Bryan | The occurrence and seasonal variation of trace metals in the scallops Pecten maximus (L.) and Chlamys opercularis (L.)[END_REF][START_REF] Berkman | Trace metal concentrations in scallops around Antartica: extending the Mussel Watch Programme to the Southern Ocean[END_REF][START_REF] Francesconi | Cadmium in the saucer scallop, Amussium balloti, from western Australian waters: concentrations in adductor muscle and redistribution following frozen storage[END_REF]. For comparison, Cd concentrations similar to those found in whole Kerguelen octopuses (excluding Pectinidae) have only encountered in filter-feeders caught in a Cd polluted area [START_REF] Boutier | La contamination par le cadmium en Gironde et son extension sur le plateau continental. Rapport IFREMER n° DERO, -86.12-MR. 28 p Boyle PR[END_REF].

The particular strong accumulation of Cd in octopuses from Kerguelen, an area without anthropogenic inputs of this metal, is difficult to explain. The Kerguelen Islands are located at the Antarctic Polar Frontal Zone (Fig. 1), and Cd enrichment in surface waters may occur due to upwelling of deep nutrient-rich waters. Unfortunately, we lack measurements of dissolved Cd in Kerguelen sea water and this hypothesis cannot be tested. Nevertheless, metal analyses of the stomach content of some Kerguelen octopuses showed elevated Cd concentrations greater than 30 µg/g dry wt (unpublished data). This suggests elevated Cd concentrations in octopus prey which could be an indicator of a Cd enrichment in Kerguelen waters or bottom fauna. In this context, food could be an important pathway of Cd uptake for Kerguelen Octopodidae. Octopus eat many prey species, mainly crustaceans, mollusks and fishes (Boyle 1990;[START_REF] Mcquaid | Feeding behaviour and selection of bivalve prey by Octopus vulgaris Cuvier[END_REF][START_REF] Laidig | Feeding on euphausiids by Octopus rubescens[END_REF] but it has been impossible to determine clearly the diets of Kerguelen octopuses from stomach contents and no fish otoliths was found. The carnivorous diets of octopuses rely on the hypotheses of low supply of Cd by the soluble phase, unlike suspensivors species which filter important volumes to feed on micro-organisms. Moreover, gills in cephalopods shown low Cd concentrations and present less than 1 % of the total Cd body burden (Table 3, Miramand & Bentley 1992).

Distribution of metals and implication in detoxification process

The dissection of a single individual of Graneledone sp. and one individual of Benthoctopus thielei (Table 3) indicate that these Kerguelen octopuses exhibit a Cd distribution in tissue similar to that found in octopuses from the Mediterranean Sea [START_REF] Miramand | High concentrations of some heavy metals in tissues of the Mediterranean octopus[END_REF], or in the English Channel [START_REF] Miramand | Concentration and distribution of heavy metals in tissues of two cephalopods, Eledone cirrhosa and Sepia officinalis, from the French coast of the English Channel[END_REF], with about 90 % of the metal contained in the digestive gland. Digestive gland of Kerguelen octopuses contained very high concentrations (Table 3). In contrast, muscle concentrations are close to or slightly greater than those encountered in other octopus species (0.1-0.5 µg/g dry wt) [START_REF] Miramand | High concentrations of some heavy metals in tissues of the Mediterranean octopus[END_REF][START_REF] Miramand | Concentration and distribution of heavy metals in tissues of two cephalopods, Eledone cirrhosa and Sepia officinalis, from the French coast of the English Channel[END_REF][START_REF] Barghigiani | Interaction between selenium and cadmium in Eledone cirrhosa of the Northern Tyrrhenian Sea[END_REF]). Thus, the high concentrations measured in whole Kerguelen octopuses were due to the high concentrations in the digestive gland.

The high Cd concentrations in the digestive gland were greater than those usually found in others cephalopods (Table 4). Only two species caught in the Pacific Ocean exhibited similar or higher concentrations: [START_REF] Martin | High copper concentrations in squid livers in association with elevated levels of silver, cadmium, and zinc[END_REF] found 287 µg/g dry wt in the squid liver of Ommastrephes bartrami and 782 µg/g dry wt in the squid liver of Symplectoteuthis oualaniensis. High concentrations of Cd in the digestive gland of cephalopods suggested that most of the detoxification processes occurred in this organ. However, studies on these mechanisms are scarce and concern only two squids species. [START_REF] Tanaka | Subcellular distribution and binding of heavy metals in the untreated liver of the squid; comparison with data from the livers of cadmium and silver exposed rats[END_REF][START_REF] Finger | Molecular association of Cu, Zn, Cd and 210 Po in the digestive gland of the squid Nototodarus gouldi[END_REF][START_REF] Finger | Molecular association of Cu, Zn, Cd and 210 Po in the digestive gland of the squid Nototodarus gouldi[END_REF] have shown an association of Cd with high molecular weight material in the digestive gland of the squids Todarodes pacificus and Nototodarus gouldi. Nevertheless Cd detoxification processes in octopuses are not known and more studies are needed to clarify this mechanism. In this context, Kerguelen octopuses appear as good species for future investigations. Branchial hearts of octopuses, which have polyhedral cells containing granules with brown pigments (adenochromes) rich in iron [START_REF] Fox | Adenochrome a glandular pigment in the branchial hearts of the octopus[END_REF][START_REF] Ghiretti-Magaldi | Pathways of terminal respiration in marine invertebrates. I. The respiratory system in cephalopods[END_REF][START_REF] Nardi | Isolation and distribution of adenochrome(s) in Octopus vulgaris[END_REF][START_REF] Schipp | Distribution of copper and iron in some central organs of Sepia officinalis (Cephalopoda). A comparative study by flamless atomic absorption and electron microscopy[END_REF], are certainly also engaged in storage and detoxification processes for some trace elements such as cobalt, copper, vanadium (Ueda et al. 1979;[START_REF] Nakahara | Peculiar accumulation of cobalt-60 by the branchial hearts of Octopus[END_REF][START_REF] Miramand | High concentrations of some heavy metals in tissues of the Mediterranean octopus[END_REF], or transuranic elements (Guary et al. 1981;[START_REF] Miramand | Association of americium-241 with adenochromes in the branchial hearts of the cephalopod Octopus vulgaris[END_REF][START_REF] Guary | Experimental studies on the biokinetics of plutonium and americium in the cephalopod Octopus vulgaris[END_REF]. However, in European octopuses with relatively low Cd concentrations in whole tissues, branchial hearts (concentrations < 0.3 ± 0.1 µg/g) do not seem to be implicated in Cd detoxification processes [START_REF] Miramand | High concentrations of some heavy metals in tissues of the Mediterranean octopus[END_REF][START_REF] Miramand | Concentration and distribution of heavy metals in tissues of two cephalopods, Eledone cirrhosa and Sepia officinalis, from the French coast of the English Channel[END_REF]. In octopuses from Kerguelen, branchial hearts exhibited high Cd concentrations (Table 3). A possible hypothesis could be a is a threshold effect, that is, beyond a certain Cd concentration the digestive gland would not be sufficient for the entire detoxification processes and branchial hearts would then be used.

The ink sac of cephalopods contents melanin, a macromolecule with the ability to act as a cation-exchange resin [START_REF] Larsson | Studies on the melanin-affinity of metal ions[END_REF]. It is known that tissues containing melanin pigments are often rich in some trace elements such as manganese, copper and zinc. The binding affinity of melanin towards certain metal ions has been investigated in some detail [START_REF] Aime | NMR studies of 1-dopa melanin-manganese (II) complex in water solution[END_REF]). The interaction is essentially electrostatic and its strength is therefore expected to be dependent on the charge to mass ratio of the metal ion. However, [START_REF] Sarzanini | Metal content in Sepia officinalis melanin[END_REF] have found in Sepia officinalis that the ability to concentrate metals by melanin is significantly lower than that observed for melanin sampled from other marine organisms, such as bivalves [START_REF] Simkiss | Metal detoxification and bioaccumulation in molluscs[END_REF]. The ink could be an excretion pathway for Cd while its missing in Kerguelen octopuses exclude Cd excretion by this way.

Conclusion

Due to the very high concentrations of cadmium in both Benthoctopus thielei and Graneledone sp., these cephalopods probably play an important role in the process of Cd transfer to top vertebrates predators in this region. Cd is well known for its accumulation in kidneys of vertebrates, where at high doses it causes renal diseases [START_REF] Nicholson | Cadmium and mercury nephrotoxicity[END_REF][START_REF] Nogawa | Cadmium. In: Changing Metal Cycles and Human Health[END_REF][START_REF] Lauwerys | Cadmium[END_REF]). For human consumption, a "provisional tolerable weekly intake" of 400-500 µg Cd per person has been proposed by the World Health Organisation (1972). This approximates 1µg/kg body weight for most individuals or 55-70 µg/day. In Kerguelen, the daily consumption by marine predators of one small octopus (about 10 g wet weight) is sufficient to reach the equivalent of this dose. Thus, Kerguelen top predators, which have cephalopods in their diets, could achieve high levels of Cd in their tissues, like in the South Atlantic Ocean where cephalopod-eating albatrosses have high levels of cadmium in kidney and liver [START_REF] Muirhead | Heavy metal concentrations in the tissues of seabirds from Gough Island, South Atlantic Ocean[END_REF]. In this context, research of Cd levels in tissues of top marine vertebrates from Kerguelen Islands, with particular attention to kidney, is of particular interest.

Table 3

 3 Metal concentrations (µg/g dry wt) and percentage distribution (wet wt) in the organs of one male Graneledone sp. (fresh weight = 343 g) and one female Benthoctopus thielei (fresh weight = 279 g) caught in the Kerguelen shelf waters in May/June 1995. Skin and muscles are included in remainder.

	Organs	Cd	%	Cu	%	Zn	%	Water content
								(%)
	Graneledone sp.
	Digestive gland	369	91.2	1092	79.9	102	15.8	68
	Branchial hearts	24.6	0.11	465	0.61	126	0.35	84
	Gills	22.6	0.52	530	3.59	98	1.41	84
	Digestive tract	90.5	1.96	354	2.27	92	1.25	85
	Genital tract	5.57	0.41	31	0.68	306	1.4	84
	Remainder	6.64	5.76	50	12.9	121	67.0	86
	Skin	1.94	-	67	-	121	-	90
	Muscles	0.37	-	15	-	113	-	87
	Whole individual	43.5	100	165	100	128	100	85
	Benthoctopus thielei
	Digestive gland	215	88.6	42	24.8	416	52.6	69
	Branchial hearts	31.5	0.15	306	3.46	172	0.26	85
	Gills	49.1	0.89	168	7.07	147	0.82	84
	Digestive tract	85.1	1.30	35	1.24	202	0.95	86
	Genital tract	10.3	0.47	34	3.59	101	1.41	84
	Remainder	7.06	8.54	22	59.8	118	43.9	85
	Skin	0.81	-	18	-	95	-	90
	Muscles	0.21	-	3	-	138	-	82
	Whole individual	36.2	100	25	100	159	100	84

Acknowledgments. We thank Pascal Robidou for collecting octopuses on the French trawler 'Kerguelen de Trémarec' in February 1994, and Guy Duhamel for providing us with other specimens collected in May/June 1995. This work was supported financially by the Regional Council of Poitou-Charentes and Rhône-Poulenc, and by the Institut Français pour la Recherche et la Technologie Polaires and the Terres Australes et Antarctiques Françaises.

 [START_REF] Koubbi | Environmental influences on spatio-temporal oceanic distribution of ichthyoplankton around the Kerguelen Islands (Southern Ocean)[END_REF].

Graneledone sp.

Benthoctopus thielei