Syrine Aouadi
email: syrine.aouadi@eleves.ec-nantes.fr

Arnaud Lanoix
email: arnaud.lanoix@univ-nantes.fr

Reliability in Fully Probabilistic Event-B: How to Bound the Enabling of Events

Keywords: Event-B, Probabilistic Event-B, Probabilistic properties, Reliability, Weight, Proof obligations

In previous work, we have proposed a fully probabilistic version of Event-B where all the non-deterministic choices are replaced by probabilistic ones and, particularly, the events are equipped with weights that allow us to consider their enabling probability. In this work, we focus on the reliability of the system by proposing to constraint the probability of enabling an event (or a set of events) to control its importance with regard to the intended system behaviour. We add a specific upper bound which must limit the enabling probabilities of the chosen events and we consider the necessary proof obligations to check that the considered events respect the bound. At the end, we illustrate our work by presenting a case study specified in probabilistic Event-B and where bounding the enabling of some events is mandatory.

Introduction

Systems using randomized algorithms [START_REF] Motwani | Randomized algorithms[END_REF], probabilistic protocols [START_REF] Abrial | A mechanically proved and incremental development of IEEE 1394 tree identify protocol[END_REF] or failing components become more and more complex. It is then necessary to add new modeling features in order to take into account the inherent complexity of the system properties such as reliability [3], responsiveness [START_REF] Chu | Estimating task response time with contentions for real-time distributed systems[END_REF][START_REF] Trivedi | Recent advances in modeling response-time distributions in real-time systems[END_REF], continuous evolution, energy consumption etc. One of these features is probabilistic reasoning, which can be used in order to introduce uncertainty in a model or to mimic randomized behavior. Probabilistic modeling formalisms have therefore been developed in the past, mainly extending automatabased formalisms [START_REF] Stoelinga | An introduction to probabilistic automata[END_REF][START_REF] Puterman | Markov decision processes: discrete stochastic dynamic programming[END_REF]. Abstraction [START_REF] Katoen | Abstraction of probabilistic systems[END_REF][START_REF] Dehnert | On abstraction of probabilistic systems[END_REF], refinement [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] and model-checking algorithms [START_REF] Bianco | Model checking of probabilistic and nondeterministic systems[END_REF][START_REF] Baier | Principles of model checking[END_REF] have been successfully studied in this context. However, the introduction of probabilistic reasoning in proof-based modeling formalisms has been, to the best of our knowledge, quite limited [START_REF] Haghighi | A Z-Based formalism to specify markov chains[END_REF][START_REF] Sere | Probabilities in action systems[END_REF][START_REF] Hoang | The development of a probabilistic B-method and a supporting toolkit[END_REF][START_REF] Goldreich | Probabilistic proof systems[END_REF][START_REF] Barthe | Probabilistic relational verification for cryptographic implementations[END_REF][START_REF] Hurd | Probabilistic guarded commands mechanized in HOL[END_REF][START_REF] Audebaud | Proofs of randomized algorithms in Coq[END_REF][START_REF] Hurd | Formal verification of probabilistic algorithms[END_REF]. Although translations from proof-based models to automata-based models are always possible, the use of automata-based verification techniques in the context of proof-based models is most of the time inconvenient because of possible state-space explosion introduced in the translation.

Event-B [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF] is a proof-based formal method used for modeling discrete systems. It is equipped with Rodin [START_REF] Abrial | Rodin: an open toolset for modelling and reasoning in Event-B[END_REF], an open toolset for modeling and proving systems. This toolset can easily be extended, which makes Event-B a good candidate for introducing probabilistic reasoning in a proof-based modeling formalism. So far, several research works have focused on the extension of Event-B to allow the expression of probabilistic information in Event-B models. In [START_REF] Morgan | The challenge of probabilistic Event B -extended abstract[END_REF], Abrial et al. have summarized the difficulties of embedding probabilities into Event-B. This paper suggests that probabilities need to be introduced as a refinement of non-determinism. In Event-B, non-determinism occurs in several places such as the choice between enabled events in a given state, the choice of the parameter values in a given event, and the choice of the value given to a variable through some non-deterministic assignments. To the best of our knowledge, the existing works on extending Event-B with probabilities have mostly focused on refining non-deterministic assignments into probabilistic assignments. Other sources of non-determinism have been left untouched. In [START_REF] Hallerstede | Qualitative probabilistic modelling in Event-B[END_REF], Hallerstede et al. propose to focus on a qualitative aspect of probability. They refine non-deterministic assignments into qualitative probabilistic assignments where the actual probability values are not specified, and adapt the Event-B semantics and proof obligations to this new setting. In [START_REF] Yilmaz | Tool support for qualitative reasoning in Event-B[END_REF], the same authors study the refinement of qualitative probabilistic Event-B models and propose tool support inside Rodin. Other works [START_REF] Tarasyuk | Reliability assessment in Event-B development[END_REF][START_REF] Tarasyuk | Integrating stochastic reasoning into Event-B development[END_REF][START_REF] Tarasyuk | Towards probabilistic modelling in Event-B[END_REF] have extended this approach by refining non-deterministic assignments into quantitative probabilistic assignments where, unlike in [START_REF] Hallerstede | Qualitative probabilistic modelling in Event-B[END_REF], the actual probability values are specified. This new proposition is then exploited in order to assess several system properties such as reliability and responsiveness.

Unfortunately, sources of non-determinism other than assignments have been left untouched, although the authors argue that probabilistic choice between events or parameter values can be achieved by transformations of the models that embed these choices inside probabilistic assignments. While this is unarguably true, such transformations are not trivial and greatly impede the understanding of Event-B models. Moreover, these transformations would need to be included in the refinement chain when designers need it, which would certainly be counter-intuitive to engineers.

In previous works [START_REF] Aouadhi | Moving from Event-B to probabilistic Event-B[END_REF][START_REF] Aouadhi | Introducing probabilistic reasoning within Event-B. Software & Systems Modeling[END_REF] we pursued these works by proposing a probabilistic extension of Event-B and presenting some ways of introducing probabilistic reasoning within Event-B. We have proposed some new syntactic elements for writing fully probabilistic Event-B models in the Event-B framework. The consistency of such models has been expressed, as in standard Event-B, in terms of proof obligations. In the standard Event-B setting, convergence is a required property for proving a refinement step as soon as new events are introduced in the model. The counterpart property in the probabilistic setting is almost-certain convergence, which has already been studied in [START_REF] Hallerstede | Qualitative probabilistic modelling in Event-B[END_REF], in the context of non-deterministic models with only probabilistic assignments. We therefore have exhibited new sufficient conditions, expressed in terms of proof obligations, for the almost-certain convergence of a set of fully probabilistic events. While the conditions we exhibit are more constrained than those from [START_REF] Hallerstede | Qualitative probabilistic modelling in Event-B[END_REF] concerning events and parameters, they are also less restrictive concerning probabilistic assignments. Finally, some of the previously mentioned results have been implemented in a prototype plugin for Rodin.

In the probabilistic Event-B context, the probabilistic events are equipped with weights, in order to easily consider the enabling probability of each event in any configuration. In this paper, we extend the previous work by considering a kind of probabilistic invariant that allows us to model and verify properties concerning reliability: we add a specific upper bound to constraint the enabled probability of an event (or a set of events) in order to limit their importance with regards to the system behavior. As in the previous work, we check that the considered events respect the bound by means of new proof obligations. These new proof obligations ensure that in any configurations where the considered event can be enabled, this enabled probability is lower than the considered bound. Finally, we illustrate our work on an industrial simplified case study: the PCB manufacturing and control system [START_REF] Gaiero | ICT Vs FCT Test : case studies[END_REF][START_REF]PCP Inspection Techniques And Technologies[END_REF]. Particularly, we show the requirements for applying the enabled bound property on a realistic used system.

Outline. The paper is structured as follows. Section 2 presents the scientific background of this paper in terms of Probabilistic Event-B. In Section 3, we focus on how to constraint the enabling of events, and the necessary proof obligations on such models. Section 4 introduces our case study: a simple PCB manufacturing and control system which illustrate the use of the previously mentioned property. Finally, Section 5 concludes the paper.

2 Preliminaries: Probabilistic Event-B Event-B [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF] is a formal method used for the development of complex discrete systems. Systems are described in Event-B by means of models. We have previously extended standard Event-B models to introduce probabilistic reasoning. In Event-B, nondeterminism can appear in three places: the choice of the enabled event to be executed, the choice of the parameter value to be taken and the choice of the value to be assigned to a given variable in a non-deterministic assignment. To obtain a fully probabilistic Event-B model, we have proposed to replace all these non-deterministic choices with probabilistic ones.

MODEL M VARIABLES v INVARIANTS I ( v) VARIANT V( v) EVENTS Init = . . . e 1 = . . . . . . e n = . . .

END

For the sake of simplicity, we assume in the rest of the paper that a fully probabilistic Event-B model is expressed by a tuple M=( v,I( v ), V( v),PEvts, Init ) where v= {v 1 . . . v n } is a set of variables, I ( v) is an invariant, V( v) is an (optional) variant used for proving the (almost-certain) convergence of the model, PEvts is a set of probabilistic events and Init ∈ PEvts is the initialization event. The invariant I ( v) is a conjunction of predicates over the variables of the system specifying properties that must always hold.

Probabilistic events A probabilistic event has the following structure where e i is the name of the event, W i ( v) is the weight of the event, t = {t 1 . . . t n } represents the (optional) set of parameters of the event, G i (t , v) is the (optional) guard of the event and S i ( t , v) is the action of the event. A probabilistic event is enabled in a given valuation of the variables (also called a configuration) if and only if i) there exists a parameter valuation such that its guard G i (t , v) is fulfilled in this context and ii) its weight W i ( v) is strictly positive.

event e i = weight W i ( v) any t where G i (t , v) then SP i (t , v) end
In standard Event-B, when several events are enabled, the event to be executed is chosen non-deterministically. The weight W i ( v) of the event resolves this non-deterministic choice: in configurations where several probabilistic events are enabled, the probability of enabling one of them will therefore be computed as the ratio of its weight against the total value of the weights of all enabled events in this state. Moreover, for the sake of expressibility, we propose to express the weight W i ( v) of a probabilistic event e i as an expression over the variables v of the fully probabilistic Event-B model. The probability of enabling a given event can therefore evolve as the system progresses.

For the events equipped with parameters t , a valuation of the parameters is chosen such that the guard G i (t , v) of the event is satisfied. In standard Event-B, when there are several such parameter valuations, one of them is selected non-deterministically. We therefore have proposed to replace this non-deterministic choice by a uniform choice over all parameter valuations ensuring that the guard of the event is satisfied.

Probabilistic assignments

The action SP i (t , v) of a probabilistic event may contain several assignments that are executed in parallel. An assignment can be expressed in one of the following forms:

-Deterministic assignment: x:= E(t, v) means that the expression E(t , v) is assigned to the variable x. -Predicate probabilistic assignment: x:⊕Q(t, v,x,x') means that the variable x is assigned a new value x' such that the predicate Q(t , v,x,x ') is satisfied. Instead of choosing non-deterministically among the values of x' such that the predicate Q(t , v,x,x ') is true as in standard predicate non-deterministic assignments, we propose to choose this new value using an uniform distribution. -Enumerated probabilistic assignment: x := E 1 (t, v) @ p 1 ⊕ . . . ⊕ E n (t, v) @ p n means that the variable x is assigned the expression E i with probability p i . In order to define a correct probability distribution, each p i must be strictly positive and smaller or equal to 1, and they must sum up to 1. Although rational numbers are not natively handled in Event-B, we assume that an adequate context is present. That can be done by defining a "Rational" theory in Rodin using the theory plug-in providing capabilities to define and use mathematical extensions to the Event-B language and the proving infrastructure [START_REF] Butler | Practical theory extension in Event-B. In: Theories of Programming and Formal Methods[END_REF].

Before-after predicate and semantics The formal semantics of an assignment is described by means of a before-after predicate (BA) Q(t , v,x,x ') , which describes the relationship between the values of the variable before (x) and after (x') the execution of an assignment.

-The BA of a deterministic assignment is x'= E(t , v).

-The BA of a predicate probabilistic assignment is Q(t , v,x,x ') .

-The BA of an enumerated probabilistic assignment is

x'∈{E 1 (t, v) . . . E n (t , v)}.
Recall that the action S i ( t , v) of a given event e i may contain several assignments that are executed in parallel. Assume that v 1 . . . v i are the variables assigned in S i ( t , v) -variables v i+1 . . . v n are thus not modified -and let Q(t , v,v 1 ,v' 1 ) . . . Q(t , v,v i ,v' i ) be their corresponding BA. Then the BA S i ( t , v, v ') of the event action S i ( t , v) is:

S i ( t , v, v ') = Q(t, v,v 1 ,v' 1 ) ∧ . . . ∧ Q(t, v,v i ,v' i ) ∧ (v' i+1 =v i+1 ) ∧ . . . (v' n =v n )
Proof obligations The consistency of a standard Event-B model is characterized by means of proof obligations (POs) formally defined in [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF] which must be discharged. Discharging all the necessary POs allows to prove that the model is sound with respect to some underlaying behavioral semantics. The consistency of a fully probabilistic Event-B model is also characterized by means of POs to be discharged. Among all of them, the first ones are adaptation of the standard POs and the second ones are POs specific to fully probabilistic Event-B.

In the following, we recall the adaptation of the most important of the standard POs: (event/pINV) for invariant preservation, which states that the invariant still holds after the execution of each probabilistic event in the Event-B model M. Given an event e i with a guard G i (t , v) and an action S i ( t , v), this PO is expressed as follows:

I ( v) ∧ G i (t , v) ∧ W i ( v) > 0 ∧ SP i (t, v, v') I ( v ') (event/INV)
Then, we give some of the new POs specific to fully probabilistic Event-B:

we impose that the expression W i ( v) representing the weight of a given probabilistic event must evaluate to natural numbers.

I ( v) ∧ G i (t , v) W i ( v) ∈ NAT (event/WGHT/NAT)
-In order to be able to use a discrete uniform distribution over the set of parameter valuations ensuring that the guard of a probabilistic event is satisfied, we impose that this set must be finite.

I ( v) finite ({t | G i (t , v)}) (event/param/pWD)
-Probability values p i in enumerated probabilistic assignments are strictly positive and smaller or equal to 1.

0 < p i ≤ 1 (event/assign/pWD1)
-The sum of the probability values p 1 . . . p n in enumerated probabilistic assignments must be equal to 1.

p 1 + . . . + p n = 1 (event/assign/pWD2)
Feasibility of enumerated probabilistic assignments is trivial: as soon as at least one expression E i ( t , v) is present and well-defined, it always returns a value. -In order to define a discrete uniform distribution over the set of values of a variable

x making the predicate Q x (t , v,x ') of the corresponding assignment satisfied, we impose that this set must be finite.

I ( v) ∧ G i (t , v) ∧ W i ( v)>0 finite ({x' | Q x (t , v,x ') }) (event/assign/pWD3)
Feasibility of predicate probabilistic assignments is ensured by the standard feasibility PO [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF] inherited from Event-B. It ensures that the set {x' | Q x (t , v,x ') } is not empty.

Contribution: Limiting the Enabling of Probabilistic Events

We recall that, in standard Event-B, when several events are enabled in a given configuration, the event to be executed is chosen non-deterministically. In order to resolve this non-deterministic choice, we have proposed to equip each event with a weight W i ( v) that is an expression over the variables v of the fully probabilistic Event-B model. Note that using weights instead of actual probability values is convenient as the set of enabled events evolves with the configurations of the system. Using probability values instead would require to normalize them in all configurations.

Enabling probability A probabilistic event is enabled in a given configuration if and only if there exists a parameter valuation such that its guard G i (t , v) is fulfilled and its weight W i ( v) is positive. In configurations where several probabilistic events are enabled, the probability of choosing one of them will therefore be computed as the ratio of its weight against the total value of the weights of all enabled events in this configuration. Formally, this enabling probability is defined as follows.

Let M=( v,I( v ), V( v),PEvts, Init ) be a fully probabilistic Event-B model. Given an event e i in PEvts and a valuation σ of the variables v of the model, the enabling probability of e i in σ is formally defined by

P(e i , σ) = [σ]W i ( v) ∑ e j ∈PEvts ([σ]W j ( v | [σ]W j ( v) > 0 ∧ ∃ θ .[σ, θ ]G j ( v, t) = ) (1) if ∃ θ.[σ, θ]G i ( v, t) = and [σ]W i ( v) > 0 (2) = 0 otherwise ( 3
)
where θ and θ are possible valuations of the parameters t .

The probability of enabling a given event can therefore evolve as the system progresses. Equation (1) represents the ratio of the weight of the considered event e i against the total value of the weights of all the enabled events (including the weight of e i ), when Equation ( 2) is verified i.e. the event e i is enabled. Otherwise as Equation (3) the enabling probability of e i is equal to 0.

Enabled bound property

In standard and probabilistic Event-B, the events for which we want to study their termination are annotated as convergent. We adopt the same principle and we annotate by bounded the events for which we want to limit their enabling probabilities. We also introduce a specific upper bound EB( v) (notice ENABLED_BOUND into the B model) as an expression over the variables v of the fully probabilistic Event-B model to limit the enabling probability of the bounded events. Note that this upper bound can evolve as the system progresses.

Considering a bounded event e i , it must verify the enabled bound property, i.e. in all configurations in which e i could be enabled, then its enabling probability must be lower than or equal to the value of the enabled upper bound EB( v) in that configuration. Formally

∀σ. ∃ θ.[σ, θ]G i ( v, t) = ∧ [σ]W i ( v) > 0 ⇒ P(e i , σ) ≤ [σ]EB( v) (4)
Proof obligations Checking standard or probabilistic Event-B models consists of discharging proof obligations. We then propose necessary POs to check the above mentioned enabled bound property on a fully probabilistic Event-B model. Let M=( v,I( v ), V( v),PEvts, Init ) be a fully probabilistic Event-B model. Let e i be a bounded event from PEvts= {e 1 . . . e i . . . e n }. Let EB( v) be the enabled upper bound. Then, necessary POs are defined as follows.

1. The enabled upper bound EB( v) must always be a rational number i.e. a positive non-zero value strictly lower than 1:

I ( v) 0 < EB( v)< 1 (eBOUND/WD)
2. Each bounded event e i satisfies the enabled bound property (see Equation ( 4)), i.e. its enabling probability is always lower than or equal to the enabled upper bound.

I ( v) ∧ G i (t , v) ∧ W i ( v) > 0 (event/WGHT/eBOUND) W i ( v) ∑ (e j ).( W j ( v) | G j (t , v) ∧ W j ( v) > 0) ≤ EB( v)
4 Case Study: the PCB Manufacturing and Control System

In this section, our purpose is to highlight on a concrete case study the interest of the enabled bound property. We then propose a fully probabilistic Event-B model of a simplified industrial case study: the Printed Circuit Boards (PCB) manufacturing and control system [START_REF] Gaiero | ICT Vs FCT Test : case studies[END_REF][START_REF]PCP Inspection Techniques And Technologies[END_REF]. This case study interests electronic cards manufacturers that face the ever increasing requirement of reducing their cost and improving products quality. That requires having a fine control strategy through which we evaluate the produced electronic cards by detecting possible errors from the tests performed.

In the considered case study, we will focus on two kinds of tests: the ICT ("In Circuit Testing") tests check the presence of all the attempted components and the FCT ("Functional Testing") tests verify the functional behavior of each PCB.

Our proposed model simply abstracts the manufacturing and control process. We only identify each manufactured card by a unique identifier and we introduce two events, one representing the fair cards manufacturing, the other modeling the deficient cards manufacturing. The PCB manufacturing and control system must provide a history about the produced PCB and the error reporting.

Informal description of this system imposes two probabilistic requirements (i) the risk of having a deficient card must decrease with the increasing number of reported errors; (ii) having fair cards increases with correct cards production rise.

In fact, the manufacturing and control system must be a self-corrective maneuver on the PCB production line.

Event-B Context

To model the static aspects of the system, we propose the Event-B context as depicted by Figure 1 the constant Max_Cards models the maximum number of cards that can be produced whereas the constant Max_Errors models the maximum number of errors that can be reported; the set Error_State represents the tree kind of errors that can be reported during the test phase:

• the constant ICT_error designs an "In Circuit" error;

• the constant FCT_error Designs a "Functional" error;

• the constant ICT_FCT_error designs a double error, i.e. "In Circuit" and "Functional" errors simultaneously.

Note that Error_State is syntactically expressed as a partition between ICT_error, FCT_error and ICT_FCT_error, i.e. Error_State = {ICT_error,FCT_error,ICT_FCT_error}.

The maximum number of reported errors must be lower than or equal to the maximum number of produced cards. Only one kind of error is reported for a specific card.

Event-B model

We propose to model the system's state by means of three state variables, as depicted by Figure 2: the set Cards represents all the produced cards; the partial function Errors models the history of all the cards which have reporting errors, i.e. it associates to each necessary card, the corresponding reported error; the variable Next_ID identifies the nextly produced card.

We then model the dynamic of the system using three (probabilistic) events.

the event init initializes the model: regarding Cards and Errors, they are initialized to empty sets and Next_ID is initialized to any chosen integer value (10 on the illustrated specification); the event Manufacturing_OK models the fair cards production. Cards could be produced when the maximum number of produced cards is not reached and the maximum number of errors is also not reached; The number of the newly produced card is added to Cards, and the Next_ID is incremented; the event Manufacturing_Error represents the production of deficient cards: The event's parameter error chooses a kind of errors among the Error_State, i.e. a "In Circuit" error, a "Functional" error or the both simultaneously. The newly produced card is also registered, the Next_ID is incremented and the reported error is added to Errors : Next_ID → error.

MODEL PCBsystem SEES PCBctx VARIABLES Cards Errors Next_ID INVARIANTS Cards ⊆ N 1 ∧ Errors ∈ Cards →Error_State ∧ Next_ID ∈ N 1 ∧ finite (Cards) ∧ finite (Errors) ∧ card(Cards) ≤ Max_Cards ∧ card(
We note that the system stops running when the allowed numbers of reported errors or total cards produced are reached.

Probabilities appear in weights associated to each events and in the uniform choice between the kind of errors in the event Manufacturing_Error. We recall that informal description of this system imposes two probabilistic requirements: the risk of having a deficient card must decrease with the increasing number of reported errors and having fair cards increases with cards production rising, due to the the manufacturing and control system must be a self-corrective maneuver on the PCB production line. In other words, the more errors are reported, the less errors will be reported, whereas the more cards are produced, the more fair care will be produced. As the events Manufacturing_OK and Manufacturing_Error will be enabled simultaneously, their respective probabilities computed from their weights translate the requirements:

the weight of the event Manufacturing_OK increases with the number of produced cards, that corresponds to the requirement "the more cards are produced, the more fair care will be produced"; the weight of the event Manufacturing_Error decreases with the number of reported errors, that correspond to the requirement "the more errors are reported, the less errors will be reported".

To illustrate the attempted behavior of the specified system, we give in Figure 4 a sub-part of the corresponding probabilistic transition system, with Max_Errors fixed to 2 and Max_Cards fixed to 3.

Clearly, when we take account the hypothesis given line 3, the goal is obviously discharged.

In this example, we showed how demonstrate the necessary POs by hand, but in an industrial context, the Rodin toolset will be used and their embedded automatic provers will be in charge of discharging the POs. Discharging the POs (eBOUND/WD) and (event/WGHT/eBOUND) ensures that the enabled bound property is proved on the PCBsystem, i.e. always errors on cards are less reported than fair cards are produced.

Conclusion

Some properties as invariance, deadlock-freeness or convergence are natively managed in Event-B. In our probabilistic extension of Event-B, we have studied the almost certain convergence of a set of events. Moreover, a variety of research works treated the expression and verification of other probabilistic properties such as reliability or reactivity. In this paper we pursue our investigation of probabilistic properties and how to verify them using proof-based techniques. We proposed to express and check an enabled bound property where an event's probability is bounded by a fixed limit described during the requirements specification phase. This property can be used in a wide class of industrial systems, especially those where errors execution have a limit that must not be crossed. Hence, we illustrated a simplified use case of control and manufacturing of printed circuit boards where the enabled bound property was imperative to check if the likelihood of manufacturing an erroneous card can be at most equal to that of producing a correct card.

Fig. 2 .

 2 Fig. 2. PCB manufacturing system model

  . Precisely,

	CONTEXT
	PCBctx
	SETS
	Error_State
	CONSTANTS
	Max_Cards
	Max_Errors
	ICT_Error
	FCT_Error
	ICT_FCT_Error
	AXIOMS
	Max_Cards ∈ N 1
	∧ Max_Errors ∈N 1
	∧ partition (Error_State,{ICT_Error},{FCT_Error},{ICT_FCT_Error})
	∧ Max_Errors ≤ Max_Cards
	END
	Fig. 1. PCB manufacturing system context

/ ( Max_Cards + card(Cards) + Max_Errorscard(Errors) +2 )

Verification We consider that the consistency of the Event-B model PCBsystem presented above is verified by discharging all the necessary consistency proof obligations. We only focus on the verification of the enabled bound property depicted in Section 3. we annotate by bounded the event Manufacturing_Error and we add an ENABLED_BOUND: the enabling probability of Manufacturing_Error must be always limited by the value of the ENABLED_BOUND. We have chosen as ENABLED_BOUND an expression which corresponds to the enabling probability of the event Manufacturing _OK to ensure that always errors are reported less than fair cards are produced; it is a specific case: in a more general case, any expression could be chosen with respect to the case study.

To prove that the enabled bound property is verified, we must discharge the POs (eBOUND/WD) and (event/WGHT/eBOUND). The PO (eBOUND/WD) is instantiated as follows on the Event-B model PCBsystem:

 ------------------We have to show that the goal (lines 11-14) could be established using the hypotheses (lines 1-9). It is obvious since the sum given line 12 is strictly positive when taking account of the hypotheses lines 1 and 8. The hypotheses lines 5 and 9 imply that the difference (Max_Errors + 1 -Max_Cards) is also strictly positive. Thus, numerator given line 12 is strictly lower than denominator given line 13. So, the considered fraction is strictly lower than 1 and the PO (eBOUND/WD) is discharged.

Secondly, we instantiate the PO (event/WGHT/eBOUND) in the context of the bounded event Manufacturing_Error. Note that the event Manufacturing_Ok could always be triggered with Manufacturing_Error so the PO becomes as follows: -----------------


Jean Baptiste Barré
email: jean-baptiste.barre@irstea.fr

Franck Bourrier

Lauric Cécillon

Loic Brancheriau

Marie France Thévenon

Freddy Rey

David Bertrand

Loïc Brancheriau

Predicting mechanical degradation indicators of silver fir wooden strips using near infrared spectroscopy

of determination (r 2 p ) of 0.79. The Dw MOR model

Introduction

Ecological engineering structures, such as wooden check dams and timber log crib walls, are structurally based on timber structures. These structures, made from a framework of logs, require specific attention since wood may be degraded by a microbial community composed of a variety of micro-organisms or insects. In wet conditions, the most efficient ones are the wood-rotting Basidiomycetes (brown and white rots), Ascomycetes (soft and white rots) and Deuteromycetes (soft rot) that use the wood?s chemical components for their nutrition. This results in losses in wood strength and stiffness with potential risk for the structure's integrity. For that reason, practitioners have based their field investigations mainly on direct or indirect density measurement such as resistance drilling or penetration methods (Kasal and Tannert 2011; Mkip and Linkosalo 2011) and visual inspections. However, wood has already lost significant strength when fungi effects become visible and the mass loss is quantifiable [START_REF] Wilcox | Review of literature on the effects of early stages of decay on wood strength[END_REF]. Alternative approaches used, for example, on time-domain reflectometry water content [START_REF] Previati | Evaluation of wood degradation for timber check dams using time domain reflectometry water content measurements[END_REF]) and stress-wave measurement [START_REF] Dackermann | In situ assessment of structural timber using stress-wave measurements[END_REF] provide experts with more relevant information. These approaches are based on the in-situ measurement of wood decay indicators such as mass loss, hardness loss and mechanical property variations.

Specific gravity is a widely used indicator to quantify the extent of fungal attack. However, strength (Haines et al. Abstract The management of ecological engineering structures making up a timber structure requires periodical evaluations, including the level of decay of the constituent parts of the timber structure. Methods exist to measure the level of decay in the laboratory or in the field. However, they are rarely suitable for the conditions of ecological engineering structures, or give partial information. The aim of this study was to predict two mechanical degradation indicators (Dw MOE and Dw MOR ) of silver fir (Abies alba) wooden strips during microbial decomposition using nearinfrared spectroscopy (NIRS). For 1.5 years, the degradation of 180 squared wooden strips, 30 mm wide and 500 mm long, buried in a greenhouse near Grenoble, France (Altitude: 200 m) was monitored. Dw MOE and Dw MOR were set from the normalized losses in modulus of elasticity (MOE) and modulus of rupture (MOR), two mechanical properties classically used for timber-structure design. A calibration set of 109 samples was selected to build two separate predictive models of Dw MOE and Dw MOR using partial least square regression. The NIR-based models applied to a validation set of 47 samples indicated good prediction performance. The model has a root mean square error of prediction (RMSEP) of 0.15 and a coefficient 1996) and stiffness [START_REF] Przewloka | Assessment of biodeterioration for the screening of new wood preservatives: calculation of stiffness loss in rapid decay testing[END_REF]) losses are more suitable indicators at the early stage of decay [START_REF] Curling | Relationships between mechanical properties, weight loss, and chemical composition of wood during incipient brown-rot decay[END_REF]. The fungi actually alter the lignocellulosic matrix by various mechanisms [START_REF] Blanchette | Degradation of the lignocellulose complex in wood[END_REF], and therefore the mechanical properties [START_REF] Rowell | Chemistry of wood strength[END_REF]. Mechanical properties are all the more important since structural design according to the Eurocode 5 standard (CEN 2005) is based on these properties. Thus, the modulus of elasticity (MOE) and the modulus of rupture (MOR) are of interest both for structural design and to define decay indicators. However, MOE and MOR remain impossible to measure in-situ using classical methods because a bench test is necessary. An alternative solution lies in the use of the near infrared spectroscopy (NIRS) applied to milled cores sampled on structure parts to predict changes in MOE and MOR.

Functional groups of the wood molecules submitted to an electromagnetic radiation vibrate and absorb a part of the radiation. NIRS (wavelengths from 800 to 2500 nm) measures this absorbance or reflection depending on the device used. The returned spectrum is analysed statistically to extract the meaningful information. The spectral data are often used to build predictive models of variables characterizing the data set. Previous studies [START_REF] Tsuchikawa | A review of recent near-infrared research for wood and paper (Part 2)[END_REF] have shown that MOE and MOR could be predicted from near infrared (NIR) spectra using multivariate statistics. [START_REF] Kelley | Use of near infrared spectroscopy to predict the mechanical properties of six softwoods[END_REF] obtained not only accurate predictions of these mechanical properties for solid loblolly pine (Pinus taeda) samples, but also, of their chemical compounds, i.e. lignin, glucose, mannose and extractives. Sandak et al. (2015a) also reported that NIRS has been used to investigate degradation in wood structural members. Fackler et al. (2007c) analysed chemical changes due to the fungal activity. Green et al. (2010b) predicted levels of degradation in southern pine (Pinus spp.). [START_REF] Kelley | Use of NIR and pyrolysis-MBMS coupled with multivariate analysis for detecting the chemical changes associated with brown-rot biodegradation of spruce wood[END_REF] detected the chemical changes associated with brown-rot biodegradation of spruce wood.

However, they inoculated samples with only one fungus at a time and stored them in an incubator controlling humidity and temperature. On the contrary, wood inoculated with a microbial community has never been studied by NIRS to assess the level of decay.

The aim of this study was to assess the decay extent of silver fir wooden strips degraded by a microbial community using NIRS in semi-controlled conditions. First, the level of decay was defined from two degradation indicators Dw MOE and Dw MOR . They were set from the normalized losses in MOE and in MOR, respectively, between intact and decayed states. Then, partial least square regressions were performed between spectra and Dw MOE or Dw MOR to establish a predictive model of these indicators.

Materials and methods

Wood samples preparation

As intra-tree mechanical properties variation is greater than inter-tree variation [START_REF] Gonzalez-Rodrigo | Variation throughout the tree stem in the physical-mechanical properties of the wood of Abies alba Mill. From the Spanish Pyrenees[END_REF]), a single freshly-cut log of European silver fir (Abies alba sp.) was selected to supply the 209 samples (600 × 30 × 30 mm 3 ). No specific attention was paid to defects such as knots. Two pieces sized 50 × 30 × 30 mm 3 were collected from each sample: one for moisture content (MC) measurement and the other for NIRS acquisition. The residual pieces sized 500 × 30 × 30 mm 3 were used for mechanical tests (intact state), then for the degradation process.

The degradation process took place inside a greenhouse between March, 2013 and October, 2014 in Grenoble, France (Fig. 1a). The progression of decay was assumed to be heterogeneous in the cross-section and in the longitudinal direction. Nevertheless, the samples have been buried to limit the influence of heterogeneous fungal growth in the longitudinal direction compared to stakes in the field test according to the EN 252 standard (CEN 2014). One hundred and eighty of the 209 samples were buried with two layers of different materials. The first layer was made of decayed silver fir debris collected in a silver fir forest stand. This layer included an appropriate fungal community that had already been active (Fig. 1b). The second is a 5-cm local soil layer (Fig. 1c). The only controlled parameter during the degradation process was the MC of the samples, which was kept by soil humidification above the fibre saturation point (FSP), i.e. 29% according to the Tropix database (CIRAD 2011). The resistive wood moisture sensor Humitest Timb plus (Domosystem) was used to check MC in-situ. The 29 remaining samples were used to be mechanically tested until rupture at the intact state.

In the greenhouse, the samples were divided into six sets of 30 samples. The sets were successively removed from the greenhouse after 44, 73, 112, 149, 178 and 505 days. The decayed samples were prepared for measurements similar to that for the intact state: for each sample, two pieces sized 50 × 30 × 30 mm 3 were collected for NIRS and den- sity measurement. The residual sample,sized 400 × 30 × 30 mm 3 , was kept for the mechanical test. Each sample was cleaned of soil and mycelium by careful brushing prior to measurement.

Measurement of moisture content and mechanical properties

Measurement of the MC and mechanical properties was based on the assumption that they were equally distributed within the entire specimen. The MC of the samples was calculated for both intact and decayed pieces (Eq. 1). The oven-dry weight (W 0 ) was measured after sample drying until weight stabilization using a Memmert oven set at 103.5 • C.

where W h is the wet weight. MOE and MOR were measured using three point bending tests shortly after taking the samples from the greenhouse so that the variation in MC could be ignored. The cross-head loading velocity for all measurements was 2 mm/min to remain in quasi-static conditions. The MOE was calculated in the initial linear part of the load-deflection curve using Eq. 2. For practical reasons, the span-to-depth ratio was limited to 13.33 for intact samples and 10.67 for decayed samples. As a consequence, the measured deflection f included both bending and shear effects. In this case, the calculated MOE corresponded to an apparent modulus of elasticity.

where F is the applied force, L the length between the two supports, f the deflection of the sample corrected by the indentations at the supports and the head-load, and I G the moment of inertia of the cross section.

(1)

MC = [(W h -W 0 )∕W 0 ]×100 (2) MOE = F ⋅ L 3 48 ⋅ f ⋅ I G
The MOR is defined from the maximum load supported by the sample using Eq. 3 (Dinwoodie 2000b).

where F max is the maximum applied force, l the length between the two supports, b the sample width, h the sample height.

From these two properties, two mechanical indicators Dw MOE and Dw MOR were defined depending on each sam- ple's rate of degradation. They are considered as reference values used to build the predictive models. Dw MOE is the normalized loss in the MOE of the same sample between intact and decayed states (Eq. 4).

where MOE i and MOE d are the MOE of a sample in intact and decayed states, respectively.

Dw MOR is the normalized loss in the MOR. The MOR cannot be evaluated in intact and decayed states for the same sample because it has to be brought to failure to measure the MOR. Thus, the MOR of a set of 29 samples, randomly selected amongst 209 and not buried in the greenhouse were measured and averaged into one MOR * i value. Dw MOR was next calculated for each sample accord- ing to Eq. 5.

where MOR * i is the mean MOR of 29 samples in the intact states, MOR d the MOR of the sample in the decayed state.

This definition of the indicators based on normalization allows one to limit the shear effect assuming that it remains the same, whatever the level of decay. Furthermore, given that the samples's MC was kept above FSP by watering, it was assumed that MC differences had no influence on the mechanical properties and consequently on the indicators (Dinwoodie 2000a).

Near infrared spectroscopy measurements

A piece of each intact or decayed sample, a transversal slice measuring 50 × 30 × 30 mm 3 , was collected for the NIRS measurement and dried for 12 h in an oven set at 40 • C to ease the grinding. In the next step, these cut off parts of the samples were milled to a fine powder (0, 25 mm) in a Retsch ZM 200 mill. They were ground to reduce the spatial heterogeneity of wood properties existing in intact wood and reinforced by the fungal colonization [START_REF] Schwarze | Wood decay under the microscope[END_REF]. The powder was dehydrated again

(3) MOR = 3 ⋅ F max ⋅ l 2 ⋅ b ⋅ h 2 (4) Dw MOE = MOE i -MOE d MOE i (5) Dw MOR = MOR * i -MOR d MOR * i
for 12 h in an oven to limit the adverse effect of water during spectrum acquisition. Intact NIRS-sample refers to the powder obtained from an intact sample and intact spectrum to the corresponding infrared spectrum. Likewise, the powder obtained from the decayed sample was called decayed NIRS-sample and its spectrum decayed spectrum. The NIRS measurements were taken using a diffuse reflectance module with the Thermo Scientific Antaris 2 FT-NIR analyser. This instrument records the absorbance in the spectral region (3999, 10,001 cm -1 ) at a resolution of 4 cm -1 . The spectra are thus composed of 1557 wavenumbers. With the same parameters, spectra were acquired from cellulose and lignin kraft extracted from Pinus pinaster sp. samples to ease spectrum interpretations.

Spectral data treatments

The information contained in the spectra were highlighted by specific treatments. All data processing was done using R software (R Core Team 2013). The spectra were managed using the hyperSpec package [START_REF] Beleites | Critical review of chemometric indicators commonly used for assessing the quality of the prediction of soil attributes by NIR spectroscopy[END_REF].

The pre-processing step followed recommendations of Rinnan et al. ( 2009) for limiting the scattering effect usually observed with milled samples and adjusting the baseline shifts between samples. A single pre-processing step was performed on the spectra to limit the model's complexity. The spectra were adjusted by a de-trending method (baseline correction) using the baseline package [START_REF] Liland | Baseline: baseline correction of spectra Mevik BH, Cederkvist HR (2004) Mean squared error of prediction (MSEP) estimates for principal component regression (PCR) and partial least squares regression (PLSR)[END_REF].

The proposed method aims to assess the level of decay by comparing of intact and decayed spectra. A differential spectrum S diff was calculated for each decayed sample from the difference between a mean intact spectrum, the average of all intact spectra, and the spectrum of a decayed NIRSsample (Eq. 6). This methodology was selected for two reasons. Firstly, it was considered that intact spectra would not be available throughout real structure investigations. The proposal aims to consider the mean intact spectrum to establish a spectral reference for the silver fir samples. Secondly, the saproxylic community present in the greenhouse was potentially highly diverse [START_REF] Stokland | Biodiversity in dead wood. Ecology, biodiversity, and conservation[END_REF] and was not determined for practical reasons. In particular, the three types of wood-inhabiting fungus (brown, white and soft rots) might be expected. No assumption can be made on a predominantly decayed chemical compound. However, no studies have been published on the effect of the fungal community on NIR spectra. Most NIRS studies of decayed wood have investigated spectral modifications caused by known fungal species in controlled conditions. These species are mainly white or brown rot types [START_REF] Fackler | How spectroscopy and microspectroscopy of degraded wood contribute to understand fungal wood decay[END_REF][START_REF] Green | Assessment of the early signs of decay of Populus deltoides wafers exposed to Trametes versicolor by near infrared spectroscopy[END_REF]) and seldom soft rot [START_REF] Sila | soil.spec: soil spectral file conversion, data exploration and regression[END_REF]). Hence, it was proposed to highlight the affected parts of the spectra by means of S diff .

where i indicates the wavelength, abs i g.mean is the baselinecorrected absorbance of the mean intact spectrum and abs i d is the baseline-corrected absorbance of the decayed sample.

Spectral analysis

The data set exploration started with a principal component analysis (PCA) on the whole spectra. PCA facilitates the understanding of complex data sets with many variables. The partial least square regression (PLSR) was next used to develop predictive models of Dw MOE and Dw MOR from differential spectra. PLSR is a multivariate regression method used in spectroscopy because it is adapted when collinear variables are used [START_REF] Wold | PLS-regression: a basic tool of chemometrics[END_REF]. Sandak et al. (2015b) referred to several studies using PLSR in a quantitative manner in decayed-wood investigations. The process of model construction was divided into calibration and validation phases (Fig. 2).

The validation phase consists of applying the PLSR function from the pls package [START_REF] Mevik | pls: partial least squares and principal component regression Mkip R, Linkosalo T[END_REF] to a calibration set of 109 samples using the Kennard-Stone algorithm, as implemented in the soil.spec package [START_REF] Sila | soil.spec: soil spectral file conversion, data exploration and regression[END_REF]. In this phase, the models were internally validated by the leave-oneout (LOO) cross-validation method. The quality of the PLSR models was assessed using the coefficient of multiple determination r 2 c and the root mean squared error of calibration (RMSEC), i.e. the residuals of the calibration data. Likewise, the results of the cross validation has been characterized by r 2 cv , the root mean squared error of cross-validation (RMSECV) (Mevik and Cederkvist 2004) prediction (RMSEP), the ratio of performance to deviation (RPD), calculated as the ratio of the standard deviation of the reference data to the RMSEP [START_REF] Schimleck | Estimation of the physical wood properties of green Pinus taeda radial samples by near infrared spectroscopy[END_REF], and the bias, calculated as the difference of the mean of the predicted values versus the mean of the true values [START_REF] Beleites | Critical review of chemometric indicators commonly used for assessing the quality of the prediction of soil attributes by NIR spectroscopy[END_REF]. The value of the bias should be close to 0 for accurate calibration.

Wavelength selection

Following the recommendations of [START_REF] Schwanninger | A review of band assignments in near infrared spectra of wood and wood components[END_REF], the spectral range was reduced to improve the model's performance. The principle adopted consisted in retaining regions where differences between decay and the mean intact spectra were considered high. For this purpose, a process in two-step was developed. Firstly, the standard deviation (SD) of absorbances abs i diff among the different S diff spectra was calculated for each wave- length. Only the wavelengths corresponding to SD larger than a threshold value SD lim were kept in the PLSR. Sec- ondly, an iterative test was developed to determine the best wavelength range, i.e. those that minimize RMSEP. Thus, different thresholds were tested by varying SD lim from 0 to the optimal SD lim which corresponded to the lower RMSEP. Furthermore, the laboratory climate was not fully controlled and dried wood samples are very hydrophilic. Thus, the wavelengths associated with water (5150-5220, 5051, 7073 cm -1 ) were removed from the analysis, even if they corresponded to wavelengths associated with OH-bonds of wood compounds [START_REF] Schwanninger | A review of band assignments in near infrared spectra of wood and wood components[END_REF]. OH-bonds are nevertheless related to other wavelengths, in particular those from 4620 to 4890 cm -1 , where spectra variations due to fungi were observed [START_REF] Sandak | Monitoring of wood decay by near infrared spectroscopy[END_REF].

Results and discussion

The aim of this study was to quantify the level of decay of silver fir strips degraded by a fungal community using NIRS. For this purpose, reference indicators Dw MOE and Dw MOR were defined from MOE and MOR measured in the intact and decayed states. The intact wooden strips were buried in a greenhouse for a period of 44-505 days. After the decay process, the evidence of fungal activity was visually observed at the surface of the samples. Mycelium was noted on all samples with variable intensities in terms of spatial distribution (Fig. 3). Small cracks were present on the most severely decayed samples. The slicing of samples made it possible to visually ascertain that discolourations were present inside the wood to a variable extent. It was assumed that fungi penetrated wood a short time after inoculation.

Mechanical degradation indicators Dw MOE and Dw MOR

For the 109 samples of the calibration set, the mean MOE was 8211 MPa (i.e N∕mm 2 ) (SD 951 MPa; Table 1). The mean MOR, calculated from 29 of the intact samples, was 41.9 MPa (SD 7.0 MPa). The mean MC was 106%, always greater than 30%. For the 47 samples of the validation set, the mean MOE was 8172 MPa (SD 829 MPa). The mean MC was 113%. For decayed samples, the mean MOE was 3889 MPa and 2966 MPa (SD 2191 and 2486 MPa) for the calibration and validation sets, respectively. The mean MOR was 30.1 and 23.9 MPa (SD 14.2 and 17.1 MPa) for the calibration and validation sets, respectively. For the last series (i.e. 505 degradation days, 25 samples), the MOE and MOR were set at 0 MPa because the samples were too degraded to be tested using bending tests and could easily be broken by hand. The MOE and MOR were correlated in the intact and decayed states (Fig. 4). Indeed, an increase in MOE induces an increase in MOR. Assuming a linear relationship between these two variables gives coefficients of determination r 2 of 0.72 and 0.86, respectively. The MOE and MOR measurements in decayed conditions were skewed by the heterogeneity of fungal decay visually observed in the cross-section given that Eqs. 2 and 3 were defined assuming an isotropic material. However, it gave coherent values from a decay-assessment perspective. Thus, the degradation process tested in the greenhouse provided a large data set of 156 Dw MOE and Dw MOR val- ues (Fig. 5). Regarding Dw MOR , 28 negative values ranging from -0.27 to 0 (mean of negative Dw MOR : -0.09) were observed as the MOR of decayed samples was compared to a mean MOR of intact samples. This is in particular the consequence of the MOR's variability rated at 9 MPa (SD for silver fir-Tropix 7). From a mechanical point of view, both indicators have different meanings and appear to be complementary in the context of timber structure design and monitoring. Dw MOE is related to the bending stiffness and therefore linked to wooden beam deformation. Dw MOE could therefore be used to assess a capacity of deformation before rupture. Dw MOR is related to the bending strength and thus to the material rupture.

Near-infrared spectra

Spectrum exploration using PCA performed with all wavenumbers showed a separation between intact and decayed NIRS-samples (Fig. 7a). The first component (PC1) loadings (Fig. 7b) were characterized by three main peaks (around 4502, 5361 and 7577 cm -1 ) corresponding to wavenumbers where baseline-corrected absorbances are extremely low (Fig. 6). These three peaks were also observed on the second component (PC2) loadings (4995, 5331, 5390, 7553 and 7658 cm -1 ). The PC2 pointed to a lesser extent to five other wavenumbers: 4142, 4870, 5022, 5770, 9045 cm -1 . PCA performed only on decayed NIRS-samples showed a graduation of Dw MOE (Fig. 8a) or Dw MOR (Fig. 8b) visible along PC1 axes.

The mean intact and decayed spectra followed the same pattern but decayed spectra had lower baseline-corrected absorbance values in the whole NIR spectral range (4000-10,000 cm -1 ) (Fig. 6).

The findings of this study confirm that NIRS spectra contain relevant information regarding the microbial activity in wood, even at the early stage. The first feature highlighted by PCA (Fig. 7a) is a difference between the spectra of intact and decayed samples, whatever the duration of decay. This is also observed on the spectrum plot (Fig. 9). The loss in baseline-corrected absorbance of decayed spectra compared to the intact spectra is visible in regions associated with cellulose (peaks 5865 and 6727 cm -1 ) or lignin (peaks, 6875 and 5972 cm -1 ) [START_REF] Schwanninger | A review of band assignments in near infrared spectra of wood and wood components[END_REF]). Similar observations have been described with different wood species decayed by brown or white rots (Fackler et al. 2007a;[START_REF] Sandak | Monitoring of wood decay by near infrared spectroscopy[END_REF], remembering that soft rot may be involved in the experiment given that the samples were subjected to a microbial community. This constant difference Wavenumber (cm -1 ) Baseline corrected absorbance between spectra confirms the value of calculating a differential spectrum that extracts the meaningful spectral information. PCA of decayed NIRS-samples (Fig. 8) also distinguishes strongly decayed samples (Dw MOE > 0.75 and Dw MOR > 0.75 ) from samples that are less decayed along the PC1 axis. PCA is, however, limited for further investigation because of an aggregation of less decayed NIRS-samples. PCA loadings (Fig. 7b) reveal no specific wavelength except one associated with OH-bonds (peak, 5021 cm -1 ) and others where baseline-corrected absorbance is low (peaks, 4502, 5361, 7577 and 9036 cm -1 ).

The differential spectra provide evidence of some spectral regions where differences between the mean intact spectrum and decayed spectra are of interest (Fig. 11). Nevertheless, these regions are distributed all along the NIR range. PLSR performed in the whole NIR range should be sufficient to assess decay, as other studies did [START_REF] Sila | soil.spec: soil spectral file conversion, data exploration and regression[END_REF][START_REF] Leinonen | FT-NIR spectroscopy in predicting the decay resistance related characteristics of solid Scots pine (Pinus sylvestris L.) heartwood[END_REF][START_REF] Green | Assessment of the early signs of decay of Populus deltoides wafers exposed to Trametes versicolor by near infrared spectroscopy[END_REF]. But this solution would not be optimal according to suggestions by [START_REF] Nadler | The prediction error in CLS and PLS: the importance of feature selection prior to multivariate calibration[END_REF] and [START_REF] Cécillon | Variable selection in near infrared spectra for the biological characterization of soil and earthworm casts[END_REF] that prescribe wavelength range reduction to the root mean square error of PLSR. This motivated the development of the wavelength selection method presented in this study.

Prediction of mechanical degradation indicators

Dw MOE and Dw MOR using the PLSR of differential spectra

Wavelength selection

The optimal SD values to determine wavenumbers ranges optimizing the PLSR are 0.0062 (Dw MOE ) and 0.0055 (Dw MOR ) (Fig. 10). Figure 11 presents the different spectral ranges kept for the PLSR. In both cases, six similar ranges were selected. Amongst the six regions identified, regions 2, 3, 4 and 5 of both models (Fig. 11) had similarities to those obtained by other research on decay effects on wood spectra. Fackler et al. (2007b) found the best regression for weight loss of brown rotted beech wood in the NIR region (7235-6106 and 5384-4150 cm -1 ). They reported that this model was not applicable to white rot fungi. [START_REF] Ishizuka | Quantifying lignin and holocellulose content in coniferous decayed wood using nearinfrared reflectance spectroscopy[END_REF] retained 4050-5000 and 5800-6800 cm -1 for PLSR to predict lignin and cellulose contents. The main difference between the two studies and the results presented herein remains in the (5800-6000 cm -1 ) region associated with lignin and identified as being important in the case of white rot. This range was not included in region 5, which starts at 6163 and 6144 cm -1 for Dw MOE and Dw MOR , respectively. It was concluded that lignin might be less affected than polysaccharides by the fungal community involved. In natural conditions, the composition of the fungal community changes over time and depends on early established and long-lived species [START_REF] Ottoson | Succession of wood-inhabiting fungal communities[END_REF]. Thus, further investigations of the method on various fungal communities in natural conditions would be highly valuable.

PLSR models With these spectral ranges, two PLSR models were developed from differential spectra S diff to pre- dict Dw MOE or Dw MOR . The results obtained after the LOO validation were significant with RMSECV of 0.16 for both indicators and r 2 v of 0.63 and 0.77 for Dw MOE and Dw MOR prediction, respectively (Table 2). These models applied to the validation set confirm the consistency of the results: to predict Dw MOE and Dw MOR , RMSEP was 0.15 and 0.13, r 2 p was 0.79 and 0.91, RPD was 2.0 and 3.2, and the bias was 0.032 and 0.036, respectively. The relationships between measured and NIR-predicted values for both indicators and their associated prediction residuals are shown in Fig. 12.

The current results support previous research (Tsuchikawa and Schwanninger 2013) that reported a statistical link between NIRS spectra and mechanical properties The dashed lines correspond to the optimal SD lim , i.e. where RMSEP is minimal using PLSR. However, while most studies work with intact wood, the current models establish relationships between NIRS differential spectra S diff and losses in MOE and MOR of decayed wood (Table 2). Green et al. (2010a) already used NIRS and PLSR to predict the level of decay in wood measured by compression strength in particular. They obtained appreciable results with r 2 p of 0.69 and RPD of 2.61 (model with raw spectra). While this study showed that NIRS could predict wood decay, it used Gloeophyllum trabeum (brown rot type) to inoculate samples. The current study shows similar results (r 2 p 0.79 and RPD 2.0 for Dw MOE prediction. r 2 p 0.91 and RPD 3.2 for Dw MOR predic- tion) for predicting the level of decay in silver fir wooden strips inoculated with a microbial community.

Finally, from a practical standpoint, these methods may be applied to real structures by means of core collection [START_REF] Noetzli | Influence of decay fungi, construction characteristics, and environmental conditions on the quality of wooden check-dams[END_REF]. Spectral acquisition of cores could be directly acquired at different parts of the cores or on milled cores [START_REF] Schimleck | Near-infrared spectroscopy: a rapid non-destructive method for measuring wood properties and its application to tree breeding[END_REF]. Cores 5 mm in diameter have very limited mechanical damage against the diameter of the logs generally used in ecological engineering structures (diameter above 150 mm) and are easy to reduce into powder. This would give practitioners quantitative information about the level of decay of parts located by their expertise. However, the method needs to be tested previously on beams similar to those used in ecological engineering structures, i.e. wooden logs. The mean intact spectrum of silver fir should also be enriched by spectra from other locations to ensure that it covers the heterogeneity of the species.

Conclusion

The main purpose of this study was to predict degradation indicators of silver fir wooden strips decayed by a microbial community using NIRS. Two indicators of the level Fig. 11 Mean spectrum and standard deviation of the differential spectra S diff . The red ribbons (lengthwise stripes) show the excluded wavenumbers for PLSR. a Dw MOE prediction, range 1: 3900-4104 cm -1 , range 2: 4211-4420 cm -1 , range 3: 4632-4929 cm -1 , range 4: 5079-5145 cm -1 , range 5: 6163-7243 cm -1 , range 6: 8080-8539 cm -1 . b Dw MOR prediction. range 1: 3900-4107 cm -1 , range 2: 4200-4423 cm -1 , range 3: 4624-4933 cm -1 , range 4: 5068-5145 cm -1 , range 5: 6144-7343 cm -1 , range 6: 8079-8604 cm -1 0.00 0.02 0.04 4000 6000 8000 10000

Wavenumbers (cm -1 ) Baseline corrected absorbance of decay, Dw MOE and Dw MOR , were developed allowing an accurate evaluation of the level of decay in terms of mechanical properties. These indicators were related to the near infra-red spectra seen as estimators of the chemical compounds. The analysis of the NIRS spectra of intact and decayed milled samples confirmed the NIRS sensitivity to decay even under semi-controlled conditions. This sensitivity is observable over the full spectral range and nonattributable to one specific chemical compound (i.e. lignin, cellulose or hemicellulose). Based on these observations, two models were developed from spectra to predict Dw MOE and Dw MOR using PLSR. Predicted and measured values were highly correlated with r 2 p values of 0.79 (Dw MOE ) and 0.91 (Dw MOR ). These models can provide useful tools for the rapid screening of wood residual properties of structural members. For that purpose, complementary investigations are needed. The scattering effects may be corrected by several methods, the multiplicative scatter corrections in particular (Rinnan et al. 2009), that should be compared in the context of the assessment of the level of decay. Furthermore, the method has been intentionally developed with a data set of limited variability (samples were sampled from one log). The generalisation of the method with a data set taking into account an extensive variability is necessary.

Fig. 1

 1 Fig. 1 Successive steps of sample installation in the greenhouse. a Intact samples divided into series; b samples covered with the first layer of woody debris; c samples covered by the second layer of soil

Fig. 2

 2 Fig. 2 Details of the validation process of the predictive models

Fig. 3 a

 3 Fig. 3 a Mycelium observed on the surface of a sample degraded for 73 days. The tape measure is in centimetre. b The mycelium may have a higly variable spatial extent. Sample degraded for 112 days

Fig. 4 Fig. 5

 45 Fig. 4 Relationship between the MOE and MOR in intact (black points) and decayed (grey points) states

Fig. 6 Fig. 7 a

 67 Fig.6Mean intact spectrum (solid line) and the mean decayed spectra (solid line with ribbon) with the ribbon that represents the absorbance standard deviation

Fig. 8 Fig. 9

 89 Fig. 8 Principal component analysis of the baselinecorrected spectra of decayed samples. Grey scale and sizes are a function of the level of decay according to Dw MOE (a) and Dw MOR (b)

Fig. 10

 10 Fig. 10Standard deviation of the differential spectra S diff with the optimal SD lim (dashed lines) for PLSR with Dw MOE (a), and with Dw MOR (b). RMSEP variation is a function of SD lim for Dw MOE(c)

Fig. 12

 12 Fig. 12 Comparison between measured and predicted values for Dw MOE (a) and Dw MOR (c). The empty dots indicate the calibration set and the filled dots indicate the validation set. Prediction residuals Dw MOE (b) and Dw MOR (d) of for the validation set

Table 1

 1 Physical and mechanical measurements and indicators of the level of decayRange and standard deviation (SD)

		Calibration set, n=109		Validation set, n=47
	Wood property	Mean	Min.	Max.	SD	Mean	Min.	Max.	SD
	Intact samples
	Moisture content (%)	106	32	179	44	113	35	181	47
	MOE intact (MPa)	8211	5672	10275	951	8172	5792	9460	829
	MOR intact (MPa) a	41.9	28.3	56.6	7.0	-	-	-	-
	Decayed samples
	Moisture content (%)	104	42	175	37	106	47	170	35
	MOE decay (MPa)	3889	0	9001	2191	2966	0	6905	2486
	MOR decay (MPa)	29.8	0	53.3	14.2	23.9	0	49.9	17.1
	Indicators
	Dw MOE (-)	0.52	0.06	1	0.27	0.64	0.13	1	0.30
	Dw MOR (-)	0.29	-0.27	1	0.34	0.43	-0.19	1	0.42
	a Measured for 29 intact samples

Table 2

 2 Main model characteristics developed for predicting indicators Dw MOE and Dw MOR NF number of factors, RMSEC root mean squared error of calibration, RMSEC root mean squared error of cross validation, RMSEP root mean squared error of prediction, RPD relative percent difference ratio of SD to RMSEP, Bias the difference of the mean of the predicted versus the mean of the true values

	Mechanical indicator	Calibration phase, n = 109 Calibration	LOO cross-validation	Validation phase, n = 47 Prediction
		NF	r 2 c	RMSEC	NF	r 2 v	RMSECV	r 2 p	RMSEP	RPD	Bias
	Dw MOE	11	0.75	0.14	11	0.64	0.16	0.79	0.15	2.0	0.032
	Dw MOR	11	0.85	0.13	11	0.77	0.16	0.91	0.13	3.2	0.036

Acknowledgements This work has been financed within the framework of projects SEDALP (Interreg Alpine space program. [2013][2014][2015] and Arc Environnement (Rhône Alpes Region, France).