Françoise Bellegarde
email: bellegar@lifc.univ-fcomte.fr

Jacques Julliand
email: julliand@lifc.univ-fcomte.fr

Hassan Mountassir
email: mountass@lifc.univ-fcomte.fr

Emilie Oudot
email: oudot@lifc.univ-fcomte.fr

Experiments in the use of τ -simulations for the components-verification of real-time systems

Keywords: τ -simulation, integration of components, timed systems, preservation of linear-time properties

We present a verification framework exploiting τ -simulations as a way to preserve local linear properties checked on the components of real-time systems. Therefore, we consider a component-based modeling of real-time systems. Their properties are expressed in a timed logic, Mitl (Metric Interval Temporal Logic). For component-based models, traditional verification techniques are generally applied to the complete composed model, even if some properties only concern some components of the system, if not only one. We show that it is possible to check such local linear properties (safety as well as liveness) on the components they concern, and then to ensure their preservation using τ -simulation relations. We show the interest of the method by applying it on two real-time systems examples and by comparing the results with traditional verification techniques.

MOTIVATIONS

Component-based modeling is a modeling method that receives more and more attention. In particular, timed systems are often modeled this way. First, it consists in decomposing the system into a set of sub-systems, called components. The complete model is obtained by putting all the components together, thanks to some parallel composition operator. To ensure their correctness, such models have global requirements to meet, i.e., requirements about the behaviour of the complete model, as well as so-called local requirements. Local requirements are properties concerning the components (or subsets of components) of the system. Model-checking is a verification method that can be used in order to verify these properties on the model. For both kinds of properties, the verification is performed on the global model. However, this method is generally not applicable on large-sized systems, due to the exponential blow-up of the state space. We propose a verification method for local linear properties of real-time systems modeled in a compositional framework, by taking advantage of the modeling process. We propose to model systems incrementally, by integration of components: instead of building once the complete model, components (or assembling of components) are integrated step by step to the others, and local properties are checked on these components (or assembling of components) before integration. Model-checking is still applicable since the size of each component / assembling of components is small enough. To ensure that locally established properties continue to hold after integration, we propose to use timed τ -simulations, i.e., simulation relations extended to handle timing aspects and internal activity of the models. Indeed, it is known that in the untimed case, classic τ -simulations preserve linear safety properties. Divergence-sensitive and stabilityrespecting τ -simulations [START_REF] Glabbeck | The Linear Time -Branching Time Spectrum II ; The semantics of sequential systems with silent moves[END_REF] also handle the preservation of linear liveness properties. For that matter, this last kind of τ -simulation is already used in other incremental modeling processes, such as the refinement of B event systems [START_REF] Oudot | Extending B without changing it (for developing distributed systems)[END_REF], which preserves Ltl properties [START_REF] Darlot | Refinement Preserves PLTL Properties[END_REF]. In [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF], we defined a timed τ -simulation adapted for timed systems and showed that it preserves safety (un)timed properties. Moreover, we showed that it is well-adapted with integration of components made with the classic parallel composition operator ||. That is, given two components A and B, A τ -simulates A||B and B τ -simulates A||B. In terms of preservation of properties, this means that linear safety properties of A and B are preserved for free when A and B are merged together. The timed τ -simulation is also compatible with the operator ||: given a third component C, if B τ -simulates A, then B||C τ -simulates A||C. Compatibility allows to benefit of the compositionnality property:

given components A, B, C and D, if B τ -simulates A and D τ -simulates C, then B||D τ -simulates A||C. Thus, this first timed τ -simulation has nice properties w.r.t. parallel composition. However, as it only preserves safety properties, we extended it into a divergence-sensitive and stabilityrespecting (DS) timed τ -simulation to preserve a larger spectrum of properties, such as liveness or bounded liveness properties. We proved in [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF] this new relation preserves all properties which can be expressed by the linear-time logic Mitl [START_REF] Alur | The benefits of relaxing punctuality[END_REF].

In this paper, we aim at showing the interest of the verification method we propose by applying it to the verification of the local properties of two timed systems. In both examples, we compare the application of our method with the classic verification method, consisting in verifying directly all the properties on the complete model. The first example is a production cell, made up of at least seven components. We focus in particular on the local properties of one of these components, and perform the verification locally on this component before verifying the preservation thanks to the timed τ -simulations. This example shows that the cost of this kind of verification (local verification and preservation checking) is lower than the cost of the classic verification method, in terms of computation times. The second example is a well-known protocol, the CSMA/CD protocol, composed of a medium and at least two senders. With this example, we show that one of the main properties of the protocol can be checked by only considering the smallest possible number of senders, i.e. two, instead of verifying it with a greater number of senders. Moreover, in both examples, we identify cases where the classic verification method is not applicable while the method we propose is.

The paper is organized as follows. In section 2, we present the model we use for modeling timed systems -timed automata [START_REF] Alur | A theory of timed automata[END_REF], the logical formalism Mitl used to formulate their properties and the parallel composition || used for the integration of components. In section 3, we recall the definitions and results of [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF], where we defined timed τsimulations and gave its properties w.r.t. the preservation of Mitl properties and the compatibility with parallel composition. Section 4 shows the interest in practice of the verification method we propose, by applying it to two examples of timed systems and comparing the results with the classic verification method. Finally, section 5 sums up the results presented in the paper and plans the future works. Related works. Numerous works have been devoted to the study of timed simulation relations and their preservation ability. A time-abstracting simulation has been studied in [START_REF] Henzinger | Computing simulations on finite and infinite graphs[END_REF], where an algorithm to check the relation is proposed. However, timed properties are not preserved by this relation. A timed simulation was defined in [START_REF] Tasiran | Verifying Abstractions of Timed Systems[END_REF]. The authors showed that the problem of verifying the existence of this timed simulation is EXPTIME. But, internal activity is not handled by this relation. The closest notion of simulation, in comparison with our timed τ -simulation, is the timed ready simulation of [START_REF] Jensen | Scaling up Uppaal : Automatic verification of real-time systems using compositionnality and abstraction[END_REF]. Internal activity is also considered. As our (DS) timed τ -simulation, this relation also handles the preservation of safety properties, but does not preserve other kind of properties, such that liveness properties. To our knowledge, there is no previous definition or use of simulation relations handling internal activity as well as timing constraints, and preserving safety and, especially, liveness properties.

MODELING TIMED SYSTEMS

Timed automata [START_REF] Alur | A theory of timed automata[END_REF] are amongst the most studied formal models for timed systems. They are classical finite automata with real-valued variables called clocks modeling the time elapsing.

Clock valuations and clocks constraints

Let X be a set of clocks. A clock valuation over X is a function v : X → R + assigning to each clock in X a real value. For δ ∈ R + , the valuation v + δ is obtained by adding δ to the value of each clock. Given Y ⊆ X, and a valuation v over X, the dimension-restricting projection of v on Y [START_REF] Tripakis | The analysis of timed systems in practice[END_REF], written v Y , is a new valuation containing only the values in v concerning the clocks in Y . The reset operation on v of the clocks in Y , written [Y := 0]v, creates a valuation obtained from v by setting to zero all clocks in Y , and leaving the values of other clocks (∈ X\Y ) unchanged. A clock constraint over X is a predicate of the form

g ::= x ∼ c | g ∧ g | true where x ∈ X, c ∈ N and ∼∈ {<, ≤, =, ≥, >}
The set of all clock constraints over X is called C(X). We say that a valuation v satisfies a constraint x ∼ c, written v ∈ x ∼ c, if v(x) ∼ c. Note that a clock constraint over X defines a X-polyhedron. The reset operation defined on valuations can be extended straightforwardly to polyhedra. The backward diagonal projection of a polyhedron g defines a new polyhedron g s.

t. v ∈ g if ∃δ ∈ R + • v + δ ∈ g.

Timed automata (TA)

Syntax. Let P rops be a set of atomic propositions. A timed automaton A over P rops is a tuple Q, q 0 , Labels, X, T, Invar, L where Q is a finite set of locations, q0 is the initial location, Labels is a finite set of names of actions and X is a finite set of clocks. Invar : Q → C(X) is a function associating to each location a clock constraint called its invariant. The invariant of a location defines the time progress condition for this location. L : Q → 2 P rops is the labelling function for the locations. T ⊆ Q × C(X) × Labels × 2 X × Q is a finite set of transitions. Each transition can reset clocks and is equiped with a clock constraint called its guard, defining when the transition can be taken. We write a transition e as a tuple (q, g, a, λ, q ) where q and q are respectively the source and target location of the transition, g is its guard, a its label and λ the set of clocks to be reset by the transition.

In the rest of the paper, we use the notations source(e) and target(e) for q and q , guard(e) for g, label(e) for a and reset(e) for λ.

Semantics. The semantics of A is an infinite graph where states 1 are pairs (q, v) composed of a location q of A (the discrete part of the state) and a clock valuation v s.t. v ∈ Invar(q). The initial state is the pair (q0, v0) where v0 is the clock valuation assigning 0 to each clock in X. The transitions of the graph are either discrete transitions or time transitions:

• discrete transitions: given a transition e = (q, g, a, λ, q ) of A, (q, v) e → (q , v ) is a discrete transition of the graph if v ∈ g and v ∈ Invar(q ). The valuation v is obtained from v by resetting the clocks in λ. We call (q , v ) a discrete successor of (q, v),

• time transitions: (q, v) δ → (q, v + δ) is a time transition of the graph, for δ ∈ R + , if v + δ ∈ Invar(q). We call (q, v + δ) a time successor of (q, v).

Runs. A run ρ = (q0, v0) δ 0 → (q0, v1) e 0 → (q1, v2) δ 1 → (q1, v3) δ 2 → (q1, v4) e 1 → (q2, v5) • • • of a TA A is
a path in its semantic graph. Note that consecutive time transitions are not concatenated. We note Γ(A) the set of runs of A. A run ρ is non-zeno if time can progress along ρ without upper bound. We write time(ρ) for the total time elapsed during ρ. If time(ρ) = ∞ then ρ is called non-zeno.

Properties of timed systems

Mitl (Metric Interval Temporal Logic) [START_REF] Alur | The benefits of relaxing punctuality[END_REF] is a logical formalism allowing to express linear timed properties. It can be viewed as an extension of the (untimed) linear logic Ltl [START_REF] Pnueli | The temporal logic of programs[END_REF], where each temporal operator used in the formulas is constrained by a non singular interval with integer bounds (a singular interval is of the form [a, a], i.e., it is closed and the left and right bounds are equal). Mitl formulas are defined inductively by the following grammar:

ϕ ::= ap | ¬ϕ | φ ∨ ψ | φ UI ψ
where ap is an atomic proposition and I is a non singular interval with integer bounds. Other classical temporal operators can be defined: 3I ϕ = true UI ϕ (eventually ϕ) and

I ϕ = ¬3I ¬ϕ (always ϕ).
Mitl properties are interpreted over runs of a timed automaton. Intuitively, a property φ UI ψ holds on a run if, when φ is met, φ holds until ψ is true. Moreover, ψ must hold at a time t within the time interval I following the moment when φ was true. An Mitl property is satisfied by a timed automaton if it holds on each run of the automaton.

Integration of components

Consider a timed system composed of a set of components A1, A2, • • • , An, each one modeled by a TA. Integration of components is a type of incremental modeling, which consists in first considering one component, for instance A1. Then, the other components are successively added to A1, until obtaining the complete system. We consider that this integration is achieved by using the classic parallel composition operator ||. This composition is defined as a synchronized product where the synchronizations are done on actions with the same label, while other actions interleave. Formally, consider two TA Ai = Q i , q 0 i , Labelsi, Xi, Ti, Invari, Li , for i = 1, 2, s.t. X1 ∩ X2 = ∅. The parallel composition of A1 and A2, written A1||A2, creates a new TA which set of clocks is X1 ∪ X2 and which labels are the set Labels1 ∪ Labels2. The set Q of locations consists of pairs (q1, q2) composed of a location of each Ai. Invar((q1, q2)) is defined as Invar(q1) ∧ Invar(q2) and L((q1, q2)) is the set L(q1) ∪ L(q2). The initial location is the pair (q0 1 , q0 2 ). The set of transitions T is given by the three following rules: Synchronization:

(q 1 ,g 1 ,a,λ 1 ,q 1 ) ∈ T 1 , (q 2 ,g 2 ,a,λ 2 ,q 2 ) ∈ T 2 ((q 1 ,q 2 ),g 1 ∧g 2 ,a,λ 1 ∪λ 2 ,(q 1 ,q 2 )) ∈ T

Interleaving:

(q 1 ,q 2 )∈Q , (q 1 ,g 1 ,a,λ 1 ,q 1 ) ∈ T 1 , a ∈Labels 2 ((q 1 ,q 2 ),g 1 ,a,λ 1 ,(q 1 ,q 2 )) ∈ T (q 1 ,q 2 )∈Q , (q 2 ,g 2 ,a,λ 2 ,q 2 ) ∈ T 2 , a ∈Labels 1 ((q 1 ,q 2 ),g 2 ,a,λ 2 ,(q 1 ,q 2 )) ∈ T

Incremental modeling, and in particular integration of components, is a way to cope with the complexity of the verification when large-sized model are treated. Indeed, it could allow to verify local properties of the components at each step of the modeling, i.e., at each integration of components, instead of performing the verification directly on the complete system. However, this reasoning is valid only if the integration preserves the properties already checked.

EXPLOITING SIMULATIONS TO PRE-SERVE LOCAL PROPERTIES

We showed in [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF] that timed τ -simulations are sufficient conditions for the preservation of Mitl properties during incremental modeling, and in particular, integration of components. That is, if a component τ -simulates the whole system w.r.t. some τ -simulation relation, then already established properties of the component are preserved after integration in its environment. We defined in [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF] two τ -simulation relations: one dealing with safety Mitl properties (called a timed τ -simulation)2 , and the other to handle all Mitl properties (divergence-sensitive and stability-respecting timed τsimulation).

Timed τ -simulations

Consider a TA A1 that has to be integrated in an environment E. We note A2 = A1||E the result of the integration. Consider also that A1 and E have a common subset of labels of actions -the synchronized actions -, i.e., labelsA 1 ∩ labelsE = ∅. Let us rename by τ all the labels of the own actions of the environment (the non-common labels of E) and call them τ -actions. The timed τ -simulation S between the semantic graphs of A2 and A1 is characterized by the following points: if A2 can make an action of A1 after some amount of time (that is, either a synchronized action or an own action of A1), then A1 could also do the same action after the same amount of time (clauses 1 and 2 of Definition 1), and own actions of E (τ -actions) stutter (clause 3).

Definition 1 (Timed τ -simulation S). Let A1 = Q 1 , q 0 1 , Labels1, X1, T1, Invar1, L1 and A2 = Q 2 , q 0 2 , Labels1∪ {τ }, X2, T2, Invar2, L2 be two TA such that X1 ⊆ X2. S1
and S2 are the respective set of states of A1 and A2. The relation S is included in S2 × S1. We say that (q2, v2)S(q1, v1) if v2 X 1 = v1 and 1. Strict simulation:

(q2, v2) e 2 → (q 2 , v 2 ) ∧ label(e2) ∈ Σ1 ⇒ ∃(q 1 , v 1 )• ((q1, v1) e 1 → (q 1 , v 1 ) ∧ label(e1) = label(e2) ∧ (q 2 , v 2 ) S (q 1 , v 1 )).

Time transitions:

(q2, v2) δ → (q2, v 2 ) ⇒ ∃(q1, v 1 ) • ((q1, v1) δ → (q1, v 1 ) ∧ (q2, v 2 ) S (q1, v 1 )).

Stuttering:

(q2, v2) e 2 → (q 2 , v 2 ) ∧ label(e2) = τ ⇒ (q 2 , v 2 ) S (q1, v1).
We say that A1 τ -simulates A2 w.r.t. S, written A2 A1, if s0 2 S s0 1 , where s0 1 and s0 2 are the respective initial states of A1 and A2. This τ -simulation only preserves safety properties. To preserve also liveness properties, it has to be (1) stability -respecting: the integration of A1 in E must not create deadlocks in comparison with A1 (all the deadlocks appearing in A1||E must already exist in A1), and (2) divergencesensitive: the own actions of the environment E must not have the possibility to take the control forever, i.e., A1||E must not contain non-zeno runs composed of an infinite sequence of successive τ -actions. Such a run is called a nonzeno τ -cycle, and a TA containing such a run is called τdivergent.

The predicate free. To deal with the non-introduction of deadlocks during the integration, we use the predicate free introduced in [START_REF] Tripakis | The analysis of timed systems in practice[END_REF]. Informally, free(q) computes the set of valuations of the states with discrete part q that can let some time pass and then take a discrete transition (i.e., non-blocking states):

free(q) = [ e∈out (q)
(guard(e)∩([reset(e) := 0]Invar(target(e))))

where out(q) is the set of discrete transitions leaving from q.

Non-zeno τ -cycles. Let A be a TA where some labels of actions are renamed by τ . We say that A does not contain any non-zeno τ -cycles (and thus that A is not τ -divergent) if:

∀ρ, k • (ρ ∈ Γ(A) ∧ time(ρ) = ∞ ∧ k ≥ 0 ⇒ ∃k , e • (k ≥ k ∧ (ρ, k ) e → (ρ, k + 1) ∧ label(e) = τ )).
We restrict the timed τ -simulation of Def. 1 by adding conditions imposing divergence-sensitivity and stability-respect. This Divergence-sensitive and Stability-respecting (DS) timed τ -simulation is defined as follows.

Definition 2 (DS timed τ -simulation S ds ). Consider two TA A1 = Q 1 , q 0 1 , Labels1, X1, T1, Invar1, L1 and A2 = Q 2 , q 0 2 , Labels1∪{τ }, X2, T2, Invar2, L2 , such that X1 ⊆ X2 and A2 is not τ -divergent. S1 and S2 are the respective set of states of A1 and A2. The relation S ds is included in S2 × S1. We say that (q2, v2)S ds (q1, v1) if

(q 2 , v 2 )S(q 1 , v 1 ) and v 2 ∈ free(q 2 ) ⇒ v 1 ∈ free(q 1 )
We say that A1 τ -simulates A2 w.r.t. S ds , written A2 ds A1, if s0 2 S ds s0 1 .

Properties of timed τ -simulations

We give in this section the main propositions and theorem showing the interest of the timed τ -simulations for the incremental modeling of timed systems. Indeed, the timed τ -simulation is well-adapted to the parallel composition operator || (Proposition 1). Moreover, this operator does not add τ -divergence if the environment in which a component is integrated is not τ -divergent (Proposition 2). Theorem 1 is the main result, showing that the DS timed τ -simulation preserves Mitl properties. Proofs can be found in [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF]. Therefore, in the context of integration of components, the preservation of local safety properties can be obtained for free, since parallel composition is compatible with the timed τ -simulation. The preservation of local linear liveness properties of a component can be ensured only by checking that its integration in an environment does not create deadlocks and that this environment is not τ -divergent.

Remark 1. T ctl [START_REF] Alur | Model-Checking in Dense Real-time[END_REF] is a branching-time logic which is often used to express timed properties. However, T ctl properties are not preserved by the DS timed τ -simulation. Indeed, even in the untimed case, simulation relations can not handle the preservation of branching-time properties. This kind of properties gives the possibility to add existential or universal quantifiers in the formulas. In particular, properties including existential quantifications, such as reachability properties, are not preserved (note that each M itl formula is implicitly preceded by a universal quantification, meaning that the property must hold on all runs). One often need to use bisimulation relations to ensure the preservation of such properties, but they are not appropriate to formalize incremental modeling, and thus, integration of components.

Checking the simulations

To check the DS timed τ -simulation, we developped the tool Vesta3 . The structure of the tool was guided by the structure of the tool Open-Kronos [START_REF] Tripakis | The analysis of timed systems in practice[END_REF], allowing an easy connection to the Open-Caesar platform [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation and Testing[END_REF]. It takes as input two TA A1 and A2, where A2 represents the integration of A1 in an environment E, i.e. A1||E. The tool performs a joint on-the-fly depth-first search on symbolic graphs representing the two TA (the so-called simulation graphs [START_REF] Tripakis | The analysis of timed systems in practice[END_REF]), and checks if A2 ds A1. This verification is in O

((|Z1| + | -→1 |) × (|Z2| + | -→2 |))
, where Zi and -→i, for i = 1, 2, are respectively the set of states and transitions of the simulations graphs of each Ai. If the verification fails, the tool returns a diagnostic. This diagnostic consists in a trace of A2 containing a state which does not satisfy the relation, and the corresponding trace in A1. To check if A2 is τ -divergent, we use the tool Profounder [START_REF] Tripakis | Checking Timed Büchi Automata Emptiness Efficiently[END_REF], which can in particular detect non-zeno cycles. Thus, we use it to detect non-zeno τ -cycles first in E, then in A2 if τ -cycles are detected in E.

EXPERIMENTS

We present in this section examples on which we lead experiments to show the interest of timed τ -simulations. For each case study, the verification of the properties was achieved with the tool Kronos [START_REF] Yovine | Kronos: A verification tool for real-time systems[END_REF]. Kronos is a verification tool for timed systems which performs Tctl modelchecking [START_REF] Alur | Model-Checking in Dense Real-time[END_REF], in particular for component-based models (indeed, Kronos can compute the parallel composition of TA). Tctl is a logical formalism that allows to express branchingtime properties. It can be seen as the timed extension of the untimed logic Ctl [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF][START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF]. To our knowledge, there is no tool performing Mitl model-checking. Thus, we focused on linear-time properties that can also be expressed in Tctl to lead the verification with Kronos. The verification of the simulations was done with Vesta.

Production Cell

The production cell case study was developed by FZI (the Research Center for Information Technologies, in Karlsruhe) as part of the Korso project. The goal was to study the impact of the use of formal methods when treating industrial applications. Thus, this case study was treated in about thirty different formalisms. We treat it with timed automata, as it was in [START_REF] Burns | How to verify a safe real-time system: The application of model-checking and timed automata to the production cell case study[END_REF]. Modeling. The cell consists of six devices: a feed-belt and a deposit-belt, from which pieces to be treated arrive and are evacuated, a sensor detecting the arrival of the pieces, an elevating rotary table, a two-arms robot and a press (see Fig. 1). The sensor, on the feed-belt, detects when a piece passes in front of it and sends a signal to the robot to inform that a piece is going to be available. When the piece arrives at the end of the feed-belt, it is transfered to the table which goes up while turning until being in a position where the piece can be taken by the arm A of the robot. The robot turns 90 • so that the arm A can put down the piece on the press, where it is processed and then transported by the arm B to the deposit belt. In the following, we focus on local properties concerning the robot. Thus, let us give details about its behaviour: when a piece is available on the table, the robot picks it up and moves to the press so that its arm B is in front of the press. If there is a piece on the press, the arm B takes it, otherwise the robot goes on turning to place the arm A in front of the press to put its piece down. Next, if the arm B is full, the robot goes to the deposit belt to unload its piece (and then goes back to the table), else it goes to an intermediary position, called wait position. From this wait position, the robot can either go back to the table to pick a new piece up or to the press to get a processed piece. The cell is modeled by at least seven components, one for each device, and one or several pieces. Each component is modeled by a TA. These TA can be found in [START_REF] Burns | How to verify a safe real-time system: The application of model-checking and timed automata to the production cell case study[END_REF]. The complete model is obtained by making the parallel composition of all these components. The timing constraints of the plant are shown in Fig. 2. We give in Fig. 3 Verification. To ensure that the modeling is correct, there are several properties to check. We focus on the local properties of the components, and in particular on the local properties concerning the robot. Here is a non-exhaustive list of dynamic properties to check on the robot component. Properties 1 and 2 are safety requirements, properties 3 and 4 are liveness requirements and properties 5 to 7 are boundedresponse requirements:

¡ ¡ ¡ ¡ ¡ ¡ ¢ ¡¢ ¡¢ ¡¢ ¡¢ ¡¢ ¡¢ £ ¡£ ¡£ ¡£ ¡£ ¡£ ¡£ ¤ ¡¤ ¡¤ ¡¤ ¡¤ ¡¤ ¡¤ ¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¡¥ ¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦ ¡¦

§ ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡ § ¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡ ¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡¡p
(1) When the robot is in wait position, its two arms are empty,

(2) The robot is not waiting in front of the table if the arm A is full,

(3) If there is a piece on arm B, the robot will eventually go to the deposit belt, (4) If there is a piece on arm A, the robot will eventually go to the press,

(5) When the robot is in front of the deposit belt, then it goes back to the table within 25 time units (t.u.) if there are no pieces on the press, (6) When the robot is in front of the deposit belt, then it goes to the wait position within 22 t.u. if there is a piece on the press, [START_REF] Burns | How to verify a safe real-time system: The application of model-checking and timed automata to the production cell case study[END_REF] When it is in wait position, either the robot goes to the press within 2 t.u. to unload it or it goes back to the table within 3 t.u. to pick a new piece.

The following liveness property concerns the correct interaction between the robot and the press :

(8) If arm A is full then the press will eventually be free.

We used two approaches to verify these properties on the plant. As a first approach, we verified the properties in a classic way, directly on the global model, with only one piece. As a result, we obtained that all the properties hold on this model of the plant. The second approach consisted in verifying the properties locally, i.e., on the robot component for properties 1 to 7, and on the composition robot||press for property 8. Here again, the verification succeeded. Next, to guarantee the preservation of these properties, first when integrating the robot with the press, then when integrating the composition robot||press with the rest of the components, we used the DS timed τ -simulation. We used our tool Vesta to check it for both cases, and obtained as a result that the verification was successful. Thus, properties are preserved. Fig. 4 gives the results of the comparison of the two approaches in terms of verification times (in seconds). We can see that, even on this small example, the second approach only needs 0,57 sec. of computation time to ensure that the properties hold on the cell, whereas the classic approach consumes 19,58 sec. Note that, in both approaches, we focused on a global system which contains only one piece. The reason is the following. First, in the case of the second approach, adding other pieces to the global system does not affect the results of the preservation. As the component piece already exists in the global system and that there are no synchronizations between the pieces, no new deadlocks can appear while adding a new piece. Indeed, the system can behave like it did with only one piece, or synchronize with the new piece. In this last case, as the environment of the pieces could synchronize with one piece without introducing deadlocks, then it will synchronize with the new pieces in the same way, thus without introducing deadlocks. On the other hand, in the first approach, adding pieces considerably increase the computation time for the verification of liveness or bounded-response properties. Indeed, even with few pieces, the memory needed to perform classic verification of such properties is too large for the verification to be run to completion.

CSMA/CD protocol

The CSMA/CD protocol (Carrier Sense, Multiple Access with Collision Detection protocol) [START_REF] Nicollin | Compiling real-time specifications into extended automata[END_REF] is used in broadcast networks with a single channel, to which many stations try to access. The protocol solves the problem of how to assign the use of the channel to one of the stations and allows to detect collisions when two stations try to send data simultaneously.

Modeling. The protocol works as follows: a station tries to send a data. If the channel is busy, it waits some amount of time and then retries to send. Otherwise, it begins to send its data. If two or more stations begin to send a data simultaneously, and thus a collision arises, these stations detect the collision and wait some amount of time to begin retransmitting the data. At least two TA are used to model the protocol: one per station, called sender, and a medium. These TA are shown in Fig. 5. Transitions cdi represent a collision detection by the i th sender, and cdM models this detection by the medium. The complete model of the protocol can contain several senders. For n senders, the synchronizations are the following: for a ∈ {begin, busy, end}, there is a synchronized transition ai||aM4 , for i ∈ [1..n]. Moreover, the cd transitions of each TA are synchronized, i.e., in the parallel composition, there is a transition cdM ||cd1|| • • • ||cdn.

Verification. A main property of the protocol is that whatever the number of stations, if a collision occurs between two stations i and j, i = j, both detect it within 26 t.u. This is a bounded-response property, written in Mitl by:

(transm i ∧ transm j ⇒ 3 ≤26 (coll detected i ∧ coll detected j )).
This property holds in the case of a modeling with only two senders S1 and S2. The verification with Kronos takes less than 0.001 seconds of computation time. We want to ensure that adding other senders does not alter the result of the verification. That is, we want that, with a number n > 2 of senders, if S1 and S2 transmit their data simultaneously, they still detect the collision. To preserve this boundedliveness property, we have to check that

S1||S2||S3|| • • • ||Sn||M edium ds S1||S2||M edium.
As the senders Si are not τ -divergent, and with Proposition 1, we only have to check that the addition of S3, • • • , Sn does not add deadlocks to S1||S2||M edium. As in the production cell example, there already exist two senders in the system. Thus, when adding a new sender, the synchronizations of this sender with the medium (actions begin, end and busy) can take place as they did with only two senders. Thus, no deadlocks can be introduced by these synchronizations. The main difference with the production cell example is that there exists synchronizations between all the components of the system, i.e., all the senders and the medium (action cd ). That is, when two senders detect a collision and try to take action cd between the locations transmi and coll detectedi, all other senders must allow them to detect the collision and thus, must allow them to

cd i cd i , {x i } {x i } {x i } begin i , cd i {x i } cd i , send i , {x i } x i = 782, end i , {x i } busy i , {x i } x i ≤ 782 x i ≤ 52 init i coll detected i transm i ready to send i end M , {x M } x M < 26 x M ≤ 26 x M ≥ 26 busy M init M transm M coll detected M begin M , {x M } begin M , {x M } cd M , {x M } x M ≤ 26 x i = 0 retry i ,
Figure 5: Timed automata for the i th sender and the medium of the CSMA/CD protocol take this transition. If not, a new deadlock occurs, since the synchronization can not take place, whereas it could be taken with two senders. However, we see that, at each location of the TA of the senders, the transition cd appears. This means that whenever a collision must be detected by two senders (i.e., taking transition cd between the locations transmi and coll detectedi ), the other senders also have the possibility to take a transition cd, allowing the two first senders to detect the collision. No deadlocks can appear while adding new senders, and thus, the property is preserved whatever the number of senders may be. We compared our approach with a classic verification approach, and tried to verify this property, for instance, for two senders S1 and S2, using the tool Kronos:

• Up to six senders (S1 to S6), the property can be checked successfully. The computation times for the verification changed from less than 0,5 seconds (three senders) to more than 57 minutes (six senders). These computations times take into account the time consumed to make the parallel composition of all the components and the verification time. Note that, in the last case, the verification time takes about 30 seconds, while the construction of the composition takes almost 57 minutes.

• For seven senders or more, the construction of the TA resulting of the parallel composition of all the components takes a considerably long time. For instance, we aborted the construction for seven senders after ten hours of computation without results. Thus, as the composition could not be obtained, it was impossible to perform the verification of the property.

CONCLUSION AND FUTURE WORKS

We aimed at treating the problem of the verification of linear-time properties, expressed in Mitl, of timed systems. We considered timed systems modeled in a compositional framework, and focused on the verification of local properties of the components.

In [START_REF] Bellegarde | On the contribution of a τ -simulation in the incremental modeling of timed systems[END_REF], we proposed to use timed τ -simulations as a way to verify these properties at a lower cost. The main thesis is that a local linear property can be checked only on the component it concerns, instead of on the complete composed system, and that the preservation of the property when integrating the component in its environment can be checked by means of timed τ -simulation relations. More precisely, we defined two such relations: a timed τ -simulation handling the preservation of linear safety properties, and a divergencesensitive and stability-respecting timed τ -simulation for the preservation of all Mitl properties, in particular liveness properties.

In this paper, we studied the impact in practice of this methodology. We applied it to two timed systems, and compared the results with the ones obtained by a direct verification on the complete system. It turns out that, in terms of computation times, the methodology appears to be more efficient. Moreover, both examples show the interest of the methodology when a system S is susceptible to include an indeterminate number n of components Ci,i=1..n of the same "kind", i.e., S = E||C1|| • • • ||Cn. In this case, we say that S has n as a parameter. For instance, the parameter of the production cell is the number of pieces on the cell, while in the CSMA/CD protocol, it is the number of senders. In such a parametrized system, the interesting cases are when the verification can be performed with a small fixed number l of such components, that is S l = E||C1|| • • • ||C l , implying the preservation of the properties on Sm = E||C1|| • • • ||Cm, ∀m ≥ l, under some simple conditions. As the parallel composition is compatible with the timed τ -simulation, it is enough that the conditions ensure that adding the Cis does not introduce any deadlocks. For instance, for the production cell example, the condition is that there are no synchronizations between the pieces. Thus, an interesting work is to determine such simple conditions.

Another work direction would be to study the compatibility of the timed τ -simulations with other composition operators, in particular those preserving deadlock-freedom, such as the one presented in [START_REF] Bornot | Modeling Urgency in Timed Systems[END_REF]. Indeed, this analysis would allow to evaluate the interest of the methodology we propose in a more general framework, i.e., also for systems using composition paradigms which differ from the classic parallel composition one.

Proposition 1 .Proposition 2 .Theorem 1 .

 121 Let A, B, C and D be TA. Then, we have the following: 1. A||B A, 2. if A B then A||C B||C, 3. if A B and C D then A||C B||D. Consider two TA A and B s.t. some actions of B are renamed by τ . If B is not τ -divergent, then neither is A||B. Let ϕ be a M itl property, A and B be TA. If A |= ϕ and B ds A, then B |= ϕ.

Figure 1 :

 1 Figure 1: The Production Cell

Figure 3 :

 3 Figure 3: Size of the simulation graphs of each component of the production cell

  the size, in terms of number of states and transitions, of the simulation graphs of each component.

	Device	Description			Time
	Robot	moves to press			5
	Robot	turns 90 •			15
	Robot	moves to deposit belt		5
	Robot	from deposit belt to table		25
	Robot	from deposit belt to wait pos.	22
	Robot	from press to wait pos.		17
	Robot	from wait pos. to table		3
	Robot	from wait pos. to press		2
	Robot	at wait pos.			2
	Feed Belt	piece moves to sensor		3
	Feed Belt	piece moves to table		1
	Table	raises and turns			2
	Table	returns and turns		2
	Press	presses a piece			22-25
	Press	ready for a new piece		18-20
	Deposit Belt evacuates a piece		4
	Figure 2: Timing constraints for the production cell
	Component	Robot	Press	Feed belt		Dep. Belt
	States/Trans.	39/40	7/7	6/6		4/4
	Component	Table	Sensor	Piece	Complete Model
	States/Trans.	6/6	2/2	7/7		1655/2395

In the rest of the paper, we directly call these states, the states of A, instead of the states of the semantic graph of A.

Note that, although deadlock-freedom properties can be classified as safety properties, we do not consider them like this, but as a separate class of properties. Thus, this kind of properties are not preserved by the timed τ -simulation.

available at: http://lifc.univ-fcomte.fr/∼oudot/VeSTA

Note that, for more simplicity, we extend here the notation || initially defined on timed automata, to transitions. Thus, a||b denotes the transition resulting of the synchronization of transitions a and b.


E Piron

; D Miclet

; S Villette

CEMIB: an innovative bench for spreader eco-design

Keywords: Bench, Centrifugal spreading, Fertiliser, Optimisation

This paper presents the CEMIB device developed by the Cemagref as a global tool to boost innovations, as well for spreader developments as for fertilisers one. The new bench method is shortly described and the advantages regarding the traditional EN13739 standard method are highlighted. Technical advantages to use the 3D spread pattern knowledge the CEMIB provides are illustrated regarding different real problems, gradually complex, for which manufacturer are commonly faced as soon as they need to improve or develop new spreader technologies or new fertiliser formulations. Then, the greater part of the paper is organise to explain some computed tools which have been developed by the Cemagref to value the most as possible information enclosed in the 3D spread pattern. The CEMIB global offer is really well positioned in the eco-design context: (i) practically, testing facilities required are around 10 times less expensive than transverse classical ones, (ii) it allows time and fertilisers saving during innovated phases of fertiliser and spreader developments, i.e. real tests can be replaced by computing simulations, and (iii) it allows analyses which should not be possible, in any case, using only the transverse spread pattern.

Introduction

Most of the time in Europe, mineral fertiliser application is an agricultural operation carried out using centrifugal spreaders. Relatively small, simple, and of low cost, they are also attractive because of their capacity to reach high spreading efficiency (important working widths, high tractor speed …). Nevertheless, the spreading application uniformity is strongly dependant to numerous variable, for example the settings chosen on the spreader, or the physical fertiliser properties. Relatively complex to modelize, knowledge about the global comportment of the fertiliser granules during the spreading process, i.e. from the hopper to the ground, passing throw the vanes acceleration, are not so important and precise. In any case they are not sufficient today to design, optimise, and draw out setting tables. That's the main reason why test benches are very often used. Numerous methods using collection tray are available throughout the world and are described in different standards. A lot of them use a row of collection trays aligned perpendicularly to the displacement axis of the spreader. It's in particular the case of the European standard EN 13739. The way this test is performed induces an important practical drawback nowadays, because of the reached spreading performances. For the most powerful couples spreaders / fertilisers, the spread covered area on the ground is around 85m*50m, inducing test facility dimensions around 90m*60m, considering the longitudinal needed displacement to perform the tests. Such test benches are too expensive, as well for the building or to maintain them. Mainly performed to establish setting tables, the final goal of these tests is to obtain the variation coefficient (CV) curve from which the best working widths can be extracted: after the different spreading runs, all of the global collected quantities are weighed, allowing establishing the transverse distribution curve; this last one is after used to compute the needed transverse overlapped distributions, and the linked CV values. Several tests are also necessary to correctly work out setting tables because the method generates results hard to extrapolate: the transverse curve integrates the tractor displacement, and isn't representative of the real physical ground distribution of fertiliser granules. Computed predictions under setting variations are also impossible to develop.

A new test bench device, the CEMIB, as been drowned by the Cemagref and is used from 2006. Of a considerable practical interest, it also provides results from which many calculations can be done, simplifying the design of the spreaders, and also setting tables working out. After a short presentation of the CEMIB device and the results it allows to obtain, technical advantages of the 3D distribution knowledge are explained. Then, practical computer tools developed by the Cemagref are described, of particular interest to provide new (eco) conception methods, or increase setting table robustness.

CEMIB: method description and provided results

As two main drawbacks were identify when using the traditional EN13739 standard method, i.e. practical limitation due to the needed test hall size, and technical limitation due to the integrative result it provides, the challenge was to propose a new method which should solve these two particular points. One of the best devices to map a spread pattern should be to place a ground of sensor every where in the spread covered area! As it is evident this way should be technically, practically and economically unrealistic, a sample method becomes obligatory. A first way to sample the spread pattern is the one described for example in the EN13739 standard: the row of collection tray is lined perpendicularly to the travel axis of the spreader. Even if it is possible to obtain the 3D spread pattern by this way, using continuous measurements of all the weighing sensors and of a specific other one for the longitudinal position, this method presents practical limitations, described in the first paragraph. A second way consists in a radial measurement principle: the spread pattern is sampled angular sectors after angular sectors, but in a continuous way. It's this device which has been adopted and patented by the Cemagref; the name chosen is CEMIB (short for CEmagref MIneral Bench). A fixed line of trays, equipped with sensors, represents the "sensible" part of the device, which will sample the spread pattern. At one of the extremity of these row of trays is placed the spreader to test, coupled to a rotary carrier. The angular velocity of this one can be set between 0,5 and 8°.s -1 , depending to the flow rate. During the test, thanks to the carrier, the spreader revolves around itself around an axis not far from the disc axis (Fig. 1), in such a way that each point of the spread pattern passes the collection trays vertically at a certain point (Fig. 2). The 3D spread pattern obtained (Fig. 2) is a fertiliser density matrix on the ground, obtained after mathematic calculations, in particular a spatial interpolation which allows going from densities expressed as polar coordinates to densities expressed as Cartesian one. From this fertiliser spread pattern, the transverse distribution, explained in the EN13739 standard, can be obtained using a summation column by column (Fig. 3). All the following calculation described by the standard can also be computed (overlapped curve, CV curve, global rate applied …), as well for main field applications as for border applications.

In a very small test hall facility (40m*10m are enough), this device allows assessing the same results as the one obtained using the standard method, and in addition, the 3D spread pattern is measured, on which many interesting calculation can be work out (see paragraph 3). From 2005 when it was developed and presented [START_REF] Piron | Centrifugal fertiliser spreaders: a new method for their evaluation and testing[END_REF], many complementary comparative and round-robin tests have been carried out between different test facilities in Europe, using EN13739 standard. All the results show a global valid correlation between both methods. In addition, some experimental and scientific works have been carried out in order to prove the validity of this evaluation device in any using case. On an economical point of view, such a solution presents a very important upside because the total costs induced to build the test facility is around 10 times less important than for a transverse test bench as described in the EN13739. Always in opposition to the transverse bench, running costs are very low, because of the test hall area and volume difference (between 10 and 15 times less important) and all the linked costs as air conditioning and heating, time to clean …

Technical advantages to use 3D spread pattern

The different spreader factories used many different way to set there spreader. Variation of horizontal vanes inclinations on the disc or of there length, variation of the global spreader horizontality in both axis longitudinal or transversal, variation of the fertiliser drop zone position, of the disc angular velocity, … More and more, with great working widths, a correct homogeneity distribution is obtained using 2 or 3 different of these settings on the same spreader, then it becomes very hard to go fast to the correct choice. The 3D spread pattern knowledge is in these cases of great interest, and the strongest results are obtained using the 3D spread pattern measured from only one disc. The values obtained do enable phenomena to be explained or assessed, and therefore it is possible to predict some reactions, to modelize …

Test comparison one disc spread pattern vs both disc spread pattern

Using a spreader equipped with 2 equivalent discs, the right disc (RD) and the left one (LD), 3 successive tests are carried out with identical settings and the same fertiliser. The feeding of the discs is different for each test: RD feeding only, then LD feeding only, and finally both discs feeding together (RD+LD). Both spread pattern RD and LD are expressed in their respective disc axis repair while the RD+LD spread pattern is expressed in the spreader repair, i.e. the X value "0" is in this case at the middle of the 2 discs. RD and LD spread pattern are added together after repair changing, and the result is compared to RD+LD spread pattern. This comparison is showed on the Fig. 4. It can be seen that, except differences due to experimental errors, the results are the same, as well for the transverse curve, as for the CV one. As soon as the goals of the tests is the spreading process comprehension, or specific spreading pieces design, or setting tables work out, the best way is to measure with only one disc. Since the spreading process is isolated, extrapolations aren't by this way necessary.

Tools developed to increase spreading development efficiency

Regarding the setting to be used, predictions of results are more or less easy to obtain. For many of them, physical models are required in addition to the 3D distribution in order to predict the distribution using another setting. That's the case for example for the spreader inclination. Horizontality angle of the vane on the disc required to go upper in the understanding of the work of each vane before to be able to predict anything. Anyway, it's possible using more or less elaborate strategies to reach the objectives.

Two settings are more directly useful for spreading predictions: the angular variation of fertiliser drop zone on the disc, or the variation of the disc angular velocity. For the first one, the fertiliser is dropped with more or less the same deposition shape on the disc, but with different possible angular positions around the centre of the disc, in regard with the spreader travel axis. For each possible setting index, the way the fertiliser granules are accelerated by the vanes is then exactly the same (i.e. the acceleration time, the relative mass angular distribution, the absolute granules velocities …). The only spreading consequence induced is the absolute angular rotation of the spread pattern according to the absolute drop zone angle.

The knowledge of the mechanical building characteristics of a spreader allows in this case reducing a lot the number of real bench tests to reach a working width objective, using initially only 1 real measurement (Fig. 5). In this example, a first test (Initial test (a)) shows a setting index with which the working width is too large regarding the wanted objective: optimum working width can be seen equal to 30m, with a 10% CV value. Taking this test result in the computer simulator, 7,5° of rotation angle is found to be optimum to work at 24m (part (b) on the Fig. 5). The fertiliser density difference (b)-(a) shows this 7,5° global rotation (red and yellow points mean densities higher than 0, and blue points correspond to densities lower than 0. After modifying the spreader setting according to this objective of rotation, the second test is performed (c). A first comparison between prediction and reality is obtained computing the fertiliser density difference (c)-(b): the red, yellow and blue points are regularly laid-out everywhere which means a global equivalence of both 3D distributions. The second comparison is obtained regarding the matched correspondence between transverse simulated curves and real measured one. The CV calculations confirm this equivalence since both curves are exactly the same, in particular with an identical CV value of 2% for the best 24m working width.

Fig. 5: Presentation of the working progress of the comparison tool.

The developed tool allows selecting one or two different 3D distributions for each spread pattern to compare, in order to associate them together with more or less rotation shifts, flow rates, fertiliser angular velocities …, and decide the way to follow for vane or disc design … Identical ways of simulation are available on the tool developed, in particular to predict the results using different disc angular velocities. The other spreader settings consequences and there implementation to predict results are in development.

Tools developed to automate setting table establishment

This computer simulation way has been completed to assess an automatic research of the best settings for one fertiliser, spread with a specific spreader, on all the realistic working widths, and using only one test (Fig. 6). Using a spread pattern measured and different parameters as the setting index chosen for the test, the mechanical characteristics of the spreader, an experimental law giving the projection distance in relation with the disc angular velocity …, the developed computer tool calculates all the possible spread patterns which can be obtained with the available spreader settings (Fig. 6-a). It can also compute each corresponding transverse distributions (Fig. 6-b) and their associated CV curves (Fig. 6-c). These last ones are stored in a CV matrix results (Fig. 6-d), where spreader settings (Y axis) can be crossed with the working widths (X axis) to find all the predicted CV values (Z axis). This pool of "best settings" is reported on a 2D graph (b) which directly show the setting to choose (Y axis) regarding the wanted working width (X axis). Two different types of markers are represented: circle filled marker, and squared filled markers. If the marker is a circle, pop upped with a square, it means the best setting found to spread at the considered working width is the absolute best setting in the total matrix, but also a local minimum of one of the CV curve results (case which occurred for working width between 17 and 23m on the figure).

If both circle and squared markers are dissociated, it means the traditional way to determine the best setting does not give the absolute best possible result. It's the case for 28m in the example where 3 different settings can be found as local minimum CV, but where another setting (not a local minimum) allows to reach a best result.

Fig. 7: Illustration of the results obtained using automatic research of the predicted homogeneity distributions (a), and of the extraction of the valuable information to be used by the spreader factory (b).

In addition of this improvement for the setting research process, other criteria are automatically computed and indicated to help factories to draw setting tables. For example, the ratio Tw Ww . 2 (Ww is the working width, and Tw is the Throwing width) is drawn for 7 different values between 0,55 and 1,45. It's an indication for the technician to place the spreading pattern area in correlation with the working width. The value

1 . 2 = Tw
Ww means a perfect overlapping will be obtained using this pattern to spread this working width. Higher or lower values mean respectively the pattern is too small or too large regarding the working width. By this way, setting tables can be easily simplified and adjusted to perform the best objectives. The CV value is also not the only criteria to be used, but robustness of the results can also be predicted and associated to reach more accurate results. The true colored area on the Fig. 7-a and 7-b outlines the best setting area, issued from a combined analyse based on a traditional homogeneity analyse and on the Tw Ww . 2 criteria. Two different analyses can be performed around the robustness side, in order to express the risk to induce local important under or over applications when the tractor trajectory becomes different from the wanted one: -The bigger is the working width, the narrower is the correct possible setting range allowing working with CV lower than 15% (analyse along Y axis). Working with this couple fertiliser / spreader at such important working widths can be done correctly with a very short range of working width. In this case, a very small modification with the fertiliser (humidity …) can induce important default applications. This is not the case for lower working widths, where correct results are obtained with a relative large setting range.

-For each spreader setting, the range of possible working widths presents variability. Even if the results show some interesting working possibilities between 16 and 25m (CV < 5%), a detailed analyse of the 3D graph shows the most robust working width for this example is around 20m and setting 4 because CVs stay less important than 15% in a range of 9m between 14 and 23m (analyse around X axis). For a working width of 17m with setting 1.5, the range becomes narrower (around 5m between 14 and 19m), and for a working width of 25m, the CV deterioration becomes very important as soon as a variation of 1m occurred (26m for example).

Utility to determine a fertiliser spreading ability

As it has been shown in the previous paragraph, different information have to be crossed together to draw out setting tables because of the number of available settings … Draw out a fertiliser classification is in the same way a difficult challenge because it must be based on spreading abilities, which are closely dependant to spreader performances one. The tool presented in the previous paragraph is an answer to this problem because it allows a complete comparison between different fertiliser, using only 1 test bench measurement for every product to evaluate. The Fig. 8 presents the example of two different fertilisers tested with the same spreader and for which both transverse spread pattern presented are quite equivalent for a 28m working width: fertiliser (1) allows a 3,9% CV homogeneity, and fertiliser (2) 2,4%. The results obtained using the optimizing tool presented before show higher performances capabilities for fertiliser (1) than for fertiliser (2). Its best range of working width is around 31m while it is 25m for fertiliser (2), and the spreading working width limit using 10% of CV as a maximum accepted heterogeneity reaches 39m for fertiliser (1) while it reaches only 33m for fertiliser (2). Moreover, this type of tests can be carried out, in the same conditions, but at different time period, and it's a very good way for fertiliser manufacturer to verify regularly the fertiliser improvement on a spreading point of view. It's also a really efficient method to have a quick overview of the different spreading characteristics of many different fertilisers.

Conclusion

This paper shows important new opportunities for developing centrifugal spreader and fertiliser performances. First, the test bench CEMIB, developed by the Cemagref, is an economical device which provides a lot of valuable information in a very short time. The 3D spread pattern which is measured is robust, and represents strong information to start prediction calculations. As the obtained spread pattern is an experimental result, the predictions which can be calculated are very closed to the reality, at least for settings inducing direct effects as the angular drop zone variation, or the disc angular velocity.

Complementary works are on the go considering the prediction of setting effects which are less direct, as spreader inclination, vane inclination on the disc … They need to introduce complementary information as physical comportment laws in the different models, before to be in order to predict setting consequences.

A very important thing is the time consuming to compute the results, which is very small regarding the one needed to perform a real test. It can be assumed that this way of work cannot be replaced by an experimental one, because of the number of needed tests which should be induced. Complementary analyses are in particular possible as robustness criteria, which represent the base for a "risk analyse", to produce always more valuable information for the technician, the factories (spreader or fertiliser), in order to produce innovations as environmentally friendly as possible. This is possible because the developed computing tools allow establishing specific crossed gauges, using the maximum valuable knowledge content in the measurement.

Over the possibility which is given to develop environmentally friendly innovations, the device to produce these innovations (i.e. the bench and the associated tools) is in itself environmentally friendly. Globally, a lot of crossing analyses can be performed with it, which replace a indefinable number of transverse tests which should be necessary without a good measurement of the 3D spread pattern.

In continuous research development, this global tool is available for eco-design; it can be used as well by spreader manufacturers as by fertilisers ones.

Using the method, the definition of the "fertiliser spreadability" isn't a dream, but can be planned for a near future, as well as a spreader eco-evalution could be achieved.

Fig. 1 :

 1 Fig. 1: CEMIB device photograph, with a real spreader coupled for testing.

Fig. 2 :

 2 Fig. 2: General principle of operation.

Fig. 3 :

 3 Fig. 3: Transverse distribution obtaining from spatial distribution.

Fig. 4 :

 4 Fig. 4: Comparison of results obtained measuring spread pattern of each disc separately then add them together, with the spread pattern obtained using both discs simultaneously.

Fig. 6 :

 6 Fig. 6: Illustration of the computed progress used by the optimization tool to predict as well as possible spreading homogeneities, i.e. CV values, regarding all the available settings, and a range of possible working widths, using only one real spreading measurement.

Fig. 8 :

 8 Fig. 8: Illustration of the comparison of 2 fertiliser spreading abilities obtained using the optimization developed tool.

Author-produced version of the paper presented at AGENG 2020 Conference, Septembre 6-8 2010, Clermont-Ferrand, France