J Cebeiro

M K Nguyen

M A Morvidone
email: mmorvidone@unsam.edu.ar

A Noumowé

New "improved" Compton scatter tomography modality for investigative imaging of one-sided large objects

Keywords: Radon transforms, gamma-ray imaging, Compton scattering, Radon transform

In an effort to promote Compton scatter tomography (CST) as an adequate modality for imaging the inner parts of large objects limited in a half-space of R 3

AQ1

, we show that the standard CST can be 'improved' in some particular sense by 'doubling' the scanning mechanism. To this end, one needs to record for each position of a detector the scattered flux densities at two energies of scattered radiation, instead of one. Curiously, thanks to geometric inversion, this 'double' scanning may be converted into a transmission scanning on an apparent object, not along a straight line path as usual, but along a folded line in the shape of a V -line path. It has been proved that this V -line transmission scanning admits a well-defined reconstruction procedure. Therefore, the proposed CST with 'double' scanning, which solves the above imaging inverse problem, shows an 'improved' reconstructed image as compared to the standard one. We present theoretical arguments to support this claim as well as numerical simulations to illustrate its working and its viability AQ2 .

Introduction

Imaging technology has brought tremendous progress in medical diagnostics as well as in many other fields such as non-destructive surveillance and control, underground exploration, astronomy, homeland security, etc. In most of the cases, objects of interest are of small sizes and imaging equipment blue is designed to fit these object sizes. For very 5 large objects, in particular massive ones but presenting a very large flat surface, there is a need of special imaging devices which can accommodate such structures. Existing imaging systems are based on acoustic waves and electromagnetic waves propagation properties.

One may cite e.g. Sonar imaging or Ground Radar Imaging, which deliver undersea images of sunken ships or underground images of buried pipes, etc. Image reconstruction is based 10 mostly on information given by backscattered waves and this procedure requires ad-hoc algorithms. Moreover, sound and electromagnetic waves have limited penetration in dense matter. To reveal finer structure there is a need to penetrate further in dense matter with shorter GIPE 1281920 18-1-2017 Initial CE:YS QA:CL wavelengths. This is why ionizing radiation is appropriate for probing the inner structure of dense matter, which is proper to industrial objects as well as rocky medium or concrete. The interest in using ionizing radiation to explore the inner structure of objects has been proposed a long time ago and has known in the recent years a renewed interest. Ionizing radiation is in fact the ideal tool to prospect the inner structure of matter because of its strong penetrating property. However, information on the probed object matter can only be retrieved if one manages to record the outgoing radiation, which has undergone an interaction inside matter. Of course one may register backscattered for acoustic as well as for electromagnetic waves. Several concepts for gathering backscattered radiation have been proposed in the past, see e.g. [START_REF] Shengli | EGS4 simulation of Compton scattering for nondestructive testing[END_REF][START_REF] Gerl | Gamma-ray imaging exploiting the Compton effect[END_REF][START_REF] Abdul-Majid | Imaging corrosion under insulation by gamma ray backscattering method[END_REF]

AQ3

. Here there is a possibility of recover scattered waves which are far more versatile. In particular in the energy range around 150 keV, the only relevant radiation interaction is Compton scattering. This is why the concept of Compton imaging was initiated and developed in last few decades. We shall not recall the early steps of Compton imaging and refer the reader to [START_REF] Truong | Recent developments in Compton scatter tomography: theory and numerical simulations[END_REF], but give some references on recent interests in Compton imaging for historical object research and conservation [START_REF] Harding | Compton scatter imaging: a tool for historical exploration[END_REF], land mine detection [START_REF] Hussein | On the use of radiation scattering for the detection of landmines[END_REF], agricultural measurements [START_REF] Cruvinel | Compton scattering tomography for agricultural measurements[END_REF], battery functioning [START_REF] Itou | Compton scattering imaging of a working battery using synchrotron high-energy X-rays[END_REF], nondestructive testing [START_REF] Lange | X-ray Compton tomography[END_REF] and soil studies [START_REF] Adejumo | Developing a Compton scattering tomography system for soil studies: theory[END_REF].

One of the main advantages of Compton scattering imaging over X-ray transmission imaging is its high sensitivity to the local electron density, even for materials with high X-ray absorption coefficients. This is because Compton scattering imaging measures the X-ray intensity from a local probing volume, while X-ray transmission imaging records the total absorption along the X-ray path. This is very beneficial for large objects.

To this end, Compton scatter tomography (CST) has been advocated for investigating the hidden structure of one-sided large objects [11,[START_REF] Norton | Compton scattering tomography[END_REF], when this investigation is done slice by slice on this object. However, it has not yet emerged as a widely used modality in this field mainly due to poor sensitivity of image reconstruction. In this work, we reanalyse the properties of this classical CST modality to explain its functioning principle and then propose a new modality which, in principle exhibits an enhanced image reconstruction, potentially more efficiency in the study of 'beyond the wall' structure of large one-sided objects or half-space extended medium. In CST, data acquisition can be done by a detector located on the same side of the object under investigation: this is not the case in conventional transmission tomography. CST is expected to give high contrast, high spatial resolution and stoichiometric independent images of two-dimensional slices of objects. CST is appropriate for imaging continuing flow of liquids in pipes, solid propellant rocket engines, ships hulls, aircraft parts, large castings, etc. in particular when the need of obtaining access to both sides of the structure is denied. This is really advantageous at a time when new generation of position-and energy-sensitive radiation detectors have appeared. Throughout the years, there has been substantial progress in development of CST modalities [START_REF] Truong | Recent developments in Compton scatter tomography: theory and numerical simulations[END_REF]. However in this work, we shall concentrate on a new modality, which was proposed recently [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF] but not assessed numerically as far as feasibility and realizability are concerned. The purpose of this paper is to close this gap by giving detailed computation on image formation as well as reconstruction and image quality evaluation.

As always, an imaging modality relies on a mathematical tool which supports its image formation and provides a way to reconstruct an image. In conventional computed tomography, this role was played by the well-known classical Radon transform. For CST, it has been established that a variety of Radon transforms on circular arcs forms the support for image formation when higher order radiation scattering is not taken into account. Moreover, these generalized Radon transforms are shown to be invertible paving the way to image reconstruction in CST. Here we shall investigate the imaging capabilities of a newly proposed Radon transform, which is defined on a pair of circular arcs (instead of a single circular arc), introduced in [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF]. Its invertibility is shown to be transferred to the invertibility of the so-called Radon transforms on V -lines by geometric inversion of the coordinate variables. This type of transfer has been known for a long time for the Radon transform on circles intersecting a fixed point in a plane, which become simply the classical Radon transform on straight lines of the same plane [14]. The V -line is the geometric object which consists of two half-lines ending at a vertex-point on an horizontal axis and disposed symmetrically around the vertical axis at the vertex-point and making a variable angle with it. We adopt this terminology in order to distinguish it from the so-called Radon transform on broken lines introduced by [START_REF] Florescu | Inversion formulas for the broken-ray Radon transform[END_REF] AQ4 , which is defined on the set of geometric figures made of two half-lines making a fixed angle between them and of arbitrary location and orientation in the plane.

The paper is structured as follows. The fundamentals of Compton scattering tomography, in particular the classical CST modality proposed by S. J. Norton in 1994 [START_REF] Norton | Compton scattering tomography[END_REF] are reviewed in some details, in which we recall the Compton scattering phenomena and its properties. We also recast the conventional CST modality of S. J. Norton in the framework of the Radon transform on half-lines and describe its solution, which solves the inverse problem of CST imaging. The next Section 3 concerns the new CST modality. We show how the scanning on a pair of supplementary circular arcs is beneficial for imaging an object via conversion into a transmission scanning problem on a V -line. We also demonstrate theoretically why the reconstruction scheme yields an 'improved' result as compared to the standard one. A major point is the introduction of the inversion procedure as a filtered back projection (FBP), which is widely used in conventional tomography and provides an elegant way to deal with divergencies in coordinate space. A working algorithm is given to show the working of the numerical simulations in Section 5. The numerical simulations results, with a careful analysis of image quality under different working conditions, illustrate the feasibility and viability of this new CST imaging modality. The paper ends with a conclusion and some future directions of investigation.

Compton scattering tomography: a review

Compton scattering tomography (CST) was introduced in the early 80s, see e.g. [START_REF] Gautam | Compton interaction tomography[END_REF], but it was S. J. Norton who gave a full theoretical treatment in 1994 [START_REF] Norton | Compton scattering tomography[END_REF]. A threedimensional object is illuminated by a penetrating radiation external point source S of calibrated intensity. Since tomography considers only one planar slice of this object, this point source will be placed between two collimator plates, which are parallel to the slice and separated by a small distance to restrict the emitted radiation to a plane in fact a thin slice, before it irradiates the object situated beyond these collimator plates. First-order scattered radiation of specific energy is registered by a point detector D placed at a distance ξ from the source, also located in between the collimator plates. The detector is assumed to be highly energy sensitive and of sufficiently small size (because the intensity of scattered radiation is low), in order to be able to generate a very large amount of data. In the present work, radiation attenuation is not taken into account as we concentrate on the working principle. It is expected that radiation attenuation is important before and after scattering inside matter and should be corrected. However, it is known that including attenuation in such processes usually does not allow an analytic solution. Even in the case of simple emission imaging the inclusion of arbitrary attenuation was only exactly solved in 2002 [START_REF] Novikov | An inversion formula for the attenuated X-ray transform[END_REF]. However, a constant attenuation may be manageable, a kind of pre-correction may be performed such as in [START_REF] Rigaud | Novel numerical inversions of two circular-arc radon transforms in Compton scattering tomography[END_REF] and shall be deferred to a future investigation. The claim of CST is that the totality of such measurement is sufficient to reconstruct an image of the inner part of the object, which consists of the electron density of its interior. Figure 1 summarizes the working of this modality. As penetrating radiation consists of X-(or -gamma) rays, an object, represented by the shaded area is subjected to the illuminating radiation carrying an original energy E 0 of an isotropic source S placed at the origin of a Cartesian coordinate system. A point-like detector at site D, at a distance ξ from S, with a flat collimator under it to allow only the recording of scattered radiation of scattered energy E(ω) (and not of energy E(π -ω)), moves on the axis SD and registers a radiation flux density at a single Compton scattered energy E(ω), which is related to the scattering angle ω by the so-called Compton relation

E(ω) = E 0 1 + E 0 mc 2 (1 -cos ω) , ( 1
)
where mc 2 represents the energy of the electron at rest (511 keV). Inspection shows that the totality of radiation flux density at a detecting site D situated at a distance ξ from S is due to all scattering sites M located on a circular arc starting from S and ending at D, subtending an inscribed angle (π -ω), which is constant for each measurement. The kinematics of Compton scattering (see Figure 2) is encoded in the Klein-Nishina differential cross section dσ d = πr 2 e P(ω), where σ is the Compton scattering cross-section, r e is the classical electron radius and P(ω) is the Klein-Nishina probability to be scattered in the solid angle . The expression of P(ω) is given in [19].

Let us introduce a Cartesian coordinate system xSy centred at S with D on the x-axis. The registered scattered radiation flux density at D is essentially the integral of the electric charge density of the object on a circular arc, which has a radius ρ = ξ 2 sin ω and a centre at ξ 2 , ξ 2τ , where τ = tan ω. Let f (x, y) be this electric charge density. To preserve the clarity of the exposition, we shall neglect propagation photometric effects and radiation attenuation in matter, as stated before. Let us assume that the source S emits isotropically radiation of energy E 0 and that the point detector D has also spherical symmetry. The amount of radiation registered at D is then of the form

R C f (ξ , ω) = K(ω) C f (x, y) ds C , ( 3 )
where the ω-dependent factor K(ω) contains besides the Klein-Nishina probability P(ω) all other kinematic factors of the scattering at site M = (x, y), C is the circular arc SMD and its arc element ds C . So the quantity R C f (ξ , ω)/K(ω), from now on called the renormalized data, is the integral of an unknown function f (x, y) on a set of circular arcs subtending an inscribed angle (π -ω) starting at the source point S and ending at the detection point D.

It is a function of (ξ , ω) ∈ R × [0, π].
The problem is now how to reconstruct the electric charge density f (x, y) from the set of measurements R C f (ξ , ω). There are several possible approaches. S. J. Norton has argued that if the object is 'above' the axis Sx, there is no harm to carry out the integration on the full circle, which is of variable centre in the plane but always passing through the fixed point S. R C f (ξ , ω)/K(ω) is thus the Radon transform of f (x, y) on the set of circles of the plane intersecting a fixed point S. But already in 1965, A. M. Cormack has studied such a Radon transform [14] and he has also given the corresponding inverse formula. 1 This situation is applicable whenever the object has a compact support. Numerical implementation of this procedure has been given recently in [START_REF] Rigaud | Novel numerical inversions of two circular-arc radon transforms in Compton scattering tomography[END_REF] using the so-called circular component expansion.

Recently, it has been shown in [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF] that the Radon transform of a function f (x, y) on the above circular arcs can be converted, by geometric inversion of centre S and inversion circle of radius R into a Radon transform on half-lines contained in upper half plane of the line SD, not for f (x, y) but for a modified function g R (x , y ), given by

g R (x , y ) = R 2 x 2 + y 2 f R 2 x x 2 + y 2 , R 2 y x 2 + y 2 , ( 4
)
where the transform by geometric inversion of a point M = (x, y) in the xSy plane is M = (x , y ) given by

(x , y ) = R 2 x 2 + y 2 (x, y). ( 5
)
Figure 3 shows how the circular arc SMD is converted by this geometric inversion into the half-line D M , such that

ξ = R 2 ξ , and SM = R 2 SM . ( 6
)
The circular arc SMD subtends an angle (π -ω). This arc is transformed into a half-line starting at site D at a distance ξ from S on the axis Sx. This half-line makes an angle φ = (ω -π/2) with the vertical direction. This is so because the line SNN going through the centre of the circle SMND is perpendicular to the half-line D N M . Note that in Figure 3, ξ > 0 and the scattering angle ω is chosen to be larger than π/2, hence φ is positive. The equation of the circular arc SMD, with centre at

= ( ξ 2 , ξ 2τ ) is x - ξ 2 2 + y - ξ 2τ 2 = ξ 2 sin ω
where τ = 1 τ . Let us denote the Radon transform on half-lines by R , see [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF]. Then for a function h(x , y ), its integral on the half-line of Equation ( 8) is (see Figure 4)

R h(ξ , τ ) = ∞ 0 dy 1 + τ 2 h(ξ -y τ , y ), ( 9
)
where s = SN = ξ cos φ = ξ sin ω, with (ξ , τ ) ∈ R 2 . Now by identifying the circular arc Radon data R C f (ξ , ω)/K(ω) to the data of a Radon transform on half-lines R according to

R C f (ξ , ω) K(ω) = R g R (ξ , τ ), ( 10
)
we can use the inverse formula for the Radon transform of half-lines of the plane (given in [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF]), applied to the data

R g R (ξ , τ ) to reconstruct g R (x , y ), or g R (x , y ) = - 1 2π 2 H(y ) R 2 dξ dτ √ 1 + τ 2 1 ξ -x -y τ ∂ ∂ξ R g R (ξ , τ ), ( 11
)
where H(y ) is the Heaviside function of y . f (x, y) is recovered through

f (x, y) = R 2 x 2 + y 2 g R R 2 x x 2 + y 2 , R 2 y x 2 + y 2 . ( 12
)
Note that the parameter R drops out at the end of the reconstruction of f (x, y).

New 'improved' modality for CST

In imaging science, the aim is to obtain the most appropriate imaging modality. For CST, following a recent suggestion in [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF], which consists in gathering measured data not only on one circular arc but on two circular arcs, see Figure 5, we undertake to explore the performances of this new modality. Previously, on a circular arc SMD subtending an angle (π -ω) and based on a chord SD = ξ , the integration path of the electron density has a length which can be at most equal to ωξ/ sin ω. By adding a new circular arc SND to gather data one may expect a longer integration path. In fact for reasons that become clear later, we shall use a second circular arc SND which subtends an angle ω and based on the same chord SD = ξ . Then the total integration path used for data collection will be always the full circumference of length πξ/ sin ω, which is clearly larger than ωξ/ sin ω, since 0 < ω < π. Intuitively, one may suspect that this data acquisition would be more beneficial to image reconstruction. But this must be checked.

To simplify notations, we shall denote generically the circular arc SMD (resp. SPD) by C (resp. C ) in Figure 5. So at site D, two measurements of scattered radiation at energy E(ω) and at energy E(π -ω) will be made and recorded according to

R C f (ξ , ω) = K(ω) C f (x, y) ds C , and R C f (ξ , ω) = K(π -ω) C f (x, y) ds C . ( 13
)
Note that ds C = ds C . Now if one sums up the renormalized data after division by the corresponding K(ω) and K(π -ω) factors as R CC f (ξ , ω), which is the data of a Radon transform on a pair of supplementary circular arcs CC of a function f (x, y), the problem is now how to obtain f (x, y) from this data

R C f (ξ , ω) K(ω) + R C f (ξ , π -ω) K(π -ω) = R CC f (ξ , ω), ( 1 4 )
R CC f (ξ , ω).
Following the idea of Section 2, we may apply the same geometric inversion to the pair of circular arcs SMD (or C) and SPD (or C ), each of which subtends, respectively, the angle (π -ω) and ω, see Figure 6. Each of the circular arcs will be transformed into a half-line starting at site D at a distance ξ = R 2 /ξ from S on the axis Sx. Each of these half-lines makes an angle φ = (ω -π/2) with the vertical direction. This is so because the line SNN going through the centre of the circle SMND is perpendicular to the half-line D N M . The resulting figure N D P is a so-called V -line as stated in [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF].

Thus geometric inversion turns this data into the data for a Radon transform on V -lines for the function g R (x , y ) encountered before in Equation (11). Let R V g R (ξ , τ ) be the Radon transform on V -lines of g R (x , y ). Then we may identify

R CC f (ξ , ω) = R V g R (ξ , τ ), ( 15
)
with τ = cot ω. Recall that the V -line transform of g R (x , y ) is given by

R V g R (ξ , τ ) = 1 + τ 2 ∞ 0 dy g R (ξ -y τ , y ) + g R (ξ + y τ , y ) . ( 16
)
In Figure 7, is represented the V -line on which a function is integrated and s = ξ cos φ = ξ sin ω as before.

Knowing that the Radon transform on V -lines is invertible (see [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF]), we can write down its inverse formula, in which we put the data collected from R CC , the Radon transform on double circular arcs as transformed by Equation ( 14)

-ξ | = y τ used in R V Radon transform. g R (x , y ) = - 1 2π 2 ∞ 0 dτ √ 1 + τ 2 R dξ 1 ξ -x -y τ + 1 ξ -x + y τ ∂ ∂ξ R CC f R 2 ξ , ω . ( 17
)
The electron density f (x, y) is finally recovered as before by Equation [START_REF] Norton | Compton scattering tomography[END_REF]. At this point it is natural to ask what differentiates the two CST modalities? (i.e. the one using a single scanning circular arc and the other using a pair of supplementary scanning circular arcs). Or more precisely, what differentiates their imaging integral transforms which are the Radon transforms, respectively, on one scanning circular arc and on two scanning supplementary circular arcs? To answer this question, it may be simpler to look at their geometric inverse partners, which are, respectively, the half-line Radon transform and the V -line Radon transform. These Radon transforms may be viewed as supporting apparent emission imaging problems in the upper half part of a plane (see Figure 3 in [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF] and Figure 3 in [START_REF] Truong | On new V-line Radon transforms in R2 and their inversion[END_REF]). Therefore we shall discuss the relation connecting the half-line Radon transform to the V -line Radon transform in the upper part of a plane and then extrapolate the conclusion to the two CST modalities.

A relation between the half-line Radon transform and the V-line Radon transform

We recall the essential properties of R (resp. R V ) the half-line (resp. V -line) Radon transform and refer the reader to [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF]. In this section, we use the standard Cartesian coordinate system (xOy), since the discussion is intrinsically independent of the previous sections.

Half-line Radon transform

The R transform of an integrable function f (x, y) in R 2 is defined as

R f (ξ , τ ) = 1 + τ 2 ∞ 0 dy f (ξ -yτ , y), (18)
where (ξ , τ ) ∈ R 2 . Thus R f (ξ , τ ) is a function defined in R 2 , obtained by integrating f (x, y) on the half-line of equations x = ξyτ with y > 0. Its inversion is given by the reconstruction formula (see [START_REF] Truong | New properties of the V-line Radon transforms and their imaging applications[END_REF])

f (x, y) = - 1 2π 2 H(y) R 2 dτ dξ √ 1 + τ 2 1 ξ -x -yτ ∂ ∂ξ R f (ξ , τ ). ( 19
)
This formula resembles the reconstruction formula for the standard Radon transform except for the Heaviside function H(y), which means that the only data gathered is in the upper plane. Thus, one can only reconstruct the function in the upper plane. A priori, no evident symmetry exists and no extension to the lower part of the plane is available. Only the part of f (x, y) for y > 0 is reconstructed and nothing can be said on f (x, y) for y < 0.

V-line Radon transform

The V -line Radon transform was defined originally as the integral transform which assigns to a function f (x, y) its integral on a standing V -line with vertex on the Ox-axis and opening angle ω. This V -line figure is in fact a two-dimensional version of a circular cone with vertical axis in R 3 . Recently many variants of this so-called V -line Radon transform have appeared in the literature, see [START_REF] Florescu | Inversion formulas for the broken-ray Radon transform[END_REF][START_REF] Amabartsoumain | A series formula for inversion of the V-line Radon transform in 25 a disc[END_REF][START_REF] Katsevich | Broken ray transform: inversion and a range condition[END_REF][START_REF] Ilmairta | Broken ray tomography in the disc[END_REF][START_REF] Zhao | Inversion of the star transform[END_REF]. In a Cartesian coordinate system with origin O, the equation of the V -line is |x -ξ | = yτ . The vertex is on the Ox axis at abscissa ξ . The slope of the two branches with respect to the vertical direction is given by ±τ . Thus the transform R V f of an function f is

R V f (ξ , τ ) = 1 + τ 2 ∞ 0 dy {f (ξ -yτ , y) + f (ξ + yτ , y)}, (20)
with 0 < τ < ∞. Again we see that R V f 'sweeps' the upper half-plane y > 0 as R . Lemma 4.1:

R V f (ξ , τ ), although defined for 0 < τ < ∞, is invariant under τ → -τ . Hence R V f (ξ , τ ) is extendable into τ < 0 by R V f (ξ , τ ) = R V f (ξ , -τ ). ( 21
)
It is a symmetric function of τ . Moreover, in view of the definition of R , we have also the lemma Lemma 4.2: The V-line Radon transform data is related to the half-line Radon data by

R V f (ξ , τ ) = R f (ξ , τ ) + R f (ξ , -τ ). ( 22
)
The τ -symmetry of R V f (ξ , τ ) is now explicit. For the V -line Radon transform, a function f (x, y) is reconstructed from its data

R V f (ξ , τ ) via the formula f (x, y) = - 1 2π 2 ∞ 0 dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ + 1 ξ -x + yτ ∂ ∂ξ R V f (ξ , τ ).
(23) Note the τ -symmetry of the integrand under the integral sign.

Then it is legitimate to ask whether it is possible to express the reconstruction formula of the V -line Radon transform in terms of the reconstruction formula of the half-line Radon transform. This is the content of the next theorem Theorem 4.3: When applied to the data R V f (ξ , τ ), the following two inverse integral operators

R V (x, y) -1 = - 1 2π 2 ∞ 0 dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ + 1 ξ -x + yτ ∂ ∂ξ , ( 24
)
and

R (x, y) -1 = - H(y) 2π 2 R 2 dτ dξ √ 1 + τ 2 1 ξ -x -yτ ∂ ∂ξ , ( 25
)
give the same result.

Proof: Start with Equation ( 23), and use the τ -symmetry to extend the τ -integration to R,

f (x, y) = - 1 4π 2 ∞ -∞ dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ + 1 ξ -x + yτ ∂ ∂ξ R V f (ξ , τ ).
(26) It is the sum of two integrals, the first one with a denominator (ξxyτ ). Rewrite the second one with a denominator (ξx + yτ ) in terms of τ = -τ , then using Equation ( 21) it becomes

- 1 4π 2 ∞ -∞ dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ ∂ ∂ξ R V f (ξ , τ ). ( 27
)
Putting together and relabel τ by τ , we get

f (x, y) = - 1 2π 2 ∞ -∞ dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ ∂ ∂ξ R V f (ξ , τ ). ( 28
)
Now because of Equation ( 22), we get

f (x, y) = - 1 2π 2 ∞ -∞ dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ ∂ ∂ξ R f (ξ , τ ) - 1 2π 2 ∞ -∞ dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ ∂ ∂ξ R f (ξ , -τ ). ( 29
)
GIPE 1281920 18-1-2017 Initial CE:YS QA:CL

The first line is just the reconstruction by R using the half-line Radon data R f (ξ , τ ), see Equation ( 19). So it is expected that the second integral on the data R f (ξ , -τ ) should vanish. This is the object of the next proposition Proposition 4.4: R f (ξ , -τ ) belongs to the null space of the half-line reconstruction operator R

-1 R -1 R f (ξ , -τ ) = - 1 2π 2 ∞ -∞ dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ ∂ ∂ξ R f (ξ , -τ ) = 0. ( 30
)
Proof: We use Equation ( 18) to replace R f (ξ , -τ ) by its defining integral. Then the left-hand-side of Equation (30) becomes

- 1 2π 2 ∞ -∞ dτ √ 1 + τ 2 ∞ -∞ dξ 1 ξ -x -yτ ∂ ∂ξ 1 + τ 2 ∞ 0 dz f (ξ + zτ , z). ( 31
)
Now insert the two-dimensional Fourier representation of f (x, y)

f (x, y) = R 2 dp dq f (p, q) e 2iπ(px+qy) , ( 32
)
and use the well-known Fourier transform formula

∞ 0 dz e 2iπ(pτ +q)z = 1 2 δ(pτ + q) - 1 iπ 1 pτ + q , ( 33
)
as well as

∞ -∞ dξ ξ -(x + yτ ) = e 2iπ(x+yτ ) iπ sgn(p), ( 3 4 )
in Equation ( 31), to get a new form of (31) 2

- 1 2π 2 R 2 dp dq f (p, q) e 2iπ px iπ sgn(p) 2iπp × ∞ -∞ dτ 1 2 δ(pτ + q) - 1 iπ 1 pτ + q e 2iπ pyτ . ( 35
)
The factor 2iπp comes from the ξ derivative of R f (ξ , -τ ). Note that |p| = p sgnp, and δ(pτ + q) = 1/|p| δ(τ + q/p). Performing the τ integral and using again Equation (32) give 1 2 f (x, -y) -

R 2 dp dq f (p, q) sgn(p) 2iπ e 2iπx ∞ -∞ dτ e 2iπpyτ τ + q p , (36)
or using again

∞ -∞ dτ e 2iπpyτ τ + q p = e -2iπ qy iπ sgn(py), ( 3 7 )
one ends up with the result

1 2 f (x, -y) -sgn(y)f (x, -y) , (38)
GIPE 1281920 18-1-2017 Initial CE:YS QA:CL which is zero for y > 0 as expected and equal to f (x, -y) for y < 0, also as expected.

Hence we have shown that

R V -1 = R -1 , (39)
whenever these two inverse operators act on the data R V . Consequently, we deduce that symbolically

R CC -1 = R C -1 , (40)
with the corresponding provision on the scattering angle for each Radon transform

ω ∈ [π/2, π] for R CC (41) ω ∈ [0, π] for R . ( 42
)
What can be concluded from this? If we count each R V f (ξ , τ ) as one measurement in the R V -procedure (resp. each R f (ξ , τ ) as one measurement in the R -procedure), then the number of measurements in the R V procedure is just one half the number of measurements in the R procedure. This observation has an impact at the discretization level of the two inverse formulas as well as at the practical level of physical data collection. Thus discretized data shall appear as R f (ξ j , τ k ) and R V f (ξ j , τ k ), where (j, k) and (j , k ) are pairs of integers. The result of Theorem 4.3 means that the number of values taken by k is twice the number of values taken by k . Consequently, this conclusion remains valid when transcribed to R CC and to R C . This is the sense attributed to the 'improved' character given to a CST functioning with a pair of supplementary scanning circular arcs as compared to a CST functioning solely on a single scanning circular arc. Remark 4.5: Equation (39) does not show that R V is a pre-conditioned R . If this were the case, then one should have

R V = R P -1 , ( 43
)
where P is a non-singular pre-conditioner operator, lowering the condition number of R . Of course the statement is to be understood at the discretized level, where each of the integral operator is replaced by its finite dimensional matrix representative. But this is not what Equation (40) shows.

Numerical simulations

As pointed out above, the inversion of the Radon transform on a pair of supplementary circular arcs R CC is transferred to the inversion of the Radon transform on V -lines R V by geometric inversion. So, in order to establish a numerical framework for practical reconstruction of functions, one must work first with the inverse formula of R V . The idea is to circumvent the divergent behaviour of the poles in Equation [START_REF] Novikov | An inversion formula for the attenuated X-ray transform[END_REF], by going to Fourier space to throw the divergence to infinity. But then one can 'apodize', as it is done currently with the Radon transform on full lines in the plane under the form of a FBP inversion method.

The reconstruction algorithm can be formulated as follows:

• From the two measurements at site D, work out the mathematical data R CC (ξ , ω) (given by Equations ( 14) and (3) as a function of (ξ , τ )), for a real object defined by f (x, y), GIPE 1281920 18-1-2017 Initial CE:YS QA:CL

• Use Equations ( 15) and ( 6) to generate mathematical data for R V as a function of [START_REF] Novikov | An inversion formula for the attenuated X-ray transform[END_REF] to perform the inversion of the R V transform or to obtain the reconstruction of the 'apparent' object function

(ξ , τ ), i.e. R CC f (ξ , ω) = R V g R (ξ , τ ), • Use formula
g R (x , y ) = - 1 2π 2 ∞ 0 dτ √ 1 + τ 2 × R dξ 1 ξ -x -y τ + 1 ξ -x + y τ ∂ ∂ξ R V g R (ξ , τ ), (44)
• Rewrite this formula using the Fourier transforms

R V g R (ξ , τ ) = R dq e 2iπ qξ R V g R (q, τ ), ( 45
) 1 ξ -x ± y τ = iπ R dq e -2iπq (ξ -x ±y τ ) sgnq . ( 46
)
We get, with |q| = q sgnq,

g R (x , y ) = R dτ √ 1 + τ 2 R dq |q| R V g R (q, τ ) e 2iπqx 2 cos (2πqy τ ). ( 47
)
Recalling that τ = cot ω, this reconstruction formula can be given the form of a FBP, as known in conventional Radon transform and also in [START_REF] Morvidone | On the V-line Radon transform an its imaging applications[END_REF],

• Recover the original object f (x, y) using Equation [START_REF] Norton | Compton scattering tomography[END_REF].

• The term |q| grows linearly at infinity. In order to approximate numerically this growth, one introduces a cut-off at the infinity bound (apodization).

Projections

The forward model given by ( 14) can be alternatively written in polar coordinates (r, θ) that are more suitable for numerical integration on circular paths. Thus, keeping for readability the name of the function f (r, θ), we have

R CC f (ξ , ω) = I CC (ρ, ω) = π 0 dθ 2ρ f 2ρ cos θ -ω + π 2 , θ) + f 2ρ cos (θ + ω - π 2 , θ , (48)
that represents the integrations on two supplementary circular arcs of radius

ρ = ξ 2 sin ω . ( 49
)
Each scanning arc is linked to a scattering angle: either ω or (π -ω) (i.e. they are supplementary arcs of circle). For numerical simulations, we considered square (N × N, N = 256) objects in the (x, y) plane ( x = y = 1) located at a distance L = N of the source S (i.e. the origin of coordinates, see Figure 6) and at a height H 0 = N/4 from the horizontal axis. The radius of the scanning arcs was discretized by Nρ = 2048. The number of scattering angles considered was N ω = 2048, with the parameter in ω ∈ ( π 2 , π) that corresponds to scattering angles in the full interval (0, π). For the discretization of the polar angle we used N θ = 1024 leading to an integration step θ = θ max -θ min N θ . The bounds of the interval are 0 < θ max , θ min < π 2 because the object considered was in the first quadrant. Simulated data is then used in reconstruction of functions.

Reconstructions

Reconstructions from data generated by (48) were performed according to the scheme outlined above and summarized in Figure 8. Equations ( 15) and (49) establish a link between R V g R (ξ , τ ) and I CC (ρ, ω). Data obtained through (48) is rearranged in the form of R V g R (ξ , τ ) projections corresponding to the Radon transform on V -lines. For this purpose, geometric inversion was used with an inversion circle of radius R = 100. The parameter ξ (the distance to the origin) in the R V projections was discretized as ξ min = -90, ξ max = 130 and N ξ = 2048. The discretization of ξ (N ξ ) and the scattering angle (N ω = 2048) provides enough data to reconstruct a 256 × 256 (N = 256) object. After rearrangement, reconstruction is performed using filtered back-projection algorithm (47). In order to compensate the divergence of the ramp filter, we multiply by a cosine apodization window to obtain the final filter:

W(q) = |q| 1 + cos 2πq 2 , ( 50
)
where q is the normalized frequency, dual to the variable ξ . The choice of this filter is motivated by the results obtained earlier in [START_REF] Cebeiro | Back-projection inversion of a Conical Radon transform[END_REF] where reconstruction from noisy and noiseless scatter radiation data was performed using a 3D filtered back-projection algorithm. In [START_REF] Cebeiro | Back-projection inversion of a Conical Radon transform[END_REF], several apodization windows (cosine, Shepp-Logan and Hamming) were tested and no significant differences between them were found. Finally, the desired reconstructions are obtained through [START_REF] Norton | Compton scattering tomography[END_REF], again with R = 100.

Results

In order to illustrate the working of our new algorithm, we present numerical simulations applied on two objects: a cracked bar and a block of reinforced concrete. Each studied object 1.

has different features that are useful to highlight the performance of the reconstruction technique applied. While the bar exhibits a thin structure, approximately % of the region of interest (ROI), with a homogeneous electronic density and a small detail in it (i.e. a crack), the block is a large massive-object made of different electronic densities (i.e. metal and concrete) and covering the whole ROI (100 %). Figure 9 shows the original objects GIPE 1281920 18-1-2017 Initial CE:YS QA:CL together with projections I CC (ρ, ω), rearranged data in the form of V -line projections (we show R V g R (ξ , φ) = R V g R (ξ , τ ) with τ =tan φ and we kept the name R V g R for readability, and reconstructions. Notice the two branches in R CC f (ξ , ω), each one corresponding to a different circular path in (48). The missing data in R V g R (ξ , φ) (in the neighbourhood of ξ = 0) corresponds large scanning circumferences (i.e. ρ large) and can be reduced by increasing ρ.

In addition, we study the robustness of the algorithm in front of noisy data. Projections calculated according previous section are now corrupted with Gaussian additive noise with three different signal to noise ratios (SNR): 20 dB, 15 dB and 10 dB. Reconstructions were performed as in previous section and are shown in Figure 10. Finally, the quality of all reconstructions is assessed with the Normalized Mean Square Error [START_REF] Cebeiro | Back-projection inversion of a Conical Radon transform[END_REF]27] as a measurement of the accuracy of the method:

NMSE = 100 N 2 i=1 fi -f i 2 / N 2 max i {f i } ,
where vectors f and f are the reference and reconstructed functions, respectively. All results are summarized in Table 1.

Discussion

Results show a good performance of the inversion method proposed to reconstruct objects scanned with the CST modality on supplementary circle arcs. The crack in the bar is properly recovered, even in its thinnest part towards the bottom. The shape of the metal bars inside the block of reinforced concrete is clearly seen. The main features of the non-metallic part are recovered although some blurring is present in the smallest details. Regarding figures of merit, the obtained NMSEs are reasonable. In the case of the bar (NMSE = 0.41 %), the most contributing factor is the non-zero background (see Figure 9) present in the original image that is slightly amplified in the reconstruction. Nevertheless, this does not alter significantly the appearance of the reconstructed image. On the other hand, inside the reinforced concrete block, the error (NMSE = 3.82 %) is completely due to the object itself since there is not background. Missing data in R V does not seem to be critical for reconstructions. In what concerns noisy data (SNR=20 dB and 15 dB), although there is some degradation in the quality of the recovered images, the small structures or the important details of the objects (i.e. the crack in the bar and the state of the metal skeleton in the reinforced concrete) are well observed even without using any de-noising technique. With SNR=10 dB or lower some previous treatment may be necessary.

Conclusion and perspectives

In this paper, we have introduced a new modality of CST which is suitable for one-sided large objects located in a half space in R 3 . This corresponds to the growing need of imaging objects of interest in those fields cited in Section 1. It consists in 'doubling' the Compton effect scanning of the sample as compared to the 'single' of the conventional modality of CST. Theoretically, image reconstruction should be of enhanced quality as

Figure 1 .

 1 Figure 1. Classical CST.

Figure 2 .

 2 Figure 2. Compton scattering.

Figure 3 .

 3 Figure 3. Geometric inversion of a circular arc.

2 ,Figure 4 .

 24 Figure 4. Half-line of equation ξ -x -y τ = 0 with y > 0 used in R Radon transform.

Figure 5 .

 5 Figure 5. Double supplementary arcs CST.

Figure 6 .

 6 Figure 6. Geometric inversion of a pair of supplementary circular arcs.

Figure 7 .

 7 Figure 7. V-line of equation |x -ξ | = y τ used in R V Radon transform.

Figure 8 .

 8 Figure 8. General reconstruction scheme for the modality CST on supplementary circle arcs.

Figure 9 .

 9 Figure 9. Radon Transform on supplementary circle arcs. Left column: reinforced concrete block. Right column: cracked bar. Row 1: original objects. Row 2: projection data: I CC (ρ, ω). Row 3: Rearranged data as a V-line Radon Transform R V g R (ξ , φ) (τ =tan φ). Row 4: reconstructions. See figures of merit in Table1.

Figure 10 .

 10 Figure 10. Reconstructions from noisy projections with the R CC . Row 1: 20 dB. Row 2: dB. Row 3: 10 dB. See figures of merit in Table1.

4 .Notes 1 . 2 .

 412 Numerical simulations results support this aspect of the new CST and open the way to further research development directions taking into account attenuation corrections, photometric propagation effects as well as non-isotropic, nonmonochromatic source before it can become as a well-established imaging procedure for wide use in the fields mentioned AQ5 . S. J. Norton has also worked out a related inversion formula based on the result of A. M. Cormack. Here sgn(p) is the sign function of p.

Table 1 .

 1

	GIPE 1281920 18-1-2017	Initial	CE:YS QA:CL

Table 1 .

 1 Normalized mean square error (%).

		Noiseless	20 dB	15 dB	10 dB
	Cracked bar	0.41	0.47	0.59	0.97
	Reinforced concrete	3.82	4.29	5.34	8.41

Acknowledgements

The authors would like to thank all the referees for their critical remarks and suggestions which have contributed to the improvement of this paper.

Funding J. Cebeiro research work is supported by a CONICET [grant number Nro. Legajo 146618]. The work of J. Cebeiro and M. A. Morvidone is partially supported by SOARD-AFOSR [grant number FA9550-14-1-0276]. J. Cebeiro acknowledges support from Programa BEC.AR for financial funding of a visit to ETIS (ENSEA/ Université de Cergy-Pontoise/UMR CNRS 8051) in 2015. M. A. Morvidone was partially supported by MINCyT-CONICET-CNRS (International Cooperation Programme, CONICET Resol. 147/15).

Disclosure statement

No potential conflict of interest was AQ6 reported by the authors.


Mohand Lounes Bentaha

Olga Battaïa
email: battaia@emse.fr

Alexandre Dolgui
email: dolgui@emse.fr

A Stochastic Formulation of the Disassembly Line Balancing Problem

Keywords: Sustainable Development, Disassembly Line Design, Stochastic Programming, L-shaped Method

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The growing amount of postconsumer products poses challenges for business and society at large [START_REF] Güngör | Issues in Environmentally Conscious Manufacturing and Product Recovery : a Survey[END_REF]. To decrease the amount of waste to be sent to landfills, more and more manufacturers turn to end-of-life processing of products [START_REF] Güngör | A Solution Approach to the Disassembly Line Balancing Problem in the Presence of Task Failures[END_REF]. The selective separation of desired parts and materials, executed by disassembly, is a mandatory step before recycling or remanufacturing [START_REF] Güngör | Disassembly Line in Product Recovery[END_REF]. As a consequence, disassembly systems tend to play an important role in industry. Since their design results in complex optimization problems, including disassembly planning, balancing and sequencing, efficient mathematical tools are needed in order to improve their performances and their cost effectiveness. Such tools must take into account the high degree of uncertainty in the structure and the quality of the products to be disassembled because of varying conditions affecting them before they arrive in a disassembly system. This paper deals with the uncertainty related to the disassembly task times and proposes a new mathematical formulation for the stochastic disassembly line balancing problem (DLBP) as well as an exact method to solve it efficiently.

Problem Formulation

The Disassembly Line Balancing Problem considered here aims to assign a given set of disassembly tasks I ൌ ሼ1,2, … , ܰሽ to an ordered sequence of workstations ܬ ൌ ሼ1,2, … , ܯሽ under precedence and cycle time constraints. A task cannot be split between two workstations. Disassembly task times ݐ are assumed random variables with normal probability distributions having known mean ߤ and variance ߪ ଶ , ݅. ݁. ݐ ൌ ߞ ሚ , ߞ ሚ ~ࣨሺߤ , ߪ ሻ, ݐ 0, ݅ ∈ ,ܫ [START_REF] Dolgui | Supply Chain Engineering: Useful Methods and Techniques[END_REF], [START_REF] Sarin | A Methodology for Solving Single-Model, Stochastic Assembly Line Balancing Problem[END_REF][START_REF] Silverman | A Cost-based Methodology for Stochastic Line Balancing with Intermittent Line Stoppages[END_REF]. The task times of set I are modeled by random vector ߦ ሚ ൌ ൫ߞ ሚ ଵ , ߞ ሚ ଶ , … , ߞ ሚ ே ൯ varying over a set Ξ ⊂ Ը ା ே in given probability space ሺΞ, ࣠, ܲሻ. Random variables ߞ ሚ , ݅ ∈ ܫ are assumed to be mutually independent. Let ߞ ሚ ൌ ߙ ൫ߦ ሚ ൯, ݅ ∈ ܫ . The precedence relations among tasks are given by an AND/OR Graph (AOG), [START_REF] Altekin | Profit-Oriented Disassembly-Line Balancing[END_REF], [START_REF] Koc | Two Exact Formulations for Disassembly Line Balancing Problems with Task Precedence Diagram Construction Using an AND/OR Graph[END_REF], see Fig. 1. Each subassembly of the product to be disassembled is represented by an auxiliary node A in the AOG. Each disassembly task gives a basic node B . Two types of arcs define the precedence relations between the subassemblies and the disassembly tasks. AND-type arcs (in bold) dictate the normal precedence relation. ORtype arcs (remaining arcs) permit the selection of any of the successors. A dummy task ܵ is introduced into the precedence graph as a sink node, see the figure below. ݔ ൌ ቄ 1 if task from ܤ is assigned to workstation ݆, 0 otherwise.

ݔ ௌ ൌ ቄ 1 if sink task ܵ is assigned to workstation ݆, 0 otherwise. ݖ ൌ ൜ ܥ ௧ if ݔ ௌ ൌ 1, 0 otherwise.
The objective considered in this paper is to minimize the line cost including fixed workstation operating costs and recourse costs caused by exceeding ܥ ௧ . A recourse variable ݕ ൫ߦ ሚ ൯, ݆ ∈ ,ܬ measures the amount of time exceeding ܥ ௧ if there is any. The following model is used for the problem presented.

Stochastic MIP Formulation (SMIP I).

min ቐܨ ݆ ݖ

∈ + ॱ క ෨ ݍ ݕ ൫ߦ ሚ ൯ ∈ ቑ s.t. ݖ ൌ ܥ ௧ ݔ ௌ , ∀ ݆ ∈ ܬ ሺ1ሻ ݔ ∈ ∈ୗሺሻ ൌ 1 ሺ2ሻ ݔ ∈ ≤ 1, ∀ ݅ ∈ ܫ ሺ3ሻ ݔ ∈ ∈ୗሺሻ ൌ ݔ ∈ ∈ሺሻ , ∀ ݇ ∈ \ܭሼ0ሽ ሺ4ሻ ݔ ௩ ∈ୗሺሻ ≤ ݔ ௩ ୀଵ ∈ሺሻ , ∀ ݇ ∈ \ܭሼ0ሽ, ∀ ݒ ∈ ܬ ሺ5ሻ ݔ ௌ ∈ ൌ 1 ሺ6ሻ ݆ ݔ ∈ ≤ ݆ ݔ ௌ ∈ , ∀ ݅ ∈ ܫ ሺ7ሻ ߙ ൫ߦ ሚ ൯ ݔ ∈ூ െ ݕ ൫ߦ ሚ ൯ ≤ C ୲ , ∀ ݆ ∈ ܬ ሺ8ሻ ݖ ≥ 0, ∀ ݆ ∈ ܬ ሺ9ሻ ݔ ௌ , ݔ ∈ ሼ0,1ሽ, ∀ ݅ ∈ ,ܫ ∀ ݆ ∈ ܬ ሺ10ሻ ݕ ൫ߦ ሚ ൯ ≥ 0, ∀ ݆ ∈ ܬ ሺ11ሻ
The objective function includes fixed and recourse costs, where ॱ క ෨ stands for the expected value with the respect to the distribution of the random vector ߦ ሚ :

ॱ క ෨ ൣ∑ ݍ ݕ ൫ߦ ሚ ൯ ∈ ൧ ൌ  ൫∑ ݍ ݕ ൫ߦ ሚ ൯ ∈ ൯ dܲ ஆ ሺ12ሻ
Note that the integral [START_REF] Sarin | A Methodology for Solving Single-Model, Stochastic Assembly Line Balancing Problem[END_REF] makes the model nonlinear one.

Constraints (1) ensure the value of ݖ to be ܥ ௧ when dummy task ܵ is assigned to station ݆. Constraint (2) imposes the selection of only one disassembly task (ORsuccessor) to begin the disassembly process. Constraint set [START_REF] Birge | Stochastic Programming Computation and Applications[END_REF] indicates that a task is to be assigned to at most one workstation. Constraints (4) and ( 5) define OR-and AND-precedence relations, respectively. Constraint (6) imposes the assignment of the dummy task ܵ to one station. Constraints [START_REF] Güngör | Issues in Environmentally Conscious Manufacturing and Product Recovery : a Survey[END_REF] ensure the precedence relations for dummy task ܵ. The constraints [START_REF] Güngör | Disassembly Line in Product Recovery[END_REF] force the respect of the cycle time limitations. Sets ( 9)-( 11) represent the trivial constraints. Let ܺ ൌ { ݔ | constraints (1)-( 7), ( 9)-( 10) are satisfied} and ܮ ൌ ሼ1,2, … , Lሽ, L ∈ Գ * . If ߦ ሚ has a finite discrete distribution ሼሺߦ ,  ሻ, ݈ ∈ ܮሽ,  0, ∀ ݈ ∈ ܮ ( is the realization probability of ߦ of ߦ ሚ ), then the model presented is an ordinary linear program with a so-called dual decomposition structure.

Deterministic Equivalent (I').

min ቐܨ ݆ ݖ

∈ +  ݍ ݕ ሺߦ ሻ ∈ ୀଵ ቑ s.t. ߙ ሺߦ ሻ ݔ ∈ூ െ ݕ ሺߦ ሻ ≤ C ୲ , ∀ ݆ ∈ ,ܬ ∀ ݈ ∈ ܮ ݔ ∈ ܺ, ݕ ሺߦ ሻ ≥ 0, ∀ ݆ ∈ ,ܬ ∀ ݈ ∈ ܮ
Depending on the number of realizations of ߦ ሚ , L, this linear mixed integer program, may become very large in scale, but its particular block structure can be exploited by specially designed algorithms such as the L-shaped method, [START_REF] Ahmed | The Sample Average Approximation Method for Stochastic Programs with Integer Recourse[END_REF], [START_REF] Birge | Stochastic Programming Computation and Applications[END_REF][START_REF] Birge | L-shaped Method for Two-stage Problems of Stochastic Convex Programming[END_REF], [START_REF] Kall | Stochastic Programming[END_REF], [START_REF] Ntaimo | Fenchel Decomposition for Stochastic Mixed-Integer Programming[END_REF] which will be developed in the next session.

Solution Method

3.1

The L-shaped Method

The main idea of the L-shaped method is to approximate the nonlinear term in the objective function of the two-stage stochastic problems [START_REF] Birge | Stochastic Programming Computation and Applications[END_REF]. Assume a finite realizations set Ξ of the stochastic vector ߦ ሚ such as |Ξ| ൌ L. The L-shaped method for the DLBP can be written as follows.

L-shaped Algorithm

Step 0. Set ॥ ൌ ज़ ൌ ߭ ൌ 0.

Step 1. Set ߭ ൌ ߭ + 1. Solve the following LP:

minሼܿ ் ݔ + ߮ሽ s.t. ܣ ݔ ൌ ܾ ࣞ ఔ ݔ ≥ ࣸ ఔ , ߥ ൌ 1, … , ॥ ሺ13ሻ ℰ ఔ ݔ + ߮ ≥ ℯ ఔ , ߥ ൌ 1, … , ज़ ሺ14ሻ
ݔ binary, ߮ ≥ 0

Let ሺݔ జ , ߮ జ ሻ be an optimal solution.

Step 2. For ݈ ൌ 1, … , L solve the following LP:

min ࣴ ൌ ࣵ ் ݑ ା + ࣵ ் ݑ ି s.t. ܹ ݕ + ݑܫ ା െ ݑܫ ି ൌ ℎ െ ܶ ݔ జ ݕ ≥ 0, ݑ ା ≥ 0, ݑ ି ≥ 0 ࣵ ൌ ሺ1, … ,1ሻ ்
, until for some ݈ the optimal value ࣴ 0. In this case, let ߪ జ be the associated simplex multipliers, define

ࣞ ॥ାଵ ൌ ሺߪ జ ሻ ் ܶ
and

ࣸ ॥ାଵ ൌ ሺߪ జ ሻ ் ℎ
in order to generate a constraint called a feasibility cut of type [START_REF] Silverman | A Cost-based Methodology for Stochastic Line Balancing with Intermittent Line Stoppages[END_REF]. Set ॥ ൌ ॥ + 1, add constraint type (13) and return to Step 1. If for all ݈ ∈ ,ܮ ࣴ ൌ 0 , go to Step 3.

Step 3. For ൌ 1, … , L , solve the LP:

min ࣱ ൌ q ் ݕ ܹ ݕ ൌ ℎ െ ܶ ݔ జ ݕ ≥ 0
Let ߱ జ be the simplex multipliers associated with the optimal solution of problem ݈ above and define Two types of constraints are sequentially added:

ℰ ज़ାଵ ൌ  ሺ߱ జ ሻ ் ܶ ∈ and ℯ ज़ାଵ ൌ  ሺ߱ జ ሻ ் ℎ ∈ . Let ߠ జ ൌ ℯ ज़ାଵ െ ℰ ज़ାଵ ݔ జ . If ߮ జ ≥ ߠ జ ,
• feasibility cuts [START_REF] Silverman | A Cost-based Methodology for Stochastic Line Balancing with Intermittent Line Stoppages[END_REF] determining ൛ॱ|ݔ క ෨ ൣ∑ ݍ ݕ ൫ߦ ሚ ൯ ∈ ൧ < +∞ൟ;

• optimality cuts (14), which are linear approximations to ॱ క ෨ ൣ∑ ݍ ݕ ൫ߦ ሚ ൯ ∈ ൧.

Example

The method presented has been applied to the compass example illustrated in Fig. 2. It is made of seven components: (1) wheel, (2) left leg, (3) right leg, (4) left fixation screw, (5) lead, (6) tip and ( 7) right fixation screw. The AOG for this example is shown in Fig. 1. The input data for the DLBP is presented in Table 1. The L-shaped method was implemented in Microsoft Visual C++ 2008. ILOG CPLEX 12.4 was used to solve the model on a PC with Pentium(R) Dual-Core CPU 2.30 GHz and 3Go RAM. The optimal solution contains 2 workstations. Task 5 is assigned to the 1 st workstation and tasks {8,10} to the second one. The total line cost is 5.342 when the recourse cost is 0.242. The resolution time was 58 s. The overall idle time of the disassembly line, if mean time of each task selected is considered, is 0.10.

Conclusion and Perspectives

The disassembly line balancing problem was formulated under uncertainty. A twostage stochastic linear mixed integer program with fixed recourse was developed to solve it. The formulation presented can be easily adapted for the stochastic assembly line balancing problem as well. Then, the model can be considered for the disassembly task times given by, for example, triangular distribution. Further research work should be done in order to refine the proposed mathematical model and solution method in order to approach real-world problems where uncertainty does not only concern the disassembly task times but the quantity and the quality of the inputs and outputs of the disassembly line as well.

Fig. 1 .

 1 Fig. 1. AND/OR precedence graph. The following notations have to be introduced. Parameters. ܫ ൌ ሼ1,2, … , ܰሽ, disassembly tasks' index set, ܰ ∈ Գ * ; ܬ ൌ ሼ1,2, … , ܯሽ, workstations' index set, ܯ ∈ Գ * ; ܭ ൌ ሼ0,1, … , ܩ െ 1ሽ, index set of the AND/OR precedence graph's auxiliary nodes, ܩ ∈ Գ * ; A : Auxiliary node of the AND/OR graph, ݇ ∈ ܭ ; B : Disassembly task, ݅ ∈ ܫ ; ܵ : The AND/OR graph's sink node, ݐ ௌ ൌ 0; ܨ : Fixed cost per unit time of operating the workstations;

Fig. 2 .

 2 Fig. 2. The Compass example.

  stop; ݔ జ is an optimal solution. Else, generate a constraint called optimality cut of type (14), set ज़ ൌ ज़ + 1, add constraint type (14) and return to Step 1.

	This method approximates ॱ క ෨ ൣ∑ ݍ ݕ ൫ߦ ሚ ൯ ∈ linearization.	൧ ൌ  ൫∑ ݍ ݕ ൫ߦ ሚ ൯ ∈ ஆ	൯ dܲ	using an outer

Table 1 .

 1 Input data

	Task 1 2 3 4 5 6 7 8	ߤ 0.21 0.21 0.50 0.21 0.50 0.21 0.50 0.21	ߪ 0.05 0.05 0.10 0.05 0.10 0.05 0.10 0.05	Subassembly Component 1:5 6;7 1:3,6,7 4;5 2,4,5 1;3 1:3 4;5 2,4,5/3,6,7 1 1:3 6;7 3,6,7 1;2 --2;4;5	|Ξ| ൌ 1024 ܬ ൌ ሼ1,2,3ሽ ܭ ൌ ሼ0,1, … ,5ሽ ܨ ൌ 5 ݍ ൌ 7, ݆ ∈ ܬ ܥ ௧ ൌ 0.51
	9	0.50	0.10	--	1;2;3
	10	0.21	0.05	--	3;6;7

Acknowledgement

This work was partially supported by Research Cluster on Operational Research (GDR RO) of the National Centre for Scientific Research, France.


Vincent Leilde

Vincent Ribaud
email: ribaud@univ-brest.fr

Philippe Dhaussy

An Organizing System to Perform and Enable Verification and Diagnosis Activities

Keywords: verification, model-checking, diagnosis, organizing system

Introduction

System verification is used to establish that the design or product under consideration possesses certain properties. Formal verification has been advocated as a way forward to address verification tasks of complex embedded systems. Formal methods, within the field of computer science, is the formal treatment of problems related to the analysis of designs, but "it does not yet generally offer what its name seems to suggests, viz. methods for the application of formal techniques [START_REF] Ruys | Managing the verification trajectory[END_REF]." Our research work is underlined by the observation that verification "in the large" causes a proliferation of interrelated models and verification sessions "that must be carefully managed in order to control the overall verification process [START_REF] Ruys | Managing the verification trajectory[END_REF]." The main technique discussed in this paper is verification by model-checking. "Model checking is a formal verification technique which allows for desired behavioral properties of a given system to be verified on the basis of a suitable model of the system through systematic inspection of all states of the model [START_REF] Larsen | Model-checking for real-time systems[END_REF]."

Model-checking walks through different phases within an iterative process [START_REF] Baier | Principles of model checking[END_REF]: modelling, running the model-checker and analyzing the results. Moreover, the entire verification should be planned, administered, and organized.

The applicability of model-checking to large systems suffers of two practical problems. A verification session refines the model, and because properties are verified one by one, previously verified properties need or need not to be verified again, depending on the refinement performed. When the model-checker runs out of memory, some divide-and-conquer techniques should be employed to reduce the model. These techniques exploit regularities in the structure of the models or of the verification process itself that are difficult to understand and their performance may vary considerably.

A second practical problem arises from the difficulty to judge whether the formalized problem statement (model + properties) is an adequate reflection of the actual problem. This is known as the validation problem. If the verifier suspects the validity of a property, the property needs to be re-formalized and it starts the whole verification again. If the verifier suspects the validity of the design, the verification process restarts after an improvement of the design. The complexity of the involved system, as well as the lack of precision of the informal specification of the system's functionality, makes it hard to answer the validation problem satisfactorily [START_REF] Ruys | Managing the verification trajectory[END_REF], [START_REF] Baier | Principles of model checking[END_REF].

Both problems require an organized verification method. Organization creates or supports capabilities by intentionally imposing order and structure. In this paper, we apply the concepts of an organizing system promoted by [START_REF] Glushko | The Discipline of Organizing[END_REF]: "an Organizing System is an intentionally arranged collection of resources and the interactions they support." As an attempt to solve the problems mentioned above, we designed and built a prototype of an Organizing System for the support of verification and diagnosis activities. In section 2, we precise the issues of the management of verification cycles; we introduce a general theory of diagnosis, and we presents some design decisions for our Organizing System. Section 3 deepens different aspects of an Organizing System: knowledge management and ontologies, technical aspects of the tiers of the organizing system. Section 4 relates our work with previous work, and Section 5 concludes.

2

Organizing System for Verification and Diagnosis activities

Managing the Verification Trajectories

There are basically three possible outcomes of a verification run: the specified property is either valid in the given model or not, or the model is faced with the state space explosion problem (it turns out to be too large to fit within the computer memory). If a state is encountered that violates the property under consideration, the model checker provides a counterexample that describes an execution path that leads from the initial system state to the faulty state. It is indisputable that the verification results obtained using a verification tool should always be reproducible [START_REF] Holzmann | The Theory and Practice of A Formal Method: NewCoRe[END_REF]. Tool support is required and we present in Fig. 2 the objects that are significant and tool-managed during the verification phases. The specification-design-modelling-verification cycles are presented in Fig. 1. The terminology in [START_REF] Baier | Principles of model checking[END_REF] is used as a reference in the paper.

Modelling.

Model checking inputs are a model of the system and a formal characterization of the property to be checked. Models are mostly expressed using finite-state automata, made of a finite set of states and a set of transitions. To allow verification, properties are described using a property specification language, relying generally on temporal logic that allows people to describe properties in a precise and unambiguous manner. Verification: running the model-checker.

Current model checkers provide the user with various options and directives to optimize and tune the functionality and performance of the verification run. Subsequently, the actual model checking takes place. Whenever a property is not valid, it may have different causes. A modelling error means that the model does not reflect the design of the system. After the model correction, verification has to be restarted with the improved model. This corresponds to the bolded cycle in Fig. 1. When there is no undue discrepancy between the design and its model, then either a design error has been exposed, or a property error has taken place (this case is not considered in the paper). In case of a design error, the verification is concluded with a negative result, and the design (together with its model) has to be improved. The designer will proceed through iterative refinements; a situation depicted with a plain cycle in Fig. 1.

Interpreting the error(s).

The main advantage of model checking is the production of counterexamples demonstrating that a system does not satisfy a specification. Extracting the essence of an error from even a detailed source-level trace of a failing run requires a great deal of human-effort [START_REF] Groce | What went wrong: Explaining counterexamples[END_REF] and a lot of research work focus on counterexample processing to produce an error explanation. Hence, correcting the error(s) starts with an error diagnosis, and more precisely, using the fault, error, and failure nomenclature of [START_REF] Avižienis | Basic concepts and taxonomy of dependable and secure computing. Dependable and Secure Computing[END_REF], it starts with a failure diagnosis. Failure diagnosis is the process of identifying the fault that has led to an observed failure of a system or its constituent components.

Model-based diagnosis.

The technique we use for failure diagnosis is a model-based diagnosis (also called reasoning from first principles) based on a theory of diagnosis established by [START_REF] Reiter | A theory of diagnosis from first principles[END_REF]. A diagnosis is as a set of assumptions about a system component's abnormal behavior such that observations of one component's misbehavior are consistent with the assumptions that all the other components are acting correctly [START_REF] Reiter | A theory of diagnosis from first principles[END_REF]. The computational problem is to determine all possible diagnoses for a given faulty system. The representation of the knowledge of the problem domain should achieve the desired coverage and quality of diagnoses while remaining computationally tractable [START_REF] Peischl | Model-based diagnosis or reasoning from first principles[END_REF].

Verification organization.

Whether the verification trajectory is incorporated in an adaptive design strategy or focused on modelling-and-verifying cycles, the entire model-checking process should be well organized, well structured, and well planned. According to [START_REF] Baier | Principles of model checking[END_REF], different models are describing different parts of the system, various versions of the verification models are established, and plenty of verification parameters and results are available. We propose to use an organizing system to manage a practical model-checking process and to allow the reproduction of the experiments carried out by the engineers.

Robert J. Glushko and al. [START_REF] Glushko | The Discipline of Organizing[END_REF] promote The Discipline of Organizing (TDO) approach. Library and information science, informatics and other fields focus on the characteristic types of resources and collections that define those disciplines. In contrast, TDO complements the focus on specific resource and collection types with a framework that views organizing systems as existing in a multi-dimensional design space in which we can consider many types of resources at the same time and see the relationships among them. The framework assesses what is being organized, why, how much, when and by what means. It leads to an Organizing System defined as "an intentionally arranged collection of resources and the interactions they support [START_REF] Glushko | The Discipline of Organizing[END_REF]."

To sum up the problem statement of this section, managing the verification trajectories is an indispensable support for using model checkers "in the large". Moreover the proliferation of verification resources and the variety of possible interactions with them requires an Organizing System. "The concept of the Organizing System highlights the design dimensions and decisions that collectively determine the extent and nature of resource organization and the capabilities of the processes that compare, combine, transform and interact with the organized resources [START_REF] Glushko | The Discipline of Organizing[END_REF]."

A Theory of Diagnosis from First Principles

A variety of failure diagnosis techniques drawing from diverse areas of computing and mathematics such as artificial intelligence, machine learning, statistics, stochastic modelling, Bayesian inference, rule-based inference, information theory, and graph theory have been studied in the literature [START_REF] Kavulya | Failure Diagnosis of Complex Systems[END_REF]. In the model-based diagnosis, often referred as diagnosis from first principles, one is given a description of a system, to-gether with an observation of the system's behavior which conflicts with the way the system is meant to behave. "The diagnostic problem is to determine those components of the system which, when assumed to be functioning abnormally, will explain the discrepancy between the observed and correct system behavior [START_REF] Reiter | A theory of diagnosis from first principles[END_REF]." At the other end of the spectrum, there are methods that do not assume any form of model information and rely only on historic process data [START_REF] Venkatasubramanian | A review of process fault detection and diagnosis: Part I: Quantitative model-based methods[END_REF]." Without denying the importance of other approaches, we use a theory of diagnosis from first principles based on Reiter's work [START_REF] Reiter | A theory of diagnosis from first principles[END_REF] as a general theory of diagnosis.

One begins with a description of a system, including desired properties and the structure of the system's interacting components. Whatever one's choice of representation, the description will specify how that system normally behaves on the assumption that all its components are functioning correctly. We need a diagnosis if we have available an observation of the system's actual behavior and if this observation is logically inconsistent with the way the system is meant to behave. Intuitively, a diagnosis determines system components which, when assumed to be functioning abnormally, will explain the discrepancy between the observed and correct system behavior [START_REF] Reiter | A theory of diagnosis from first principles[END_REF]. There may be several competing explanations (diagnoses) for the same faulty system, the computational problem, then, is to determine all possible diagnoses.

Design Decisions

Explicitly or by default, establishing an Organizing System (OS) requires many decisions. These decisions are deeply intertwined, but it is easier to introduce them as if they were independent. In [START_REF] Glushko | The Discipline of Organizing[END_REF], authors introduce five groups of design decisions.

What is being organized?

System models, verification runs and diagnosis are our primary source of interest. There are all made of digital resources, but we can make a distinction between primary resources (such as [parts of] models, properties, verification runs, and counterexamples) and description resources about the primary resources and their relationships. Verification benchmarks (e.g. BEEM, BEnchmarks for Explicit Model checkers [START_REF] Pelánek | BEEM: Benchmarks for explicit model checkers[END_REF]) provide valuable inputs and need to be organized in collections. Any OS user can also organize her own verification endeavors in collections, sub-collections of resources.

Why it is being organized?

OS users are modelling and verification engineers, working alone or in teams, who need "to deal with the data explosion of the modelling phase and the versioned product space explosion of the verification phase [START_REF] Ruys | Managing the verification trajectory[END_REF]." The OS gathers and organizes quantitative and qualitative information to support knowledge creation and automated diagnosis reasoning. OS users share knowledge without being constrained to espouse a given formalism. OS users need to navigate efficiently through the resources space. The OS supports a reverification procedure to make sure that errors found in the model do not invalidate previous verification runs.

How much is it being organized?

The simplest OS can be a software configuration management system controlling the release and change of each digital resource, leaving the burden of organization outside of the OS. At the opposite of the spectrum, the OS can be a full ontology where any relationship between any piece of information is carefully defined and controlled, allowing many reasoning possibilities. For our point of view, the OS manages essentially documents (models, results, traces). Each document organizes its knowledge structure and content, according to its document type, and the engineer writes and reads information according to this structure. The reification of the underlying knowledge structure for reasoning purposes is done automatically by the OS.

When is it being organized?

The OS is intended to assist the engineer in her daily modelling and verification tasks, hence resources are organized continuously. However, the OS should offer an ingestion feature that helps to enter inputs into the OS. Ingest feature provides the services and functions to accept complex verification endeavors or benchmark collections and prepares the contents for storage and management within the OS. Conversely, an access feature provides the services and functions that support users in determining the existence, description, location and availability of information stored in the OS, and allowing users to extract information in a parametrized manner.

How or by whom, or by what computational processes, is it being organized?

Although a single verification engineer will benefit of the OS use, the OS is intended to support teamwork and to share knowledge about models and verification endeavors. Automated processes should extract as much knowledge as possible from the documents internal structure and from the collections organization. As a collaborative teamwork, organization is performed in a distributed, bottom-up manner.

3

Inside the Organizing System

Knowledge Management and Ontologies

In [START_REF] Abecker | Toward a Technology for Organizational Memories[END_REF], the authors state that knowledge is an enterprise's most important assets and define the basic activities of knowledge management: identification, acquisition, development, dissemination, use, and preservation of the enterprise's knowledge. They advocate a corporate or organizational memory (OM) at the core of a learning organization, supporting sharing and reuse of individual and corporate knowledge and lessons learned [START_REF] Abecker | Toward a Technology for Organizational Memories[END_REF]. The concept of an organizing system intended to knowledge management (KM) is a modern reincarnation of the organizational memory and we can benefit from the results gained in this research area. Knowledge acquisition and maintenance pose a serious challenge for organizational memories and [START_REF] Abecker | Toward a Technology for Organizational Memories[END_REF] recommend adhering to the following principles: -exploit easily available information sources ; -forgo a complete formalization of knowledge; -use automatic knowledgeacquisition tools; -encourage user feedback and suggestions for improvements;check the consistency of newly suggested knowledge.

An organizational memory or a KM organizing system relies substantially on existing information sources, which constitute the first tier of its architecture, called the object level in [START_REF] Abecker | Toward a Technology for Organizational Memories[END_REF] and the storage tier in [START_REF] Glushko | The Discipline of Organizing[END_REF]. This level or tier is characterized by a variety of sources, heterogeneous with respect to several dimensions concerning form and content properties. An organizational memory or an information organizing system offers presentation facilities in the access tier, called the application-specific level in [START_REF] Abecker | Toward a Technology for Organizational Memories[END_REF] and the presentation tier in [START_REF] Glushko | The Discipline of Organizing[END_REF]. This level or tier performs the mapping from the application-specific information needs to these heterogeneous object-level sources via a uniform access and utilization method on the basis of a logic-based, knowledgerich level, a middle tier called the knowledge description level in [START_REF] Abecker | Toward a Technology for Organizational Memories[END_REF] and the logic tier in [START_REF] Glushko | The Discipline of Organizing[END_REF]. The knowledge-rich level has the central role of a shared language to connect people to people, people to information, and information to information [START_REF] Abecker | Ontologies for knowledge management[END_REF], and the level includes ontologies as a core enabler. As major knowledge-based KM applications, ontologies are used for the following three general purposes [START_REF] Abecker | Ontologies for knowledge management[END_REF]: to support knowledge visualization; to support knowledge search, retrieval, and personalization; to serve as the basis for information gathering and integration. Fig. 2 represents the main concepts and relationships of our ontology. A system is referred to by several propositional objects: system requirements (sentences and formalized properties), the system model (and its components), observations generally made about verification runs that are organized within verification endeavors. A diagnosis is a conjecture that certain of the components are faulty (Abnormal) and the rest normal, stemming from an observation inconsistent with the system descriptions. All information on a particular verification run is not detailed here, and include, among others, checked properties, run outcomes, model-checker options and statistics.

Technical Aspects of the Tiers of the Organizing System

Modern applications separate the storage of data, the business logic or functions that use the data, and the user interface or presentation components through which users or other applications interact with the data. For each tier, we kept the design as simple as possible, relying on straightforward and widely-used solutions.

The storage tier.

As mentioned in the introduction, a practical difficulty of using model checkers "in the large" is the management of all (generated) data during the verification endeavors. A disciplined recording of information on the different models during the verification phase becomes even more indispensable when errors are found, because, once the erroneous models have been corrected and re-verified, all models that have been verified previously and which are affected by the error should be re-verified as well [START_REF] Ruys | Managing the verification trajectory[END_REF]. We propose to use a Software Configuration Management (SCM) system to control the versioned artifacts produced during modelling and verification phases.

We do not impose any arrangement to the verification engineers. Hence, a verification endeavor is associated with a directory, with a total freedom to arrange endeavors and runs in a recursive manner. Using the combination of SCM feature and tools (e.g., the tool make) able to process automatically the building of software artifacts, each engineer organizes her endeavors in an arranged hierarchy or a rake of runs.

Complex objects such as set of properties or models decomposition are managed in the same manner, with a root directory and a freedom of organization. In order to ease the integration of each single object at the logical level, an XML description file stores information about the objects, a feature called a version description in a SCM system. The structure of the XML (its schema) is used by the software components (providing ingest and access features) to maintain an up-to-date ontological network in the logical level.

Avoiding the building of an information silo was also a concern. A silo is an insular management system that is unable to operate with any other systems. Files, directories, XML description, source version control ensure an access independent of any management system.

The access tier.

One of the main goals of an Organizing System is to support the design and implementation of the actions, functions or services that make use of the resources. In classical 3-tier architecture, the presentation tier is the tier in which users interact with an application. Typical user interactions are ingestions (importing new resources into the OS), searches, browsing, tagging and annotations, retrieval, information extraction. An Organizing System is also intended to interact with other applications and should provide information exchange features with or without semantic transformations. Because any of the user interactions mentioned above might be performed in a dedicated tool, in this perspective, the presentation layer is merely an access layer and its main concern is tool interoperability. Among possible solutions, we choose a pragmatic approach, called conceptual interoperability based on the concept of the federation of models [START_REF] Guychard | Conceptual interoperability through Models Federation[END_REF] and its open source tooling (http://research.openflexo.org). The Openflexo tool set provides support for building conceptual views expanding upon existing models and tools.

The ontological tier.

From a conceptual perspective, the ontological layer is divided into two parts. The semantic network of types, on one hand, consists of semantic types linked by types of semantic relations, equivalent to an entity-relationship model or an UML class diagram). The semantic network of objects, on the other hand, contains a node for each fine-grained object plus nodes for the composite objects, each of which is assigned to one or more semantic types and linked to other objects by semantic relations.

The ontological tier is evolving continuously over time, because new resources types and new resources can be added at any time. People and organizations developing information and knowledge application systems are using different ontologies and there will be a need to reconcile these ontologies with a common upper ontology. We use the CIDOC CRM (http://www.cidoc-crm.org/official_release_cidoc.html), a standardized structure (ISO 21127:2014) for describing the implicit and explicit concepts and relationships used in cultural heritage documentation, as an upper ontology.

Technically, the ontological layer is stored in a TDB triple store; and we use the Apache Jena API to extract data from and write to RDF graphs (http://jena.apache.org/). There is an isomorphism between physical objects in the storage layer and semantic objects in the ontological layer; it is the access layer responsibility to maintain the isomorphism when items are updated in the storage tier.

An Organizing System to perform and enable the verifier's activities

Our team develops and maintains a model-checking toolkit. The system is described using the Fiacre language [START_REF] Berthomieu | Fiacre: an Intermediate Language for Model Verification in the Topcased Environment[END_REF], which enables the specification of interacting behaviors and timing constraints through timed-automata. Our approach, called Contextaware Verification, focuses on the explicit modelling of the environment as one or more contexts. Interaction contexts are described with the Context Description Language (CDL). CDL enables also the specification of requirements through predicates and properties. The requirements are verified within the contexts that correspond to the environmental conditions in which they should be satisfied. All these developments are implemented in the OBP tool kit [START_REF] Dhaussy | Improving Model Checking with Context Modelling[END_REF] and are freely available 1 .

Recall that this research work aims to contribute to the solving of two practical problems: to deal with many verification objects (that have to be carefully managed and often re-verified); and to facilitate the judgement of the validation problem (is the formalized problem statement an adequate reflection of the actual problem?).

The first problem requires essentially a methodology of verification and a support tool. Each verification engineer work process is made of slightly different activities using their own resources through different verification tools; hence each engineer defines her methodology or uses a given one. Our aim is to provide an integration framework for the tools and methodologies; this is precisely the goal of an Organizing System to arrange resources and to support interactions with.

The second problem is part of a larger problem of computer-supported diagnosis that, as mentioned in Section 2.2, has been addressed with a multitude of techniques, among which we choose a model-based approach. Our hypothesis is that the logical tier of the OS, knowledge-rich and ontology-based, serves as the basis for information gathering, information integration, knowledge creation and knowledge sharing. Thanks to the access layer, tools interoperability is made easier and tools collaboration provides the user with the required help. The OS acts as a backbone to add tools supporting techniques such as case-based reasoning.

Case-based reasoning.

The main limitation of model-based diagnosis is that it requires a model. What does mean a modelling error in a model-checking approach? It means that, upon studying the error it is discovered that the model does not reflect the design of the system and that implies a correction of the model [START_REF] Baier | Principles of model checking[END_REF]. Hence it means that the design is the subject of diagnosis, and that we need a correct model of the design (that we do not have, in essence) to apply model-based reasoning. Fortunately, we can use case-based reasoning (CBR) to find this correct model. In CBR, a reasoner remembers previous situations similar to the current one and uses them to solve the new problem. So, we need to describe the old cases (called Problem Cases) in the OS using a Problem Case Template (mainly the problem statement, the formalized properties, the "correct" model and implementations for different model-checkers). Reasoning on a new case (called Sample Case) suggests "a model of reasoning that incorporates problem solving, understanding, and learning and integrates all with memory processes [START_REF] Kolodner | Case-based reasoning[END_REF]." A work using pattern for relate Problems and Sample Cases is under submission [START_REF] Leilde | Organizing problem and sample cases for model-based diagnosis[END_REF].

Related work

The research work of Theo C. Ruys [START_REF] Ruijs | Towards Effective Model Checking[END_REF] is the closest to ours, particularly for the first research problem addressed in this paper. The concept of managing the verification trajectory [START_REF] Ruys | Managing the verification trajectory[END_REF], by Ruys and Brinksma, has been a seminal paper for the understanding of the verification cycles and the need for a Software Configuration Management System for the verification "in the large" of real-life systems. We differ in scope because Ruys's work is focused on the use of the SPIN model-checker while we are looking for an agnostic view of model-checking that implies an intermediate abstract (and ontological) layer between the verification engineer and her verification objects. Because any resources ingested in the Organizing System is going through the access layer, the only extra price to pay for the verification engineer is to describe her organization documents (e.g. the version descriptor used in [START_REF] Ruys | Managing the verification trajectory[END_REF]; containing a description of the files included in a particular version) in a schema (e.g. in a XML Schema definition) and to relate schema components (e.g. element and attribute declarations and complex and simple type definitions) with semantic types and/or semantic relations of the OS ontological layer. If the verifiers' schema components does not exist in the ontological layer, the verification engineer has to indicate whether semantic constructs they refine and missing components will be added in the ontology. Thanks to this mapping, the particular view of any verification engineer will be shared with the other users of the OS.

Hence, our work and Ruys's work address the same issues and rely on the same solution scheme. However, our approach has two main advantages: it supports any model-checking tool and method and enlarges the community of OS users; the ontological layer permits shared knowledge and reasoning over different model-checking verification experiences, working across boundaries.

The research work of the Divine team [START_REF] Barnat | DiVinE 3.0 -An Explicit-State Model Checker for Multithreaded C & C++ Programs[END_REF] was a second source of inspiration. Divine verifies models in multiple input formats and has excellent execution performances using a cluster of multi-core machines and partial order reduction techniques, breaking through the limits of the state space explosion problem. However, our work has been more influenced by side products of the Divine team, mainly issues related to the BEEM benchmark management [START_REF] Pelánek | BEEM: Benchmarks for explicit model checkers[END_REF] and the automation of the verification process [START_REF] Barnat | DiVinE 3.0 -An Explicit-State Model Checker for Multithreaded C & C++ Programs[END_REF] by Pelanek. He agrees for the need for classifications based on a model structure and also classifications based on features of state spaces, which relate to model-based or experiential diagnosis introduced in Section 2.2. Pelanek's work perspectives mention a long term goal intended to develop an automated 'verification manager', which would be able to learn from experience [START_REF] Pelánek | Model classifications and automated verification[END_REF]. Our approach is more humble and pragmatic: to provide the user with the bigger possible set of knowledge about verification, including an ontological classification of the problem and the solution spaces. Thanks to the arranged knowledge within the Organizing System, the verification engineer can plug her plug tools to address the automated verification manager issue in her way

Conclusion

Verification "in the large" suffers of two practical problems: the verifier has to deal with many verification objects that have to be carefully managed and often reverified; it is often difficult to judge whether the formalized problem statement is an adequate reflection of the actual problem. We designed and built a prototype of an organizing system (OS) -an intentionally arranged collection of resources and the interactions they supportthat makes easier the management of verification objects and supports reasoning interactions that facilitates diagnosis decisions. Key points and driving issues of this research work are the ability of the OS to host a large variety of model-checking tools, techniques and methods; and the interoperability of the OS with external tools, providing the user with the freedom to use the proper approach to her problems.

However, we keep in mind that "any verification using model-based techniques is only as good as the model of the system. [START_REF] Baier | Principles of model checking[END_REF]." Hence, a particular attention to the validity of the problem formalization will drive our future research efforts.

Fig. 1 .

 1 Fig. 1. The specification-design-modelling-verification process and its cycles

Fig. 2 .

 2 Fig. 2. Main elements of the ontological level.

1OBP Languages and Tool kit website: http://www.obpcdl.org