Quentin Nivon

Gwen Salaün

Debugging of BPMN Processes using Coloring Techniques

A business process is a collection of related tasks organized in a specific order whose overall execution solves a specific service or product. BPMN has become the standard workflow-based notation for developing business processes. Designing business processes using BPMN is however error-prone. Recent works have proposed verification techniques for analyzing processes and for detecting possible issues. In particular, model checking is an established technique for automatically verifying that a model (e.g., a BPMN process) satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the process is not an easy task, especially if the counterexample is not expressed using the original notation (BPMN here). In this paper, we focus on the model checking of BPMN processes. When properties are violated, we propose to transform counterexamples back on to the original BPMN process in order to simplify the debugging steps. To do so, we rely on coloration techniques. The approach proposed in this paper is fully automated using several tools and was validated on many examples.

Introduction

For decades, business processes used by industries and companies have not stopped evolving and becoming more complicated. This had the consequence of enlarging the already existing gap between business analysts, developers and end users. Reducing this gap has been one of the main motivations for the BPMN notation to be invented. Business Process Model and Notation is a notation allowing to graphically describe a business process, with the goal of making it easily understandable for any type of users. In some companies, especially the ones dealing with safety-critical or safety-related systems, it is very important to perform verifications of the behaviour of the BPMN model(s) describing their process(es). Model checking is a well-known technique to perform such tasks, widely used since its beginnings in the 1980's. Indeed, if the property is verified in each point of the model, the model checker returns T rue. Otherwise it returns F alse and gives a counterexample corresponding to a path in the specification that does not satisfy the property. Nonetheless, understanding this counterexample can be complex, even for expert users. It is even more complex for beginners and BPMN users, as the counterexample returned by the model checker is either textual (sequence of actions violating the property), or visual (graphical representation of the sequence of actions violating the property), but it is not expressed in the BPMN notation.

In this paper, we focus on the model checking of BPMN processes. The main goal of this work is to transform counterexamples back on to the original BPMN process in order to simplify the debugging steps. To do so, we rely on some already existing techniques. The first one, called VBPMN [START_REF] Krishna | VBPMN: Automated Verification of BPMN Processes[END_REF], is used for converting BPMN into LNT. The second one is model checking [START_REF] Milner | Communication and Concurrency[END_REF], that we use for analyzing and debugging LNT specifications with respect to some temporal logic properties. The last one, called CLEAR [START_REF] Barbon | Debugging of Concurrent Systems Using Counterexample Analysis[END_REF] is used for generating a colored LTS representing the full set of traces violating the property, called a counterexample LTS (CLTS) [START_REF] Barbon | Debugging of Concurrent Systems Using Counterexample Analysis[END_REF]. This CLTS can however be hard to understand, for several reasons: (i) the CLTS notation strongly differs from the BPMN notation, (ii) the CLTS can be quite large if there are lots of bugs or if the BPMN contains certain types of constructs, such as parallel gateways, and (iii) the CLTS does not show exactly the source of the bugs.

In practice, the CLTS may give enough information regarding the bug(s) for expert users, but is not sufficient for beginner users, for whom the size of the CLTS and its syntactic differences with the BPMN notation may be a problem. To handle this problem, the main idea of our approach is to transform the information available in the CLTS model on to the BPMN model for simplifying the debugging phase. To do so, the approach consists of three cases or steps, which are handled one after the other. The first step, called matching analysis, aims at verifying whether the satisfaction/violation of the property can be directly represented on the initial BPMN process. If this is the case, we color this BPMN process and give it back to the user. This is the best case, because no modification of the initial BPMN process is required. If this can not be done, we generate a new BPMN process. This second step is called unfolding. This generated process is semantically equivalent to the initial one. Moreover, it has, by construction, the advantage of allowing us to color it to represent the satisfaction and the violation of the property. However, this generated BPMN process can possibly be quite large, in terms of number of nodes. In this case, understanding this process can be difficult for the user. To limit this, we propose a solution in which we try to reduce the size of this BPMN process by restructuring parts of the process using, for instance, parallel gateways. This third step preserves the semantics of the input process and is called folding.

Note that the class of temporal properties handled in this work is the class of safety properties, which is widely used in the verification of real-time and critical systems. Safety properties state that "something bad must not happen".

Figure 1 gives an overview of the contributions presented in this paper. The approach takes as input the initial BPMN process and the temporal logic property to verify. The first step is performed by the VBPMN tool [START_REF] Krishna | VBPMN: Automated Verification of BPMN Processes[END_REF], which takes the BPMN process given as input and transforms it into LNT. Then, the LNT specification and the temporal logic property are given to CLEAR [START_REF] Barbon | Debugging of Behavioural Models with CLEAR[END_REF], which generates a CLTS. Starting from this CLTS and the BPMN process, we perform the matching analysis. If a matching is found between the CLTS and the BPMN process, the BPMN process is colored according to the CLTS. Otherwise, we generate a new BPMN process with the help of the CLTS, we try to fold it, and finally we color the resulting process.

All the steps of the approach are fully automated by a prototype tool we implemented. As for evaluation, we carried out two experimental studies in order to assess the usability and performance of the approach on real-world and large examples. The rest of this paper is organized as follows. Section 2 introduces several useful notions regarding BPMN and model checking. Section 3 presents the main steps of our approach for visualizing counterexamples at the BPMN level. Section 4 describes the tool support and experiments. Section 5 surveys related work and Section 6 concludes the paper.

Background

In this section, we introduce some notions needed to understand this work. First, we describe BPMN, which serves as input model to our approach. Then, we give an overview of Labelled Transition Systems and model checking. Finally, we explain what is a Counterexample LTS (CLTS).

Business Process Model and Notation (BPMN) is a business process modeling method aiming at describing business processes used by industries and companies. The main goal of this notation is to provide a way of representing precisely the process used by the company, and to make it understandable to every one (business analysts, developers, end users). This notation has been first introduced in 2004 by the Business Process Management Initiative and has become an ISO/IEC standard in 2013 [START_REF]Information technology -Object Management Group Business Process Model and Notation[END_REF]. It is now widely used across the world. The current version of BPMN is BPMN 2.0 and more details about it can be found in [START_REF]Information technology -Object Management Group Business Process Model and Notation[END_REF]. In this work, we focus on a subset of the BPMN syntax. This subset, described in Figure 2, takes into account initial and end events, tasks and gateways. A gateway is either a split or a merge. A split gateway consists of a single incoming flow and multiple outgoing flows. A merge gateway consists of multiple incoming flows and a single outgoing flow. Several types of gateways are available, such as exclusive, parallel, and inclusive gateways. An exclusive gateway corresponds to a choice among several flows. A parallel gateway executes all possible flows at the same time. An inclusive gateway executes one or several flows. A study made in [START_REF] Krishna | Checking Business Process Evolution[END_REF] on more that 800 real-world BPMN processes shows that the subset used in this paper suffices to build more than 90% of these real-world BPMN processes. Definition 1. (BPMN Graph) A BPMN process can be represented as a graph B =(S N ,S E ) where S N is a set of nodes (tasks, event, gateways, ...) and S E is a set of edges (sequence flows). Definition 2. (LTS) An LTS is a tuple M =(S,s 0 ,Σ,T ) where S is a finite set of states, s 0 ∈S is the initial state, Σ is a finite set of labels, T ⊆S×Σ×S is a finite set of transitions. A transition is represented as s l -→s ′ ∈T , where l ∈Σ.

An LTS can be seen as the semantical model of a BPMN process. Thus, both models have the same semantics. Indeed, all the elements of the BPMN process have a corresponding element in the LTS, and vice-versa. The correspondence is the following: each state of the LTS is either a sequence flow or an exclusive gateway in the BPMN process, and each transition is a task in the BPMN process. An LTS exhibits all possible executions of a system. One specific execution is called a trace. Definition 3. (Trace) Given an LTS M = (S,s 0 ,Σ,T ), a trace of size n ∈ N is a sequence of labels l 1 ,l 2 ,...,l n ∈Σ such that s 0 l1 -→s 1 ∈T,s 1 l2 -→s 2 ∈T,...,s n-1 ln -→s n ∈T . A trace is either infinite because of loops or finite when the last state s n has no outgoing transitions. The set of all traces of M is written as t(M).

Model checking consists in verifying that a behavioural model or specification (LOTOS New Technology (LNT) [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator[END_REF] in this work) satisfies a given temporal property P , which specifies some expected requirement of the system. Temporal properties are usually divided into two main families: safety and liveness properties [START_REF] Milner | Communication and Concurrency[END_REF]. In this work, we focus on safety properties, which are widely used in the verification of real-world systems. Safety properties state that "something bad must not happen". A safety property is usually formalized using a temporal logic. We use MCL (Model Checking Language) [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF] in this work, which is an action-based, branching-time temporal logic suitable for expressing properties of concurrent systems. MCL is an extension of alternation-free µ-calculus with regular expressions, data-based constructs, and fairness operators. A safety property can be semantically characterized by an infinite set of traces t P , corresponding to the traces that violate the property P in an LTS. If the LTS model does not satisfy the property, the model checker returns a counterexample, which is one of the traces belonging to t P . Definition 4. (Counterexample) Given an LTS M =(S,s 0 ,Σ,T ) and a property P , a counterexample is any trace which belongs to t(M)∩t P .

The approach presented in [START_REF] Barbon | Debugging of Concurrent Systems Using Counterexample Analysis[END_REF][START_REF] Barbon | Debugging of behavioural models using counterexample analysis[END_REF] takes as input an LNT specification, which compiles into an LTS model, and a temporal property. The original idea of this work is to identify decision points where the specification (and the corresponding LTS model) goes from a (potentially) correct behaviour to an incorrect one. These choices turn out to be very useful to understand the source of the bug. These decision points are called faulty states in the LTS model. In order to detect these faulty states, we first need to categorize the transitions in the model into different types. The transition type allows to highlight the compliance with the property of the paths in the model that traverse that given transition. Transitions in the counterexample LTS can be categorized into three types:

correct transitions, which only belong to paths in the model that represent behaviours which always satisfy the property. incorrect transitions, which only belong to paths in the model that represent behaviours which always violate the property. neutral transitions, which belong to portions of paths in the model which are common to correct and incorrect behaviours.

The information concerning the detected transitions type (correct, incorrect and neutral transitions) is added to the initial LTS in the form of tags. The set of transition tags is defined as Γ = {correct,incorrect,neutral}. Given an LTS M = (S,s 0 ,Σ,T ), a tagged transition is represented as s (l,γ)

---→s ′ , where s, s ′ ∈S, l ∈Σ and γ ∈Γ . Thus, an LTS in which each transition has been tagged with a type is called a tagged LTS. Definition 5. (Tagged LTS) Given an LTS M =(S,s 0 ,Σ,T ), and the set of transition tags Γ , the tagged LTS is a tuple M T =(S T ,s 0 T ,Σ T ,T T ) where S T =S, s 0 T =s 0 , Σ T =Σ, and T T ⊆S T ×Σ T ×Γ ×S T .

The tagged LTS where transitions have been typed allows us to identify faulty states, which are those in which an incoming neutral transition is followed by a choice between at least two transitions with different types (correct, incorrect, neutral). Such a faulty state consists of all the neutral incoming transitions and all the outgoing transitions.

Definition 6. (Faulty State) Given the tagged LTS M T =(S T ,s 0 T , Σ T ,T T ), a state s∈S T , such that ∃t=s ′ (l,γ)
---→s∈T T , t is a neutral transition, and ∃t ′ =s

(l,γ)
---→s ′′ ∈T T , t ′ is a correct or an incorrect transition, the faulty state s consists of the set of transitions T nb ⊆ T T such that for each t ′′ ∈ T nb , either

t ′′ = s ′ (l,γ) ---→ s ∈ T T or t ′′ =s (l,γ) ---→s ′′′ ∈T T .
By looking at outgoing transitions of a faulty state, we can identify four categories of faulty states (Figure 3): Finally, a CLTS can be defined as a tagged LTS with faulty states.

BPMN Coloration

In this section, we first give an overview of the whole approach for simplifying the debugging of BPMN processes. Second, we present in details the folding step, because it is the most complex step of the approach. More details about the whole approach can be found in [START_REF] Nivon | Model Checking and Debugging of BPMN Processes using Coloration techniques[END_REF].

Overview

In this subsection, we give an overview of the three main steps of the approach, which are summarized in Figure 1.

Matching Analysis. The goal of this first step is to determine whether the counterexamples of the temporal logic property appearing in the CLTS can be represented directly on the initial BPMN process. This verification proceeds in two steps. In the first step, we verify whether all the transitions of the CLTS having the same label have the same color. Such a situation can happen whenever we reach a BPMN task that can either violate and satisfy the property, regarding its position in the execution flow. If it is not the case, we know that the initial BPMN process can not be colored directly. Indeed, if two transitions with the same label have different colors, the corresponding (unique) task of the BPMN process should have two different colors at the same time, which is not possible. To solve this issue, we duplicate this task, making by the same time the initial BPMN process not colorable directly. Otherwise, we perform the second step. In this step, we try to associate each faulty state of the CLTS to a unique node of the BPMN process. Such an association is found whenever a BPMN node has ancestor tasks (resp. descendant tasks) for which labels correspond to the labels of the incoming transitions (resp. outgoing transitions) of the current faulty state, and the current BPMN node has not already been associated to a faulty state. If this association is found for each faulty state of the CLTS, then a matching exists between the BPMN process B and the CLTS M, noted Match(B,M). Then, we color the initial BPMN process, and return it to the user. Figure 4 illustrates this second step. Note that the four faulty states, namely states 3, 4, 5 and 6, have been mapped to four unique nodes of the initial BPMN process. Thus, a matching was found between the initial BPMN process and the CLTS, so the initial BPMN process is colored and returned to the user. If no such matching can be found, we perform a step called unfolding.

Fig. 4: Example of matching between the CLTS and the BPMN process

Unfolding. In this second step, we generate a new BPMN process that is semantically equivalent to the initial one. This equivalence is preserved because each element of the CLTS has a corresponding element in the BPMN process. More precisely, a transition in the CLTS corresponds to a task in the BPMN process, and a state in the CLTS corresponds either to a sequence flow or to an exclusive split gateway in the BPMN process. As this generated BPMN process is semantically equivalent to the CLTS, and the CLTS is colored, this BPMN process has the advantage of being colorable. Nonetheless, some constructions in the initial BPMN process may generate large BPMN processes during this phase, such as parallel gateways that will be rewritten in their exclusive versions according to Milner's theorem [START_REF] Baier | Principles of Model Checking[END_REF] 1 . This phenomenon is accentuated by an implemental step called flattening, which occurs during the unfolding. In this step, each state of the CLTS having more than one incoming transition will be duplicated. More precisely, if the CLTS contains states s such that ∃s ′ l1 -→s and s ′′ l2 -→s, then the flattening step will generate a new state s ′′′ equivalent to s such that s ′′ l2 -→s ′′′ , and discard the transition s ′′ l2 -→s. The flattening is necessary to be able to detect unfolded parallel gateways and replace them by their folded version, while remaining semantically equivalent to the initial BPMN process. Figure 5 illustrates the unfolding phase, along with the flattening step. As the reader can see, each transition of the CLTS has become a BPMN task, while each state has become a sequence flow or an exclusive gateway. Moreover, one can see that the number of nodes in the generated BPMN process is greater than the number of states and transitions in the CLTS. To mitigate this state explosion, we perform a third and last step called folding. Folding. This third and last step aims at reducing the size (in terms of number of nodes) of the generated BPMN process, while increasing the understandability of this process. To do so, we focus on the detection of specific patterns, that we call interleavings or diamonds. Figure 6 illustrates with an example of such diamond.

Fig. 6: Example of diamond pattern

As the reader can see, the first task of the upper path corresponds to the second task of the bottom path, and vice versa. In fact, such diamonds result of the rewriting of parallel gateways into their exclusive versions, according to Milner's theorem. Milner's theorem also states that the reverse transformation is possible, allowing us to rewrite this diamond into a parallel gateway containing tasks T 1 and T 2 . This transformation may seem of minor interest in this example, as it only reduces the number of tasks from four to two. However, detecting unfolded parallel gateways containing three or more elements may lead to significant reductions of the total number of tasks of the process. Once such gateways have been detected, we generate their semantically equivalent folded version, and we replace the unfolded version by the folded one in the generated BPMN process. This transformation is of prime interest, because it reduces the number of nodes of the BPMN process, while making it syntactically closer to the initial one, and consequently, more understandable for the user.

Folding

In this section, we focus on the folding step, which is the most crucial and complex one in our approach. In the following, only exclusive gateways are considered, as inclusive and parallel gateways have been rewritten in their exclusive versions according to Milner's theorem. In this context, the word gateway will abusively refer to exclusive gateways all along this subsection. Second, the term folding will be used to refer to the transformation of a set of tasks belonging to an exclusive gateway into a set of tasks belonging to a parallel gateway. Finally, the word BPMN process will refer to the unfolded version of the initial BPMN process. Before detailing the folding approach, we need to differentiate two types of gateways: the nested gateways and the outer gateways. The difference between them is that a nested gateway is included in at least another gateway, while an outer gateway is not included in any other gateway. Note that this a strict categorization, because any gateway is either a nested gateway, or an outer gateway. The folding approach proposed is composed of four main steps:

-Step 1 retrieves all the outer gateways of the BPMN process that contain only nodes with identical colors, and separate each outer gateway and its subnodes into groups. In the rest of this section, we focus on Step 3, which is the core step of this approach. Indeed, this step determines if and how each gateway of the generated BPMN process can be folded. Before going further, it is worth noticing that the notion of maximum foldability represents the maximum size of the equivalent folded gateway. This notion is a maximum because, in practice, the effective foldability of a gateway can be lower than its maximum foldability, or even null if the gateway is not foldable. Now, let us detail Step 3.

Step 3 is decomposed into two phases: one for gateways of maximum foldability 2, and one for gateways of maximum foldability strictly higher than 2. In this paper, we detail the first phase, managing gateways of maximum foldability 2. In this phase, we analyse all the paths starting from the current gateway in order to extract three pieces of information about it. The first two concern the foldability of the gateway. To decide whether a gateway is foldable or not, we analyze its outgoing paths. The outgoing paths is a set containing all possible paths that can be taken from a node, and which finish either by an element that is already in the path (loop), or by an end event. During this step, we check whether there exists a couple of paths for which the first node of the first path corresponds to the second node of the second path, and vice versa. Such paths are called size-2 diamond-shaped paths. ∀(i,j)∈[1;|Out(G E )|],i̸ =j, if ∃p i =(e i,1 ,...,e i,n ), p j =(e j,1 ,...,e j,m )∈Out(G E ),n,m≥2 s.t. e i,1 =e j,2 and e i,2 =e j,1 , then p i and p j are size-2 diamond-shaped paths.

Figure 6 illustrates a gateway having size-2 diamond-shaped paths. Note that the first node of the first path corresponds to the second node of the second path, and vice versa. If such paths are found, we compute the second information. To compute it, we differenciate the outgoing paths of the current gateway in three sets: those starting with the first size-2 diamond-shaped path, those starting with the second size-2 diamond-shaped path, and the others that are ignored. We keep the first two sets, and remove the first two tasks from each path of each set. The remaining paths in each set are called out-of-scope paths. Once we have computed those two sets of out-of-scope paths, we compare them. If they are identical, we conclude that the current gateway is foldable, with an effective foldability value of 2. We then mark this gateway as foldable in a parallel gateway of size 2. The tasks belonging to this parallel gateway correspond to the first two tasks of the size-2 diamond-shaped paths found. We also store all the out-of-scope paths computed.

If the gateway has been marked as foldable, we compute the third information. This information is used to know whether all the children of the current gateway are parallelizable or not. In practice, if the number of children of a gateway exceeds its effective foldability value, then we know that some of these children are not parallelizable. We called this information gateway purity.

Definition 9. (Gateway Purity) Let G F E be a foldable exclusive split gateway of effective foldability n∈N ≥2 . G F E is pure if and only if size(G F E )=n.

Once the purity characteristic has been evaluated, we fill the metadata with the paths making the gateway not pure, if they exist. We call them impure paths. Figure 9 shows an example of impure path. In this example, the path containing the tasks Inspect Documents and Perform Data Analysis is an impure path. Indeed, this gateway can be reduced to a parallel gateway of size 2 containing the tasks Update Info Records and Background Verification, so the path circled in red on the figure is an impure path.

Fig. 9: Example of gateway having 1 impure path When all this information has been computed, we know precisely if and how each gateway of maximum foldability 2 is foldable. Then, we make use of this information to compute the foldability of gateways of maximum foldability 3, then 4, and so on. For these gateways, the approach is slightly different than the one we have presented above. Indeed, in such cases, we make use of the knowledge we have about the foldability of the inner gateways of maximum foldability lower than the maximum foldability of the current gateway by 1 to know whether it is foldable. A gateway of maximum foldability f ≥3 is foldable if and only if it has f children and for which each child is parent of a pure gateway of maximum foldability f -1 containing all the children of the initial gateway except the current child. Figure 10 shows equivalence relationships between gateways illustrating how this step works in practice. As the reader can see, the first picture contains only exclusive gateways. After computing information about gateways of maximum foldability 2, we are able to generate the BPMN process shown in the second picture. With this knowledge, we understand that the whole gateway is a parallel gateway containing three tasks that have been unfolded. Thus, we are able to fold it back, as shown in picture 3. Now, we have a full representation of the foldabilities that can be processed, thanks to the metadata. Figure 11 illustrates this knowledge by giving a textual representation of the metadata of the 3 gateways G 1 , G 2 and G 3 visible on the figure. Following this information, we fold the foldable gateways and replace them Fig. 10: Equivalence relationships during the folding process in the unfolded BPMN process. Then, we return this BPMN process to the user. Figure 12 gives an overview of the whole folding process. It is worth noticing that, starting from a BPMN process containing 24 tasks, the folding step returned a semantically equivalent process consisting of 7 tasks. In the end, we give back to the user a colored BPMN process, containing either black, green, or red tasks. From this process, the user knows that all the paths containing red tasks violate the given property, while paths containing green tasks satisfy it.

Tool and Experiments

Tool

The prototype tool implementing the approach was written in Java and consists of about 10,000 lines of code. It is worth noting that the prototype tool contains a lot of processing steps which have not been described previously in this paper, and which mostly consists in rewriting elements in other formats, such as BPMN Fig. 12: Example of the whole folding process to graph, BPMN to CLTS, CLTS to graph, etc. The tool allows the user to perform all the steps detailed in the previous section. It is worth noting that the tool has been tested and validated on about 150 BPMN processes.

Empirical Study

The goal of this study was to evaluate the usability of our approach in practice by quantifying the number of BPMN processes that are directly colorable, and if they are not, the number of processes that can be folded after the unfolding step. We used for this study 13 real-world processes taken from the literature, and corresponding to various application domains (such as transport, finance, or metallurgy). These processes have been given to the tool along with one well-suited safety property of the kind "T 1 must not be executed before T 2 ". The results of this study are the following: 21% of the BPMN processes were directly colorable, and 29% were succesfully folded after unfolding. Overall, in 50% of the cases, we were either able to color the initial BPMN process or to improve the unfolded one.

Performance Study

This study aimed at evaluating the performance of our approach following two different points of view: (i) assessing the scalability of the prototype tool over real-world examples, and (ii) evaluating the scalability of the prototype tool when increasing the size of the BPMN processes (in terms of nodes). Therefore, the BPMN processes used in this study are of three different kinds: 1: Results of the performance study on real-world BPMN processes As far as real-world BPMN processes are concerned, the empirical study shows that the execution time is rather low. The highest time in the table is reached for the first process (vacations booking), for which the tool takes three seconds to execute all the steps of our approach. Performance of the tool is thus good for real-world BPMN processes. Table 2 presents the results of the study for larger examples. This table contains a first column containing the identifier of the BPMN process, followed by three columns presenting the sizes of the BPMN process and the LTS, and ends with four columns containing the execution times of each element of the toolchain and the global execution time. As for the processes with many nodes (rows 1 to 4), one can see that the main source of computation time is due to the use of VBPMN and CLEAR, which take more than 99% of the execution time. As an example, this the case for process 4 in the table, which consists of hundreds of nodes, and for which our tool takes about 3 seconds to complete. Let us now focus on the examples with a high level of parallelism (rows 5 to 9). The unfolding phase of our approach generates processes with a high number of nodes (up to almost two hundreds of thousands nodes in the table for row 9). In such extreme situations, our prototype tool takes minutes or even hours to execute and complete its tasks. However, it is worth reminding that we have not found any real-world process with such a high level of parallelism. One may also mention that performing only partial unfolding would lead to a significant decrease of the execution time of the prototype on highly parallel processes. Nonetheless,

Related Work

Several previous works have focused on providing formal semantics and verification techniques for BPMN processes using a rewriting of BPMN into Petri nets, such as [START_REF] Martens | Analyzing Web Service Based Business Processes[END_REF][START_REF] Decker | Interaction-centric Modeling of Process Choreographies[END_REF][START_REF] Dijkman | Semantics and Analysis of Business Process Models in BPMN[END_REF][START_REF] Raedts | Transformation of BPMN Models for Behaviour Analysis[END_REF][START_REF] Corradini | An Operational Semantics of BPMN Collaboration[END_REF]. In these works, the focus is mostly on the verification of behavioural or syntactic problems of the BPMN, such as deadlock or livelock. As far as rewriting logic is concerned, in [START_REF] El-Saber | BPMN Formalization and Verification using Maude[END_REF], the authors propose a translation of BPMN into rewriting logic with a special focus on data objects and data-based decision gateways. They provide new mechanisms to avoid structural issues in workflows such as flow divergence by introducing the notion of well-formed BPMN process.

Rewriting logic is also used in [START_REF] Durán | Verifying Timed BPMN Processes using Maude[END_REF] for analyzing BPMN processes with time using simulation, reachability analysis, and model checking to evaluate timing properties such as degree of parallelism and minimum/maximum processing times.

Let us now concentrate on those using process algebras for formalizing and verifying BPMN processes, which are closer to the approach proposed in this paper. The authors of [START_REF] Wong | A Process Semantics for BPMN[END_REF] present a formal semantics for BPMN by encoding it into the CSP process algebra. They show in [START_REF] Wong | Verifying Business Process Compatibility[END_REF] how this semantic model can be used to verify compatibility between business participants in a collaboration. This work was extended in [START_REF] Wong | A Relative Timed Semantics for BPMN[END_REF] to propose a timed semantics of BPMN with delays. [START_REF] Capel | Automating the Transformation from BPMN Models to CSP+T Specifications[END_REF][START_REF] Mendoza-Morales | Conceptual Framework for Business Processes Compositional Verification[END_REF] focus on the semantics proposed in [START_REF] Wong | A Process Semantics for BPMN[END_REF][START_REF] Wong | A Relative Timed Semantics for BPMN[END_REF] and propose an automated transformation from BPMN to timed CSP. In [START_REF] Güdemann | VerChor: A Framework for the Design and Verification of Choreographies[END_REF] the authors have proposed a first transformation from BPMN to LNT, targeted at checking the of a BPMN choreography. In [START_REF] Corradini | An Operational Semantics of BPMN Collaboration[END_REF], the authors propose a new operational semantics of a subset of BPMN focusing on collaboration diagrams and message exchange. The BPMN subset is quite restricted (no support of the inclusive merge gateway for instance) and no tool support is provided yet.

The approach presented in [START_REF] Krishna | VBPMN: Automated Verification of BPMN Processes[END_REF] proposes verification and comparison techniques based on model checking. The BPMN process is translated into LNT, which is then mapped to LTS before being given as input to a model checker. This approach is close to ours, in the sense that it allows the user to verify a safety temporal logic property over a BPMN process, while providing him a counterexample in the form of an LTS if the property is violated. Other works, such as [START_REF] Kherbouche | Using model checking to control the structural errors in BPMN models[END_REF] and [START_REF] Maarouk | Formalization and Model Checking of BPMN Collaboration Diagrams with DD-LOTOS[END_REF] are also making use of model checking to perform verifications of temporal logic properties over BPMN processes.

All the approaches presented beforehand in this section are close to what we propose since they focus on the verification of BPMN processes. However, none of these works provide any solution to support the debugging of BPMN processes or to visualize counterexamples at the BPMN level.

Finally, we present the approach proposed in [START_REF] Muram | Counterexample Analysis for Supporting Containment Checking of Business Process Model[END_REF], which is the closest to ours. This approach aims at representing visually violations of temporal logic properties regarding a given BPMN process. The authors focus on what they called containment checking. Containment checking consists of verifying properties built from high-level BPMN processes (e.g., representations of BPMN processes without many details) over low-level models (e.g., complete representation of BPMN processes). In this work, the high-level BPMN process is translated into Linear Temporal Logic properties [START_REF] Kröger | Temporal Logic and State Systems[END_REF] while the lowlevel model is translated into SMV [START_REF] Bérard | SMV -Symbolic Model Checking[END_REF]. Both are given as input to the nuSMV [START_REF] Cimatti | NUSMV: a new symbolic model checker[END_REF] model checker which generates counterexamples if the property is violated. Then, the results are given to the visualization engine that represents, in BPMN notation, the counterexamples given by nuSMV. Both works differ in terms of verification: model checking of safety properties for us whereas [START_REF] Muram | Counterexample Analysis for Supporting Containment Checking of Business Process Model[END_REF] performs conformance verification of a model regarding a higher-level model. Moreover, they visualize the counterexample only if it can be represented on the initial BPMN process (i.e., if a matching exists), while we go beyond this case by providing additional coloration solutions if a matching does not exist.

Concluding Remarks

In this paper, we have proposed a way of improving and simplifying the comprehension and the visualization of safety property violations. The main objectives of the approach were (i) to give a visual feedback of the violation expressed in BPMN notation, (ii) to stay as syntactically close as possible to the initial BPMN process while remaining semantically equivalent, and (iii) to be as minimal as possible in terms of BPMN nodes in the final process. To reach these goals, we chose the coloration of BPMN processes as visualization technique. More precisely, we have first presented a solution in which the original BPMN process is directly colored according to the satisfaction/violation of the property given as input. However, even if this is the best solution because no modification of the original BPMN process is performed, there are cases in which it is not applicable. Therefore, we have proposed a complementary approach which, in a first step, generates a new BPMN process from the CLTS (unfolding), and in a second step, performs some minimization over it to lower the number of nodes (folding). The different steps of the approach presented in this paper were implemented in a tool written in Java consisting of about 10,000 lines of code. In order to evaluate the usability and the scalability of this prototype tool, we performed two studies: an empirical one to get insights on the behaviour of this approach on real-world examples, and a performance one aiming at ensuring that the prototype runs in reasonable time on real-world examples, and at verifying its scalability on large BPMN processes.

The main perspective of this work is to support liveness properties. In this case, counterexamples and counterexample LTSs have different shapes (lassos) [START_REF] Barbon | Counterexample Simplification for Liveness Property Violation[END_REF], and the approach thus deserves to be revisited to take this specificity into account.

Fig. 1 :

 1 Fig. 1: Overview of the approach

Fig. 2 :

 2 Fig. 2: Supported BPMN syntax

Fig. 3 :

 3 Fig. 3: The four types of faulty states

Fig. 5 :

 5 Fig. 5: Example of generation of a BPMN process from a CLTS (Unfolding)

Definition 7 .

 7 (Nested Gateway) Let B =(S N ,S E ) be a BPMN process, and S G N ⊂ S N the set of gateways composing B. ∀g ∈ S G N , g is a nested gateway if and only if ∃ path p = (e 1 ,...,e n ) s.t. e n = g, ∃i ∈ [1...(n-1)] where e i is a split gateway and ∃p ′ =(e ′ 1 ,...,e ′ m ) starting from e i for which g ∈p ′ . Definition 8. (Outer Gateway) Let B =(S N ,S E ) be a BPMN process, and S G N ⊂S N the set of gateways composing B. ∀g ∈S G N , g is an outer gateway if and only if g is not a nested gateway.

Figure 7

 7 Figure7illustrates nested gateways. As the reader can see, gateways SG2 and MG2, circled in red, are nested gateways, because they are part of the gateways SG1 and MG1. Conversely, these last are outer gateways, are they are not included in any other gateways. The folding approach proposed is composed of four main steps:

Fig. 7 :

 7 Fig. 7: Example of nested gateways

Proposition 1 .

 1 (Size-2 Diamond-Shaped Paths) Let G E be an exclusive split gateway and Out(G E ) the set of outgoing paths of G E .

Proposition 2 .

 2 (Out-of-scope Paths) Let G E be an exclusive split gateway of maximum foldability 2, (p 1 ,p 2 ) the size-2 diamond-shaped paths of G E , and DSP the set of outgoing paths of G E starting with p 1 or p 2 . ∀p=(e 1 ,...,e n )∈DSP , if size(p) ≥ 3, then the path p ′ =(e 3 ,...,e n ) is an out-of-scope path.

Figure 8

 8 Figure 8 shows an example of four out-of-scope paths belonging to two distincts sets of out-of-scope paths. One can see that round tasks and square tasks form two distinct out-of-scope paths, belonging to the same set. The same remark applies to triangle and diamond tasks.

Fig. 8 :

 8 Fig. 8: Example of gateway having 2 sets of 2 out-of-scope paths

Fig. 11 :

 11 Fig. 11: Textual representation of the gateways' metadata

  1. real-world examples of the empirical study presented in the previous section. 2. handcrafted examples that contain a high number of nodes. 3. handcrafted examples that are highly parallel.The results of this performance study are presented in Table1 and 2. Table1consists of three columns containing a short description of the BPMN process, the number of nodes in this process, and the execution time of the prototype tool.

	BPMN Process	Number of nodes	Execution time of the prototype tool (s)
	1. Vacations Booking	13	3.436
	2. Account Opening	22	1.209
	3. Publication Process	20	1.351
	4. Steel Transformation	42	1.478
	5. Plane Entry	27	2.235
	6. Mortgage Application	15	1.974
	7. Denoising	16	1.756
	8. Credit Offer	15	1.004
	9. Buying Process	29	1.540
	10. Business Process	15	1.325
	11. Job Hiring	29	1.798
	12. Login Process	17	1.204
	13. Support Ticket	22	1.431
	Table

Table 2 :

 2 Results of the performance study on two types of handcrafted BPMN processes the proposed approach is based on model checking techniques that perform a full unfolding of the BPMN process in order to verify the given property. As our starting point is the output of the model checker, we can not perform this partial unfolding.

	BPMN Process	Number of BPMN nodes	Number of states in the LTS	Number of nodes in the unfolded BPMN process	VBPMN execution time (s)	CLEAR execution time (s)	Prototype tool execution time (s)	Global execution time (s)
	1. Generated Large 1	62	140	62	15.98	0.164	1.881	18.03
	2. Generated Large 2	126	284	126	32.04	2.080	1.376	33.50
	3. Generated Large 3	254	572	254	165.4	6.461	2.440	174.2
	4. Generated Large 4	510	1,148	510	902.3	124.3	3.643	1030
	5. Generated Parallel 1	19	529	11,582	13.07	0.086	19.76	32.92
	6. Generated Parallel 2	20	606	23,165	13.15	0.089	82.68	95.92
	7. Generated Parallel 3	21	683	43,614	13.23	0.088	466.8	480.1
	8. Generated Parallel 4	22	770	87,229	13.61	0.082	3948	3961
	9. Generated Parallel 5	23	857	165,307	17.81	0.122	10100 10117

A parallel execution of two actions 'a' and 'b' for instance is equivalent to a choice between executing 'a' followed by 'b' or 'b' followed by 'a'.


BURY RISE, GALE CRATER, MARS. J M Comellas

A Essunfeld

R Morris

N Lanza

P J Gasda

D Delapp

R C Wiens

O Gasnault

S Clegg

C C Bedford

E Dehouck

B C Clark

R Anderson

W Fisher

V Lueth

EVIDENCE OF MULTIPLE FLUID EVENTS IN ELEVATED-MN CHEMCAM TARGETS IN THE BRAD

Evidence of multiple fluid events in elevated-mn chemcam targets in the brad-bury rise, gale crater, mars

Introduction: High concentrations of manganese in rocks on Mars could provide clues to the ancient climatic and atmospheric conditions of the planet. On Earth, it is well understood that elevated amounts of Mn oxides may be evidence of highly oxidizing conditions, because in most cases, Mn is only sensitive to high potential oxidants [1]. E.g., Mn is only recorded in the terrestrial rock record after the Great Oxidation Event, when microbial photosynthesis began to produce oxygen, causing a highly oxidizing environment conducive to Mn oxide precipitation [1,2]. Mn 2+ is a relatively mobile species, especially in more acidic and reducing water lacking CO2 [1].

Our analysis of rocks with MnO content greater than the mean bedrock value for MnO in Gale crater (0.2 wt.%) shows evidence of multiple early-to late-stage fluid events. We have observed that elevated Mn is often associated with diagenetic materials and typically decoupled from the initial stages of aqueous alteration [3].

Methods: In the first 600 sols of the NASA Curiosity rover's traverse across Gale crater, we identified 201 elevated-Mn targets in ChemCam data [4] and sorted them into 16 unique facies using the classification system developed by [4].

We created 576 binary oxide plots, one for every pair of major oxides within each facies. Due to the complexity of this dataset, we developed a technique using correlation heatmaps to determine the most interesting patterns in the data (Fig. 1) [5]. The patterns revealed in this approach guided the subsequent analysis. Results: In the ChemCam targets Selwyn and Rich-ardson_2, we observed both elevated-Mn points and Ca sulfate veins (Fig. 2). Both of these targets were sorted into the miscellaneous category (group 12) [4] and consist primarily of calcium sulfate deposits surrounded by dark-toned regions of elevated Mn. The elevated-Mn points in these targets plot along a possible mixing line between nontronite, a sodium iron aluminum silicate clay, and the soluble elements Ca, Na and K in an A-CNK-FM ternary diagram (Fig. 2).

Facies 13 contains targets with "light-toned crystals surrounded by a dark-toned matrix" [3]. We interpret these targets as altered basaltic material. The points that have elevated Mn generally lie on the dark-toned regions of targets in this facies (e.g., Fig. 3).

The elevated-Mn points in Facies 13 also plot along the possible nontronite-CNK mixing line (Fig. 4). The light-toned points in Fig. 4 have high amounts of Al2O3 and plot on the felsic end of the mafic-felsic line, but trend towards the Al2O3 apex. These points have a high chemical index of alteration (which suggests that they might be clay-rich, but of a different phase compared to nontronite). However, they are not elevated in Mn or Ca.

As described in [5], correlation heatmaps (e.g., Fig. 1) between Al2O3 and the other major oxides help illuminate any strong correlations with aluminum. Fe and Al are positively correlated in Facies 9, 10 and, 11, the three diagenetically altered facies. These facies contain light-toned rocks with concretions, dark-toned rocks with concretions, and altered mudstones with veins, respectively [3,4]. There are elevated-Mn points within these facies, as well, that plot along the possible nontronite-CNK mixing line. Discussion: Nontronite, which typically forms in altering basaltic material, has been detected using orbital spectral measurements in many places on Mars, including in Gale crater [6]. Fe and Al do not occur in a single mineral phase in igneous rocks, so any positive correlation would imply the presence of clays, possibly nontronite. Interestingly, Al is positively correlated with Fe, Ca, and Na in Facies 9, 10, and 11 (Fig. 1), which all have diagenetic material (e.g., veins and concretions). As Mn is a fluid-mobile element in the right conditions [1], the elevated-Mn points in these facies imply that the fluid that may have caused alteration of the phases to nontronite was also Mn-rich.

In addition, in this work, as in [3], we observed a relationship between calcium-sulfate veins and elevated Mn. Many other recent studies have seen ubiquitous Mn-rich fracture fills [e.g., 1, 7] and potential concretions [e.g., 7, 8, 9] throughout Gale crater. Our more recent analysis shows a trend between elevated-Mn and other alteration materials, such as concretions and clays, e.g., nontronite. Together, these observations are further evidence of multiple diagenetic events having occurred after the original dissolution of basaltic materials. This provides a stronger foundation for our hypothesis that Mn deposition was at least partially decoupled from rock weathering, and thus multiple early-and late-stage fluid events involving Mn took place in Gale crater [7].

Conclusion:

We observed a correlation between possible clay material (e.g., nontronite) and diagenetically altered targets with elevated-Mn points. This relationship supports the hypothesis that the same fluid that altered the basaltic material to form the clay also carried and deposited Mn. The existence of other diagenetic material (e.g., veins and concretions), together with the possible elevated-Mn and nontronite correlation, could be evidence of multiple fluid events in the history of Gale crater.

Acknowledgments: NASA Mars Exploration program and CNES, France.

Fig. 1 :

 1 Fig. 1: Correlation Heatmap between Al2O3 and the other major oxide compositions of the targets in facies 0 -15 [5]. Facies are labeled on the x-axis. Degree of correlation is represented by the shade of each square (darker = stronger correlation), and the type of correlation is represented by the color (blue = negative; red = positive) [5].

Fig. 2 :

 2 Fig. 2: Ternary diagram with Al2O3 (A), FeOT+MgO (FM), and CaO+Na2O+K2O (CNK) apices. Observation points from targets in Group 12, the miscellaneous category, are shown as circles with an MnO wt.% color scale. Darker colors represent higher concentrations of MnO wt.%. The points circled in red are the high-Mn points in the targets Selwyn and Richardson_2. The blue arrow represents the possible mixing line between CNK and nontronite. The black square represents the approximate location of pure nontronite.

Fig. 3 :

 3 Fig. 3: Cropped RMI of the ChemCam target King_Leopold from sol 574 in Facies 13. The red arrow points to an area between the light-toned crystals that shows elevated MnO and plots on the possible nontronite-CNK mixing line (see Fig. 4).

Fig. 4 :

 4 Fig. 4: Ternary diagram with Al2O3 (A), FeOT+MgO (FM), and CaO+Na2O+K2O (CNK) apices. Observation points from Facies 13, targets with "light-toned crystals in dark matrix," are shown as circles with a MnO wt.% color scale. Darker colors represent higher concentrations of MnO wt.%. The points circled in red are the elevated-Mn points along the possible nontronite-CNK mixing line. The points circled in green are the points with high Chemical Index of Alteration values. The black square represents the approximate location of pure nontronite.

  References: [1] Lanza et al. (2016) Geophysical research letters, 43(14), 7398-7407, [2] Maynard et al. (2010) Economic Geology, 105(3), 535-552, [3] Comellas et al. (2021) LPSC 52#2176, [4] Essunfeld et al. (2021) LPSC 52#2180, [5] Morris et al. (2022) this meeting, [6] Gainey et al. (2014) Elsevier 194-211, [7] Gasda et al. (2021) JGR, in review, [8] Lanza et al. (2021) LPSC 52#2231, [9] Gasda et al. (2021) LPSC 52#1272. 2445.pdf 53rd Lunar and Planetary Science Conference (2022)

2445.pdf 53rd Lunar and Planetary Science Conference (2022)


E Tichtchenko

V Folliet

O Simonin

B Bédat

L Glavier

A Esteve

C Rossi

Combustion model for thermite materials integrating explicit and coupled treatment of condensed and gas phase kinetics

Keywords: Combustion, Al/CuO, nanothermite, numerical simulation, multiphase

Nanothermites are interesting energetic systems as their combustion driven by the oxidation of the metallic fuel associated with the reduction of the oxidizer, can produce extremely fast burning rates exceeding hundreds of m.s -1 . In addition, by changing the reactant (composition, stoichiometry) geometry and compaction conditions, the control of the burning rate can be achieved, allowing the designer to customize the chemical energy for each application. To date, only rough combustion models exist, most restricting the combustion mechanisms to only condensed phase processes, thus providing an approximative prediction of structure-combustion performance relationships. This work presents a tri-phasic model for the combustion of Al/CuO powder considering 9 gaseous species (Al, Cu, O2, O, Al2O, Al2O2, AlO, AlO2, N2) and 4 condensed species (Al, Cu, CuO, Al2O3) that can be liquid or solid. The reactionnal scheme involves 12 heterogeneous reactions and 2 phase changes based on diffusional kinetics, while gaseous reactions are considered through a chemical equilibrium. A detailed description of the theoretical formulation and numerical method is presented, followed by a discussion of a closed-bomb simulation. This work highlights the great impact of the Al particles initial diameter on the pressure development in the chamber. After the initiation stage, the decomposition of CuO releases gaseous O2, which is spontaneously absorbed on the surface of submicronic Al particles and diffuses through alumina to react with pure Al. At high temperature, gaseous copper, aluminum sub-oxides and aluminum condense on both particle types. By contrast, Al particle micron-size limits the quantity of O2 absorption and gaseous species surface condensation, leading to the formation of a pressure pre-peak 4 times higher than the final chamber pressure.

1 1. Introduction
Thermites are composed of nano-micro sized metals (Al, Mg, Ti, B) and metal oxides (CuO, Fe2O3, Bi2O3, MoO3 . . .), which both participate in a highly exothermic and self-propagating combustion reaction accompanied with gas release in most cases. Interestingly, the reactant (oxide, fuel) geometry, composition and compaction conditions can be varied to tune their combustion characteristics making these materials of major interest for a number of applications, such as soldering/welding, generation of biocidal-agents and as additives in propellants, pyrotechnics and explosives. This combustion behavior variability imposes to rationalize experiments, guided by suitable modeling approaches. Several continuum/analytical models have been proposed to capture the reactants size, stoichiometry and porosity effects during nanothermite powder combustion. Kim et al. [START_REF] Kim | Computational modeling of combustion wave in nanoscale thermite reaction[END_REF] developed a simplified modeling analysis based on a 1D continuum heat transfer model using an activation energy associated with Al oxidation reaction to appreciate the ignition and combustion propagation characteristics in the Al/MoO3 nanoscale thermite. Along the same line, Brotman et al. [START_REF] Brotman | A Benchmark Study of Burning Rate of Selected Thermites through an Original Gasless Theoretical Model[END_REF] proposed a 1D modelling scheme integrating further mechanisms being characteristics of thermites reaction, such as the thermally activated transports of oxygen atoms, in association with the multiple barrier layers, fuel and oxidizer phase transformation. In all these approaches, the mass transport rate driving the reaction, described by exponential Arrhenius law [START_REF] Piekiel | Initiation and Reaction in Al/Bi 2 O 3 Nanothermites: Evidence for the Predominance of Condensed Phase Chemistry[END_REF][START_REF] Tichtchenko | Modeling the self-propagation reaction in heterogeneous and dense media: Application to al/cuo thermite[END_REF], is coupled with the heat transfer in order to compute the initiation and combustion characteristics. However, they restrict the reaction mechanisms to condensed phase processes only. Interestingly, Epps et al. [START_REF] Epps | Modelling reaction propagation for Al/CuO nanothermite pellet combustion[END_REF] introduced a nondimensional continuum modelling approach accounting for the first time the advection of gas contained in the porous thermite matrix via a Darcy's law. The objective of this work being to enable a parametric investigation of the important physical characteristics during the Al/CuO nanothermite combustion (conductive vs advective combustion regimes), the global chemistry of the thermite reaction is reduced to a single Arrhenius law with a rough estimate of the gas released. Another approach developed by Baijot et al. [START_REF] Baijot | A multiphase micro-kinetic model for simulating aluminum based thermite reactions[END_REF] to study pressurization of manometric bombs integrates an set of physicochemical mechanisms, both in the condensed and gas phases, including diffusion of species, decomposition of materials, vaporization/condensation at interfaces, and gas phase reactions. No heat exchange was considered between gas and condensed phases, nor between fuel and oxidizer particles. Despite this simplification, reasonably good agreement between predicted and measured pressure development was obtained, but in a limited pressure range and for very particular experimental conditions. The purpose of the present study is to implement into the Baijot's model new physical mechanisms derived from recent advances in the fundamental understanding of Al/CuO nanothermite combustion [START_REF] Lanthony | Formation of Al/CuO bilayer films: Basic mechanisms through density functional theory calculations[END_REF][START_REF] Xiong | Interface reaction processes and reactive properties of Al/CuO nanothermite: An ab initio molecular dynamics simulation[END_REF][START_REF] Rai | Understanding the mechanism of aluminium nanoparticle oxidation[END_REF][START_REF] Nie | Initial stages of oxidation of aluminum powder in oxygen[END_REF][START_REF] Mursalat | Low-Temperature Exothermic Reactions in Al/CuO Nanothermites Producing Copper Nanodots and Accelerating Combustion[END_REF][START_REF] Lanthony | Elementary surface chemistry during CuO/Al nanolaminate-thermite synthesis: copper and oxygen deposition on aluminum (111) surfaces[END_REF].

For that purpose, a tri-phasic system (fuel, oxide and gas phases) is considered to explore the ignition and combustion of thermite powders. We computed a set of physicochemical processes in the condensed and in the gas phases. The model is applied to an Al/CuO system as it is the most documented. The system is composed of three phases: two particle phases and one gaseous noted p, q, and g respectively. Condensed species inside a particle phase (Al, Al2O3, CuO, Cu) can be liquid or solid, and phase change is considered from an energetic point of view. Condensed species are assumed immiscible and their densities constant. The particles inside a particle phase k = p, g are assumed spherical during the whole simulated time, characterized by an inner and outer diameter respectively d in k and d k : the difference between both defines the alumina shell thickness. Particles k = p, q are assumed isothermal and no mass exchange between the two particle phases is considered.

The gas phase involves 9 species (Al, Cu, O2, N2, Al2O, Al2O2, AlO, AlO2, O). Homogeneous reactions rates assumed fast, gas is treated at equilibrium and an explicit description of heterogeneous reactions is proposed based on diffusional kinetics. After the description of the theoretical formulation and numerical method, the combustion principles at constant volume is discussed at the light of structural features as well as the physico-chemical parameters which are shown to govern the combustion dynamics in Al/CuO thermite systems.

Physical model and conditions

The three phases, noted p, q and g, represent the aluminum particle phase, the copper particle phase, and the gas phase, respectively. The main heterogeneous reactions and phase transitions involved between the condensed (p, q) and the gas (g) phases are (cf. Table 1 for the set of chemical reactions) :

• Oxydation of aluminum in the p core by Ox species (O2 and O) through reactions R1, R2. • decomposition of CuO releasing oxygen species in the gas through reaction R5. • decomposition of the alumina shell, which generates molecular oxygen and atomic aluminum through reaction R3. • vaporization/condensation of Al and Cu; for the sake of simplicity, they are treated similarly to heterogeneous reactions, based on the gas/liquid equilibrium through reactions R4, R6. • heterogeneous reaction of gaseous Al suboxide species (Al2O, Al2O2, AlO, AlO2, all referred to as AlxOy) on the surface of both Al and CuO particles through reactions R7 to R14. We define the subset of reactions RAlxOy as

R AlxOy = [R7 -R14].
The total set of heterogeneous (R1 to R14) and gaseous (R15) reactions is refered as R.

+ 3 2 O 2(g) → Al 2 O 3(c) R1 2Al (c) + 3O (g) → Al 2 O 3(c) R2 Al 2 O 3(c) → 2Al (g) + 3 2 O 2(g) R3 Al (c) Al (g) R4 CuO (c) → Cu (c) + 1 2 O 2(g) R5 Cu (c) Cu (g) R6 Al 2 O (g) + O 2,(g) → Al 2 O 3(c) R7 AlO (g) + 1 4 O 2,(g) → 1 2 Al 2 O 3(c) R8 Al 2 O 2,(g) + 1 2 O 2,(g) → Al 2 O 3(c) R9 AlO 2,(g) → 1 4 O 2,(g) + 1 2 Al 2 O 3(c) R10 Al 2 O (g) → 4 3 Al (g) + 1 3 Al 2 O 3(c) R11 AlO (g) → 1 3 Al (g) + 1 3 Al 2 O 3(c) R12 Al 2 O 2,(g) → 2 3 Al (g) + 2 3 Al 2 O 3(c) R13 AlO 2,(g) + 1 3 Al (g) → 1 3 Al 2 O 3(c) R14 Al x O y,(g) ----x Al (g) + y O (g) for [x,y]∈[0,1,2] 2

R15

R1 to R14 are explicitly treated over time through a system of differential equations. Each reaction r is caracterized by the involved chemical species i and the phase the species belongs to k = p, q, g. Gaseous reactions R15 exhibit much faster kinetics than the transport and condensed decomposition mechanisms [START_REF] Suarez | Modélisation de la combustion diphasique de l'aluminium et application sur la post-combustion d'une charge explosive condensée dans l'air[END_REF], hence the gas is considered at chemical equilibrium at gas temperature.

Transfer equations

For condensed phases, the conservation equations of mass and energy are respectively Equation ( 1) and (2) :

N k dm i,k dt = r∈R ωr i,k (1)
where N k is the number of particles in a given phase k (k = p, q). m i,k is the mass of the species i in the phase k. ωr i,k is the reaction rate of the species i from reaction r relative to particle k.

The enthalpy variation for a given particle phase k = p, q is given by Equation (2) :

N k dH k dt = m =k Q m→k + Qinit (2)
H k is the enthalpy of one particle of the particle phase k. Considering the particles as isothermal, it is defined as :

H k = i m i,k hi(T k )
where hi(T k ) is the total specific enthalpy of the species i at T k taking into consideration the formation and sensible enthalpy. hi(T k ) considers the variation of both the heat capacity and phase change of species i. Q m→k is the heat flux received by a given particle phase k from either the other particle phase or the gas. Heat fluxes are symmetric, hence for any condensed or gaseous phase m and k, Q m→k equals to -Q k→m . Qinit is the energy flux brought to the Al and CuO particles to initiate the reactions.

For the gas phase, the mass conservation equation is :

d dt (ρgαgV ) = r∈R i ωr i,g = Γg (3)
where ωr i,g and Γg are the gas production rate of the species i and the total mass flux going from all the particles to the gas, respectively. Due to mass conservation, the global system respects k∈[p,q,g] i ωr i,k = 0 for each r. The species conservation equations are defined for each gaseous species i :

d dt (ρgαgV Yi,g) = r∈R ωr i,g (4)
where ρg and αg are the density and volume fraction of the gas phase, respectively. V is the volume of the system, Yi,g is the mass fraction of the species i.

The gas energy conservation equation is :

d dt (ρgαgV ug) = m=p,q Qm→g (5)
where ug = i Yiui,g(Tg) is the specific total intern energy of the gas at Tg. ui,g(Tg) is the specific total intern energy of the gaseous species i at Tg, considering both formation and sensible energy. Qm→g represents the energy fluxes received by the gas from the particle phase m.

Mass exchange and source term modelling

The details of mass variation terms of Equation ( 1) resulting from the heterogeneous reactions are specified in this section for the particle phases p and q. Reaction times are very small compared to mass transport characteristic times (by diffusion and inter-phase mass fluxes) as reported on previous DFT calculations [START_REF] Lanthony | On the early stage of aluminum oxidation: An extraction mechanism via oxygen cooperation[END_REF]. Thus, all the reaction rates of heterogeneous reactions (R1 to R14) are supposed limited by mass transport mechanisms and are written as functions of mass fluxes [START_REF] Glassman | Combustion[END_REF].

Al particles (p)

The aluminum oxidation rate ωR1 Al,p in the aluminum core is limited by the O2 transport flux through the boundary layer and the alumina shell. Using a Spalding formulation as detailed in Equation ( 7) [START_REF] Kuo | Principles of combustion[END_REF], a first mass flux is integrated over the boundary layer, and a second one is integrated over the alumina shell. Assuming a steady state, both fluxes are equal, and an analytical solution of the O2 mass fraction at the surface of the particle Y s O2 is determined. The O2 flux Φ Sp O2,g→p is computed by injecting Y s O2 in one of the two Spalding formulation. Similar treatment is applied for the oxidation rate relative to the reaction R2.

Thus, the reaction rates of O2 and O relative to aluminum core oxydation reaction are :

ωr i,g = Φ Sp i,g→p (6)
for r = (R1, R2) and i = O2, O. Reaction rates of the other species (Al2O3 and Al) relative to R1 and R2 are trivially determined using the stoichiometric ratios and molar masses of each species. The Spalding transport flux in the boundary layer of a species i is defined for

K = 1, Y out i = Yi,g, Y in i = Y s i , ρn = ρg, Di,n = Di,g as : Φ Sp i,g→p = -2πdpρnDi,n log 1 -Y out i 1 -Y in i K (7)
where Di,g, Y s i are the diffusion coefficients in the gas and the mass fraction at the particle surface of the species i, respectively. For the flux transport in a finite media between d in p and dp, the Spalding formulation is defined for

K = d in p /(dp -d in p ), Y out i = Y s i , Y in i
= 0 (instantaneous oxidation assumption), ρn = ρg, Di,n = D i,Al2O3 ; where D i,Al2O3 is the diffusion coefficient of the species i in the porous alumina shell, which follows an Arrhenius law. Note that as the aluminum is oxidized, the alumina shell grows consequently, increasing the barrier for O2 and O transport. ωR4 Al,p and ωR6 Cu,p correspond to the vaporization/condensation of aluminum and copper respectively, expressed using Equation [START_REF] Lanthony | Formation of Al/CuO bilayer films: Basic mechanisms through density functional theory calculations[END_REF]. The surface mass fractions are estimated by their staturated values obtained by a Clapeyron law at the temperature Tp. Since the evaporation is restricted to the surface where the species i is available, the surface ratio defined as Ai,p = (Vi,p/ j Vj,p) 2/3 is introduced; where Vi,p is the volume occupied by the species i in the particle p. Thus, the evaporation mass rate is ωR4,R6 i={ Al Cu ,p = Φ Sp i,g→p Ai,p. The condensation mass rate formulation is similar to evaporation but with Ai,p = 1 as it happens on the whole particle surface.

Reaction rates relative to the set of reactions R AlxOy , result from the heterogeneous reactions of gaseous Al suboxides, on the Al particle surface. Again, surface reactions involving the species i are assumed to be much faster than the diffusion of the species in the gas. Therefore, Y s i = 0 and the reaction rates relative to R AlxOy are defined by Equation (6) for r ∈ [R7 -R14] and i ∈ AlxOy. By defining the atomic richness of the suboxide gaseous mass fluxes as :

φ AlxOy = 1 2 i∈AlxOy Φ i,g→p W i n Al i 1 3 i∈AlxOy Φ i,g→p W i n O i ( 8
)
where n Al The total production rate of Al2O3: ωR AlxOy Al2O3,p , relative to the set of reactions R AlxOy is trivially determined using the stoichiometric ratios and molar masses of each species. ωR3 Al2O3,p is the Al2O3 decomposition rate approximated with an Arrhenius law (see Table 2).

CuO particles (q)

CuO particles are composed of CuO, Cu, and possibly recondensed Al or Al2O3. Hence, Equation ( 1) is developped for CuO, Cu, Al and Al2O3. ωR3 Al2O3,q and ωR5 CuO,q represent the CuO and Al2O3 decomposition (reactions R3 and R5), which kinetics are approximated again with an Arrhenius law (see Table 2). The condensed Cu production rate ωR5

Cu,q relative to CuO decomposition is trivially determined using the stoichiometric ratios and molar masses of each species.

ωR6 Cu,q , ωR4 Al,q and ωR AlxOy Al2O3,q correspond to the vaporization-condensation of Cu and Al species and the heterogeneous reactions, respectively. These terms are determined similarly to the aluminum particles (see definitions of ωR6

Cu,p , ωR4 Al,p and ωR AlxOy Al2O3,p ).

Gas phase (g)

For each gaseous species i, Equation ( 4) is solved in its non conservative form. For all heterogeneous reactions R1 to R14, the production rate of a gaseous species i involved in reaction r may be written in terms of the corresponding reaction rates in the condesed phases, as :

ωr i,g = k=p,q Wi Wj ν r i ν r j ωr j,k = k=p,q ωr i,g(k) (9)
where j is any condensed species of the reaction r (whose reaction rates have been defined previously). ωr i,g(k) is introduced as the gaseous source term of the species i relative to reaction r taking place on the condensed phase k. ν r i is the global molar stoichiometric coefficient of reaction r such as ν r i > 0 if i is a product and ν r i < 0 otherwise. Regarding the mass conservation, Equation (3) becomes :

αgV dρg dt = Γg -ρgV dαg dt (10)
The gas volume fraction time derivative dαg dt is implicitely computed using the relations α k = i N k m i,k (V ρ i,k ) -1 for k = p, q and αg = 1 -k=p,q α k where ρ i,k is the condensed density of the species i (assumed constant) and α k is the volume fraction of the particle phase k = p, q.

Finally, all the gaseous reactions rates of R15 and ?? are taken into account by the chemical equilibrium of the gas.

Heat flux and source terms

The total flux of energy received by a phase k = p, q, g, can be generally expressed for any phase m and k as :

m =k Q m→k = m =k (Q cond m→k + Q rad m→k + Q species m→k ) (11) Q species p→q
, coupled to the direct mass transfer by contact between both particle phases is not considered. The total particle phase surface is considered much larger than the system boundaries, thus radiation and conduction transfer with walls are neglected.

The conduction between the two particles is written as :

Q cond p→q = H cond p→q (Tp -Tq) (12)
where H cond p→q is computed based on the particle and intersticial gas conductance and the particle interphase coordination number [START_REF] Batchelor | Thermal or electrical conduction through a granular material[END_REF][START_REF] Moscardini | Discrete element method for effective thermal conductivity of packed pebbles accounting for the smoluchowski effect[END_REF]. Note that only effective contact is considered and the mean coordination number Npq is approximated to 3.

For particle to particle radiative transfer, as the condensed phase surfaces are assumed much larger than the system boundaries, the system can be treated as an enclosed problem [START_REF] Ozisik | Heat transfer: a basic approach[END_REF], then :

Q rad p→q = σ(T 4 p -T 4 q ) 1-εp Apεp + 1 ApFp→q + 1-εq Aq εq (13)
where A k = N k πd 2 k , and ε k are the total surface and the emissivity, approximated to 0.85, of the condensed phase k, respectively. Assuming the condensed phases being homogeneously dispersed in the considered volume, the view angle Fp→q is defined as :

Fp→q = Nqd 2 q Nqd 2 q + Npd 2 p ( 14
)
Second, let's define the energy fluxes from the particle phases m = p, q to the gas phase k = g. Radiation between the gas and the particles is assumed negligible leading to consider only the conduction and mass transfer related terms. As no mean relative motion between the gas and the particles is considered for both particle phases, it is defined as:

Q cond m→g = λgπdmN u(Tm -Tg)Np (15)
Where λg is the gas mixture conductivity and N u the Nusselt number, equals to (7 -10 αg + 5α 2 g ) as stated by Gunn [START_REF] Gunn | Transfer of heat or mass to particles in fixed and fluidised beds[END_REF]. Tm and Tg are the temperatures of the particle phase m and of the gas g, respectively.

The heat flux related to the mass transfer from the particle phase m = p, q to the gas g is evaluated at the temperature of the phase T r σ (for each reaction r), from which the mass flux comes from :

Q species m→g = r =R15 i C r i ωr i,σ u i,(σ) (T r σ ) (16)
However, for reactions R1, R2, R4, R5, R6, the difference of formation energy between gaseous and condensed species i is withdrawn from the particle (thus, for example, cooling down the particle during an evaporation process), hence :

C r i ωr i,σ u i,(σ) (T r σ ) = ωr i,g(m) u i,(g) (Tm)H( ωr i,g(m) ) -ωr i,g(m) u i,(g) (Tg)H(-ωr i,g(m) ) (17)
while, for reactions R3 and RAlxOy the difference of formation energy between gaseous and condensed species i is withdrawn from the gas, hence :

C r i ωr i,σ u i,(σ) (T r σ ) = -ωr i,m u i,(m) (Tm)H(-ωr i,m ) + ωr i,m u i,(m) (Tg)H( ωr i,m ) (18
) where u i,(g) and u i,(m) are the total energy of the gaseous and condensed species i, respectively. H is the heaviside function, specifying that the transfered energy is taken from the phase from which the mass flux of the reaction r comes from.

Simulation details and model parameters

The numerical resolution is splitted into two steps:

1. The mass and energy equations for particle phases are integrated over a time step based on the heat flux terms and heterogeneous reaction rates of R1 to R14 using an explicit Euler scheme. Based on the newly computed particle composition, the particle diameters d n+1 p and the gas volume fraction α n+1 g are updated at the iteration n + 1. Gaseous intermediate species mass fraction Ỹ n+1 i,g and energy ũn+1 g are estimated by integrating only the heterogeneous reactions rates and the heat flux terms. A semi-implicit scheme specified by Equation [START_REF] Ozisik | Heat transfer: a basic approach[END_REF], with ζ = 1, Yi,g, ug and φ ζ = d dt (ρgVgζ) is used. 2. Based on those intermediate values, the chemical equilibrium is computed at constant energy and density by Cantera [START_REF] Goodwin | Cantera: An Object-oriented Software Toolkit for Chemical Kinetics[END_REF], leading to the actual species mass fractions and temperature:

Y n+1 i,g , T n+1
g of the gas.

A dynamical computation of the time step is established based on realisability and stability conditions : ∆t ranging between 10 -7 and 10 -9 s, mainly limited by a user defined maximum gas temperature variation (stability condition) between two iterations.

ζ n+1 = (ρVgζ) n + φ n ζ ∆t (ρVg) n + Γ n ∆t (19)
3.1. Thermophysical and reaction parameters All thermodynamical data, for condensed and gaseous species, come from JANAF tables [START_REF] Chase | NIST-JANAF thermochemical tables[END_REF]. The gas transport properties are computed based on the Lennard-Jones potential using Cantera [START_REF] Goodwin | Cantera: An Object-oriented Software Toolkit for Chemical Kinetics[END_REF] considering parameters found in the litterature [START_REF] Svehla | Estimated viscosities and thermal conductivities of gases at high temperatures[END_REF][START_REF] Orlandi | Modélisation et simulation n umérique de la combustion d'une goutte isolée d'aluminiumPublisher[END_REF][START_REF] Filippova | Calculation of the parameters of the lennard-jones potential for pairs of identical atoms based on the properties of solid substances[END_REF]. The vaporization points of the aluminum metal and copper metal evolves with respect to the pressure as a function of a Clapeyron law. The three (k0, Ea) couples characterizing the kinetic of CuO, Al2O3 decomposition and Ox diffusion via an Arrhenius law, were obtained by fitting the theoretical pressure as predicted by the model to already published experimental data [START_REF] Glavier | Nanoenergetics as pressure generator for nontoxic impact primers: comparison of al/bi2o3, al/cuo, al/moo3 nanothermites and al/ptfe[END_REF]. A theoritical study of the kinetic parameters have been performed (not detailed in this article), which results are presented in Table 2. 1.5 × 10 -5 k R3 0 (kg.m -3 .s -1 ) 1.52 × 10 6 k R5 0 (kg.m -3 .s -1 ) 2.86 × 10 7 E R1,R2 a (J.mol -1 .K -1 ) 75 × 10 3 E R3 a (J.mol -1 .K -1 ) 400 × 10 3 E R5 a (J.mol -1 .K -1 ) 46 × 10 3

Initial conditions

The calculations were carried out with the initial temperature of the thermite system being set to 300 K, and adiabatic boundary conditions. The initial characteristics of the gas are calculated at atmospheric conditions. An energy of 600 kJ.kg -1 is injected at a power of 2 GW to the set of Al and CuO particles to ignite the system.

Results

Two systems of 0.5 g of Al particles, and 1.25 g of CuO particles were simulated and pressure development compared: a nanothermite (dp = dq = 100 nm) and a microthermite (dp = dq = 5 µm). Al particle purity, compaction rate and richness of both thermites are set to 0.7, 50 %T M D and 1.2, respectively. The chamber volume is fixed at 1 cm 3 .

Graphs (a,c,e,g) and (b,d,f,h) of Fig. 2 show the temporal evolution of the main observables of nano and microthermite respectively. The self-sustained combustion starts when Al particles reach 1162 K and 1133 K after 0.75 µs and 0.9 µs for nano and microthermite respectively. Both systems converge to Fig. 2: Time evolution for a nanothermite (a,c,e,g) and microthermite system (b,d,f,h) of : (a,b) the temperature of each phase (solid line) and gas pressure (dashed line), (b,d) the mass fraction of each species in the gas, (e,f) the species condensed mass in the system, (g,h) the Al particle inner (orange) and outer (blue) diameters and the for CuO particle outer diameter (dashed blue) dp = dq = 100 nm and 5 µm Nanothermite features a delayed pressurization compared to the temperature rise (Fig. 2a), which indicates that a first combustion regime (from 0.75 to 1.2 µs) occurs in the condensed phase. In that regime, all the released O2 by the CuO decomposition is captured by the large Al particles specific area (11.89 m 2 .g -1 ). After diffusion through the shell and reaction with the Al core, oxygen absorption leads to the Al2O3 growth. In the meantime, condensed Cu is generated through the CuO decomposition in the CuO particle phase (Fig. 2e). The alumina shell, characterized by the difference between the inner and outer diameters (see Fig. 2g orange and blue lines, respectively) increases during the condensed combustion process, thus increasing the resistance of Al2O3 barrier to Al oxydation. The purple vertical lines (on Fig. 2g,h) represent the moment when the temperature of the Al particle reaches the temperature of alumina liquefaction at 1.2 µs. At that point, the model of alumina shell may become questionnable. Right after reaching the alumina liquefaction temperature, the diameter of Al particle p starts deacreasing, as liquid Al evaporates, decreasing the amount of matter in the particle. The vaporized Al partially reacts with Ox in the gas to produce AlxOy (mainly Al2O), as shown from the evolution of the gas temperature being above the temperature of the particle phases. These suboxides then react quasi-instantaneously onto the CuO particles to generate Al2O3 (Fig. 2e). This fast kinetic scheme is supported by the fact that the AlxOy mass fractions are very low in the gas phase (Fig. 2c). Meanwhile alumina becomes liquid at 1.2 µs and temperature is higher than 2300 K, Al and Cu species start to vaporize (Fig. 2c) into the gas leading to a pressure rize (Fig. 2a). The pressure reaches a maximum when CuO is totally reduced (Fig. 2e) at 4300 K. An equilibrium state is thus obtained at ∼1.8 µs. During the whole simulated time, the three phases are almost at the same temperature (Fig. 2a), heat fluxes being very efficient due to the large specific are in nanothermite system. To sum up, two very clear combustion regimes are observed :

• A first condensed combustion regime when the oxygen coming from the CuO decomposition is absorbed by the Al particle, reacting with the Al in the core, until the temperature of liquefaction of alumina is reached at 1.2 µs. • A second regime, where the gas drives the reactions through the species and energy transport between both particle phases. By contrast, in the microthermite system, the specific area being very small (0.23 m 2 .g -1 ) the O2 absorption on the Al particles surface is limited leading to a slight increase of alumina shell (Fig. 2h). Indeed, in microthermite, volume reactions are much faster than the surface ones. Therefore, the Al particles do not have the time to absorb all the oxygen coming from the CuO decomposition. Hence, the gas becomes an intermediate tank for O2, damping the characteristic time differences between the surface and volume mechanisms, as the pressure rises up to 115 MPa at 7 µs.

When the pressure starts decreasing (Fig. 2b) due to oxygen absorption on the aluminum particles, Al evaporation is finally enabled at 10 µs, increasing drastically the gas temperature up to 6000 K because of the reaction with gaseous oxygen. AlxOy, mainly consisting of AlO, do not react on the particle surface as fast as in the nanothermite system and their mass fraction reach 0.25 (Fig. 2d). When the AlxOy species recondense, the system converges to its equilibrium state at 12 µs. Contrary to the nanothermite system, the three phases are at relatively different temperature (Fig. 2b). This is explained by the fact that the heat fluxes are less efficient due to the smaller specific area. Note also that, compared to nanothermite, Al2O3 produced on CuO particles is negligible (Fig. 2f).

This behavior corroborates the experimental measurements by Nicollet et al. [START_REF] Nicollet | Fast circuit breaker based on integration of Al/CuO nanothermites[END_REF] showing an overpressure peak prior to the establishment of a lower final pressure in Al/CuO nanothermites. Nevertheless, simulated pressurization rates are at least one order of magnitude higher than the ones observed experimentally, which can be explained by an insufficiently accurate estimation of the kinetic parameters (k0, Ea in Table 2) or by an overestimation of the particle surfaces that can actually agglomerate through reactive sintering.

Finally, Fig. 3 confirms the great impact of the Al particle size on the pressure development in the bomb chamber. The maximum pressurization rate increases with decreasing Al particles size as often characterized experimentally [START_REF] Weismiller | Effects of fuel and oxidizer particle dimensions on the propagation of aluminum containing thermites[END_REF]. As discussed previsouly, the nanothermite system features a maximum pressure (Pmax) due to Cu and Al gaseous species, equal to the final pressure (P f ) as no heat losses are considered here, whereas microthermite develops a pressure peak at low temperature Pmax = 115 MPa related to gaseous oxygen, before stabilizing at 22 MPa through gaseous Cu and Al.

Conclusion

A 0D Al/CuO thermite combustion model has been developped taking into consideration the different mechanisms identified in a Al/CuO reaction in a closed volume, which shows the same temporal behavior and a final pressure in the same order of magnitude as experimental data (∼ 20 MPa) [START_REF] Glavier | Nanoenergetics as pressure generator for nontoxic impact primers: comparison of al/bi2o3, al/cuo, al/moo3 nanothermites and al/ptfe[END_REF]. This model enables, for the first time, a closer examination of kinetical mechanisms driving thermite combustion. Different combustion regimes were observed depending on the particle size. They are explained by the difference in specific area between the two simulated thermite systems (11.89 m 2 .g -1 vs. 0.23 m 2 .g -1 ).

In addition, this theoritical tool can be used to predict closed-bomb experiment and can serve as a foundation for a multi-dimensionnal propagating model.

Fig. 1 :

 1 Fig. 1: Schematic view of thermite main reactions occurring on each particle: Al and CuO.

i

  and n O i are the number of element Al and O in the molecule i respectively, Baijot et al. emphasized two possible reactionnal schemes explicited here, composed of R AlxOy = [R7, R8, R9, R10] when φ AlxOy > 1 and R AlxOy = [R11, R12, R13, R14] otherwise [6].

Fig. 3 :

 3 Fig. 3: Pressurization rate, maximum and final gas pressure with respect to particle initial diameters dp = dq

Table 1 :

 1 List of reactions

	Reactions	n°2
	Al (c)

Acknowledgement

The authors acknowledge support from the European Research Council (H2020 Excellent Science) Researcher Award (grant 832889 -PyroSafe) and Ar-ianeGroup which funds Emelian Tichtchenko scholarship.