F Auzanneau

wired networks

Chaos time-domain reflectometry for distributed diagnosis of complex topology

Introduction: In many application domains, wire faults can have dramatic consequences. Live wire diagnosis is often required to ensure permanent monitoring of the health of embedded cables. Reflectometry methods are among the most commonly used methods for this purpose [START_REF] Auzanneau | Wire troubleshooting and diagnosis: review and perspectives[END_REF]. Similarly to Radar, reflectometry injects a probe signal at one end of the network under test. This signal propagates along the cables and each impedance discontinuity met (junction or defect) sends a part of its energy back to the injection port. The analysis of the measured signal provides information on the presence, the location and the type of these discontinuities. Smart energy grids are more and more used for the intelligent distribution of energy generated by several inhomogeneous sources, such as wind farms, solar power plants, nuclear and fuel power plants. They also provide additional services, such as integrated communication, sensing and measurement, to improve reliability and flexibility. In this context, the electric network structure is often complex, comprising several split points and multiple branches. Standard reflectometry methods are not suited for monitoring and diagnosis of this kind of networks, because the injected signal bounces at the junctions and creates multiple copies of itself, which propagate several times in all the cables before coming back to the injection point. The measured reflectogram is very complex and can provide ambiguous location for the defects. Ravot et al. in [START_REF] Ravot | Distributed reflectometry-based diagnosis for complex wired networks[END_REF] have proposed distributed reflectometry where several reflectometers are used simultaneously to improve the diagnosis result. This requires that the signals from each sensor do not interfere with the other distributed sensors, in order to prevent any false alarm.

Chaos theory describes systems whose behaviour is highly dependent on initial conditions, and becomes very difficult to predict in time. Chaos theory has grown and been applied in many domains, from astrophysics to economics, computer science, aerodynamics, chemistry and biology. Attractors and bifurcation diagrams, among others, help show the sensitive dependence of the evolution of a chaotic system on initial conditions. Recent works have also shown its very promising potential for high precision detection and location of defects in wires [START_REF] Xu | Location of wire faults using chaotic signal generated by an improved Colpitts oscillator[END_REF][START_REF] Zhang | Wiring fault detection with Boolean-chaos time-domain reflectometry[END_REF][START_REF] Xu | Chaos time domain reflectometry for fault location on live wires[END_REF], leading to the new chaos time-domain reflectometry (CTDR) method.

In this Letter, chaotic signals show very good auto-correlation and cross-correlation characteristics and the capacity of generating virtually an infinite number of orthogonal signals. This feature is exploited for the distributed diagnosis of complex topology networks.

Chaos time-domain reflectometry:

In CTDR, chaotic signals are generated by logistic and Bernoulli maps [START_REF] Yang | A signal model based on combination chaotic map for noise radar[END_REF]. The logistic map [START_REF] Auzanneau | Wire troubleshooting and diagnosis: review and perspectives[END_REF], with an initial parameter set {x 0 , k}, is used to generate the parameters of the Bernoulli map ( 2)

x m = kx m-1 (1 -x m-1 )
(1)

y m,n+1 = B m y m,n + 0.5 if y m,n , 0 B m y m,n -0.5 if y m,n ≥ 0 n = 1, ..., N (2)
R(t) = S(t) ⊗ S c (t) (5)
Knowing the propagation speed in the cables enables to plot R as a function of the distance in the network from the injection point. The peaks on the reflectogram plot show the impedance discontinuities, either junctions, loads at cables ends or defects.

An example of complex topology has been taken from [START_REF] Ulrich | Inference of wired network topology using multipoint reflectometry[END_REF], as shown in Fig. 2. Fig. 3 plots the reflectogram when the sensor is placed at point A: although the topology does not seem very complex, the plot shows a high number of peaks, some of them further away than the largest distance in the network (from A to G: 81.1 m). The measured noise level is close to -30 dB, according to formula (4).

Online distributed diagnosis:

In such a complex reflectogram, it is not easy to precisely locate a defect in the branches of the network: a single sensor at point A cannot tell a defect from branches F-GtoF-H or from branches D-Et oD -F. To provide unambiguous defect location, one must add other sensors at other ends of the network [START_REF] Ravot | Distributed reflectometry-based diagnosis for complex wired networks[END_REF]. Such a distributed diagnosis enables to compare various reflectograms to locate more precisely the defects and cancel ambiguities. However, to prevent a signal from one sensor from triggering a false alarm in another sensor, the signals from all the reflectometers must have crosscorrelation levels lower than or similar to the noise level n:

max i=j[{sensors} S c,i (t) ⊗ S c,j (t) ≤ n(t) (6)
As shown in Fig. 1b and formula (4), CTDR naturally achieves this aim.

Conclusion:

The efficiency of CTDR for the distributed diagnosis of complex topology wired networks has been shown. CTDR's capacity of generating a quasi-infinite number of low auto-correlation sidelobes and low cross-correlation signals enables several reflectometers to simultaneously inject their signals in the cables, without any interference. Very complex topologies, with a high number of branches, can be addressed, as it is shown that adding 20 concurrent sensors still enables to process the reflectograms. Increasing the length of the chaotic signal enables to decrease the noise level.

Future work will investigate CTDR's very high noise resistance and noise management, applied to the diagnosis of soft defects in cables.

Fig. 1 a

 1 Fig. 1 a Auto-correlation b Cross-correlation of two chaotic signals, using N = 10, M = 200, k 1 = 3.9 and k 2 = 3.900001, and random initial conditions x 0

Fig. 3 Fig. 1 4 )

 314 Fig. 2 Complex network topology

Fig. 4 Fig. 4

 44 Fig. 4 Reflectogram from point A, with four emitting sensors at points C, E, G and H. CTDR signal's parameters: N = 50, M = 200, k = 3.9 + rand (0,1)/100A more complex case has been simulated in Fig.5with 10 (red curves) and 20 (blue curves) additional sensors emitting concurrently with sensor A. The reflectogram from sensor A remains processable although the noise level has increased to -24 dB for 10 sensors and close to -20 dB for 20 sensors.

Fig. 5

 5 Fig. 5 Reflectogram from point A, with 10 (red curves) and 20 (blue curves) random emitting sensors

©

  The Institution of Engineering and Technology 2016 Submitted: 2 November 2015 doi: 10.1049/el.2015.3456 One or more of the Figures in this Letter are available in colour online. F. Auzanneau (CEA, LIST, F-91191 Gif-sur-Yvette, France) ✉ E-mail: fabrice.auzanneau@cea.fr


Jean-Christophe Léchenet
email: jean-christophe.lechenet@cea.fr

Nikolai Kosmatov
email: nikolai.kosmatov@cea.fr

Pascale Le Gall
email: pascale.legall@centralesupelec.fr

Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices

Program slicing can be used to reduce a given initial program t oas m a l l e ro n e( aslice) which preserves the behavior of the initial program with respect to a chosen criterion. Verification and validation (V&V) of software can become easier on slices, but require particular care in presence of errors or non-termination in order to avoid unsound results or a poor level of reduction in slices.

This article proposes a theoretical foundation for conducting V&V activities on a slice instead of the initial program. We introduce the notion of relaxed slicing that remains efficient even in presence of errors or non-termination, and establish an appropriate soundness property. It allows us to give a precise interpretation of verification results (absence or presence of errors) obtained for a slice in terms of the initial program. Our results have been proved in Coq.

Introduction

Context. Program slicing was initially introduced by Weiser [START_REF] Weiser | Program slicing[END_REF][START_REF] Weiser | Programmers use slices when debugging[END_REF]a sat e c hnique allowing to decompose a given program into a simpler one, called a program slice, by analyzing its control and data flow. In the classic definition, a (program) slice is an executable program subset of the initial program whose behavior must be identical to a specified subset of the initial program's behavior. This specified behavior that should be preserved in the slice is called slicing criterion. A common slicing criterion is a program point l. For the purpose of this paper, we prefer this simple formulation to another criterion (l, V ) where a set of variables V is also specified. Informally speaking, program slicing with respect to the criterion l should guarantee that any variable v at program point l takes the same value in the slice and in the original program. Since Weiser's original work, many researchers have studied foundations of program slicing (e.g. [4-6, 8, 11, 14,20, 26-28]). Numerous applications of slicing have been proposed, in particular, to program understanding, software maintenance, debugging, program integration and software metrics. Comprehensive surveys on program slicing can be found e.g. in [START_REF] Binkley | A survey of empirical results on program slicing[END_REF][START_REF] Silva | A vocabulary of program slicing-based techniques[END_REF][START_REF] Tip | A survey of program slicing techniques[END_REF][START_REF] Xu | A brief survey of program slicing[END_REF]. In recent classifications of program slicing, Weiser's original approach is called static backward slicing since it simplifies the program statically, for all possible executions at the same time, and traverses it backwards from the slicing criterion in order to keep those statements that can influence this criterion. Static backward slicing based on control and data dependencies is also the purpose of this work.

Goals and Approach. Verification and Validation (V&V) can become easier on simpler programs after "cutting off irrelevant branches" [START_REF] Chebaro | Program slicing enhances a verification technique combining static and dynamic analysis[END_REF][START_REF] Ge | DyTa: dynamic symbolic execution guided with static verification results[END_REF][START_REF] Harman | Using program slicing to simplify testing[END_REF][START_REF] Kiss | Combining static and dynamic analyses for vulnerability detection: illustration on heartbleed[END_REF]. Our main goal is to address the following research question:

(RQ) Can we soundly conduct V&V activities on slices instead of the initial program? In particular, if there are no errors in a program slice, what can be said about the initial program? And if an error is found in a program slice, does it necessarily occur in the initial program?

We consider errors determined by the current program state such as runtime errors (that can either interrupt the program or lead to an undefined behavior). We also consider a realistic setting of programs with potentially non-terminating loops, even if this non-termination is unintended. So we assume neither that all loops terminate, nor that all loops do not terminate, nor that we have a preliminary knowledge of which loops terminate and which loops do not.

Dealing with potential runtime errors and non-terminating loops is very important for realistic programs since their presence cannot be a priori excluded, especially during V&V activities. Although quite different at first glance, both situations have a common point: they can in some sense interrupt normal execution of the program preventing the following statements from being executed. Therefore, slicing away (that is, removing) potentially erroneous or nonterminating sub-programs from the slice can have an impact on soundness of program slicing.

While some aspects of (RQ) were discussed in previous papers, none of them provided a complete formal answer in the considered general setting (as we detail in Sects. 2 and 6 below). To satisfy the traditional soundness property, program slicing would require to consider additional dependencies of each statement on previous loops and error-prone statements. That would lead to inefficient (that is, too large) slices, where we would systematically preserve all potentially erroneous or non-terminating statements executed before the slicing criterion. Such slices would have very limited benefit for our purpose of performing V&V on slices instead of the initial program.

This work proposes relaxed slicing, where additional dependencies on previous (potentially) erroneous or non-terminating statements are not required. This approach leads to smaller slices, but needs a new soundness property. We state and prove a suitable soundness property using a trajectory-based semantics, and show how this result can justify V&V on slices by characterizing possible verification results on slices in terms of the initial program. The proof has been formalized in the Coq proof assistant [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF] and is available in [START_REF]Formalization of relaxed slicing[END_REF].

The Contributions of this work include:

-a comprehensive analysis of issues arising for V&V on classic slices; -the notion of relaxed slicing (Definition 6) for structured programs with possible errors and non-termination, that keeps fewer statements than it would be necessary to satisfy the classic soundness property of slicing; -a new soundness property for relaxed slicing (Theorem 1); -a characterization of verification results, such as absence or presence of errors, obtained for a relaxed slice, in terms of the initial program, that constitutes a theoretical foundation for conducting V&V on slices (Theorems 2, 3); -a formalization and proof of our results in Coq.

Paper Outline. Section 2 presents our motivation and illustrating examples. The considered language and its semantics are defined in Sect. 3. Section 4 defines the notion of relaxed slice and establishes its main soundness property. Next, Sect. 5 formalizes the relationship between the errors in the initial program and in a relaxed slice. Finally, Sects. 6 and 7 present the related work and the conclusion with some future work.

Motivation and Running Examples

Errors and Assertions. We consider errors that are determined by the current program state1 including runtime errors (division by zero, out-of-bounds array access, arithmetic overflows, out-of-bounds bit shifting, etc.). Some of these errors do not always interrupt program execution and can sometimes lead to an (even more dangerous) undefined behavior, such as reading or writing an arbitrary memory location after an out-of-bounds array access in C. Since we cannot take the risk to overlook some of these "silent runtime errors", we assume that all threatening statements are annotated with explicit assertions assert(C) placed before them, that interrupt the execution whenever the condition C is false. This assumption will be convenient for the formalization in the next sections: possible runtime errors will always occur in assertions. Such assertions can be generated syntactically (for example, by the RTE plugin of the Frama-C toolset [START_REF] Kirchner | Frama-C: a software analysis perspective[END_REF]f o r C programs). For instance, line 10 in Fig. 1a prevents division by zero at line 11, while line 13 makes explicit a potential runtime error at line 14 if the array a is known to be of size N. In addition, the assert(C) keyword can be also used to express any additional user-defined properties on the current state.

Most previous applications of slicing to debugging used slices in order to better understand an already detected error, by analyzing a simpler program rather than a more complex one [START_REF] Binkley | Theoretical foundations of dynamic program slicing[END_REF][START_REF] Silva | A vocabulary of program slicing-based techniques[END_REF][START_REF] Tip | A survey of program slicing techniques[END_REF]. Our goal is quite different: to perform V&V on slices in order to discover yet unknown errors, or show their absence (cf. (RQ)). The interpretation of absence or presence of errors in a slice in terms of the initial program requires solid theoretical foundations.

Classic Soundness Property. Let p be a program, and q a slice of p w.r.t. a slicing criterion l. The classic soundness property of slicing (cf. [START_REF] Barraclough | A trajectory-based strict semantics for program slicing[END_REF]Definition 2.5] or [START_REF] Reps | The semantics of program slicing[END_REF]Slicing Th.]) can be informally stated as follows. Property 1. Let σ be an input state of p. Suppose that p halts on σ. Then q halts on σ and the executions of p and q on σ agree after each statement preserved in the slice on the variables that appear in this statement. 2This property was originally established for classic dependence-based slicing for programs without runtime errors and only for executions with terminating loops: nothing is guaranteed if p does not terminate normally on σ. Let us show why this property does not hold in presence of potential runtime errors or non-terminating loops.

Illustrating Examples. Figure 1a presents a simple (buggy) C-like program that takes as inputs an array a of length N and an integer k (with 0 k 100, 0 N 100), and computes in two different ways the average of the elements of a. We suppose that all variables and array elements are unsigned integers, and all elements of a whose index is not a multiple of k are zero, so it suffices to sum array elements over the indices multiples of k and to divide the sum by N. The sum is computed twice (in s1 at lines 3-8 and in s2 at lines 9-16), and the averages avg1 and avg2 are computed (lines 17-20) and compared (lines [START_REF] Kirchner | Frama-C: a software analysis perspective[END_REF][START_REF] Kiss | Combining static and dynamic analyses for vulnerability detection: illustration on heartbleed[END_REF]. We assume that necessary assertions with explicit guards (at lines [START_REF] Ball | Slicing programs with arbitrary control-flow[END_REF][START_REF] Blazy | Verified validation of program slicing[END_REF][START_REF] Chebaro | Program slicing enhances a verification technique combining static and dynamic analysis[END_REF][START_REF] Harman | Using program slicing to simplify testing[END_REF][START_REF] Hierons | Using program slicing to assist in the detection of equivalent mutants[END_REF] are inserted to prevent runtime errors.

Figure 1b shows a (classic dependence-based) slice of this program with respect to the statement at line 18. Intuitively, it contains only statements (at lines 1, 3, 4, 6, 7, 18) that can influence the slicing criterion, i.e. the values of variables that appear at line 18 after its execution. 3 In addition, we keep the assertions to prevent potential errors in preserved statements. Similarly, Fig. 1c shows a slice with respect to line 20, again with protecting assertions.

Figure 2 summarizes the behavior of the three programs of Fig. 1 on some test data. The elements of a do not matter here. Suppose we found an error at line 17 in slice (b) provoked by test datum σ 4 . Program (a) does not contain the same error: it fails earlier, at line 13. We say that the error at line 17 in slice (b) is hidden by the error at line 13 of the initial program. Similarly, test datum σ 5 provokes an error at line 17 in slice (b) while this error is hidden by an error at line 10 in (a). In fact, the error at line 17 cannot be reproduced on the initial program, so we say that it is totally hidden by other errors.

For slice (c), detecting an error at line 10 on test datum σ 5 would allow us to observe the same error in (a). However, if this error in slice (c) is also provoked by test datum σ 3 , this test datum does not provoke any error in (a) because the loop at line 4 does not terminate. We say that this error is (partially) hidden by a non-termination of the loop at line 4.

These examples clearly show that Property 1 is not true in presence of errors or non-terminating loops for classic slices. Indeed, the executions of p and q may disagree at least for two reasons:

(i) a previously executed non-terminating loop not preserved in the slice, or (ii) a previously executed failing statement not preserved in the slice. Let us consider another example related to error-free programs. If we suppose that 0 < k 100, 0 < N 100, and replace N/k by (N-1)/k at line 11 of Fig. 1, neither slice contains any error. If we manage to verify the absence of errors on both slices, can we be sure that the initial program is error-free as well? Bigger Slices vs. Weaker Soundness Property. One solution (adopted by [START_REF] Harman | Slicing programs in the presence of errors[END_REF][START_REF] Podgurski | A formal model of program dependences and its implications for software testing, debugging, and maintenance[END_REF][START_REF] Ranganath | A new foundation for control dependence and slicing for modern program structures[END_REF]), cf. Sect. 6) proposes to ensure Property 1 even in presence of errors and potentially non-terminating loops by considering additional dependencies. This approach would basically lead to always preserving in the slice any (potentially non-terminating) loop or error-prone statement that can be executed before the slicing criterion. The resulting slices would be much bigger, and the benefit of performing V&V on slices would be very limited.

For instance, to ensure that the executions of program (a) and slice (b) activated by test datum σ 4 agree on all statements of slice (b), line 13 should be preserved in slice (b). That would result (by transitivity of dependencies) in keeping e.g. the loop at line 12 and lines 9-11 in slice (b) as well. Similarly, the loop at line 4 should be kept in slice (c) to avoid disagreeing executions for test datum σ 3 . The slices can become much bigger in this approach.

In this paper we propose relaxed slicing, an alternative approach that does not require to keep all loops or error-prone statements that can be executed before the slicing criterion, but ensures a weaker soundness property. We demonstrate that the new soundness property is sufficient to justify V&V on slices instead of the initial program. In particular, we show that reasons (i) and (ii) above are the only possible reasons of a hidden error, and investigate when the absence of errors in slices implies the absence of errors in the initial program.

The Considered Language and Its Semantics

Language. In this study, we consider a simple WHILE language (with integer variables, fixed-size arrays, pure expressions, conditionals, assertions and loops) that is representative for our formalization of slicing in presence of runtime errors and non-termination. The language is defined by the following grammar:

Prog ::= Stmt * Stmt ::= l : skip | l : x = e | if (l : b) Prog else Prog | while (l : b) Prog | l : assert (b, l ′ )
where l, l ′ denote labels, e an expression and b a boolean expression. A program (Prog) is a possibly empty list of statements (Stmt). The empty list is denoted λ, and the list separator is ";". We assume that the labels of any given program are distinct, so that a label uniquely identifies a statement. Assignments, conditions and loops have the usual semantics. As its name suggests, skip does nothing.

The assertion assert(b, l ′ ) stops program execution in an error state (denoted ε)ifb is false, otherwise execution continues normally. As said earlier, we assume that assertions are added to protect all threatening statements. The label l ′ allows us to associate the assertion with another statement that should be protected by the assertion (e.g. because it could provoke a runtime error). An assertion often protects the following line (like in Fig. 1, where the protected label is not indicated). Two simple cases however need more flexibility (cf. Fig. 3). Some assertions have to be themselves protected by assertions when they contain a threatening expression. Figure 3a gives such an example where, instead l3 : assert (z != 0, l1); l2 : assert (w != 0, l); l1 : assert ((y/z) + 1 != 0, l); l : z = x / ((y/z) + 1) + v/w; Assertions can be also added by the user to check other properties than runtime errors. If the user does not need to indicate the protected statement, they can choose for l ′ either the label l of the assertion itself or any label not used elsewhere in the program. User-defined assertions should be also protected against errors by other assertions if necessary.

Semantics. Let p be a program. A program state is a mapping from variables to values. Let Σ denote the set of all valid states, and Σ ε = Σ ∪{ε}, where ε is the error state. Let σ be an initial state of p.T h etrajectory of the execution of p on σ, denoted T p σ, is the sequence of pairs (l 1 ,σ 1 ) ...(l k ,σ k ) ... , where l 1 ,...,l k ,... is the sequence of labels of the executed instructions, and σ i is the state of the program after the execution of instruction l i . T can be seen as a (partial) function

T : Prog → Σ → Seq(L × Σ ε )
where Seq(L × Σ ε ) is the set of sequences of pairs (l, σ) ∈ L × Σ ε . Trajectories can be finite or (countably) infinite. A finite subsequence at the beginning of a trajectory T is called a prefix of T . The empty sequence is denoted . Let ⊕ be the concatenation operator over sequences. For a finite trajectory T , we denote by LS σ (T ) the last state of T (i.e. the state component of its last element) if T = ,a n dσ otherwise. The definition of T 1 ⊕ T 2 is standard if T 1 is finite. If T 1 is infinite or ends with the error state ε, then we set T 1 ⊕ T 2 = T 1 for any T 2 ( a n de v e ni fT 2 is not well-defined, in other words, ⊕ performs lazy evaluation of its arguments).

We denote by E an evaluation function for expressions, that is standard and not detailed here. For any (pure) expression e and state σ ∈ Σ, E e σ is the evaluation of expression e using σ to evaluate the variables present in e.T h e error state is only reached through a failed assert. Thanks to the assumption that all potentially failing statements are protected by assertions, we do not need to model errors in expressions or other statements: errors always occur in assertions. We also suppose for simplicity that all variables appearing in p are initialized in any initial state of p, that ensures the absence of expressions that cannot be evaluated due to an uninitialized variable. These assumptions slightly simplify the presentation without loss of generality for our purpose: loops and errors (in assertions) are present in the language.

Figure 4 gives the inductive definition of T for any valid state σ ∈ Σ.T h e definitions for a loop and a conditional rely on the notation (v → T 1 ,T 2 ) also defined in Fig. 4. For any state σ, variable x and value v, σ[x ← v] denotes σ overridden by the association x → v. Notice that in the definitions for a sequence and a loop, it is important that ⊕ does not evaluate the second parameter when the first trajectory is infinite or ends with the error state since the execution of the remaining part is not defined in this case. Thus ε can appear only once at the very end of a trajectory.

We illustrate these definitions on slice (b) of Fig. 1, denoted p b . For every initial state σ of p b and unsigned integer i, we define

σ i = σ[s 1 ← (i•a[0] mod M u )],
where M u denotes the maximal representable value of an unsigned integer. Then the trajectory on σ 3 is infinite, while the trajectory on σ 5 leads to an error:

T p b σ3 = (1,σ 0 3 )(3,σ 0 3 )(4,σ 0 3 )(5,σ 0 3 )(6,σ 1 3 )(7,σ 1 3 )(4,σ 1 3 )(5,σ 1 3 )(6,σ 2 3 )(7,σ 2 3 ) ... , T p b σ5 = (1,σ 0 5 )(3,σ 0 5 )(4,σ 0 5 )(17,ε) .
4 Relaxed Program Slicing For instance, in Fig. 1a, lines 5-7 are control-dependent on line 4, while lines 13-15 are control-dependent on line 12.

To define data dependence, we need the notion of (finite syntactic) paths. Let us denote again by ⊕ the concatenation of paths, extend ⊕ to sets of paths as the set of concatenations of their elements, and denote by " * " Kleene closure.

Definition 2 (Finite Syntactic Paths). The set of finite syntactic paths P(p) of a program p is inductively defined as follows:

P( λ )={λ}, P( s; p )=P(s) ⊕P(p), P( l : skip )={l}, P( l : x = e )={l}, P( if (l : b) p else q )={l}⊕(P(p) ∪P(q)), P( while (l : b) p )=({l}⊕P(p)) * ⊕{l}, P( l : assert(b, l ′ ) )={l}.

For a given label l, let def(l) denote the set of variables defined at l (that is, def(l)={v} if l is an assignment of variable v,a n d∅ otherwise), and let ref(l) be the set of variables referenced at l.I fl designates a conditional (or a loop) statement, ref(l) is the set of variables appearing in the condition; other variables appearing in its branches (or loop body) do not belong to ref(l). We denote by used(l) the set def(l) ∪ ref(l). Definition 3 (Data Dependence D d ). Let l and l ′ be labels of a program p. We say that there is a data dependency l

D d --→ p l ′ if def(l) = ∅ and def(l) ⊆ ref(l ′ )
and there exists a path π = π 1 lπ 2 l ′ π 3 ∈P(p) such that for all l ′′ ∈ π 2 , def(l ′′ ) = def(l).E a c hπ i may be empty.

For instance, in Fig. 1b, line 18 is data-dependent on line 1 (with π = 1, 3, 4, 17, 18) and on line 6 (with π =1 , 3, 4, 5, 6, 7, 4, 17, 18), while line 6 is data-dependent on lines 1, 3, 6 and 7.

A slice of p is expected to be a quotient of p, that is, a well-formed program obtained from p by removing zero, one or more statements. A quotient can be identified by the set of labels of preserved statements. Notice that when a conditional (or a loop) statement is removed, it is removed with all statements of its both branches (or its loop body) to preserve the structure of the initial program in the quotient.

Given a dependence relation D and L 0 ⊆ L(P ), the slice based on D w.r.t. L 0 will be also identified by the set of labels of preserved statements. The following lemma justifies the correctness of the definitions of slices given hereafter. We denote by D * the reflexive transitive closure of D, and by (D * ) -1 (L 0 )t h es e to f all labels l ′ ∈ L(p) such that there exists l ∈ L 0 with l ′ D * --→ p l.

Lemma 1. Let L 0 ⊆ L(P ).IfD is a dependence relation on p such that D c ⊆D, then (D * ) -1 (L 0 ) is the set of labels of a (uniquely defined) quotient of p.

Assertion Dependence and Relaxed Slices

Soundness of classic slicing for programs without runtime errors or non-terminating loops can be expressed by Property 1 in Sect. 2. As we illustrated, to generalize this property in presence of runtime errors and for non-terminating executions one would need to add additional dependencies and systematically preserve in the slice all potentially erroneous or non-terminating statements executed before (a statement of) the slicing criterion. We propose here an alternative approach, called relaxed slicing, where only one additional dependency type is considered. For instance, in Fig. 1a, there would be an assertion dependence of each threatening statement on the corresponding protecting assertion (written on the previous line). Therefore both slices (b) and (c) of Fig. 1 (in which we artificially preserved assertions in Sect. 2) are in fact relaxed slices where assertions are naturally preserved thanks to the assertion dependence.

Assertion dependence brings two benefits. It ensures that a potentially threatening instruction is never kept without its protecting assertion. At the same time, an assertion can be preserved without its protected statement, that is quite useful for V&V that focus on assertions: slicing w.r.t. assertions may produce smaller slices if we do not need the whole threatening statement. For example, a relaxed slice w.r.t. the assertion at line 17 would contain only this unique line.

Notice that a relaxed slice does not require to include potentially erroneous or non-terminating statements that can prevent the slicing criterion from being executed (like in [START_REF] Harman | Slicing programs in the presence of errors[END_REF][START_REF] Podgurski | A formal model of program dependences and its implications for software testing, debugging, and maintenance[END_REF][START_REF] Ranganath | A new foundation for control dependence and slicing for modern program structures[END_REF]). For example, slice (b) does not include the potential error at line 13, and slice (c) does not include the loop of line 4.

Soundness of Relaxed Slicing

We cannot directly compare the trajectory of the original program with a slice, since it may refer to statements and variables not preserved in the slice. We use projections of trajectories that reduce them to selected labels and variables.

Definition 7 (Projection of a State). The projection of a state σ to a set of variables V , denoted σ↓V , is the restriction of σ to V if σ = ε,a n dε otherwise.

Definition 8 (Projection of a Trajectory).

The projection of a one-element sequence (l, σ) to a set of labels L, denoted (l, σ) ↓L,i sd e fi n e da sf o l l o w s :

(l, σ) ↓L = (l, σ↓ used(l)) if l ∈ L, otherwise.
The projection of a trajectory T = (l 1 ,σ 1 ) ...(l k ,σ k ) ... to L, denoted Proj L (T ), is defined element-wise: Proj L (T )= (l 1 ,σ 1 ) ↓L ⊕ ...⊕ (l k ,σ k ) ↓L ⊕ ... .

We can now state and prove the soundness property of relaxed slices.

Theorem 1 (Soundness of a Relaxed Slice). Let L 0 ⊆ L(p) be a slicing criterion of program p.L e tq be the relaxed slice of p with respect to L 0 ,a n d L = L(q) the set of labels preserved in q. Then for any initial state σ ∈ Σ of p and finite prefix T of T p σ, there exists a prefix T ′ of T q σ, such that:

Proj L (T )=Proj L (T ′ )
Moreover, if p terminates without error on σ, T p σ and T q σ are finite, and

Proj L (T p σ)=Proj L (T q σ) Proof. Let σ ∈ Σ, T p σ = (l 1 ,σ 1 )(l 2 ,σ 2 ) ... ,a n dT q σ = (l ′ 1 ,σ ′ 1 )(l ′ 2 ,σ ′ 2
) ... .LetT = (l 1 ,σ 1 ) ...(l i ,σ i ) be a finite prefix of T p σ. By Definition 8,the projections of T q σ and T to L = L(q) have the following form

Proj L (T q σ)= (l ′ 1 ,σ ′ 1 ↓ used(l ′ 1 ))(l ′ 2 ,σ ′ 2 ↓ used(l ′ 2 )) ... , Proj L (T )= (l f (1) ,σ f (1) ↓ used(l f (1) )) ... (l f (j) ,σ f (j) ↓ used(l f (j) )) ,
where j ≤ i and f is a strictly increasing function.

Let us denote by k the greatest natural number such that k ≤ j and such that the prefix of T q σ of length k exists and satisfies (Proj L (T )) k = Proj L ((T q σ) k ), where we denote by U k the prefix of length k for any trajectory U .L e tT ′ = (l ′ 1 ,σ ′ 1 ) ...(l ′ k ,σ ′ k ) be the prefix (T q σ) k . By Definition 8 we have Proj

L (T ′ )= (l ′ 1 ,σ ′ 1 ↓ used(l ′ 1 )) ... (l ′ k ,σ ′ k ↓ used(l ′ k )) . Since (Proj L (T )) k =Proj L (T ′ ), for any m =1, 2,...,k we have l ′ m = l f (m) and σ ′ m ↓ used(l ′ m )=σ f (m) ↓ used(l f (m) ). Set σ 0 = σ ′ 0 = σ.
Let us prove that k = j. We reason by contradiction and assume that k<j. By maximality of k, there can be three different cases:

1. T q σ is of size k,o r 2. l ′ k+1 exists, but l ′ k+1 = l f (k+1) ,o r 3. l ′ k+1 exists, l ′ k+1 = l f (k+1) , but σ ′ k+1 ↓ used(l ′ k+1 ) = σ f (k+1) ↓ used(l f (k+1) ). Since l ′ k = l f (k)
, cases 1 and 2 can be only due to a diverging evaluation of a control flow statement (i.e. if, while or assert) situated in the execution of p between l f (k) and l f (k+1)-1 . If such a statement occurs at label l ′ k = l f (k) , its condition would be evaluated identically in both executions since

σ ′ k ↓ used(l ′ k )= σ f (k) ↓ used(l f (k)
). The first non-equal label l f (k+1) cannot be part of the body of some non-preserved if or while statement between l f (k) +1 and l f (k+1)-1 in p by definition of control dependence (cf. Definition 1). Finally, the divergence cannot be due to an assert in p between l f (k)+1 and l f (k+1)-1 either, because a passed assert has no effect, while a failing assert would make it impossible to reach l f (k+1) in p. Thus a divergence leading to cases 1 and 2 is impossible.

In case 3, the key idea is to remark that

σ ′ k ↓ ref(l ′ k+1 )=σ f (k+1)-1 ↓ ref(l f (k+1) ). Indeed, assume that there is a variable v ∈ ref(l ′ k+1 )=r e f ( l f (k+1) ) such that σ ′ k (v) = σ f (k+1)-1 (v).
The last assignment to v in the execution of p before its usage at l f (k+1) must be preserved in q because of data dependence (cf. Definition 3), so it has a label l ′ u = l f (u) for some 1 u k. By definition of k, the state projections after this statement were equal:

σ ′ u ↓ used(l ′ u )=σ f (u) ↓ used(l f (u)
), so the last values assigned to v before its usage at l f (k+1) were equal, that contradicts the assumption σ ′ k (v) = σ f (k+1)-1 (v). This shows that all variables referenced in l f (k+1) have the same values, so the resulting states cannot differ, and case 3 is not possible either. Therefore k = j,andT ′ satisfies Proj L (T )=Proj L (T ′ ).

If p terminates without error on σ, by the first part of the theorem we have a prefix T ′ of T q σ such that Proj L (T p σ)=P r o j L (T ′ ). If T ′ is a strict prefix of T q σ, this means as before that a control flow statement executed in p causes the divergence of the two trajectories. By hypothesis, there are no failing assertions in the execution of p, therefore it is due to an if or a while. By the same reasoning as in cases 1, 2 above we show that its condition must be evaluated in the same way in both trajectories and cannot lead to a divergence. Therefore, T ′ = T q σ. ⊓ ⊔

Verification on Relaxed Slices

In this section, we show how the absence and the presence of errors in relaxed slices can be soundly interpreted in terms of the initial program.

Lemma 2. Let q be a relaxed slice of p and σ ∈ Σ an initial state of p. If the preserved assertions do not fail in the execution of q on σ, they do not fail in the execution of p on σ either.

Proof. Let us show the contrapositive. Assume that T p σ ends with (l, ε) where l ∈ L(q) is a preserved assertion. Let L = L(q). From Theorem 1 applied to T = T p σ, it follows that there exists a finite prefix T ′ of T q σ such that Proj L (T )=P r oj L (T ′ ). The last state of Proj L (T ′ )i sε, therefore the last state of T ′ is ε too. It means that ε appears in T q σ, and by definition of semantics (cf. Sect. 3) this is possible only if ε is its last state. Therefore T q σ ends with (l, ε) as well.

⊓ ⊔

The following theorem and corollary immediately follow from Lemma 2.

Theorem 2. Let q be a relaxed slice of p. If all assertions contained in q never fail, then the corresponding assertions in p never fail either.

Corollary 1. Let q 1 , ..., q n be relaxed slices of p such that each assertion in p is preserved in at least one of the q i . If no assertion in any q i fails, then no assertion fails in p.

The last result justifies the detection of errors in a relaxed slice.

Theorem 3. Let q be a relaxed slice of p and σ ∈ Σ an initial state of p.W e assume that T q σ ends with an error state. Then one of the following cases holds for p:

( †) T p σ ends with an error at the same label, or ( † †) T p σ ends with an error at a label not preserved in q,o r ( † † †) T p σ is infinite.

Proof. Let L = L(q) and assume that T q σ ends with (l, ε) for some preserved assertion at label l ∈ L. We reason by contradiction and assume that T p σ does not satisfy any of the three cases. Then two cases are possible. First, T p σ ends with (l ′ ,ε) for another preserved assertion at label l ′ ∈ L (with l ′ = l). Then reasoning as in the proof of Lemma 2 we show that T q σ ends with (l ′ ,ε) as well, that contradicts l ′ = l.

Second, T p σ is finite without error. Then the second part of Theorem 1 can be applied and thus Proj L (T p σ)=P r oj L (T q σ). This is contradictory since T q σ contains an error (at label l ∈ L)a n dT p σ does not.

⊓ ⊔

For instance, consider the example of Fig. 1 with 0 < k 100, 0 < N 100. In this case we can prove that slice (b) does not contain any error, thus we can deduce by Theorem 2 that the assertions at lines 5 and 17 (preserved in slice (b)) never fail in the initial program either. If in addition we replace N/k by (N-1)/k at line 11 of Fig. 1, we can show that neither of the two slices of Fig. 1 contains any error. Since these slices cover all assertions, we can deduce by Corollary 1 that the initial program is error-free.

Theorem 3 shows that despite the fact that an error detected in q does not necessary appear in p, the detection of errors on q has a precise interpretation. It can be particularly meaningful for programs supposed to terminate, for which a non-termination within some time τ is seen as an anomaly. In this case, detection of errors in a slice is sound in the sense that if an error is found in q for initial state σ, there is an anomaly (same or earlier error, or non-termination within time τ )i np whose type can be easily determined by running p on σ.

It can be noticed that a result similar to Theorem 3 can be established for non-termination: if T q σ is infinite, then either ( † †)o r( † † †) holds for p.

Related Work

Weiser [START_REF] Weiser | Program slicing[END_REF] introduced the basics of intraprocedural and interprocedural static slicing. A thorough survey provided in [START_REF] Tip | A survey of program slicing techniques[END_REF] explores both static and dynamic slicing and compares the different approaches. It also lists the application areas of program slicing. More recent surveys can be found at [START_REF] Binkley | A survey of empirical results on program slicing[END_REF][START_REF] Silva | A vocabulary of program slicing-based techniques[END_REF][START_REF] Xu | A brief survey of program slicing[END_REF]. Foundations of program slicing have been studied e.g. in [4-6, 8,11, 14, 20, 26-28]. This section presents a selection of works that are most closely related to the present paper.

Debugging and Dynamic Slicing. Program debugging and testing are traditional application domains of slicing (e.g. [START_REF] Agrawal | Debugging with dynamic slicing and backtracking[END_REF][START_REF] Hierons | Using program slicing to assist in the detection of equivalent mutants[END_REF][START_REF] Weiser | Programmers use slices when debugging[END_REF]) where it can be used to better understand an already detected error, to prioritize test cases (e.g. in regression testing), simplify a program before testing, etc. In particular, dynamic slicing [START_REF] Binkley | Theoretical foundations of dynamic program slicing[END_REF] is used to simplify the program for a given (e.g. erroneous) execution. However, theoretical foundations of applying V&V on slices instead of the initial program (like in [START_REF] Chebaro | Program slicing enhances a verification technique combining static and dynamic analysis[END_REF][START_REF] Kiss | Combining static and dynamic analyses for vulnerability detection: illustration on heartbleed[END_REF]) in presence of errors and non-termination, that constitute the main purpose of this work, have been only partially studied.

Slicing and Non-terminating Programs. A few works tried to propose a semantics preserved by classic slicing even in presence of non-termination. Among them, we can cite the lazy semantics of [START_REF] Cartwright | The semantics of program dependence[END_REF], and the transfinite one of [START_REF] Giacobazzi | Non-standard semantics for program slicing[END_REF], improved by [START_REF] Nestra | Transfinite semantics in the form of greatest fixpoint[END_REF]. Another semantics proposed in [START_REF] Barraclough | A trajectory-based strict semantics for program slicing[END_REF] has several improvements compared to the previous ones: it is intuitive and substitutive. Despite the elegance of these proposals, they turn out to be unsuitable for our purpose because they consider non-existing trajectories, that are not adapted to V&V techniques, for example, based on path-oriented testing like in [START_REF] Chebaro | Program slicing enhances a verification technique combining static and dynamic analysis[END_REF][START_REF] Ge | DyTa: dynamic symbolic execution guided with static verification results[END_REF].

Ranganath, et al. [START_REF] Ranganath | A new foundation for control dependence and slicing for modern program structures[END_REF] provides foundations for the slicing of modern programs, i.e. programs with exceptions and potentially infinite loops, represented by control flow graphs (CFG) and program dependence graphs (PDG). Their work gives two definitions of control dependence, non-termination sensitive and non-termination insensitive, corresponding respectively to the weak and strong control dependences of [START_REF] Podgurski | A formal model of program dependences and its implications for software testing, debugging, and maintenance[END_REF] and further generalized for any finite directed graph in [START_REF] Danicic | A unifying theory of control dependence and its application to arbitrary program structures[END_REF]. [START_REF] Ranganath | A new foundation for control dependence and slicing for modern program structures[END_REF] also establishes the soundness of classic slicing with non-termination sensitive control dependence in terms of weak bisimulation, more adapted to deal with infinite executions. Their approach requires to preserve all loops, that results in much bigger slices than in relaxed slicing.

Amtoft [START_REF] Amtoft | Slicing for modern program structures: a theory for eliminating irrelevant loops[END_REF] establishes a soundness property for non-termination insensitive control dependence in terms of simulation. Ball and Horwitz [START_REF] Ball | Slicing programs with arbitrary control-flow[END_REF] describes program slicing for arbitrary control flow. Amtoft and Ball [START_REF] Amtoft | Slicing for modern program structures: a theory for eliminating irrelevant loops[END_REF][START_REF] Ball | Slicing programs with arbitrary control-flow[END_REF] state that an execution in the initial program can be a prefix of that in a slice, without carefully formalizing runtime errors. Our work establishes a similar property, and in addition performs a complete formalization of slicing in presence of errors and non-termination, explicitly formalizes errors by assertions and deduces several results on performing V&V on slices.

Slicing in Presence of Errors. Harman, et al. [START_REF] Harman | Slicing programs in the presence of errors[END_REF] notes that classic algorithms only preserve a lazy semantics. To obtain correct slices with respect to a strict semantics, it proposes to preserve all potentially erroneous statements through adding pseudo-variables in the def(l)a n dr e f ( l) sets of all potentially erroneous statements l. Our approach is more fine-grained in the sense that we can independently select assertions to be preserved in the slice and to be considered by V&V on this slice. This benefit comes from our dedicated formalization of errors with assertions and a rigorous proof of soundness using a trajectory-based semantics. In addition, we make a formal link about the presence or the absence of errors in the program and its slices. Harman and Danicic [START_REF] Harman | Using program slicing to simplify testing[END_REF] uses program slicing as well as meaning-preserving transformations to analyze a property of a program not captured by its own variables. For that, it adds variables and assignments in the same idea as our assertions. Allen and Horwitz [START_REF] Allen | Slicing java programs that throw and catch exceptions[END_REF] extends data and control dependences for Java program with exceptions. In both papers, no formal justification is given.

Certified Slicing. The ideas developed in [START_REF] Amtoft | Slicing for modern program structures: a theory for eliminating irrelevant loops[END_REF][START_REF] Ranganath | A new foundation for control dependence and slicing for modern program structures[END_REF] were applied in [START_REF] Blazy | Verified validation of program slicing[END_REF][START_REF] Wasserrab | From formal semantics to verified slicing: a modular framework with applications in language based security[END_REF]. Wasserrab [START_REF] Wasserrab | From formal semantics to verified slicing: a modular framework with applications in language based security[END_REF] builds a framework in Isabelle/HOL to formally prove a slicing defined in terms of graphs, therefore language-independent. Blazy, et al. [START_REF] Blazy | Verified validation of program slicing[END_REF] proposes an unproven but efficient slice calculator for an intermediate language of the CompCert C compiler [23], as well as a certified slice validator and a slice builder written in Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF]. The modeling of errors and the soundness of V&V on slices were not specifically addressed in these works.

To the best of our knowledge, the present work is the first complete formalization of program slicing for structured programs in presence of errors and non-termination. Moreover, it has been formalized in the Coq proof assistant on a representative structured language, that provides a certified program slicer and justifies conducting V&V on slices instead of the initial program.

Conclusion

In many domains, modern software has become very complex and increasingly critical. This explains both the growing efforts on verification and validation (V&V) and, in many cases, the difficulties to analyze the whole program. We revisit the usage of program slicing to simplify the program before V&V, and study how it can be performed in a sound way in presence of possible runtime errors (that we model by assertions) and non-terminating loops. Rather than preserving more statements in a slice in order to satisfy the classic soundness property (stating an equality of whole trajectory projections), we define smaller, relaxed slices where only assertions are kept in addition to classic control and data dependences, and prove a weaker soundness property (relating prefixes of trajectory projections). It allows us to formally justify V&V on relaxed slices instead of the initial program, and to give a complete sound interpretation of presence or absence of errors in slices. First experiments with Sante [START_REF] Chebaro | Behind the scenes in SANTE: a combination of static and dynamic analyses[END_REF][START_REF] Chebaro | Program slicing enhances a verification technique combining static and dynamic analysis[END_REF], where all-path testing is used on relaxed slices to confirm or invalidate alarms initially detected by value analysis, show that using relaxed slicing allowed to reduce the program in average by 51 % (going up to 97 % for some examples) and accelerated V&V in average by 43 %.

The present study has been formalized in Coq for a representative programming language with assertions and loops, and the results of this paper (as well as many helpful additional lemmas on dependencies and slices) were proved in Coq, providing a certified correct-by-construction slicer for the considered language [START_REF]Formalization of relaxed slicing[END_REF]. This Coq formalization represents an effort of 8 person-months of intensive Coq development resulting in more than 10,000 lines of Coq code.

Future work includes a generalization to a wider class of errors, an extension to a realistic programming language and a certification of a complete verification technique relying on program slicing. Another research direction is to precisely measure the reduction rate and benefits for V&V of relaxed slicing compared to slicing approaches systematically introducing dependencies on previous loops and erroneous statements. In an ongoing work in DEWI project, we apply relaxed slicing for verification of protocols of wireless sensor networks.

Fig. 1 .

 1 Fig. 1. (a) A program computing in two ways the average of elements of a given array a of size N whose only nonzero elements can be at indices {0,k,2k,...},a n di t st w o slices: (b) w.r.t. line 18, and (c) w.r.t. line 20.

Fig. 2 .

 2 Fig. 2. Errors ( ), non-termination ( ) and normal termination (-) of programs of Fig. 1 for some inputs.

  (a) Chained assertions l1 : assert (k != 0, l); while (l : j <= N/k) { ... l2 : assert (k != 0, l); } (b) Loop condition

Fig. 3 .

 3 Fig. 3. Two special cases of assertions

  Figure3b(inspired by the second loop of Fig.1) shows how assertions with explicit labels can be used to protect a loop condition from a runtime error. The arrows in Fig.3indicate the protected statement.

Fig. 4 .

 4 Fig. 4. Trajectory-based semantics of the language (for a valid state σ ∈ Σ)

4. 1

 1 Control and Data DependencesLet L(p) denote the set of labels of program p. Let us consider here a more general slicing criterion defined as a subset of labels L 0 ⊆ L(p), and construct a slice with respect to all statements whose labels are in L 0 . In particular, this generalization can be very useful when one wants to perform V&V on a slice with respect to several threatening statements. In this work we focus on dependencebased slicing, where a dependence relation D⊆L(p) × L(p) is used to construct a slice. We write l D -→ p l ′ to indicate that l ′ depends on l according to D, i.e.(l, l ′ ) ∈D. The definitions of control and data dependencies, denoted respectively D c and D d , are standard, and given following[START_REF] Barraclough | A trajectory-based strict semantics for program slicing[END_REF].Definition 1 (Control Dependence D c ). The control dependencies in p are defined by if and while statements in p as follows:f or any statement if (l : b) q else ra n dl ′ ∈ L(q) ∪ L(r),w e d e f i n el Dc --→ p l ′ ; f or any statement while (l : b) qa n dl ′ ∈ L(q),w e d e f i n el Dc

Lemma 1

 1 can be easily proven by structural induction. It allows us to define a slice as the set of statements on which the statements in L 0 are (directly or indirectly) dependent. Definition 4 (Dependence-based Slice). Let D be a dependence relation on p such that D c ⊆D ,a n dL 0 ⊆ L(P ).Adependence-based slice of p based on D with respect to L 0 is the quotient of p whose set of labels is (D * ) -1 (L 0 ).A classic dependence-based slice of p with respect to L 0 is based on D = D c ∪D d .

Definition 5 (Definition 6 (

 56 Assertion Dependence D a ). For every assertion l : assert (b, l ′ ) in p with l, l ′ ∈ L(p), we define an assertion dependency l Da Relaxed Slice). A relaxed slice of p with respect to L 0 is the quotient of p whose set of labels is (D * ) -1 (L 0 ),w h e r eD = D c ∪D d ∪D a .

Temporal errors (e.g. use-after-free in C) cannot be directly represented in this way.

Formally, using the notation introduced hereafter in the paper (cf. Definition 8), their projections are equal: Proj L (T p σ)=Proj L (T q σ).

By formal definitions of Sect.

[START_REF] Amtoft | Slicing for modern program structures: a theory for eliminating irrelevant loops[END_REF], one easily checks that line 18 is data-dependent on line 6, that is in turn data-dependent on lines 1,3,7 and control-dependent on line 4.

Acknowledgments. Part of the research work leading to these results has received funding for DEWI project (www.dewi-project.eu) from the ARTEMIS Joint Undertaking under grant agreement No. 621353. The authors thank Omar Chebaro, Alain Giorgetti and Jacques Julliand for many fruitful discussions and earlier work that lead to the initial ideas of this paper. Many thanks to the anonymous reviewers for lots of very helpful suggestions.