S Bensalem

M Bozga

J.-C Fernandez
email: fernandez@imag.fr

L Ghirvu

Y Lakhnech

A Transformational Approach for Generating Non-Linear Invariants ⋆

Computing invariants is the key issue in the analysis of infinite-state systems whether analysis means testing, verification or parameter synthesis. In particular, methods that allow to treat combinations of loops are of interest. We present a set of algorithms and methods that can be applied to characterize over-approximations of the set of reachable states of combinations of self-loops. We present two families of complementary techniques. The first one identifies a number of basic cases of pair of self-loops for which we provide an exact characterization of the reachable states. The second family of techniques is a set of rules based on static analysis that allow to reduce n self-loops (n ≥ 2) to n -1 independent pairs of self-loops. The results of the analysis of the pairs of self-loops can then be combined to provide an over-approximation of the reachable states of the n self-loops. We illustrate our methods by synthesizing conditions under which the Biphase Mark protocol works properly.

Introduction

This paper proposes techniques for computing over-approximations of the set of reachable states of a class of infinite state systems. The systems we consider are systems whose variables can be seen as counters that can be incremented by positive or negative constants or can be reset to some constant.

The problem of computing invariants of arithmetical programs in particular, and infinite state systems in general, has been investigated from the seventies. Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Abstract interpretation frameworks[END_REF] is a precise and a formal framework which has been used to develop techniques to tackle this problem. As pioneering work in this field, one can mention M. Karr's work [START_REF] Karr | Affine relationships among variables of a program[END_REF] based on constant propagation for computing invariants that are systems of affine equations, P. & R. Cousot's work [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF] which uses interval analysis to compute invariants of the form x ∈ [a, b], x ≤ a, etc., and the work by P. Cousot and N. Halbwachs [START_REF] Cousot | Automatic discovery of linear restraints among the variables of a program[END_REF] which provides techniques that allow to compute linear constraints that relate the program variables.

In recent years, the subject has known a renewal of interest with the development of symbolic model-checking techniques for some classes of infinite state systems as timed and hybrid automata [START_REF] Henzinger | Symbolic modelchecking for real-time systems[END_REF][START_REF] Halbwachs | Verification of linear hybrid systems by means of convex approximations[END_REF], finite communicating automata [START_REF] Boigelot | Symbolic verification of communication protocols with infinite state spaces using QDDs[END_REF][START_REF] Abdulla | On-the-fly analysis of systems with unbounded, lossy fifo channels[END_REF], parameterized networks [KMM + 97,ABJN99,BBLS], and automata with counters [START_REF] Bultan | Symbolic model checking of infinite state systems using presburger arithmetic[END_REF][START_REF] Wolper | Verifying systems with infinite but regular state spaces[END_REF].

In this paper, we consider transition systems with finite control and with counters as data variables. A transition consists of a guard and a set of assignments. A guard is given by a Presburger formula that may contain parameters, that is, variables that are neither initialized nor modified during execution. Assignments may increment the counters by positive or negative constants or set them to constant values. It should be noticed that this model is fairly general. Indeed, it is computationally equivalent to Turing machines and syntactically subsumes Timed Automa [START_REF] Alur | A Theory of Timed Automata[END_REF], Petri Nets with inhebitors, and Datalog Programs [START_REF] Fribourg | A decompositional approach for computing least fized-points of datalog programs with z-counters[END_REF]. Indeed, each of these models can easily translated into our transition systems.

Given a transition syste we are interested in computing over-approximations of the set of reachable states from parametric initial states, that is, states of the form x = x0 , where x are the variables of the system and x0 , are freeze variables (also called inactive auxiliary variables). In contrast to almost all the works mentioned above, the techniques we present allow to derive non-linear invariants. We concentrate on characterizing sets of states reachable by n-self-loops. This is not an essential restriction, since every system can be transformed into one with a single control location. Moreover, several spécification and programming languages such as UNITY [START_REF] Chandy | Parallel Program Design[END_REF] or the synchronous language Lustre [CHPP87] consist of programs where all transitions are self-loops of a single control point. Notice also that it is clear that the combined effect of self-loops cannot in general be characterized by linear constraints. We present two families of complementary techniques. The first one is presented as set of results that identify a number of basic cases of pairs of self-loops for which we provide an exact characterization of the reachable states. The second family of techniques is a set of rules based on static analysis that allow to reduce n self-loops (n ≥ 2) to n -1 independent pairs of self-loops. The results of the analysis of the pairs of self-loops can then be combined to provide an over-approximation of the reachable states of the n self-loops.

The reduction techniques we present are in the same line as the decomposition rules presented by Fribourg and Olsèn in [START_REF] Fribourg | A decompositional approach for computing least fized-points of datalog programs with z-counters[END_REF], where they consider Datalog programs, i.e., transition systems consisting of a single control location and counters and where only x > 0 is allowed as guard. Notable differences are, however, the fact that the systems they consider are syntactically more restricted and that their rules are exact.

To illustrate the techniques we present in this paper, we consider the Biphase mark protocol which is a parameterized protocol used as a convention for representing both a string of bits and clock edges in a square wave. Using our techniques we have been able to provide a full parametric analysis of this protocol.

Preliminaries

We assume an underlying assertion language A that includes first-order predicate logic and interpreted symbols for expressing the standard operations and relations over some concrete domains. We assume to have the set of integers among these domains. Assertions (we also say predicates) in A are interpreted in states that assign values to the variables of A. Given a predicate P , we denote by free(P ) the set of free variables occurring in it. Similarly, if e is an expression in A, we also write free(e) to denote the set of all variables which occur in e. As expressiveness is not our issue in this paper, we will tacitly identify a predicate with the set of its models.

As computational model we use transition systems. We restrict ourselves to transition systems where the expressions occurring in an assignment to variables x are either constants or of the form x + k. Thus, a transition system is given by a tuple (X , Q, T , E, Π) where X is a finite set of typed data variables, Q is a finite set of control locations, T is a finite set of transition names, E associates with each transition τ a pair (E 1 (τ ), E 2 (τ )) consisting of a source and a target control location, and Π associates with each transition a guard gua(τ ) which is an assertion in the Presburger fragment of A with free variables in X and a list affe(τ ) of assignments of the form x := x + k or x := k with x ∈ X and k ∈ Z Z and such that for each x ∈ X there is at most one assignment x := e in affe(t). We denote by Base(τ ) the set of variables occurring in τ . Notice that we allow parameters in the guards of the transitions; parameters can be seen as program variables that are not modified during execution. This allow us to model parameterized protocols as the Biphase protocol, which we consider later on, and to analyze these protocols using our techniques.

Clearly, (Q, T , E) builds a labeled graph which we call the control graph. Henceforth, we denote the set of transitions τ with E 1 (τ ) = E 2 (τ ) = q by L(q), i.e., L(q) is the set of self-loops in q. Moreover, we write τ (x), where x is a set of variables, for the projection of τ on x, that is, the transition whose guard is obtained from the guard of τ by existentially quantifying all variables but x and whose assignments are obtained from τ by removing all assignments to other variables than x.

A transition τ induces a relation τ -→ on configurations which are pairs of control locations and valuations of the variables in X . Given a transition τ , and configurations (q, s) and (q ′ , s ′ ), (q ′ , s ′ ) is called τ -successor of (q, s), denoted by (q, s) τ -→ (q ′ , s ′ ), if E(τ ) = (q, q ′ ), s satisfies gua(τ ) and s ′ satisfies s ′ (x) = s(e), for each x := e in affe(τ ), s ′ (x) = s(x), for each x that is not affected by τ . Given a regular language L over T and given configurations (q, s) and (q ′ , s ′ ), we say that (q ′ , s ′ ) is Lreachable from (q, s), denoted by (q, s)

L -→ (q ′ , s ′ ), if there exists a word τ 1 • • • τ n ∈ L and configurations (q i , s i ) i≤n such that (q 0 , s 0 ) = (q, s), (q n , s n ) = (q ′ , s ′ ), and (q i , s i ) τ i -→ (q i+1 , s i+1 ). If ϕ and ϕ ′ are predicates,
we write ϕ L -→ ϕ ′ to denote the fact that there exists a state s that satisfies ϕ and a state s ′ that satisfies ϕ ′ such that s L -→ s ′ . Identifying, a state with a predicate characterizing it, we also use the notations ϕ L -→ s ′ and s L -→ ϕ ′ , respectively. Henceforth, given a control location q, in case all transitions in L have q as source and target locations, we omit mentioning q in configurations. Furthermore, given a predicate ϕ(x 0 , x), where x 0 are freeze variables (also called inactive auxiliary variables), and given a set L ⊆ L(q) of self-loops, we say that ϕ(x 0 , x) is an Linvariant at q, if for every state s ′ that is L-reachable from a state s, ϕ[s(x)/x 0 , s ′ (x)/x] is valid. Thus, ϕ(x 0 , x) is the set of states reachable from a parametric state x = x0 by taking sequences of transitions in L. The predicate ϕ(x 0 , x) corresponds to the strongest postcondition of socalled most general formulas used in [START_REF] Gorelick | A complete axiomatic system for proving assertions about recursive and non-recursive programs[END_REF] and investigated in [START_REF] Apt | Completeness with finite systems of intermediate assertions for recursive program schemes[END_REF] in the context of axiomatic verification of recursive procedures.

Characterizing reachable states of self-loops

Throughout this section, we fix a transition system S = (X , Q, T , E, Π). Our goal is to transform S into a transition system S # such that S # does not contain self-loops and such that the set of states reachable from a state s in S # is a super-set of the set of states reachable from s in S, that is, S # is an abstraction of S [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Thus, we will entirely concentrate on selfloops. The motivation and justification behind this is many-fold. First, it is obvious that our model is as expressive as Turing machines, since a two counter-machine is trivially encoded in this model. Moreover, arithmetical programs, which can easily encoded in our model, represent an interesting class of programs that have been widely investigated starting with the pioneering work [START_REF] Cousot | Automatic discovery of linear restraints among the variables of a program[END_REF]. Moreover, even if we restrict the control graph to a single node, we obtain, as discussed in [START_REF] Fribourg | A decompositional approach for computing least fized-points of datalog programs with z-counters[END_REF], an interesting class of Datalog programs. Our model allows to encode in a natural way Petri Nets with inhibitors.

The main idea behind the transformation of S into S # is the following. Consider a control location q and let ϕ(x 0 , x) be an L(q)-invariant at q. Then, we obtain S # by applying the following transformations:

1. Add a new list of variables x0 with the same length as x. 2. Remove all transitions in L(q). 3. Let τ 1 , • • • , τ n be all transitions with E 2 (τ i ) = q and let x := ēi be the assignment associated to τ i . Add to x := ēi the assignment x0 := ēi . 4. Replace each assignment x := ē of a transition τ with E 1 (τ ) = q and E 2 (τ ) = q, by the predicate ∃ȳ

• ϕ(x 0 , ȳ) ∧ gua(τ ) ∧ x′ = ē[ȳ/x],
where x′ stands for the state variables after taking the transition. Note that S # does not satisfy the syntactic restrictions on assignments as introduced in Section2; it is, however, a transition system in the usual sense.

It is not difficult to check that S # is indeed an abstraction of S. Notice also that in case all predicates ϕ(x 0 , x) used in the transformation for characterizing reachable states by self-loops are exact, the obtained system S # is then an exact abstraction of S.

Our approach in computing invariants characterizing the effect of a set of loops is based on the particular case of two self-loops that satisfy syntactic conditions that allow us to analyze each self-loop in isolation and on a set of static analysis techniques which allow us to reduce the analysis of n self-loops to the analysis of a number of particular cases.

Given two transitions τ 0 and τ 1 with Base(τ 0 ) = x and Base(τ 1 ) = xȳ, where x and ȳ are two disjoint sets of variables, and such that x is assigned the list c of constants in τ 1 . We say that τ 0 enables τ 1 , if for every state s with s(x) = c, there exists a state s ′ such that s τ * 0 -→ s ′ and s ′ satisfies the projection on x of the guard of τ 1 , i.e., s ′ satisfies ∃ȳ • gua(τ 1 ). Notice that τ 0 does not enable τ 1 iff for every state s with s(x) = c, there is no state s ′ such that s τ * 0 -→ s ′ and s ′ satisfies ∃ȳ • gua(τ 1 ).

Lemma 1. Let τ 0 and τ 1 be two transitions such that Base(τ 0 ) = x, Base(τ 1 ) = xȳ, where x and ȳ are two disjoint sets of variables, and such that x is assigned the list c of constants in τ 1 .

Then, s

(τ 0 +τ 1 ) * -→ s ′ iff s τ * 0 -→ s ′
or there exists a state s ′′ such that 1)

s τ * 0 τ 1 -→ s ′′ , 2) x = c τ * 0 -→ s ′ (x)
and 3) one of the following conditions holds:

1. τ 0 enables τ 1 and s(ȳ)

τ 1 (ȳ) * -→ s ′ (ȳ) or 2. τ 0 does not enable τ 1 and s(ȳ) τ 1 -→ s ′ (ȳ).

2

Proof. We prove the implication from left to right by induction on the number of times transition τ 1 is taken from s to s ′ . Thus, suppose we have s (τ 0 +τ 1 ) * -→ s ′ . The induction basis follows immediately, since then we have s τ * 0 -→ s ′ . Suppose now that τ 1 is taken n times with n > 0. Then, we have

s τ * 0 -→ s 1 τ 1 -→ s ′′ (τ 0 +τ 1 ) * -→ s ′ and τ 1 is taken n -1 times in the computation from s ′′ to s ′ . In case, τ 0 does not enable τ 1 , we have s ′′ τ * 0 -→ s ′ . Hence, since ȳ ∩ Base(τ 0 ) = ∅, s ′ (ȳ) = s ′′ (ȳ) and x = c τ * 0 -→ s ′ (x). That is, s(ȳ) τ 1 -→ s ′ (ȳ) and x = c τ * 0 -→ s ′ (x).
Now, suppose that τ 0 enables τ 1 , then, by induction hypothesis, s ′′ (ȳ)

τ 1 (ȳ) * -→
s ′ (ȳ). Since, ȳ ∩Base(τ 0 ) = ∅, s(ȳ) = s 1 (ȳ). Consequently, s(ȳ)

τ 1 (ȳ) * -→ s ′ (ȳ).
Moreover, by induction hypothesis, x = c τ * 0 -→ s ′ (x). 2

Lemma 1 states conditions under which the set of states reachable by repeated execution of the transitions τ 0 and τ 1 can be exactly characterized by independently considering the values of the variables x that can be reached by applying τ 0 and the values of ȳ that can be reached by applying τ 1 .

In the following, we present a lemma that allows us to apply a decomposition similar to Lemma 1 while allowing τ 0 to contain additional variables z disjoint from x and ȳ that are not modified by τ 1 .

Lemma 2. Let τ 0 and τ 1 be two transitions such that Base(τ 0 ) = xz, Base(τ 1 ) = xȳ, where x, ȳ and z are mutually disjoint sets of variables, and such that the following conditions are satisfied:

1. For every state s ′ , if true τ 1 -→ s ′ then s ′ does not satisfy the guard of τ 1 . 2. x is assigned the list c of constants in τ 1 . 3. There is a list c′ of constants such that, for every states s and s ′ with s(x) = c and s

τ * 0 -→ s ′ , if s ′ satisfies the guard of τ 1 then s ′ (z) = s(z) + c′ .
4. For every state s with s(x) = c there is a state s ′ such that s τ * 0 -→ s ′ and such that s ′ satisfies the projection on x of the guard of τ 1 . 5. For all states s and s ′ with s(x) = s ′ (x) = c and for all k ≥ 0,

s τ k 0 -→ true iff s ′ τ k 0 -→ true.
Then, s

(τ 0 +τ 1 ) * -→ s ′ iff s τ * 0 -→ s ′ or there exists a state s ′′ such that 1. s τ * 0 τ 1 -→ s ′′ , x = c τ 0 (x) * -→ s ′ (x) and
2. there exists k ∈ IN and a state s ′′′ with s ′′′ (z) = s ′′ (z) + k * c, s(ȳ)

τ k+1 1 -→
s ′ (ȳ), and s ′′′ (z)

τ * 0 -→ s ′ (z). 2
Proof. (sketch).

Using Condition 1.,one can prove that s

(τ 0 +τ 1 ) * -→ s ′ iff s τ * 0 -→ s ′
or there are states s ′′ and s ′′′ and k ≥ 0 such that

s τ * 0 τ 1 -→ s ′′ (τ + 0 τ 1 ) k -→ s ′′′ τ * 0 -→ s ′ .
Let us consider the second case. Here, by Condition 2., we have s ′′ (x) = c. Hence, by Condition 3., in any state reachable from s ′′ by applying (τ + 0 τ 1 ) k ′ -times, the value of z is s ′′ (z) + k ′ * c′ . Therefore, s ′′′ (z) = s ′′ (z) + k * c.

Notice that Condition 4., is used to prove the "only if" part of the statement. Condition 5. guarantees that s ′′′ is reachable from s ′′ by (τ + 0 τ 1 ) k-times. It also guarantees that the number of times τ 0 can be taking starting in a state satisfying x = c does not depend on z.

2

Remark 1. It is important to notice that Condition 2 is syntactic, so it can be easily checked. Moreover, the remaining conditions can be checked effectively, since the sets of reachable states involved are expressible in Presburger arithmetic. Indeed, if a language L is of the form

L 1 +• • •+L n ,
where each L i is either finite or of the form w * , where w is a word, then the set of states reachable by L from a (parametric) state x = x0 is easily expressible in Presburger arithmetic. Nevertheless, it is easy to give sufficient syntactic conditions that can be easily checked. For instance, Condition 5. is satisfied, if z does not occur in the guard of transition τ 0 .

Example 1.

Let us consider the following self-loops:

τ 0 : x < T → x := x + 1; z := z + 1 τ 1 : x = T ∧ y < C → x := 0; y := y + 1
It is easy to check that the premises of Lemma 2 are satisfied. Using the characterization stated by the lemma and after simplification, we obtain the following invariant:

(x -z = x 0 -z 0 ∧ x ≥ x 0 ∧ z ≥ z 0 ∧ y = y 0 ) ∨ ∃k ≥ 1• (y = y 0 + k ∧ y ≤ C ∧ z = (z 0 -x 0 ) + k * T + x ∧ x ≤ T ) 2
Lemma 2 can be generalized as follows to the case where z is not augmented by the same list c′ of constants:

Lemma 3. Assume the same premises as in Lemma 2 but condition 3. replaced by: There is a set I of values such that, for every states s and s ′ with Then, s

(τ 0 +τ 1 ) * -→ s ′ iff s τ * 0 -→ s ′ or there exists a state s ′′ such that 1. s τ * 0 τ 1 -→ s ′′ , x = c τ 0 (x) * -→ s ′ (x)
(z) = s ′′ (z) + i=k i=1 ci with ci ∈ I, s(ȳ) τ k+1 1 -→ s ′ (ȳ)
, and s ′′′ (z)

τ * 0 -→ s ′ (z). 2 Example 2.
Let us consider the following self-loops:

τ 0 : x < T → x := x + 1; z := z + 1 τ 1 : t ≤ x ≤ T ∧ y < C → x := 0; y := y + 1
Now, applying Lemma 3 we obtain the following invariant:

(x -z = x 0 -z 0 ∧ x ≥ x 0 ∧ z ≥ z 0 ∧ y = y 0 ) ∨ ∃k ≥ 1• (y = y 0 + k ∧ y ≤ C ∧ z ∈ (z 0 -x 0 ) + [k * t, k * T ] + x ∧ x ≤ T ) 2
Remark 2. Notice that, if we remove Condition 3.b in Lemma 3, then only the "only if" part of the conclusion is true, that is, we have s

(τ 0 +τ 1 ) * -→ s ′ implies s τ * 0 -→ s ′ or there exists a state s ′′ such that 1. s τ * 0 τ 1 -→ s ′′ , x = c τ * 0 -→ s ′ (x)
τ * 0 -→ s ′ (z).
This result can of course be used to derive an invariant that is not necessarily the strongest. 2

Decomposition techniques

We present hereafter heuristics which allow us to reduce the analysis of n ≥ 2 self-loops to simpler cases such that, finally, we can apply the lemmata introduced in Section 3. Basically, we consider the case of n + 1 loosely-coupled self-loops. We show that, their global analysis can be effectively reduced to n analysis of 2 self-loop problems, when some syntactic conditions on the sets of used variables occurs. The decomposition technique is stated by the following lemma and can be seen as a direct generalization of lemma 1.

Lemma 4. Let τ 0 , τ 1 , • • • , τ n be transitions such that Base(τ 0 ) = x1 • • • xn , Base(τ i ) = xi ȳi and for each i = 1, • • • , n, xi
is assigned by τ i the list ci of constants, and the sets of variables xi and ȳi are all pairwise disjoint.

If

each ϕ i is a (τ 0 ( xi )+τ i ) * -invariant, then n i=1 ϕ i is a (τ 0 +• • •+τ n ) * - invariant. 2
Example 3. Let us consider the following three self-loops borrowed from the description of the Biphase protocol, which we will consider in Section 5:

     τ 0 : x < max ∧ y < max → x := x + 1 y := y + 1 τ 1 : x ≥ min ∧ n < cell → x := 0 n := n + 1 τ 2 : y ≥ min ∧ m < sample → y := 0 m := m + 1
We can easily check that the premises of Lemma 4 are satisfied. Hence, we can split the analysis of the three self-loops into the independent analysis of the following sets each consisting of two self-loops, as shown below:

τ 0 (x) : x < max → x := x + 1 τ 1 : x ≥ min ∧ n < cell → x := 0 n := n + 1 τ 0 (y) : y < max → y := y + 1 τ 2 : y ≥ min ∧ m < sample → y := 0 m := m + 1
Each case can be analyzed independently using the results established in the previous section. We obtain that

ϕ 1 = (x ≤ max ∧ n ≤ cell) is a (τ 0 (x) + τ 1 ) * -invariant and that ϕ 2 = (y ≤ max ∧ m ≤ sample) is a (τ 0 (y) + τ 2 ) * -invariant.
Thus, we can infer that

ϕ 1 ∧ ϕ 2 = (x ≤ max ∧ n ≤ cell ∧ y ≤ max ∧ m ≤ sample) is a (τ 0 + τ 1 + τ 2 ) * -invariant. 2
However, the invariants obtained in this way are too weak. The reason is that by the decomposition of the set of loops we lost the overall constraint induced on x variables by the τ 0 loop. That is, all variables occurring in τ 0 are strongly related by this transition, and it is no more the case when taking the projections. The following lemma solves this problem by adding some re-synchronization variables in order to be able to reconstruct (at least partially) the existing relation among the x variables.

Lemma 5. Let τ 0 , τ 1 , • • • , τ n be transitions s.t. the premises of Lemma 4 are satisfied. Let (z i ) i=1,n be fresh variables and let τ ′ 0 ( xi ) be the transition obtained from τ 0 ( xi ) augmented with the assignment

z i := z i + 1. If each ϕ ′ i is a (τ ′ 0 ( xi ) + τ i ) * -invariant, then ∃z 1 , • • • z n .(z 1 = • • • = z n ∧ n i=1 ϕ ′ i ) is a (τ 0 + • • • + τ n ) * -invariant.
Intuitively, variables z i keep track of the number of times the transition τ 0 is executed in each case. In this way, the global invariant can be strengthened by adding the equality on z i variables. That is, when considered together, the number of times τ 0 is executed must be the same in all 1 ≤ i ≤ n cases.

Example 4. Let us consider again the three-loops presented above. After splitting them and augmentation with fresh variables z x and z y , we obtain the following sets of self-loops to be analyzed:

τ 0 (x) : x < max → x := x + 1 z x := z x + 1 τ 1 : x ≥ min ∧ n < cell → x := 0 n := n + 1 τ 0 (y) : y < max → y := y + 1 z y := z y + 1 τ 2 : y ≥ min ∧ m < sample → y := 0 m := m + 1
Applying, Lemma 3, we obtain that

ϕ ′ 1 = (x ≤ max ∧ n ≤ cell ∧ n • min + x ≤ z x ≤ n • max + x)
is a (τ ′ 0 (x) + τ 1 ) * -invariant and that

ϕ ′ 2 = (y ≤ max ∧ m ≤ sample ∧ m • min + y ≤ z y ≤ m • max + y)
is a (τ ′ 0 (y) + τ 2 ) * -invariant. The global invariant computed is then ∃z x , z y .(z x = z y ∧ ϕ ′ 1 ∧ ϕ ′ 2 ), which can be simplified to

x ≤ max ∧ n ≤ cell ∧ y ≤ max ∧ m ≤ sample ∧ n • min + x ≤ m • max + y ∧ m • min + y ≤ n • max + x.
This invariant is indeed stronger than the one computed in Example 3. 2

The Biphase protocol

The biphase mark protocol is a convention for representing both a string of bits and clock edges in a square wave. It is widely used in applications where data written by one device is read by another. It is for instance used in commercially available micro-controllers as the Intel 82530 Serial Communication Controller and in the Ethernet.

We borrow the following informal description of the protocol from J. S. Moore:

In the biphase mark protocol, each bit of messages is encoded in a cell which is logically divided into a mark subcell and a code subcell. During the mark subcell, the signal is held at the negation of its value at the end of the previous cell, providing an edge in the signal train which marks the beginning of the new cell. During the code subcell, the signal either returns to its previous value or does not, depending on whether the cell encodes a "1" or "0". The receiver is generally waiting for the edge that marks the arrival of a cell. When the edge is detected, the receiver counts off a fixed number of cycles, called sampling distance, and samples the signal there. The sampling distance is determined so as to make the receiver sample in the middle of the code subcell. If the sample is the same as the mark, a "0" was sent; otherwise a "1" was sent. The receiver takes up waiting for the next edge, thus phase locking onto the sender's clock.

The main interesting aspect (from the verification point of view) of this protocol is the analysis of the tolerable asynchrony between the sender and the receiver. Put more directly, the derivation of sufficient conditions on the jitter between the clock of the sender and the clock of the receiver such that the protocol works properly.

To our knowledge, there has been some work on the verification of instances of the protocol either using theorem-proving techniques [START_REF] Moore | A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol[END_REF] or model-checking [START_REF] Ivanov | Verification of a biphase mark protocol[END_REF][START_REF] Vaandrager | Analysis of a biphase mark protocol with uppaal[END_REF] and one work presenting full parameter analysis using PVS and the Duration Calculus, however, without clock jitter.

Using the techniques presented earlier in this paper, we have been able to fully analyze the protocol and to derive parameterized sufficient conditions for its correctness.

Protocol Modeling

We use extended transition systems to model the protocol which consists of a sender and a receiver exchanging boolean value. Some of the transitions are marked with synchronization labels. Following, Vaandrager we model the clock drifts and jitter using two different clocks which will be reset independently and using two parameters min and max to bound the drift between these clocks. The models of the sender, the receiver and their product are given in Figure 1

: x < max → x := x + 1 τ s 111 : x ≥ min ∧ n < cell → x := 0 n := n + 1 τ s 112 : x ≥ min ∧ n = cell → x := 0 n := 0 v := ¬v get !false τ s 12 : x ≥ min ∧ n = cell → x := 0 n := 0 v := ¬v get !true τ s 220 : x < max → x := x + 1 τ s 221 : x ≥ min ∧ n < mark → x := 0 n := n + 1 τ s 21 : x ≥ min ∧ n = mark → x := 0 n := n + 1 v := ¬v mark

Invariant generation

Using the techniques presented before we are able to construct the following invariants for the product control locations:

ϕ 13 = x ≤ max ∧ y ≤ max ∧ n ≤ cell ϕ 14 = x ≤ max ∧ y ≤ max ∧ n ≤ cell ∧ m ≤ sample m • min + y ≤ n • max + x ∧ n • min + x ≤ m • max + y ϕ 23 = x ≤ max ∧ y ≤ max ∧ n ≤ mark ϕ 24 = x ≤ max ∧ y ≤ max ∧ n ≤ mark ∧ m ≤ sample m • min + y ≤ n • max + x ∧ n • min + x ≤ m • max + y

Parameter synthesis

One of requirements for correctness of the protocol states that the receiver does not sample too late. That is, a bad behavior is obtained by allowing to take two consecutive get actions by the protocol, without no put action in between. For instance, such a scenario is possible when in state 14, the get transitions τ s 112 or τ s 12 are enabled before the put transition τ r 43 . To avoid such a situation, a sufficient condition will be if ϕ 14 ∧(gua(τ s 112 )∨gua(τ s 12 )) is not satisfiable. This condition is the following:

x ≤ max ∧ y ≤ max ∧ n ≤ cell ∧ m ≤ sample m • min + y ≤ n • max + x ∧ n • min + x ≤ m • max + y x ≥ min ∧ n = cell
and is equivalent after simplification to :

(cell + 1) • min > (sample + 1) • max

A second requirement states that the receiver does not sample too early. That is, wrong behavior occurs when the receiver samples before the mark sub-cell started. In this case, a bad scenario is that one in state 24 the put transition τ r 43 is enabled before the mark transition τ s 21 . Here also, this behavior can be avoided if the condition ϕ 24 ∧ gua(τ r 43 ) is not satisfiable. We obtained in this case:

x ≤ max ∧ y ≤ max ∧ n ≤ mark ∧ m ≤ sample m • min + y ≤ n • max + x ∧ n • min + x ≤ m • max + y y ≥ min ∧ m = sample
and can be further simplified to the following condition depending only on parameters:

(sample + 1) • min > (mark + 1) • max

Conclusions

In this paper, we presented a set of techniques which allow to compute an over-approximation of the set of reachable states of a set of self-loops. The techniques we presented can be partitioned in two classes: 1.) exact techniques that under effectively checkable conditions allow to characterize the set of reachable states of pairs of self-loops without loss of information and 2.) techniques that allow to reduce more general cases of a set of self-loops to the analysis of a set of pairs of self-loops. Using, our techniques we have been able to synthesize a set of conditions on the parameters of the Biphase protocol that are sufficient to ensure its correctness.

We plan to implement our techniques using decision procedures for Presburger arithmetic to decide the conditions necessary for applying them. We also plan to apply these techniques for generating test cases for protocols and test objectives that involve data.

s(x) = c and s τ * 0 - 0 -

 00 → s ′ , if s ′ satisfies the guard of τ 1 then 3.a there is c′ ∈ I with s ′ (z) = s(z) + c′ and 3.b for every c′′ ∈ I there is a state s ′′ with s ′′ (z) = s(z) + c′′ , s τ * → s ′′ , and such that s ′′ satisfies the guard of τ 1 .

  , Figure 2, and Figure 3.

Fig

  Fig. 1. The sender

partially supported by Région Rhône-Alpes, France


Marius Bozga
email: marius.bozga@imag.fr

Jean-Claude Fernandez
email: claude.fernandez@imag.fr

Lucian Ghirvu
email: lucian.ghirvu@imag.fr

Using Static Analysis To Improve Automatic Test Generation

Keywords: conformance testing, asynchronous systems, static analysis, slicing, bisimulation

Conformance testing is still the main industrial validation technique for telecommunication protocols. The automatic construction of test cases based on the model approach is hindered by the state explosion problem. Our method reduces its magnitude by reconsidering the test case generation at a higher level and by taking advantage of some static analysis techniques, in particular the slicing techniques. The speci cation is simpli ed by pipelining a set of three modules, each one implementing a di erent slicing technique.

Introduction

Conformance testing is a well-established technique for the validation of telecommunication protocols. Currently, it is still the main validation technique used at an industrial scale, given the inherent complexity of more ambitious techniques such as formal veri cation. Moreover, in the case of protocols, the conformance testing was completely formalized by [START_REF] Tretmans | A Formal Approach to Conformance Testing[END_REF][START_REF] Brinksma | A Formal Approach to Conformance Testing[END_REF][START_REF]Information Retrieval, Transfer and Management for OSI; Framework: Formal Methods in Conformance Testing[END_REF] and is also standardized within 12]. Test cases can be automatically generated from formal speci cations and tools such as tgv 11], tveda 18], autolink 21] or torx 2] concretely implement this activity.

In the model-based approach, test cases are usually constructed by exploring a synchronous product between the model of the speci cation and some test purpose, both represented as labeled transition systems. The central problem arising here is the well known state explosion problem. To deal with it we propose to reconsider the test generation at a higher level i.e., to work with speci cations and test purposes represented by some kind of extended automata and to perform relevant static simpli cations before generating test cases. In this paper, we consider speci cations as asynchronously communicating extended automata and test purposes as acyclic automata with constraints. We want to generate tests describing a nite interaction between the tester and the implementation under test. Moreover, by the fact that the test purpose is an automaton with constraints, it is possible to generate symbolic tests.

We propose to simplify speci cations by means of slicing 23]. A rst slicing consists in taking into account the set of interactions between speci cation components, starting from inputs enabled in the test purpose, and regardless the signal parameters. We obtain a rst reduction of the speci cation, consisting of the part of it which is reachable given the enabled inputs. Then, for the second slicing, we look at the set of variables and parameters which are relevant to outputs observed by the test purpose and safely discard the others. Finally, the speci cation is sliced with respect to constraints attached to the test purpose. These analyses transform speci cations without loss of information with respect to the test purpose. They are independent of each other and can be implemented separately. Each of them inputs a speci cation, performs a slicing on it, and then outputs a new equivalent one. They can be applied in any order, until no more reduction can be obtained. Concerning the overall simpli cation on the initial speci cation, our experiments showed very good results.

The idea of using static analysis to improve model checking and test generation was already being investigated in di erent contexts. For instance, tveda 18] produces test cases from sdl speci cations by performing simple syntactic transformations on them. Slicing is used in the context of automatic generation of test data for sequential programs. [START_REF] Gupta | Program Slicing-Based Regression Testing Techniques[END_REF], the authors present an approach to selective regression testing using slicing. Selective regression approach identi es the parts of the program that are a ected by a change. In 14], slicing is used for veri cation purposes, to extract nite-state machines from multi-threaded programs.

The paper is structured as follows. Section 2 brie y remember the notions of conformance testing and presents the underlying model. In section 3 we propose and formalize three new slicing techniques of the speci cation with respect to the test purpose. Finally, we give some results in section 4 and we conclude in section 5.

Conformance test case generation

This section reviews some notions of conformance testing and presents the underlying model, which is parallel asynchronous processes communicating via queues.

Conformance testing is a black-box testing method, which aims at validating that the implementations of protocols conform to their speci cations. Conformance testing activity is standardized in 12] and work has been done to formalize it 22]. In this context, our purpose is to generate automatically conformance test cases for telecommunication protocols.

In the classi cation of testing architectures from 12, 20], our method is a local single-layer test method with synchronous communication between the tester and the implementation under test (iut). It is local because in the interactions between the tester and the iut no event caused by the surrounding environment appears. It is single-layer because we test implementations of speci cations organized in one layer. The tester interacts with the iut via some points of control and observation (pcos), which, in our case, are seen as external queues of the speci cation (see below). The communication at the pcos is synchronous. This architecture is pictured in Figure 1.

In order to assure the feasibility of our method (correctness, compatibility with the industrial practice) we require that the tester, the iut and the specication satisfy some conditions :

1. controllability condition : the tester always controls its outputs and can feed the speci cation only at one pco at the time (therefore, for each state of the test purpose, whenever an input is enabled, it is the only transition starting in this state), 2. consistency relation : between the test purpose and the speci cation (which ensures that the set of behaviors described by the test purpose is included in the set of behaviors described by the speci cation)1 , 3. conformance relation : ensures that the outputs of the implementation must be produced also by the speci cation.

The speci cation

We consider speci cations consisting of asynchronous parallel composition of a number of processes that communicate through parameterized signals passing via a set of unbounded fo queues. We distinguish between internal queues (closed inside the speci cation) and external queues (opened to the environment). In the context of conformance testing with local tester, external queues contents are controlled by the tester. Then, we make explicit the assumption of synchronicity between the tester and the iut. Processes are extended nite-state automata. They perform actions on queues and local variables. For the sake of simplicity, the actions are simple guarded commands.

De nition 1 (speci cation syntax). A speci cation SP is a tuple (S; C; P) where S is the set of signals, C = C int C ext is the set of queues (internal and external ones) and P is the set of processes. A process p 2 P is a tuple (X p ; Q p ; T p ; q 0 p ) where X p is a set of local variables, Q p is a set of states, p is a set of actions which can be performed by p, and T p Q p p Q p is a set of transitions. An action can be either a guarded assignment b ] x := e, a guarded input b ] c?s(x), or a guarded output b ] c!s(e). Above, b and e are expressions, x 2 X p is a variable, c 2 C is a queue and s 2 S is a signal.

We give the semantics of speci cations in terms of labeled transition systems.

We assume the existence of the universal domain D which contains the values of variables and signal parameters. We suppose that the boolean values ft; fg and also the special unde ned ? value are contained in D. We de ne variable contexts as being total mappings : S p2P X p ! D which associate to each variable x a value v from the domain. We extend these mappings to expressions in the usual way. We de ne internal queue contexts as being also total mappings : C int ! (S D) which associates to each internal queue c a sequence (s 1 ; v 1 ); :::; (s k ; v k ) of messages, that is pairs (s; v) noted also by s(v), where s is a signal and v is the carried parameter value. We assume also the existence of some special unde ned message . The empty sequence is noted with .

De nition 2 (speci cation semantics). The semantics of a speci cation SP is given by a labeled transition system d SP = ( b Q sp ; b T sp ; q0 sp ). States qsp of this system are triples of the form ( ; ; ), where is a variable context, is a queue context and = hq 1 ; :::q n i 2 p2P Q p is a global control state. Transitions are either internal and labeled with , when derived from assignments or internal communication, either visible and labeled with the concrete action when derived from external communication. Transitions are constructed by the following rules: q p b] x:=e ?! q 0 p (b) = t (e) = v ( ; ; ) ?!( v=x]; ; 0 ) q p b] c!s(e) ?! q 0 p (b) = t (e) = v c 2 C ext ( ; ; ) c!s(v) ?! ( ; ; 0 ) q p b] c!s(e)

?! q 0 p (b) = t (e) = v c 2 C int (c) = w ( ; ; ) ?!( ; w:s

(v)=c]; 0 ) q p b] c?s(x) ?! q 0 p (b) = t c 2 C ext ( ; ; ) c?s(v) ?! ( v=x]; ; 0 ) q p b] c?s(x) ?! q 0 p (b) = t c 2 C int (c) = s(v):w ( ; ; ) ?!( v=x]; w=c]; 0 )
where 0 was obtained from by considering one step in process p from q p to q 0 p , and the initial state q0 sp is obtained considering the default value of the variables, empty queues and processes initial states.

Test purpose

The test purpose is an acyclic nite state automaton which describe a pattern of interactions between the tester and the iut. It is described from the implementation side i.e., inputs and outputs in the test purpose means respectively inputs and outputs in the implementation. It contains both constrained signal inputs and unconstrained signal outputs.

A constraint C is a boolean combination of atoms, each of them being a particular restriction on the used value. For example, we can test the containment of an element to an interval or to a set of values. The notation v j = C stands for the value v satis es the constraint C. For a given input of the test purpose, there is a constraint related to the signal parameter 12]. There are no relational dependencies between constraints attached to di erent inputs.

This test purpose de nition was inspired by ttcn and has the following intuition : if the tester provide a signal to the implementation with the value of its parameter satisfying a constraint then we would like to approximate the value of outputs parameters.

De nition 3 (test purpose).

A test purpose TP is a tuple (Q tp ; T tp ; q 0 tp ; Q acc tp ) where Q tp is a set of states, T tp Q tp tp Q tp is a set of transitions and Q acc tp Q tp is a set of accepting states, without successors by T tp . tp is the set of interactions tp which can be xed within the test purpose. This set contains both constrained signal inputs of the form c?s(C) and unconstrained signal outputs of the form c!s( ), where c 2 C ext is an external queue and s 2 S is a signal. C denotes a generic constraint e.g., interval constraint, on the received value and denotes any value.

The feeds are the set of inputs we intend to supply to the iut during the test. Feeds are a parameter completely controlled by the tester. They will be taken into account during the test case generation process. That is, any external input in the speci cation will be enabled if and only if it is contained in the set of feeds. Intuitively, the set of feeds must cover the set of inputs given in the test purpose.

De nition 4 (feeds). The feeds f are a set of constrained signal inputs fc?s(C) j c 2 C ext ; s 2 Sg.

Synchronous product

The tests are automatically derived by exploring a kind of synchronous product between the model of the speci cation ( b Q sp ; b T sp ; q0 sp ), the test purpose (Q tp ; T tp ; q 0 tp ; Q acc tp ), and taking into account the set of feeds f = fc?s(C) j c 2 C ext ; s 2 Sg. De nition 5 (synchronous product). We de ne the synchronous product Q ( d SP; TP; f ) as the labeled transition system (Q ; T ; q 0 ), with Q b Q sp Q tp , where Q and T are the smallest sets obtained by the application of the following rules: ? (q 0 sp ; q 0 tp ) 2 Q (q sp ; q tp ) 2 Q qsp ?!q 0 sp q tp 6 2 Q acc tp (q 0 sp ; q tp ) 2 Q (q sp ; q tp ) ?!(q 0 sp ; q tp ) (q sp ; q tp ) 2 Q qsp c?s(v)

?! q0 sp q tp c?s(C) ?! q 0 tp v j = C (q 0 sp ; q 0 tp ) 2 Q (q sp ; q tp ) c?s(v) ?! (q 0 sp ; q 0 tp ) (q sp ; q tp ) 2 Q qsp c?s(v)

?! q0 sp c?s(C) 2 f v j = C (q 0 sp ; q tp ) 2 Q (q sp ; q tp ) c?s(v) ?! (q 0 sp ; q tp ) (q sp ; q tp ) 2 Q qsp c!s(v) ?! q0 sp q tp c!s( ) ?! q 0 tp (q 0 sp ; q 0 tp ) 2 Q (q sp ; q tp ) c!s(v) ?! (q 0 sp ; q 0 tp )

(q sp ; q tp ) 2 Q qsp c!s(v)
?! q0 sp (q 0 sp ; q tp ) 2 Q (q sp ; q tp ) c!s(v) ?! (q 0 sp ; q tp ) Example 1. The previous de nitions are exempli ed in Figure 2. The speci cation is composed of two processes which communicate through an internal queue cl 2 C int . The external queues of the speci cation are ci; co 2 C ext . The set of feeds are f = fci?sr( 1; 10])g. This example will be used throughout the paper in order to picture the changes of the speci cation induced by the following slicing algorithms. The purpose of static analysis is to compute, given the test purpose and the feeds, the part of the speci cation which is relevant to them. We present three kinds of analyses : 1. the relevant control analysis: restricts the processes contained in the specication, to the sets of states and transitions which might be statically reached, given the set of feeds, 2. the relevant variables analysis: computes and simpli es processes, with respect to variables which might be used to compute values needed for outputs mentioned in the test purpose and 3. the constraint propagation: aims to further simplify processes, given the concrete constraints attached to feeds. Each one of the analysis takes as input a speci cation and provides an equivalent one with respect to the test generation method presented below. They are completely independent and can be applied in any order. Furthermore, they could be applied iteratively as the code optimization techniques [START_REF] Muchnick | Advanced Compiler Design Implementation[END_REF]). The reduction obtained by one can be further exploited by another and so on, until no more reductions are possible.

We detail each one of these analysis below and illustrate them on the example presented before.

Relevant control analysis

A conservative approximation for the speci cation is computed, by taking into account the set of feeds. We restrict each process to the set of states and transitions that might be reached given the feeds. Intuitively, this analysis can be seen as building the largest sub-processes, after the removal of external inputs uncovered by feeds, and subsequently the internal inputs uncovered by internal outputs.

De nition 6 (slicing wrt feeds). We de ne the slice of a speci cation SP = (S; C; P) with respect to a set of feeds f to be the speci cation SP n f f = (S; C; P n f f ), where P n f f contains a sliced process p 0 for each process p 2 P. The slice for a process p = (X p ; Q p ; T p ; q 0 p ) 2 P is de ned as the process p 0 = (X p ; Q 0 p ; T 0 p ; q 0 p ), with the same sets of variables. The sets of states Q 0 p Q p and transitions T 0 p T p are de ned as the smallest ones which satisfy the following rules: ? q 0 p 2 Q 0 p q p 2 Q 0 p q p b]x:=e ?! q 0 p q 0 p 2 Q 0 p q p b]x:=e ?! q 0 p 2 T 0 p q p 2 Q 0 p q p b]c!s(e)

?! q 0 p q 0 p 2 Q 0 p q p b]c!s(e)

?! q 0 p 2 T 0 p q p 2 Q 0 p q p b]c?s(x)

?! q 0 p c 2 C ext c?s(C) 2 f q 0 p 2 Q 0 p q p b]c?s(x)

?! q 0 p 2 T 0 p q p 2 Q 0 p q p b]c?s(x)

?! q 0 p c 2 C int 9r:q r b 0 ]c!s(e)

?! q 0 r 2 T 0 r q 0 p 2 Q 0 p q p b]c?s(x)

?! q 0 p 2 T 0 p We must notice here the input/output propagation between processes. That is, we keep an input inside some process p if and only if there exists some dual output enabled in some other process r.

The algorithm computing the sliced system proceeds in an iterative manner. It maintains the sets of states and transitions reached for each process. Initially, the sets of states contain the initial state of the processes, and the sets of transitions are empty. Then, at each step, one of the rules before is applied until the least xed point is reached and no more rule is applicable. This algorithm is similar to reachability analysis but it is performed at the control level.

Example 2. If one applies the previous algorithm for the speci cation and the feeds from Figure 2, one obtains the speci cation shown in Figure 3. The external input ci?pr(n) is uncovered by the feeds so its elimination induces the elimination of cl!p(n) and thus cl?p(n) is no more covered by an internal output so it is eliminated together with br := f. The slicing with respect to feeds preserves the synchronous product, that is, the following proposition holds.

Proposition 1 (slicing wrt feeds correctness). Let SP = (S; C; P) be a speci cation, TP a test purpose and f a set of feeds which covers TP. The synchronous products between the models of SP and respectively SP n f f with the test purpose TP, given the feeds f are strongly bisimilar. That is, Q ( d SP; TP; f ) Q ( \ SP n f f ; TP; f ).

Relevant variables analysis

This calculus is an extension of live variable analysis 4]. It attempts to compute, for each process, the set of relevant variables in each state. The relevance is de ned with respect to test purpose outputs: a variable will be relevant in a state if its value at that state might be used to compute the parameter value of some signal output occurring in the test purpose. Or, similar to the live variables de nition, we consider a variable to be relevant in a state if and only if there exists a path starting at that state such that the variable is used before being rede ned on the path. But, in our case, we consider a variable to be used only in external outputs mentioned by the test purpose, or in assignments (eventually via internal inputs) to relevant variables. De nition 7 (relevant variables wrt outputs). Let SP = (S; C; P) be a speci cation and TP = (Q tp ; T tp ; q 0 tp ; Q acc tp ) be a test purpose. Let o be the set of signal outputs mentioned in the test purpose. The relevant variables are de ned for each process p = (X p ; Q p ; T p ; q 0 p ) 2 P by a function Rlv p : Q p ! 2 X p mapping states to subsets of variables. The sets Rlv p (q p ) for states q p 2 Q p are de ned as the least xed point of the following equation system: Rlv p (q p ) = S t p :q p ?!q 0 p Rlv(q 0 p ) n Def p (t p ) Use p (t p )

where

Def p (t p ) = Use p (t p ) = 8 > > > > > < > > > > > : fxg if t p = q p b]x:=e ?! q 0 p or t p = q p b]c?s(x) ?! q 0 p ; otherwise 8 > > > > > > > > > > > < > > > > > > > > > > > :
vars(b) vars(e) if t p = q p b]x:=e ?! q 0 p and x 2 Rlv p (q 0 p ) or t p = q p b]c!s(e)

?! q 0 p and c 2 C ext and 9q tp c!s( ) ?! q 0 tp 2 T tp or c 2 C int and 9r:q r c?s(x) ?! q 0 r 2 T r and x 2 Rlv r (q 0 r )

vars(b) otherwise

The relevant variables are computed simultaneously for all processes. The algorithm operates in a backward manner on the control graphs. It starts with empty sets of variables for each state, and at each step one transition is analyzed: the set of used variables is recomputed in the current context and then, the relevant variables set for the source state is updated. The algorithms ends when the least xed point is reached and no more change in the relevance sets occurs for any of the transitions.

For this analysis too, we notice that the relevance of variables is propagated interprocesses. In fact, variables used in expressions sent through internal channels will become relevant only if, at the destination side their value is further relevant.

The slicing with respect to relevant variables attempts to reduce the number of variables used inside processes. Concretely, we cut o all the de nitions assigning irrelevant variables. Irrelevant variables used in inputs are replaced by some special, don't care, variable >. Finally, expressions occurring in unused outputs are replaced by the unde ned value ?. This transformation is formally described below.

De nition 8 (slicing wrt outputs). Let SP = (S; C; P) be a speci cation and TP be a test purpose. We de ne the slice of the speci cation SP given the relevant variables computed wrt outputs to be the speci cation SP n o o = (S; C; P n o o ), where P n o o contains a sliced process p 0 for each process p 2 P. The slice for a process p = (X p ; Q p ; T p ; q 0 p ) is de ned as a process p 0 = (X 0 p ; Q p ; T 0 p ; q 0 p ) which has the same set of states and the same initial state, but operates only on relevant variables. We put X 0 p = S q p 2Q p Rlv p (q p ) and transitions T 0 p are constructed from T p such that they do not more de ne irrelevant variables : q p b]x:=e ?! q 0 p x 2 Rlv p (q 0 p ) q p b]x:=e ?! q 0 p 2 T 0 p q p b]x:=e ?! q 0 p x 6 2 Rlv p (q 0 p ) q p b]

?!q 0 p 2 T 0 p q p b]c?s(x)

?! q 0 p x 2 Rlv p (q 0 p ) q p b]c?s(x)

?! q 0 p 2 T 0 p q p b]c?s(x)

?! q 0 p x 6 2 Rlv p (q 0 p )

q p b]c?s(>) ?! q 0 p 2 T 0 p q p b]c!s(e) ?! q 0 p Use(c!s) q p b]c!s(e) ?! q 0 p 2 T 0 p q p b]c!s(e)
?! q 0 p :Use(c!s) q p b]c!s(?) ?! q 0 p 2 T 0 p where Use(c!s) = 9q tp c!s( ) ?! q 0 tp 2 T tp or 9r:q r c?s(x)

?! q 0 r 2 T r and x 2 Rlv r (q 0 r )

denote the global utility of outputs of the form c!s.

Example 3. The slicing wrt outputs algorithm, applied for the speci cation and the test purpose from Figure 3, produces the speci cation shown in Figure 4.

The transitions labeled y := 1 and y := y i are relabeled with and the output co!pa(y) become co!pa(?) because :Use(co!pa). Proposition 2 (slicing wrt outputs correctness). Let SP = (S; C; P) be a speci cation and TP = (Q tp ; T tp ; q 0 tp ; Q acc tp ). The model of SP renamed with respect to the observable outputs o and respectively the model of SP n o o are strongly bisimilar, that is, d SP # o \ SP n o o .

A nal remark concerns a more general utility of relevant variables. In fact, we tried here to exploit them at a purely syntactic level e.g., by eliminating the irrelevant ones and their dependencies in the speci cation. However, it is possible to take them into account in a deeper manner. For instance, using a technique similar to 4], one can reinitialize them with a default value as soon as they become irrelevant, thereby achieving a bisimilar reduced model.

Constraint propagation

This section provides an approach to simplify the speci cation, using the constraints imposed on the feeds and the inputs of the test purpose. First, these constraints will be attached to possible matching inputs. Then, by using some intra/interprocesses data ow analysis algorithms, the constraints are propagated in the speci cation. Thus, for each control state, a conservative approximation of the set of possible values for each variable is computed. Finally, this information is used to evaluate the transitions guards and to eliminate those ones never rable.

In the following we will sketch the constraint propagation problem and how to solve it. It is a data ow analysis problem whose basic components are :

1. the ow graph is composed of the states and the transitions of each process and some auxiliary constructions in order to simulate the internal queues, 2. the complete powerset lattice of D, the constraints being some of its elements, 3. the class of transfer functions Transfer t p , for each transition t p .

4. the con uence functions F , one for each state.

Let us observe that by choosing the constraints to be the elements of 2 D we have ensured the possibility of testing the emptiness of a constraint and also the possibility of having a partial order among them.

In order to de ne the transfer functions for transitions, one has to ensure that the actions of transitions (assignments and arithmetic operations) can be realized with constraints (that is, with set of values of D instead of only one value of D). This requirement is ful lled by de ning the operations with set of values similarly as in the interval arithmetic 19].

Having seen what are the basic requirements and an approach to ful ll them, the de nition of constraint propagation problem follows below.

De nition 9 (constraint propagation). Let SP = (S; C; P) be the specication and f the set of feeds. Constraints are represented, for each process, as a function Val : Q p ! 2 D . With the notations presented before, the constraint propagation problem is de ned as nding the least x point solution of the following equation system:

Val(q 0 p ) = F t p :q p ?!q 0 p Transfer t p (Val(q p )) In order to solve this problem we have considered the cases where constraints are expressed by means of constants and by integer intervals. This is due to the fact that in ttcn 12] the constraints have this kind of simple forms. The formal framework de ned above is applicable in these cases, using the Galois connection, a classical abstract interpretation technique 8].

The algorithm used for solving the constraint propagation problem in the case of the lattice of constants is the classical iterative algorithm from 16] with an interprocesses variant such as 9]. In the case of the integer intervals lattice, due to the fact that it has in nite height, we use for each process a widening technique as in 3].

The results of the constraint propagation problem are used in simplifying the speci cation by means of slicing. However, they also allow, for the outgoing output transitions of a control state, to have a conservative approximation of the parameters of the signals, thereby enabling generation of symbolic test cases.

De nition 10 (slicing wrt constraints). Let SP = (S; C; P) be a speci cation and f a set of feeds. We de ne the slice of the speci cation SP given the constraints computed wrt feeds to be the speci cation SP n c f = (S; C; P n c f ), where P n c f contains a sliced process p 0 for each process p 2 P. The slice for a process p = (X p ; Q p ; T p ; q 0 p ) is de ned as a process p 0 = (X p ; Q 0 p ; T 0 p ; q 0 p ), which operates on the same set of variables X p . The sets of states Q 0 p Q p and transitions T 0 p T p are the smallest ones which satisfy the following rules: ? q 0 p 2 Q 0 p q p 2 Q 0 p t p = q p ?!q 0 p Transfer t p (V al p (q p )) 6 = ; q 0 p 2 Q 0 p t p = q p ?!q 0 p 2 T 0 p Example 4. The slicing wrt constraints algorithm, applied for the speci cation and the test purpose from Figure 4, produces the speci cation shown in Figure 5. The value t for br is propagated to the source state of the transition with the guard :br] and thus determining that this transition and the following co!pa(?) will be never red. These transitions are detached from the speci cation. The constraint propagation problem, in this case, given the feed ci?sr( 1; 10]), provides for the parameter x in the transition co!sa(x) the interval 1; 100].

We have the following preservation result.

Proposition 3 (slicing wrt constraints correctness). Let SP = (S; C; P) be a speci cation, TP = (Q tp ; T tp ; q 0 tp ; Q acc tp ) and f a set of feeds which cover TP. The synchronous product between the models of SP and respectively SP n c f with the test purpose given the feeds f are strongly bisimilar, that is

Q ( d SP; TP; f ) Q ( \ SP n c f ; TP; f )

Experimentation

These techniques were implemented and currently we are experimenting with them on some case studies. We use the if 5] framework, which is an interme- The techniques presented before were applied to improve test case generation for the sscop protocol 6], a layer from the atm protocols stack. Previous work was already done on it in the context of the forma research action 6] and despite its success, it shows also the limitations of the existing test generation technology. We were interested to see what are the concrete bene ts of our addons.

We started with an sdl version of the protocol provided by cnet France Telecom. It is about 2000 lines of code which describes the whole protocol as a single sdl process. It was translated into an if extended automaton, with 1075 states, 1291 transitions and 134 variables. We considered 10 test purposes conceived for di erent phases of the protocol (connection, data transmission). The results obtained using previous analysis are summarized below: slicing wrt feeds: By carefully choosing the appropriate set of feeds for each test purpose, we obtained reductions up to 80% of the speci cation. That is, we started usually with the smallest set of feeds covering the test purpose inputs. This choice is often too restrictive i.e., test cases cannot be constructed from the model of sliced speci cation. Thus, we iteratively added other inputs to the feeds until the model became su ciently large to cover the test purpose behavior. In this way, we are able to work on some minimal version of the speci cation, still allowing the generation of test cases. slicing wrt outputs: This analysis gives very good results too. When applied on the sliced speci cation wrt to feeds, it reduces the number of variables up to 40%. More generally, for the sscop protocol we obtained, in average, that, from total number of variables, 30% are relevant with respect to outputs, while the maximum reaches 60%. Also, when used at the model generation time, the relevant variables still allow important reductions on the number of model states and transitions. constraint propagation: The constraint propagation is still under development. At this time, we experimented only the constant propagation algorithm. The results obtained are good, mainly when the test purpose and the feeds contains punctual constraints i.e., the values provided in test purpose inputs are xed at some constants. We work currently to adapt the interval propagation algorithm.

These results are very encouraging. However, given the particular nature of the sscop protocol, we need further experimentations to clearly set up our techniques. We will consider experimentations for interprocesses slicing and the interaction between the three slicing techniques.

Conclusion and future work

In this paper, we show that automatic test generation can take advantages of static analysis. Our test generation method, derived from the so-called on the y model checking, consists in traversing a product de ned between the speci cation and the test purpose. Before test generation, simpli cations may be made on the speci cation, by collecting informations on the test purposes.

Our general approach to de ne static analysis is based on the following considerations and remarks. The speci cation is a set of extended automata, asynchronously communicating via a set of queues. The test purpose is also an extended automaton with constraints. In the context of test generation, we distinguish between inputs and outputs. The static analysis we de ne transform speci cations into others, smaller ones, without loss of information with respect to test purpose. This approach is compatible with the standard de nition of conformance testing.

In this work, we proposed three kinds of slicing, based on di erent analysis. The rst one consists in restricting each automaton, starting from the set of feeds. It includes the propagation through the dependence relation between the input of a process and the outputs of the others process. The second analysis computes the set of variables, necessary to determine values occurring into the outputs, and safely discards the others. The last analysis is the constraint propagation.

We have shown that the combination of these three interprocesses analyses may reduce the speci cation. We have implemented these analysis in the context of if tools and we obtain very good results on the sscop protocol.

Our results can be further extended in several directions. Firstly, we aim at experimenting more systematically the static analysis in the context of test case generation for industrial protocols. The results on sscop were very encouraging but other experimentations are further needed to conclude the practical use of our techniques.

At short term too, we plan to extend these analysis techniques to work on timed speci cations. In fact, the generated test cases usually uses timers, which are set and test to more or less arbitrarily values in order to observe deadlocks or livelocks in the implementation. However, a more ne analysis can be done on timed speci cations to obtain relevant values to be used in this context.

A more speculative direction concerns the generation of symbolic tests. In this respect, we are currently thinking about the appropriate extension for the test purposes concept. For instance, the explicit use of variables in addition to constraints can make them much more expressive. Furthermore, it may be interesting to reconsider the de nition of the synchronous product i.e., to be done at a higher level in such a way that it will allow the derivation of symbolic test cases.

  Fig. 1. Test architecture

  Fig. 2. Example 3 Static analysis for testing

Fig. 3 .

 3 Fig. 3. Example slicing wrt feeds

Fig. 4 .

 4 Fig. 4. Example slicing wrt outputs Intuitively, the slicing wrt relevant outputs preserves the model of the specication up to concrete values carried by signals not observed in the test purpose. We de ne the renaming of the speci cation model d SP with respect to the set of output actions o in the following way: each visible output action c!s(v) which is not speci ed by the test purpose i.e., c!s( ) 6 2 o , is renamed into c!s(?). The other actions are left unchanged. In this way, we left out the exact parameter values for outputs, other than ones occurring in the test purpose. We note the renamed model with d SP # o . The following proposition holds.

Fig. 5 .

 5 Fig. 5. Example slicing wrt constraints diate program representation for protocols, based on asynchronously communicating timed automata. if was designed right from the beginning to support the application of static analysis techniques used in compiler optimization 1, 17].The techniques presented before were applied to improve test case generation for the sscop protocol 6], a layer from the atm protocols stack. Previous work was already done on it in the context of the forma research action 6] and despite its success, it shows also the limitations of the existing test generation technology. We were interested to see what are the concrete bene ts of our addons.We started with an sdl version of the protocol provided by cnet France Telecom. It is about 2000 lines of code which describes the whole protocol as a single sdl process. It was translated into an if extended automaton, with 1075 states, 1291 transitions and 134 variables. We considered 10 test purposes conceived for di erent phases of the protocol (connection, data transmission). The results obtained using previous analysis are summarized below:

? Work partially supported by R egion Rhône-Alpes, France ? ? ? VERIMAG is a joint laboratory of CNRS, UJF and INPG Grenoble

This assumption is strong, however it can be veri ed during the test generation process (as in tgv 10]).


Mehrdad Yaghoobi
email: yaghoobi@ieee.org

Laurent Daudet
email: daudet@lam.jussieu.fr

Mike E Davies
email: mike.davies@ed.ac.uk

Parametric Dictionary Design for Sparse Coding

Keywords: Sparse Approximation, Dictionary Design, Incoherent Dictionary, Parametric Dictionary, Gammatone Filter Banks, Exact Sparse Recovery

. A problem in using these parametric dictionaries is how to choose the parameters. In practice these parameters have been chosen by an expert or through a set of experiments. In the sparse approximation context, it has been shown that an incoherent dictionary is appropriate for the sparse approximation methods. In this paper we first characterize the dictionary design problem, subject to a minimum coherence constraint. Then we briefly explain that equiangular tight frames have minimum coherence. The parametric dictionary design is then to find an admissible dictionary close to being tight frame. The complexity of the problem does not allow it to be solved exactly. We introduce a practical method to approximately solve it. Some experiments show the advantages one gets by using these dictionaries.

I. INTRODUCTION

S PARSE modeling of signals has recently received much attention as it has shown promising results in different applications. A basic assumption to apply this model is that the given class of signals can be sparsely represented or approximated in an underdetermined linear generative model. In this framework, one can use a matrix D d×N ∈ R d×N : d < N , called dictionary, to represent the signal approximately using y ≈ Dx. Let y ∈ R d and x ∈ R N be the given signal and the coefficient vector respectively. A sparse approximation would be,

x = arg min

x x 0 s. t. y -Dx 2 ≤ ξ, (1)
where . 0 is the sparsity measure that counts the number of the non-zero coefficients and ξ is a small positive constant. Because this problem is generally NP-hard, numerous algorithms have been proposed to find an approximate solution. The sparsity of the approximation is increased using an appropriate dictionary for the given class of signals. A dictionary often is selected by concatenating orthogonal bases [START_REF] Gribonval | Sparse representations in unions of bases[END_REF] or using a tight frame [START_REF] Candes | The curvelet representation of wave propagators is optimally sparse[END_REF]. These dictionaries can be improved by dictionary learning methods, see [START_REF] Yaghoobi | Dictionary learning for sparse approximations with the majorization method[END_REF] and references therein. These methods adapt an initial dictionary to a set of training samples. Therefore the aim is to learn a dictionary for which an input signal, taken from a given class of signals, has a sparse approximation.

This research was fully supported by the UK's EPSRC, grant number D000246/1. MED acknowledges support of his position from the Scottish Funding Council and their support of the Joint Research Institute with the Heriot-Watt University as a component part of the Edinburgh Research Partnership.

There is another dictionary selection method, which is called dictionary design. Different methods exist to design a suitable D for a set of natural signals. One method is based on a generative model of the signals. Alternatively, if these signals are to be received by the human sensory system, a more effective method to design D is to use a human perception model [START_REF] Patterson | Time-domain modeling of peripheral auditory processing: a modular architecture and a software platform[END_REF], [START_REF] Daugman | Two-dimensional spectral analysis of cortical receptive field profile[END_REF]. Here, we assume that the set of elementary functions, which are generated by the proposed model, can be described by using a set of parameters and a parametric function. For example, in the multiscale Gabor functions, the parameters are scale, time and frequency shifts and the parametric function is Gaussian. In general the parameters are in the continuous domain. To generate a dictionary based on these generative functions, we can sample these continuous parameters. The question is then how best to sample the parameters. Several researchers have introduced different methods to optimize the sampling process. In [START_REF] Lee | Image representation using 2d gabor wavelets[END_REF], a sampling scheme was introduced which finds an approximately tight frame, using 2D Gabor functions. Alternatively, some researchers optimized the parameters based on the closeness to what is observed in the perceptual systems. In practice, [START_REF] Strahl | Sparse gammatone signal model optimized for english speech does not match the human auditory filters[END_REF] showed that the optimal Gammatone parameters, found by fitting to the human auditory system, do not match the parameters estimated from English speech signals.

When we use an approximate or a relaxed method to find a sparse approximation, having an exact generative model does not guarantee that we find the best sparse approximation. An important parameter of a dictionary, for successful sparse recovery, is its coherence µ [START_REF] Tropp | Greed is good: algorithmic results for sparse approximation[END_REF]. The coherence is defined as the absolute value of the largest inner-product of two distinct atoms and it has been shown that when µ is smaller than a certain threshold MP and BPDN can recover the sparse representation of the input signal [START_REF] Gilbert | Approximation of functions over redundant dictionaries using coherence[END_REF]. It has also been shown that the coherence upper-bounds the residual error decay in MP [START_REF] Gribonval | On the exponential convergence of matching pursuits in quasi-incoherent dictionaries[END_REF] and OMP [START_REF] Tropp | Greed is good: algorithmic results for sparse approximation[END_REF]. Therefore a dictionary with small µ is desirable for sparse coding. Let G := D T D be the Gram matrix of the dictionary. The coherence of D is the maximum absolute value of the off-diagonal elements of G, whenever the columns of the dictionary are normalized. For such D if the magnitude of all off-diagonal elements of G are equal, D has minimum coherence [START_REF] Tropp | Designing structural tight frames via an alternating projection method[END_REF]. This normalized dictionary is called an Equiangular Tight Frame (ETF) [START_REF] Sustik | On the existence of equiangular tight frames[END_REF]. Although this type of frame has various nice properties, we mainly consider its advantages in the exact atom recovery [START_REF] Tropp | Greed is good: algorithmic results for sparse approximation[END_REF] and the residual error decay rate [START_REF] Gribonval | On the exponential convergence of matching pursuits in quasi-incoherent dictionaries[END_REF]. Unfortunately ETF's do not exist for any arbitrary selection of d and N [START_REF] Sustik | On the existence of equiangular tight frames[END_REF]. Therefore a dictionary design aim can be to find the nearest admissible solution. On the other hand, natural signals do not generally have sparse approximations using an ETF. Therefore, the dictionary design problem can be to find a parametric dictionary whose Gram matrix is close to being the Gram matrix of an ETF. This way, domain knowledge is incorporated into the parametric functions and the initial parameters, while the optimization aims at improving the ability of algorithms to find sparse approximations. We expect to have a sparse approximation for the given class of signals using the proposed dictionary. That is because it is generated by sampling the parameters of generative functions fitted to the signal, whilst the dictionary has nice properties that allow exact atom recovery, because it is close to being an ETF. In practice we show that the designed dictionary indeed gives advantages over the standard dictionary, in terms of efficient sparse approximation. Another advantage of the parametric dictionary is that sparse approximation methods only need to store the parameters, instead of the full dictionary, which offers a huge reduction in memory requirement (the size of parameter matrix is much smaller than the size of the corresponding dictionary).

The parametric dictionary design also has some disadvantages. The method is explicitly not a data dependent method. Another difficulty in the given problem is that the current algorithm stores the Gram matrix explicitly. Therefore for a very large block of signal, the current method is not tractable.

A. Contributions of the paper

In this paper we introduce a new framework for dictionary design. To the authors knowledge, this formulation has not been considered previously. This formulation can be used to design a dictionary when dictionary learning is not possible, or is computationally intractable. We show how we can find an approximate solution using an alternating minimization type method.

The parametric dictionary is represented using a small number of parameters (often less than 5). Therefore we do not need to store the dictionary explicitly. This can save a considerable amount of memory when using sparse approximation algorithms.

Finally we show experimentally that there are sparse approximation benefits in using such a parametric dictionary for audio coding.

II. PARAMETRIC DICTIONARY DESIGN: FORMULATION

In this section we formulate the parametric dictionary design as an optimization problem. Let D Γ ∈ D be a parametric dictionary. Γ is the parameter matrix, with γ i as its i th column and D is the set of admissible parametric dictionaries. In this paper, by letting D Γ be a matrix with the atoms d i (with the associated parameters γ i ), we implicitly assume that the generative model is discrete. To select a Γ ∈ Υ, where Υ is an admissible parameter set, we can optimize an objective. In section I we explained that for a better performance in sparse coding, we are interested to design a dictionary which is close to being an ETF. For a given normalized D, the coherence of D, µ D , is defined by

µ D = max i,j:j =i {| d i , d j |}. (2)
A column normalized dictionary D G is called ETF, when there is a γ : 0 < γ < π/2 .

| d i , d j | = cos(γ) : ∀i, j i = j (3)
Strohmer et. al. in [START_REF] Strohmer | Grassmannian frames with applications to coding and communication[END_REF] showed that if there exists an ETF in D, here the set of d by N uniform frames1 , it is the solution of, arg min

D∈D {µ D }. (4)
To study the lower bound of µ D , the existence of an ETF and its Gram matrix, [START_REF] Strohmer | Grassmannian frames with applications to coding and communication[END_REF] introduced a theorem which shows that when D ∈ R d×N is a uniform frame, µ D is lower bounded by,

µ D ≥ µ G := N -d d(N -1) . ( 5
)
Equality holds in (5) if and only if D is an ETF. Furthermore, equality in (5) can only hold if

N ≤ d(d+1) 2 . Let Θ N d be the set of Gram matrices of all d × N ETF's. If G G ∈ Θ N
d then the diagonal elements and the absolute values of the off-diagonal elements of G G are one and µ G respectively. A nearness measure of D ∈ R d×N to the set of ETF's can be defined as the minimum distance between Algorithm 1 P arametric Dictionary Design [START_REF] Tropp | Designing structural tight frames via an alternating projection method[END_REF]. To optimize the distance of a dictionary to an ETF, we can solve,

1: initialization: k = 1, D Γ 1 ∈ D, {α i } 1≤i≤K : 0 < α i ≤ 1 2: while k ≤ K do 3: G Γ k = D T Γ k D Γ k 4: G P k+1 = min G∈Λ N G Γ k -G F 5: G R k+1 = α k G P k+1 + (1 -α k )G Γ k 6: D Γ k+1 ∈ D Γ k ∪ {∀D ∈ D : D T D -G R k+1 F < G Γ k -G R k+1 F } 7: k = k + 1 8: end while the Gram matrix of D and G G ∈ Θ N d
min Γ∈Υ,GG∈Θ N d D T Γ D Γ -G G ∞ , (6)
where the matrix operator . ∞ is defined as the maximum absolute value of the elements of the matrix. Instead, we would like to use a different norm space which simplifies the problem. An advantage of using ℓ 2 measure in the given problem is that it considers the errors of all elements (and not only the maximum absolute error). In this framework, when there is no ETF in D, we find a dictionary that is close to be quasi-incoherent [START_REF] Tropp | Greed is good: algorithmic results for sparse approximation[END_REF], [START_REF] Gribonval | On the exponential convergence of matching pursuits in quasi-incoherent dictionaries[END_REF]. Therefore we use the following formulation,

min Γ∈Υ,GG∈Θ N d D T Γ D Γ -G G 2 F , (7)
where . F is the Frobenius norm. This is a non-convex optimization problem in general. It might have a set of solutions or not have any solution (e.g. Θ N d is empty as there do not always exist ETF's for arbitrary N and d). One can extend Θ N d to a convex set Λ N [START_REF] Tropp | Designing structural tight frames via an alternating projection method[END_REF], which is non-empty for any N , by

Λ N = {G ∈ R N ×N : G = G T , diag G = 1, max i =j |g i,j | ≤ µ G }.
(8) Relaxing [START_REF] Strahl | Sparse gammatone signal model optimized for english speech does not match the human auditory filters[END_REF], by replacing Θ N d with Λ N , gives the following optimization problem.

min Γ∈Υ,G∈Λ N D T Γ D Γ -G 2 F ( 9
)
An important difference between ( 7) and ( 9) is that the relaxed problem is guaranteed to have at least one solution. We therefore use the relaxed formulation from now on. We show experimentally that the approximate solutions of (9), even though the Gram matrix of the dictionary might only be close to Λ N , show good performances in sparse approximation.

In the next section we introduce a practical method to find an approximate solution to [START_REF] Gilbert | Approximation of functions over redundant dictionaries using coherence[END_REF]. Our approach has similarities with alternating minimization. This method is guaranteed not to increase the objective function in each step. Because the objective is non-negative, the algorithm is stable due to Lyapunov's second theorem. One can also show that the objective function converges. The stability of the algorithm and the convergence of the objective function do not prove the convergence of the algorithm. The conditions under which the algorithm converges to a set of accumulation points are Algorithm 2 P arameters U pdate

1: initialization: l = 1, 1 ≤ L, Γ [0] k = Γ k , ǫ ∈ R + , φ(Γ) = D T Γ D Γ -G 2 F 2: for all l ≤ L do 3: Γ [l+1] k+1 = Γ [l] k -ǫ∇ Γ φ| Γ [l] k 4: l = l + 1 5: end for 6: Γ k+1 = Γ [L] k+1 discussed in Theorem 1.
We present a sketch of proof for this theorem and refer the reader to [START_REF] Yaghoobi | Parametric dictionary design for sparse coding[END_REF] for further details.

III. PARAMETRIC DICTIONARY DESIGN: A PRACTICAL ALGORITHM

A standard method to solve ( 9) is alternating projection. In this method we alternatingly project the current solution onto the admissible sets, see Fig. 1.a. In a finite dimensional setting when the admissible sets are convex, the algorithm converges to a solution in D ∩ Λ N and when D ∩ Λ N = ∅ to a pair of solutions in D and Λ N respectively. In the following, we derive a formulation for the projection onto Λ N , but there is no easy formulation for the projection onto the set of admissible dictionaries, in general. Therefore we choose a different method which has similarities with alternating minimization, see Fig. 1.b. In the alternating minimization framework, we choose the new solutions in D and Λ N alternatingly such that the objective does not increase in each update and is thus stable. If the algorithm converges, the fixed point is either in D ∩ Λ N , or is a pair of points in D and Λ N respectively.

Although the proposed algorithm has similarities with alternating minimization, it does not follow its steps exactly. The difference is that in the stage in which we update the current solution with respect to Λ N , we choose a point which is somewhere between the current solution and the projection onto Λ N . Fig. 1.c shows a schematic representation of the proposed method. The reason for this modification is that by projection onto Λ N , the structure of the Gram matrix changes significantly so that the selection of a new point in D in the following step is very difficult. We can gradually select a closer point to the projected point on Λ N , when the current D Γ is close to Λ N . In the other step, we update D such that it does not increase the objective in [START_REF] Gilbert | Approximation of functions over redundant dictionaries using coherence[END_REF].

The parametric dictionary design is summarized in Algorithm 1. In line 4, the algorithm finds the projection onto Λ N . In line 6, a point in D is selected which is closer to G R k+1 . In the following we show how we calculate the updates in lines 4 and 6.

A. Projection onto Λ N :

In the objective function [START_REF] Gilbert | Approximation of functions over redundant dictionaries using coherence[END_REF], G is a Hermitian matrix. By sign change of any related off-diagonal pair of elements , i.e. g i,j and g j,i , we get a new G ∈ Λ N . The closest G to D T Γ D Γ , in a Frobenius norm space, is then the G with a similar sign pattern. For a given G D = D T D : D ∈ R d×N , the projection of G D onto Λ N can be found by the following operator [START_REF] Tropp | Designing structural tight frames via an alternating projection method[END_REF],

g P i,j = sign(g D i,j )µ G i = j 1 otherwise , (10)
where µ G is as defined in [START_REF] Yaghoobi | Dictionary learning for sparse approximations with the majorization method[END_REF]. This operator can be used to find G P k+1 in line 4 of Algorithm 1, by applying into G Γ k .

B. Parameter update:

Let us assume D Γ is a differentiable function on Υ and therefore ( 9) is a differentiable function on Υ. An easy way to find Γ k+1 , such that it satisfies line 6 of the Algorithm 1, is to use the gradient descent method. We rewrite (9) as a minimization problem based on Γ when G R k+1 is fixed.

min Γ∈Υ φ(Γ) , φ(Γ) := D T Γ D Γ -G R k+1 2 F ( 11
)
The gradient of the objective function in [START_REF] Tropp | Designing structural tight frames via an alternating projection method[END_REF] can be found by chain rule for the matrix functions [15, D.1.3].

∇ Γ φ = ∇ Γ D Γ ∇ D Γ φ = 4∇ Γ D Γ (D Γ D T Γ D Γ -D Γ G R k+1 ) (12)
We iteratively use the gradient descent method to find a local minimum of the problem [START_REF] Tropp | Designing structural tight frames via an alternating projection method[END_REF]. Let Γ

[0] k = Γ k , the updating formula is as follows, Γ [l+1] k+1 = Γ [l] k -ǫ∇ Γ φ| Γ [l] k , (13)
where ǫ is a small positive value. In this framework, Γ k+1 = lim l→∞ Γ

[l]

k+1 . In practice we stop after a given number of iterations or when ǫ∇ Γ φ| Γ [l] k becomes very small. Algorithm 2 summarizes this parameter update algorithm.

The convergence of Algorithm 1 is guaranteed by the following theorem.

Theorem 1: [14, Theorem 3] Let D Γ be differentiable. The Algorithm 1 converges to a set of fixed points by starting from Γ 0 ∈ Υ, where Υ is a compact set.

We only present a sketch of proof in this paper. We first show that the algorithm reduces the distance of G Γ k to G k in each parameter update. We then show that the objective function of ( 9) is a continuous function of Γ, which implies the compactness of the solution space. The proof of Theorem 1 is completed by applying Bolzano-Weierstrass theorem, which guarantees existence of at least one accumulation point for the sequences of dictionaries {D Γ k } k∈N . Line 6 of Algorithm 1 prevents the existence of a continuum of accumulation points. Therefore, the accumulation points are fixed points.

IV. CASE STUDY

The problem we formulated in this paper is developed in a general form. To show the advantages of using parametric dictionary design in practice, we choose a case study. In sparse audio processing, an important question is how to choose the dictionary [START_REF] Davies | Sparse audio representations using the MCLT[END_REF], [START_REF] Pichevar | A biologically-inspired low-bit-rate universal audio coder[END_REF]. We show that the parametric dictionary design improves the performance of audio sparse approximation and exact recovery based around a Gammatone representation.

A. Gammatone parametric dictionary

The generative function for a Gammatone dictionary is as follows,

g(t) = at n-1 e -2πbBt cos(2πf c t) (14)
where B = f c /Q+b min , f c is the center frequency and n ∈ N, a, b, Q, b min are some constants. The optimal parameter selection is not easy. The dictionary is often generated by sampling the parameters of g(tt c ), where t c is the timeshift. Here, γ = [t c f c n b] T are the optimization parameters. The parameters t c and f c change the center of the atoms in the time-frequency plane. n and b control the rise time and the width of the atoms in the time domain, respectively. The parameter a is chosen to normalize the atom to unit length. Let {γ i } 1≤i≤N be a set of the parameters and g γi (t) be the atom generated using γ i . The parameter matrix Γ and the parametric dictionary D Γ are generated using γ i and g γi (⌊tf samp ⌋) as the columns respectively, where f samp is the sampling frequency.

To use the gradient discent method for parameter update, D Γ should be differentiable with respect to Γ. We can extend [START_REF] Yaghoobi | Parametric dictionary design for sparse coding[END_REF] to a more general function using n ∈ R. This function is differentiable with respect to Γ. We can choose an upper bound for the magnitude of each parameter to generate a bounded admissible set. By including the boundary values, Υ is a compact set that guarantees convergence of the algorithm to a set of fixed points. A necessary modification in Algorithm 1 is to use a mapping to Υ, when at least one parameter goes out of Υ, and comparing to the previous solution (to make sure that we do not increase the objective by the parameter update). A simple mapping operator is the thresholding operator, where it chooses the closest admissible parameter.

B. Simulations results

We study the proposed dictionary design method using the Gammatone dictionary discussed in IV. We first investigate the characteristics of the dictionaries throughout the design iterations. We then compare the performance of the initial and the optimized dictionaries in terms of sparse approximation and exact sparse recovery. In all the simulations we choose two times overcomplete dictionaries and window size 1024.

1) Algorithm Evaluation:

We evaluate the given algorithm in three different areas. In the first step we show that the algorithm reduces, (or at least keep the same) the objective ( 9) in each iteration. The parameter B, defined after [START_REF] Yaghoobi | Parametric dictionary design for sparse coding[END_REF], is the bandwidth of the audio filterbank at the center frequency f c . We used the fixed values n = 4, Q = 9.26449, b min = 24.7, as they have been suggested in [START_REF] Slaney | Lyon's cochlear model[END_REF], and b = 0.65. To generate the initial dictionary, we sampled f c and t c . In the method introduced in [START_REF]An efficient implementation of the Patterson-Holdsworth auditory filter bank[END_REF], an extra parameter δ, called step factor, is introduced to indicate the amount of frequency overlap. In this framework the k th frequency center is calculate using the following formula.

f k c = -Qb min + (f s /2 + Qb min )e -kδ/Q (15)
f s is the maximum allowed frequency, which is half of the Nyquist frequency. In our simulations, we choose δ = 0.45.

We have chosen a similar method to sample t c . This time sampling is linear, in contrast with the logarithmic sampling in [START_REF] Dattorro | Convex Optimization and Euclidean Distance Geometry[END_REF]. Let the peak of the envelope of the impulse response of the filter be at t p and σ indicate the amount of time overlap. The l th time center is found using,

t l c = t p + σ(l -1) t p , (16)
where σ = 0.75.

To generate a dictionary of g γi (t), we windowed it to a size equal to the signal length d and made it periodic such that one period is selected as an atom by using the following formula,

d γi,j = g γi(j+d) 1 ≤ j < j ci g γi(j) j ci ≤ j ≤ d, (17)
where j ci = ⌊t ci f samp ⌋. We choose a simple sequence of {α k } using α k = α for all k and a constant α in all simulations. A more complicated sequence might improve the performance of Algorithm 1. However we have not present this here. Instead, we intend to show that the proposed algorithm works in practice, even with a simple {α k }. In the first experiment we want to investigate the effect of α. We have plotted the objective function (9) using selected α's, in Fig. 2. As we expect, simulations show reduction of the proposed objectives in each iteration. It is also demonstrated that if α is small, the algorithm converges very slowly. Although using a large α is desireable for a fast convergence, the solution is not as good as the solution found by using a medium range α. For other simulations we use α = 0.5 to find a good solution after an acceptable number of iterations.

The proposed algorithm searches for an equiangular tight frame. Therefore one way to show the performance of the proposed algorithm is to compare the singular values (SV) of the designed dictionary and the tight frame. A tight frame in R d×N has d non-zero SV equal to N/d. We have plotted the sorted SV's of the dictionaries at selected iterations in Fig. 3. It can be seen that the SV's of the designed dictionary get closer to the SV's of the tight frame after each selected number of iterations.

Given that the algorithm is based on distances in the Gram matrix domain, another way to evaluate the algorithm is to show the Gram matrix of the dictionary. We have plotted the ℓ 2 norm of each row of the Gram matrix in Fig. 4. The Gram matrix of the original dictionary and the designed dictionary, after 100 iterations, are shown in the left and right windows respectively. We have shown the ℓ 2 norm of a possible ETF with a dashed line as reference. It can be seen that the Gram matrix of the designed dictionary is closer to the desired Gram matrix.

2) Exact sparse recovery and sparse approximation: In this part we demonstrate the advantages of the parametric dictionary design in terms of exact sparse recovery [START_REF] Tropp | Greed is good: algorithmic results for sparse approximation[END_REF] and sparse approximation. In the first experiment we generate sparse coefficient vectors, with different sparsity, and plot the percentages of the exact recovery for those sparse vectors.

The location of the non-zero coefficients were selected uniformly at random and the PDF of the magnitudes were selected to be Gaussian with zero mean. The Matching Pursuit (MP) algorithm was used to find the sparse approximation. The rate of exact support recovery is calculated by the ratio of the number of correctly found non-zero coefficient places to the number of cases in which at least one location of the zero coefficient was set to be non-zero. We ran the simulations 1000 times. We have shown this ratio as the percentage of exact recovery in Fig. 5. It is clear that the design method has improved the exact recovery ratio.

For sparse approximation applications, we are more interested to have a dictionary that, if it fails to satisfy exact recovery condition [START_REF] Tropp | Greed is good: algorithmic results for sparse approximation[END_REF], still gives a sparse approximation for a given class of signals. Therefore as the second experiment, we compare the decay rates of the residual error when the MP is used for sparse approximation [START_REF] Gribonval | On the exponential convergence of matching pursuits in quasi-incoherent dictionaries[END_REF]. We used an audio signal taken from more than 8 hours recorded from BBC Radio 3, which mostly plays classic music. We first downsampled by a factor of 4 and summed the stereo channels to make a mono signal with 12K samples per second. We used the original Gammatone and the parametric designed dictionaries for 100 blocks, each with the length of 1024 samples. The average decay rate of the residual errors, in logarithmic scales, are shown in Fig. 6. This rate directly influences the performance of sparse approximation methods. That is, we can better approximate the signals with fewer coefficients using a high residual error decay rate dictionary. In Fig. 6, although the curves start with the same slope, after a few iterations, here 10, the designed dictionary shows a clear advantage.

V. CONCLUSION

We have introduced a signal independent dictionary design method. A parametric function, which is closely related to the given class of signals, was used to design a minimal coherence dictionary. In this framework we have shown that the dictionary design problem is to find an optimal set of parameters. This problem can in general not be solved exactly. Fortunately an approximate solution can be found using the proposed method. In some simulations we showed that A) the given method can find an appropriate set of parameters for the given case study and B) the designed dictionary showed promising performance advantages in terms of exact recovery and sparse approximation. The proposed framework can be extended to include extra constraints, such as to be shiftinvariance, quasi-incoherence, data dependence, to have tree structures or structures for fast implementations. That has been left for future work.

Fig. 1 .

 1 Fig. 1. Different alternating optimization methods: (a) Alternating Projection, (b) Alternating Minimization and (c) Proposed Method.

Fig. 2 .

 2 Fig. 2. The objective functions for different {α k } ∀k,α k =α , for a constant α.

Fig. 3 .

 3 Fig. 3. Eigen values plot of the dictionary.

Fig. 4 .

 4 Fig. 4. The column ℓ 2 plots of the Gram matrix of the original (left) and designed (right) dictionaries.

Fig. 5 .

 5 Fig. 5. Exact support recovery of the sparse signals.

Fig. 6 .

 6 Fig.6. The residual error using matching pursuit for sparse approximation of the audio signal.

A frame with unit column norms