Jean-Vivien Millo

S Ramesh

Shankara Narayanan

Ganesh Khandu

Compositional Verification of Evolving SPL

Keywords: Design verification, Software Product Line, SPIN, QSAT Vérification, Ligne de produits logiciels, SPIN, QSAT

This paper presents a novel approach to the design verification of Software Product Lines(SPL). The proposed approach assumes that the requirements and designs are modeled as finite state machines with variability information. The variability information at the requirement and design levels are expressed differently and at different levels of abstraction. Also the proposed approach supports verification of SPL in which new features and variability may be added incrementally. Given the design and requirements of an SPL, the proposed design verification method ensures that every product at the design level behaviorally conforms to a product at the requirement level. The conformance procedure is compositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. The method has been implemented and demonstrated in a prototype tool SPLEnD (SPL Engine for Design Verification) on a couple of fairly large case studies.

Introduction

Large industrial software systems are often developed as Software Product Line (SPL) with a common core set of features which are developed once and reused across all the products. The products in an SPL differ on a small set of features which are specified using variation points. The focus of this paper is on modeling and analysis of SPLs which have drawn the attention of researchers recently [START_REF] Benavides | Automated analysis of feature models 20 years later: a literature review[END_REF][START_REF] Classen | Symbolic model checking of software product lines[END_REF][START_REF] Cordy | Simulation relation for software product lines: Foundations for scalable model checking (to appear)[END_REF].

Many approaches have been proposed to describe SPLs, the most prominent one being feature diagrams. All these proposals seem to assume a global view of SPL as they start with a complete list of features and the variation points using a single vocabulary. All the subsequent SPL assets, like requirement documents, design models, source codes, test cases, documentations, share the same definition and vocabulary [START_REF] Czarnecki | Generative Programming: Methods, Tools, and Applications[END_REF][START_REF] Metzger | Variability management in software product line engineering[END_REF]. The assumption of a single homogeneous and global view of variability description is inapplicable in many practical settings, where there is no top level complete description of features and variabilities. They often evolve during the long lifetime of an SPL as new features and variabilities are added during the evolution. Further, SPL developers tend to use different representations and vocabulary of variability at different stages of development: at the requirement level, a more abstract and intuitive description of variation points are used, while at the design level, the efficiency of implementation of variation points is of primary concern. For example, consider the case of an automotive SPL, where one variation point is the region of sale (eg. Asia Pacific, Europe, North America etc). At the requirement level, this variation point is expressed directly as an enumeration variable assuming one value for every region. Whereas, at the design level, the variation point is expressed using two or three boolean variables; by setting the values of the boolean variable appropriately, the behavior specific to a region is selected at the time of deployment.

We present a design verification approach that is more suited to the above kind of evolving SPLs in which different representation of variabilities would be used at the requirement and design level. One natural and unique problem that arises in this context is to relate formally the variation points expressed at different levels of abstractions. Another challenge is the analysis complexity: the number of products is exponential in the number of variation points and hence product centric analyses are not scalable. We propose a compositional approach in which every feature of the SPL is first analyzed independently; the per-feature analysis results are then combined to get the analysis result for the whole SPL.

For capturing variability in the behavior of an SPL, we have extended the standard finite state machine model, which we call Finite State Machines with Variability, in short, FSMv. The behavior and variability of a feature at the requirement and design level can be modeled using FSMv. We define a conformance relation between FSMvs to relate the requirement and design models. This relation is based upon the standard language containment of state machines.

One unique feature of FSMv is that it provides a compositional operator for composing the feature state machines to obtain a model for an SPL. This operator thus enables incremental addition of features and variabilities. The proposed verification approach exploits the compositional structure of the SPL models to contain the analysis complexity. Figure 1 summarizes the proposed approach. It shows an SPL composed of features f 1 to f n . Each feature has an FSMv model of its requirements (called FSMr) and an FSMv model derived from its design (called FSMd). The proposed analysis method checks whether the FSMd of every feature conforms to its FSMr (1 st check). The output of this first step is a conformance relation between each pair of FSMr and FSMd. The obtained conformance relations are then used to check whether the actual behavior of the entire SPL conforms to the expected one (2 nd check). We reduce this check to checking the satisfiability of a Quantified Boolean Formula (QBF). There is no need to build the entire behavioral model of the SPL in the second step.

We have built a prototype tool SPLEnD based upon this approach. This tool performs the first check using SPIN [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF] while the the well-known QBF SAT solver CirQit [START_REF] Goultiaeva | Exploiting qbf duality on a circuit representation[END_REF] is used for the second step. We have experimented with the tool using modest industrial size examples with very encouraging results.

Related works

FSMv and the proposed design verification approach were developed independently but has some apparent similarities with the FTS + model [START_REF] Classen | Symbolic model checking of software product lines[END_REF], which also extends finite state machines to include certain product variability information. However, there is a motivational difference between the two formalisms. The aim of FTS + is to model the entire SPL and hence there is a single global machine with a single global vocabulary for expressing variabilities; the variability information represents the presence/absence of features in the SPL. In contrast, our approach is based upon a differnt view of SPL: a feature with variability is an increment in functionality and an SPL is a collection of features. We use a single FSMv to model a feature and a whole SPL is modeled as a parallel composition of FSMv machines.

SPL Design level

Inria

The difference in viewpoint has another consequence: FTS + models, since they model the entire SPL, tend to be large and hence has high analysis complexity. Efficient abstraction techniques are hence used for solving this problem [START_REF] Cordy | Simulation relation for software product lines: Foundations for scalable model checking (to appear)[END_REF]. Whereas, each FSMv models a fraction of functionality and hence can be analysed easily. Further, the entire SPL can be modeled as composition of FSMvs and can be efficiently analysed using composition techniques.

Many other behavioral models have also been proposed [START_REF] Kim Guldstrand Larsen | Modal i/o automata for interface and product line theories[END_REF][START_REF] Raclet | Modal interfaces: Unifying interface automata and modal specifications[END_REF][START_REF] Fantechi | Formal modeling for product families engineering[END_REF][START_REF] Gruler | Calculating and modeling common parts of software product lines[END_REF] which are usually coupled with a variability model such as OVM [START_REF] Metzger | Variability management in software product line engineering[END_REF], the Czarnecki feature model [START_REF] Czarnecki | Generative Programming: Methods, Tools, and Applications[END_REF], or VPM [START_REF] Gomaa | Managing variability in reusable requirement models for software product lines[END_REF] to attain a fair level of variability expressibility. Unlike all these approaches, FTS + [START_REF] Classen | Symbolic model checking of software product lines[END_REF] and FSMv capture the variability in an explicit way which we find more intuitive.

The Variation Point Model (VPM) of Hassan Gomaa [START_REF] Gomaa | Managing variability in reusable requirement models for software product lines[END_REF] distinguishes between variability at the requirement and design levels but no design verification approach has been presented. Kathrin Berg et al. [START_REF] Berg | Tracing software product line variability: from problem to solution space[END_REF] propose a model for variability handling throughout the life cycle of the SPL. Andreas Metzeger et al. [START_REF] Metzger | Disambiguating the documentation of variability in software product lines: A separation of concerns, formalization and automated analysis[END_REF] and M Riebisch et al. [START_REF] Riebisch | Optimizing design for variability using traceability links[END_REF] provide a similar approach but they do not consider the behavioral aspect. In the proposed approach, we extract the relation between requirement and design level variability from a behavioral analysis.

Kathi Fisler et al. [START_REF] Krishnamurthi | Foundations of incremental aspect model-checking[END_REF] have developed an analysis based on three-valued model checking of automata defined using step-wise refinement. Later on, Jing Liu et al. [START_REF] Liu | Compositional model checking of software product lines using variation point obligations[END_REF] have revisited Fisler's approach to provide a much more efficient method. Recently, Maxime Cordy et al. have extended Fisler's approach to LTL formula [START_REF] Cordy | Behavioural modelling and verification of real-time software product lines[END_REF]. Kim Lauenroth et al. [START_REF] Lauenroth | Quality assurance in the presence of variability[END_REF] as well as Andreas Classen et al. [START_REF] Classen | Symbolic model checking of software product lines[END_REF][START_REF] Cordy | Simulation relation for software product lines: Foundations for scalable model checking (to appear)[END_REF], and Gruler et al. [START_REF] Gruler | Modeling and model checking software product lines[END_REF] have developed model checking methods for SPL behavior. These methods are based on the verification of LTL/CTL/modal µ calculus formula.

All these verification methods assume a global view of variability and hence the representation of variability information is identical in both specification and the design. In contrast, in our work the specification and design involve variability information at different levels of abstraction and hence one needs mapping information between the two levels. Furthermore, our formalism allows incremental addition of functionality and variability and enables compositional verification.

Design Verification of a Single Feature

An SPL, in general consists of multiple features, each feature having different functionality and variability. A typical body control software of an automotive system is an SPL that has several features such as door lock, lighting, seat control etc. Each of these features has a distinct function and variability. For example, the locking behaviour of a door lock function has a variation point called transmission type. If the transmission type is manual then the door is locked after the speed of the vehicle exceeds a certain threshold value; for automatic transmission, the door is locked when the gear position is shifted out of park. In this section we will focus on modeling and relating the design of a single feature to its requirement.

FSMv and language refinement

Finite State Machines with Variability (FSMv) is an extension of finite state machines, to represent all possible behaviours of a feature. Let V ar be a finite set of variables, each taking a value ranging over a finite set of values. Let x ∈ V ar, and let Dom(x) be the finite set of values that x can take. Let S ⊆ Dom(x). The set of atomic formulae we consider are x = a, x = a, x ∈ S, x / ∈ S for a ∈ Dom(x) and x = y, x = y for x, y ∈ V ar. Let A V ar denote the set of atomic formulae over V ar. Let α represent a typical element of A V ar . Define ∆ ::

= α | ¬∆ | ∆ ∧ ∆ | ∆ ∨ ∆ |∆ ⇒ ∆
to be the set of all well formed predicates over V ar.

Definition 1 (FSMv). An FSMv is a tuple A = Q, q 0 , Σ, V ar, E, ρ where: (1) Q is a finite set of states; q 0 is the initial state; (2) Σ is a finite set of events; (3) V ar is a finite set of variables; (4) E ⊆ Q × ∆ × Σ × Q gives the set of transitions. A transition t = (s, g, a, s ) represents a transition from state s to state s on event a; the predicate g is called a guard of the transition t; g is consistent and defines the variability domain of the transition; (5) ρ ∈ ∆ is a consistent predicate called the global predicate.

The variables in V ar determines the variability allowed in the feature with each possible valuation of the variables corresponding to a variant. The allowed values of the variables are constrainted by the global predicate ρ. For example, if ρ is ((x = 1) ∨ (x = 2)) ∧ (x = y -1), then the allowed variants are those for which the values for the pairs (x, y) are (1, 2), [START_REF] Berg | Tracing software product line variability: from problem to solution space[END_REF][START_REF] Classen | Symbolic model checking of software product lines[END_REF]. The predicate in a transition determines the variants to which the transition is applicable. While drawing a transition t = (s, g, a, s ), the edge connecting s to s is decorated with g : a. When g is true, we simply write a on the edge. Definition 2 (Configuration). A configuration, denoted by π, is an assignment of values to the variables in V ar. The set of all configurations is denoted by Π V ar , or Π, when V ar is clear from the context. Define Π(ρ) = {π | π |= ρ} to be the set of all those configurations that satisfy ρ. The elements of Π(ρ) are called valid configurations. Given a valid configuration π and a transition t = (s, g, a, s ), we say that t is enabled by π if π |= g.

As a concrete example of an FSMv, consider the feature Door lock in automotive SPL which controls the locking of the doors when the vehicle starts. The expected behavior of this feature is modeled using the FSMv Req dl described pictorially in Figure 2. In the initial state, this feature becomes active when all the doors are closed. The doors are locked when either the speed of the vehicle exceeds a predefined value or the gear is shifted out of park. An unlock event reactivates the feature. There are four configurations for this feature all of which are described using the three variables: DL_Enable, T ransmission dl and DL_U ser_P ref

Requirement against Design

In the requirement of a product line, the variability is usually discussed in terms of variation points, which are at a high level of abstraction and focused on clarity and expressibility. The restriction of the possible configurations is expressed as general constraints on these variation points, e.g., the global predicate M anual =⇒ Speed in the Door lock example. In contrast, in a design, the variability description is constrained by efficiency, implementability, ease of reconfiguration and deployment considerations. For instance, in the automotive applications, one often finds calibration parameters ranging over a set of boolean values. Further, the constraint on the calibration parameters (ρ) takes the special form of the list of the possible configurations of the calibration parameters in order to easily configure the design.

FSMv can capture both the design as well as the requirements of a feature. We distinguish the requirement and design models by denoting them FSMr and FSMd respectively. Figure 2 presents the FSMr, Req dl , of the feature Door lock. The FSMd, Des dl , of the feature Door lock is presented in Figure 3. The structure of Des dl is similar to Req dl except that the top elliptical shaped state in Figure 2 is split into two states (the top and the bottom elliptical shaped states) in Figure 3. The top state is for auto-transmission whereas the bottom one is for manual transmission as can be seen from the configuration label of the two transitions going from the initial state. Two variables Cp1 and Cp2 encode the possible configurations in the FSMd. The box in Figure 3 depicts the set of possible values of these. Cp1 = Auto corresponds to the configuration in which the transmission is Auto whereas Cp1 = M of f corresponds to either the manual transmission or the case when Cp1 is disabled; similarly, Cp2 = Speed means that the user preference is set on Speed, while Cp2 = P of f means either P ark or the case when Cp2 is disabled.

Variants of FSMv and Conformance

Having described the design and requirement behaviour of a feature f using FSMd and FSMr respectively, we now define the notions of variants and conformance. A variant of an FSMv corresponds to one of the several possible behaviours of the feature (at the design, requirement level respectively). Given a feature f , and a (FSMd, FSMr) pair corresponding to f , we say that the design of f conforms to the requirements of f provided every variant of the FSMd has a corresponding FSMr variant.

Definition 3 (Variant of an FSMv). Let A = Q, q 0 , Σ, V ar, E, ρ be an FSMv and π ∈ Π(ρ) be a valid configuration of A. A variant of A is an FSM obtained by retaining only transitions t = (s, g, a, s ), and states s, s such that g |= π.

Once the relevant states and transitions are identified, we remove the guards g from all the transitions; ρ is also removed. The resultant FSM is denoted A ↓ π.

In the example of FSMr for the feature Door lock, the variant Req dl ↓ Enable, Auto, P ark does not contain the transitions with the event Speed > n and * . We compare the FSMd and FSMr of a feature f using their variants. Given an FSMv A, we associate with each configuration π of A the language of the FSM A ↓ π, denoted by L(A ↓ π). We say that an FSMd A d conforms to an FSMr A r if and only if the behaviour of every variant of A d is contained in the behaviour of some variant of A r .

Definition 4 (The conformance mapping Φ). Let A r and A d be a pair of FSMr and FSMd respectively with global predicates ρ d and ρ r . Let Π d , Π r be the set of all design, requirement configurations. Then

A d conforms to A r denoted A d ≤ Φ A r if there exists a mapping Φ : Π d (ρ d ) → 2 Πr(ρ r ) such that ∀π d ∈ Π d (ρ d ), ∃π r ∈ Π r (ρ r ) satisfying L(A d ↓ π d ) ⊆ L(A r ↓ π r ). Φ is called the conformance mapping.
In the feature Door lock, Φ( M of f, Speed ) contains Enable, M anual, Speed since L(Des dl ↓ M of f, Speed ) ⊆ L(Req dl ↓ Enable, M anual, Speed ).

Inria

Checking the conformance

Let f be a feature with FSMr Req f and FSMd Des f . Then the conformance checking problem is to compute a mapping Φ such that Des f ≤ Φ Req f .

The conformance mapping is computed by comparing every projection of Des f with every projection of Req f . Algorithm 1, given below, presents a possible implementation using the standard automata containment algorithm [START_REF] Vardi | An automata-theoretic approach to automatic program verification[END_REF], as implemented in the SPIN model checker [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF]. To use SPIN, one should describe the system along with the checked property in the Promela language [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF]. Out of this description, SPIN generates the pan.c file which is the verifier for the system. After compilation, the pan(.exe) executable performs the verification. The details of the conformance checking using Algorithm 1 and its correctness can be found in Appendix A. Lemma 5 proves the correctness of Algorithm 1.

Algorithm 1 implements the conformance checking using SPIN.

Input : Des f , Req f . Output : The mapping Φ when Des f ≤ Φ Req f 1. Generate a Promela file which contains Req f , Des f , the environment, the never claim, and the initialization sequence. Proof. The proof can be found in Appendix A.1.

Design Verification of SPL

In the previous section, we looked at individual features in an SPL and provided a method for comparing the design and requirements of a feature, both containing variabilities. In this section, we extend this method to verifying a whole SPL design against its requirements. An SPL is essentially a composition of multiple features satisfying certain constraints. We define a parallel composition operator over FSMv to model an SPL. The features in an SPL can interact and we follow one of the standard methods of allowing the composed FSMv models to share some common events, which correspond to two-party handshake communication events. A distinguishing aspect of the proposed parallel operator is that it takes into account the constraints across the composed machines. The constraints could be of various types, e.g. dependency and exclusion relations, and are modeled as predicates over variables of the composed features.

Definition 6 (Parallel composition of FSMv).

Let A x = Q x , q x 0 , Σ x , V ar x , E x , ρ x , x ∈ {1, 2} be two FSMv's with V ar 1 ∩ V ar 2 = ∅. Let H = Σ 1 ∩ Σ 2 be
the set of handshaking events. Let ρ 12 be a predicate over V ar 1 ∪ V ar 2 , such that ρ 12 ∧ ρ 1 ∧ ρ 2 is consistent. ρ 12 is the composition predicate capturing the possible constraints between the variabilities of the two composed features. Let

ρ = ρ 12 ∧ ρ 1 ∧ ρ 2 .
The parallel composition of A 1 and A 2 denoted by

A = A 1 A 2 is a tuple Q 1 ×Q 2 , (q 1 0 , q 2 0 ), Σ 1 ∪Σ 2 , V
) ∈ Q 1 × Q 2 , and transitions (s 1 , g 1 , a 1 , s 1 ) ∈ E 1 and (s 2 , g 2 , a 2 , s 2 ) ∈ E 2 . (1) If a 1 = a 2 = a ∈ H, define ((s 1 , s 2 ), g 1 ∧ g 2 , a, (s 1 , s 2 )) ∈ E, provided g 1 ∧ g 2 is consistent and g 1 ∧ g 2 |= ρ. (2) If a 1 ∈ Σ 1 \H, define ((s 1 , s 2 ), g 1 , a 1 , (s 1 , s 2 )) ∈ E, g 1 |= ρ. (3) If a 2 ∈ Σ 2 \H, define ((s 1 , s 2 ), g 2 , a 2 , (s 1 , s 2 )) ∈ E, g 2 |= ρ.
For illustration, consider the feature Door unlock which automates the unlocking of the doors in a vehicle. Figure 4-a gives the FSMr of the feature extracted from the requirements. From the initial state, the feature becomes active when the event Lock happens. As soon as either the key is removed from ignition or the gear is shifted to park position, the doors get unlocked and the feature Door unlock becomes inactive. Figure 4-b presents the FSMd of the feature Door unlock. It is quite similar to the requirement except that the active state is split in two: the feature reacts to the ignition Off event in one state, and to the Shift Into Park event in another state.

Let us consider the composition of the two FSMrs of the features Door lock and Door unlock. The handshake events between the two features are Lock and Unlock. In the composition, we introduce the following composition predicate: (DU _Enable = Enable ⇔ DL_Enable = Enable) ∧ T ransmission dl = T ransmission du , which brings out the natural constraints that Door lock feature is enabled if and only if Door unlock is also enabled and the transmission status has to be the same.

The valid configurations after composition are restricted by the composition predicate. We provide a few definitions to define composite valid configurations.

Definition 7 (Composing Configurations).

Let A i = (Q i , q i 0 , Σ i , V ar i , E i , ρ i ) be two FSMv's, and let A = A 1 A 2 be as given by definition 6. Let ρ = ρ 12 ∧ρ 1 ∧ρ 2 be the global predicate of A. Consider two valid configurations π 1 ∈ Π(ρ 1 ) and π 2 ∈ Π(ρ 2 ) of A 1 and A 2 . The compostion of π 1 , π 2 , denoted π 12 is a configuration over V ar 1 ∪ V ar 2 such that π 12 agrees with π 1 over V ar 1 , and agrees with π 2 over V ar 2 , and π 12 |= ρ. π 12 is a valid configuration of A and we denote it by π 12 = π 1 + π 2 . Proof. In Appendix B.

Inria

In the example of feature Door Lock, the configuration Enable, Auto, Speed from Req dl can be composed with Enable, Auto, Key from Req du because the transmission is Auto in both (which is specified in the composition predicate). Enable, Auto, Speed, Enable, Auto, Key is a configuration of the parallel composition of Req dl with Req du .

The parallel composition of FSMv's is such that each variant of the composition of two FSMv's is equal to the composition of variants of the individual FSMv's.

Lemma 9 (Variants of a composed FSMv). Let A 1 and A 2 be two FSMv machines. Let π be a valid configuration of

A 1 A 2 . Then L([A 1 A 2 ] ↓ π) = L(A 1 ↓ π) L(A 2 ↓ π). 1
Proof. In Appendix C.

Refinement and Parallel Composition

The definition of parallel composition naturally lends itself to a notion of addition of conformance mappings between design and requirement pairs. Consider FSMr's R 1 , R 2 corresponding to two features f 1 , f 2 . Let D 1 , D 2 be the corresponding FSMd's. Let ρ r 1 , ρ r 2 be the global predicates of R 1 , R 2 , and let ) in R 1 , R 2 respectively. Given this, the addition of Φ 1 , Φ 2 is defined as follows:

ρ d 1 , ρ d 2 be the global predicates of D 1 , D 2 respectively. Assume that D 1 ≤ Φ1 R 1 and D 2 ≤ Φ2 R 2 . Let ρ r = ρ r 12 ∧ ρ r 1 ∧ ρ r 2 be the global predicate of R 1 R 2 ; likewise, let ρ d = ρ d 12 ∧ ρ d 1 ∧ ρ d 2 be
Definition 10 (Addition of conformance mappings). The addition of conformance mappings Φ 1 , Φ 2 is defined to be a mapping Φ = Φ 1 + Φ 2 as follows. For every valid configuration

π d = π d 1 + π d 2 of D 1 D 2 , Φ(π d ) = {π r | π r is a valid configuration of R 1 R 2 , π r = π r 1 + π r 2 for valid configurations π r 1 ∈ Φ 1 (π d 1 ), π r 2 ∈ Φ 2 (π d 2 )}
Lemma 11 (Conformance of composition). Let R 1 and R 2 be two FSMr machines corresponding to features f 1 , f 2 , and let D 1 and D 2 be the corresponding FSMd machines. Let

D 1 ≤ Φ1 R 1 and D 2 ≤ Φ2 R 2 . Let Φ = Φ 1 + Φ 2 and π d be a valid configuration of D 1 D 2 . Then, ∀π r ∈ Φ(π d ), L([(D 1 D 2 ) ↓ π d ]) ⊆ L([(R 1 R 2 ) ↓ π r ]).
Proof. In Appendix D.

Considering the example, in the FSMr Req dl Req du with ρ r : DL_Enable = DU _Enable ∧ T ransmission dl = T ransmission du , Any configuration where DL_Enable = Enable but DU _Enable = Disable is invalid. However, Φ( Auto, Speed ) contains only configurations where DL_Enable = Enable, Φ ( M of f, P of f ) contains only configurations where DU _Enable = Disable and Auto, Speed + M of f, P of f is a valid configuration of Des dl Des du . So the design does not conform to the requirement. However, if we make the extra assumption that ρ d : Cp1 = M of f ∧ Cp2 = P of f ⇔ Cp3 = M of f ∧ Cp4 = P of f , then Auto, Speed and M of f, P of f are not compatible anymore and as a result the design conforms to the requirement.

Conformance Checking

Let F = {f 1 , ..., f n } be a set of features and F be the complete system comprising the features in F , along with the relations between the features. Let R i be the FSMr modeling the expected behavior and variability of f i , and D i the FSMd extracted from the design of f i . Let ρ r 12...n and ρ d 12...n be the compositional predicates for R 1 • • • R n and D 1 • • • D n respectively. Now we state the variability conformance problem for an SPL as follows: Does there exist a conformance mapping Φ such that

D 1 • • • D n ≤ Φ R 1 • • • . . . R n ?
A compositional approach to solve the problem is to: (i) check whether the design of every feature conforms to its requirement using Algorithm 1; (ii) check whether every valid configuration of D 1 • • • D n can be mapped to a valid configuration of R 1 • • • R n . This is the conformance condition.

Inria

Checking Conformance Using QBF

We implement the second check using QBF solving. Given FSMd's D 1 , . . . , D n and FSMr's R 1 , . . . , R n , (1) Let V ar(D i ) = {v d i1 , . . . , v d in } be the set of variables of design D i , and

V ar(R i ) = {v r i1 , . . . , v r im }, the set of variables of requirement R i . Let π d : (v d i1 = a 1 , . . . , v d in = a n ) be a configuration of D i . We denote by π d i (x i1 , . . . , x in ) a formula which takes n values from Dom(D i ), 1 ≤ i ≤ n as arguments. If (v d i1 = a 1 , . . . , v d in = a n ) is a chosen assignment, then π d i (x i1 , . . . , x in ) is the conjunction n j=1 (x ij = a j );
(2) Given n FSMd's and n FSMr's check if D i conforms to R i for all 1 ≤ i ≤ n using Algorithm 1. This gives the map Φ i . Assume Φ i (π d i ) = {π r i1 , . . . , π r im }, where each of π r i1 , . . . , π r im are configurations of R i , that have been mapped by Φ i to some configuration π d i of D i . (3) We encode the above conformance mapping using the formula Φ i (x i1 , x i2 , . . . , x in ) = m j=1 π r ij (y i1 , . . . , y il ), where x ij takes values from Dom(v d ij ), and

y ij from Dom(v r ij ). (4) Let ϕ d i,j = ρ d ∧ ρ d i ∧ ρ d j and ϕ r i,j = ρ r ∧ ρ r i ∧ ρ r j represent
respectively the propositional formulae which ensures consistency of the global predicates of D i , D j and R i , R j along with the compositional predicates ρ d and ρ r . Given a set S ⊆ {1, 2, . . . , n}, ϕ d S and ϕ r S can be appropriately written. The QBF formula for conformance checking is given by

Ψ = ∀x 11 . . . x nin [ϕ d 1,2,...,n ⇒ ∃y 11 . . . y njn (Φ 1 ∧ • • • ∧ Φ n ∧ ϕ r 1,2,...,n )]
Theorem 12. Given a SPL, let {f 1 , . . . , f n } be the set of features in a chosen product. Let D i , R i be the FSMd and FSMr for feature

f i . Then D 1 • • • D n conforms to R 1 • • • R n iff Ψ holds.
Proof. In Appendix E. Figure 5 pictorially describes the tool SPLEnD. It takes as input, a pair of xml files corresponding to FSMd, FSMr and outputs a PROMELA file. The latter is fed to SPIN, which returns the conformance mappings, or declares nonconformance; given the conformance mapping the tool computes a QBF formula Ψ which is fed to CirQit.

Implementation and Case Studies

We considered two real case studies for our experimentation: Entry Control Product Line, ECPL having 7 features and Banking Software Product Line, BSPL, composed of 25 features. Appendices F.1 and F.2, contain the details of ECPL and BSPL case studies. The FSMr, FSMd models of each feature contains less than 10 states.

The analysis results for the two case studies are summarized in Figures 7 and6 which gives the times taken by Algorithm 1. The number of product variants and the time taken for Algorithm 1 are very small in both case studies. In the case of ECPL, a bug was found in the feature Door Lock2 . In this case, after fixing the bug, for the second step we used SPIN which took 11 seconds. For BSPL, the second step was performed using the QBF approach and CirQit took just 0.005 seconds.

In the automotive domain, really very large SPLs are constructed [START_REF] Flores | Mega-scale product line engineering at general motors[END_REF]. Before undertaking the task of modeling such large examples, in order to quickly determine the scalability of our approach, we generated many random SPLs with 5000 to 25,000 features. Each of the corresponding FSMr/FSMd has two variables (four variants), and 3 to 8 states. Similar to the ECPL and BSPL cases, SPIN took very little time (less than 0.5 seconds) for each (FSMr, FSMd) pair. The composite FSMr/FSMd, and hence the QBF formula Ψ has then 10,000 to 50,000 variables. As we can see from Figure 8, the the time taken for the largest example is 196.69 seconds which is quite efficient. Encouraged by this result, we plan to take up the large industrial case studies.

Conclusion

This paper motivated the need for extending the classical design verification problem to evolving SPL in which features and variability information can be added incrementally. The novel aspects of the proposed work are: (i) it verifies that the variability at the design level conforms to that at the requirement level, (ii) it is compositional and (iii) it reduces the conformance checking problem to QBF sat solving. A prototype tool has been implemented and experimented with modest sized examples with encouraging results.

Sr

Appendix

A Conformance Checking using SPIN Algorithm 1 starts by generating a Promela file containing the definition of (i) the environment, (ii) Des f , (iii) Req f , (iv) the initialization sequence and (v) a never claim which holds for the language containment condition. During the initialization, the configuration of Des f and Req f are initialized with a random couple of configurations. Then the environment, followed by Des f and Req f are run atomically. The never claim assertion is : never((¬error(Des f ) ∧ error(Req f )), where error(X) means that X is in error state. The never claim is violated when the design is not in the error state but the requirement process is in the error state. This corresponds to a design configuration π d such that Des f ↓ π d handles an event, while Req f ↓ π r does not, for all possible requirement configurations π r . Algorithm 1 runs the full verification algorithm of SPIN for every pair (π d , π r ) of design and requirement configurations. SPIN(i.e. pan(.exe)) returns the list of pairs for which the conformance condition is violated. Every other pair is added to the conformance mapping Φ.

A.1 Proof of Lemma 5

Assume L(Des f ↓ π d ) ⊆ L(Req f ↓ π r ). Then there exists a word w ∈ L(Des f ↓ π d ) which is prefixed by u.e, with u a finite prefix of a word in L(Req f ↓ π r ), and e an event such that u.e is not a prefix of any word in L(Req f ↓ π r ). In such a situation, Des f does not go to the error state but Req f does.

Conversely, if L(Des f ↓ π d ) ⊆ L(Req f ↓ π r ), then whenever Des f is not in an error state, Req f will also not be in an error state.

B Proof of Lemma 8

Let π ∈ Π(ρ) with ρ = ρ 12 ∧ ρ 1 ∧ ρ 2 be a valid configuration of A 1 A 2 . ρ 1 and ρ 2 are the global predicates of A 1 , A 2 respectively, and ρ 12 is the composition predicate of A 1 , A 2 . By definition of valid configuration, π |= ρ; hence π |= ρ 1 and π |= ρ 2 . Since π is a configuration over V ar 1 ∪ V ar 2 , let us consider the restriction of π on V ar 1 , call the resulting configuration π 1 . Then π 1 |= ρ 1 . Similarly, call the restriction of π on V ar 2 as π 2 . Then π 2 |= ρ 2 . Then, π 1 , π 2 are respectively valid configurations of A 1 and A 2 . Hence, by definition 7, we obtain π = π 1 + π 2 .

C Proof of Lemma 9

We review some preliminary definitions before the proof. In the following, the operation stands for (i) shuffle of words, (ii) shuffle of languages, (iii)parallel Inria composition of FSMs, and (iv) parallel composition of FSMv. The context is clear in each case; hence there is no confusion. Definition 13. Let Σ 1 , . . . , Σ n be n finite sets of symbols. Let Σ be a finite set. Given a word w ∈ Σ * , we denote by w ↓ Σ i , the unique subword of w over Σ * i . For example, if Σ 1 = {a, b, e}, Σ 2 = {a, e, f }, and if we consider w = aef edef r ∈ {a, d, e, f, r} * , then w ↓ Σ 1 = aeee and w ↓ Σ 2 = aef eef . Definition 14. (Asynchronous Shuffle) Let Σ 1 , . . . , Σ n be n finite sets. Let

Σ = ∪ n i=1 Σ i . Consider n words u 1 , u 2 , . . . , u n , u i ∈ Σ * i . The asynchronous shuffle of u 1 , . . . , u n denoted u 1 • • • u n is defined as {w | w ↓ Σ i = u i }.
As an example, consider Σ 1 = {a, b, c, f }, Σ 2 = {a, d, e, f }, Σ 3 = {c, d, f }, and the words u 1 = abcf, u 2 = adf e, u 3 = dcf . Then the word w = abdcf e is in u 1 u 2 u 3 since, w ↓ Σ i = u i for i = 1, 2, 3. Similarly, the word w = adbcf e is also in u 1 u 2 u 3 . However, the word w = aebcf d is not in

u 1 u 2 u 3 , since w ↓ Σ 2 = aef d, not u 2 .
The definition of shuffle can be extended from words to languages. We use the same notation for the shuffle of sets, as well as for the shuffle of words.

The asynchronous shuffle of two languages L 1 , L 2 is defined as

L 1 L 2 = {w 1 w 2 | w 1 ∈ L 1 , w 2 ∈ L 2 }. For example, if L 1 = {abcf, abbf } is a language over Σ 1 = {a, b, c, f } and L 2 =
{adf e} is a language over {a, d, e, f }, then L 1 L 2 = {abcf adf e, abbf adf e} ={abcdf e, adbcf e, abdcf e, abbdf e, abdbf e, adbbf e}. Definition 15. Let M i = (Q i , q i , Σ i , δ i ) and M j = (Q j , q j , Σ j , δ j ) be complete FSMs. The asynchronous product of M i , M j is defined as the FSM M i M j = (Q i × Q j , (q i , q j ), Σ i ∪ Σ j , δ) where 1. δ((q, q ), a) = (δ i (q, a), δ j (q , a)), a ∈ Σ i ∩ Σ j , 2. δ((q, q ), a) = (δ i (q, a), q ), a ∈ Σ i , a / ∈ Σ j , 3. δ((q, q ), a) = (q, δ j (q , a)), a ∈ Σ j , a / ∈ Σ i .

On the common events, both FSMs move in parallel; otherwise, they move independent of each other.

It is known that L(M i M j ) = L(M i ) L(M j
). Now we start the proof of Lemma 9. Consider a valid configuration π of A 1 A 2 . As seen in Lemma 8, we can find valid configurations π 1 of A 1 and π 2 of A 2 such that π = π 1 + π 2 . The initial state of A 1 A 2 is (q 1 0 , q 2 0 ), where q 0 1 is the initial state of A 1 and q 0 2 is the initial state of A 2 . By definitions 6 and 15, if we consider a string w = a 1 a 2 . . .

a n ∈ L[A 1 A 2 ] ↓ π, then we can find strings w 1 ∈ L(A 1 ↓ π) = L(A 1 ↓ π 1 ) and w 2 ∈ L(A 2 ↓ π) = L(A 2 ↓ π 2 ) such that w = w 1 w 2 in the sense of definition 14. Hence, L[A 1 A 2 ] ↓ π ⊆ L(A 1 ↓ π) L(A 2 ↓ π).
The converse can be shown in a similar way.

for conformance of D 1 • • • D n with R 1 • • • R n does.
Since we assume that Φ exists, the QBF holds.

The converse can be shown in a similar way : that is, if the QBF formula Ψ holds, then

D 1 • • • D n will conform to R 1 • • • R n .

F Case Studies

In this section, we describe the two product lines that have been considered in the paper : (i) ECPL and (ii) BSPL.

F.1 ECPL

The Entry Control Product Line comprises all the features involved in the management of the locks in a car. In this study, we focus on the following features:

• Power lock: this is the basic locking functionality which manages the locking/unlocking according to key button press and courtesy switch press,

• Last Door Closed Lock: delays the locking of the doors until all the doors are closed. It is applicable when the lock command appends while a door is open,

• Door lock: automates the locking of doors when the vehicle starts,

• Door unlock: automates the unlocking of door(s) when the vehicle stops,

• Anti-lockout: is intended to prevent the inadvertent lockout situations: the driver is out of the car with the key inside and all the doors locked,

• Post crash unlock: unlocks all the doors in a post crash situation,

• Theft security lock: secures the car with a second lock.

Each feature is represented as a pair of state machines containing 3 to 10 states.

F.1.1 The variability constraints of the ECPL

Figure 9 presents the feature diagram of the ECPL (a la Czarnecki [START_REF] Czarnecki | Generative Programming: Methods, Tools, and Applications[END_REF]). This diagram presents the variability constraints of the ECPL at the requirement level (ρ f0 ). All the constraints represented by this diagram have to be considered during composition to guarantee the overall consistency of the SPL behavior.

The dark gray boxes are features of the ECPL: Power lock, Anti-lockout, Door lock, Door unlock, and Post crash unlock. The light gray boxes are configurations. The black arrow from the "Manual" configuration to the "Shift out of park" configuration and to the "Shift into park" configuration says that if the transmission is manual, the targeted configurations cannot be selected. i.e. In "Manual" configuration, there is no "park" gear.

F.2 BSPL

The Banking Software Product Line (BSPL) consists of 25 behavioral features.

The BSPL is used to derived the software for ATM, Bank, Online Banking and Mobile Banking. Figure 10 presents the feature diagram of the BSPL. Similar to ECPL, we ran Algorithm 1 on all the 25 features of BSPL. In section 4, Figure 6 presents the number of design configurations and execution time of Algorithm 1 for each feature. In the following, we elaborate on the FSMv of 2 features: (i) User Interface and (ii) Withdraw Money. The FSMd/FSMr Inria for all the features has states between 2 and 10 (both inclusive). Figure 11 is the FSMr for feature U ser Interf ace, which has U I as an event with global predicate ρ = {¬(uip = Disable)}. There is only one boolean variable, V ar = {uip}, uip takes values from {Enable, Disable}. corresponding to the FSMr in Figure 11 Figure 14 is the FSMd for the feature W ithdraw M oney. This FSMd shares all the events {W D, enterAmount, insuf f U serBal, inf ussAT M Bal, checkAT M Bal, Disburse, dispatch} of the FSMr. The global predicate is ρ = {(W DO = Enable ∧ ¬(med = Online)}. There are six variables, V ar = {W DO, med, p1, p2, p3, p4}. W DO takes values from {Enable, Disable}, med takes values from {Bank, AT M, Online}, p1 to p4 are boolean variables which assume the value true depending on whether a predicate is satisfied or not. These predicates can be seen in the box on the top left of Figure 14.

After running SPLEnD on the feature W ithdraw M oney, we get the illegal configuration in design as π = {W DO = Enable, med = AT M, p1 = T rue, p2 = It can be seen that the language of this FSM cannot be contained in any of the variants of the FSMr in Figure 13. So, we removed the transition in red from Figure 14, to obtain conformance. With this modified FSMd, we carried out the rest of the study. After construction of Φ for all features, SPLEnd created the QBF for the composite FSMd's and FSMr's. This QBF is converted to 'qpro' format which is an input format for CirQit QBF solver. CirQit verified this QBF formula, and returned the results to SPLEnD. The time taken by CirQit was 0.005 seconds.

Figure 1 :

 1 Figure 1: The proposed verification framework.

Figure 2 :

 2 Figure 2: The FSMv of the feature Door lock.

Figure 3 :

 3 Figure 3: Des dl : the FSMd abstracted from the design of the feature Door lock.

2 .

 2 Launch the full verification algorithm of spin 3. Build the mapping Φ from the output of spin. 4. Conclude whether the design conforms to the requirement if ∀π d ∈ Π(ρ d ), Φ(π d ) = ∅ then return true along with (Φ) else return f alse along with (π d ) {where π d has no correspondence through Φ} end if Lemma 5. Given FSMd Des f and FSMr Req f for a feature f , let (π d , π r ) be a pair of design and requirement configurations. Then, L(Des f ↓ π d ) ⊆ L(Req f ↓ π r ) if and only if ¬error(Des f ) ∧ error(Req f ).

Figure 4 :

 4 Figure 4: a) Req du : the Door unlock FSMr and b) Des du : the corresponding FSMd.

Figure 5 :

 5 Figure 5: Overview of SPLEnD

Figure 9 :

 9 Figure 9: The feature diagram of the ECPL.

Figure 10 :

 10 Figure 10: The feature diagram of the BSPL.

Figure 11 :

 11 Figure 11: FSMr for feature: U serInterf ace.

Figure 12 Figure 12 :

 1212 Figure 12 is the FSMd for feature U ser Interf ace. This FSMd shares the event U I with the FSMr and has global predicate ρ = {(type = 2D ∨ type = 3D)}. There are two variables, V ar = {type, graphics}, type takes values from {2D, 3D}, while graphics takes values from {Enable, Disable}. The xml file

Figure 13

 13 Figure 13 is the FSMr for the feature W ithdraw M oney, which has events {W D, enterAmount, insuf f U serBal, inf ussAT M Bal, checkAT M Bal, Disburse, dispatch} and global predicate ρ = {(W DO = Enable ∧ ¬(med = Online)}. There are two variables, V ar = {W DO, med}, W DO can take values from {Enable, Disable}, while med takes values from {Bank, AT M, Online}}.

Figure 13 :

 13 Figure 13: FSMr for feature: W ithdrawM oney.

Figure 14 :

 14 Figure 14: FSMd for feature: W ithdrawM oney.

Figure 15 :

 15 Figure 15: FSM for configuration π on FSMd.

  ar 1 ∪V ar 2 , E, ρ with transitions defined as follows: Consider a state (s 1 , s 2

  the global predicate of D 1 D 2 . We now want to ask if D 1 D 2 conforms to R 1 R 2 . This amounts to computing a conformance mapping between D 1 D 2 and R 1 R 2 given Φ 1 , Φ 2 . Consider any valid configuration π d of D 1 D 2 . By Lemma 8, we can write π d as π d 1 + π d 2 , where π d 1 , π d 2 are valid configurations of D 1 , D 2 respectively. Since D 1 ≤ Φ1 R 1 and D 2 ≤ Φ2 R 2 , there exists valid configurations π r 1 ∈ Φ 1 (π d 1 ) and π r 2 ∈ Φ 2 (π d 2

  is as below:The xml file for the FSMd in Figure12is as below:These two xml files are given as input to SPLEnD, which creates the PROMELA

	<group_of_final_states> </set_of_sets_of_final_states>
	<events>	<s>2</s>
	<e>UI</e>	</group_of_final_state>
	</events>	</set_of_sets_of_final_states>
	<events> <variables>
	<variable>	<e>UI</e>
	</events> <v_name>type</v_name>
	<variables> <value>2D</value>
	<variable> <value>3D</value>
	<v_name>uip</v_name> </variable>
	<variable>	<value>Enable</value>
	<value>Disable</value> <v_name>graphics</v_name>
	</variable> <value>Enable</value>
	</variables> <value>Disable</value>
	<rho> </variable>
	<conjunct>not(uip=Disable)</conjunct> </variables>
	<rho>	</<rho>
	<vds> <conjunct>or(type=2D,type=3D)</conjunct>
	</<rho>	<predicate>
	<vds>	<id>1</id>
	<equ>(uip=Enable)</equ> <predicate>
	<id>1</id>	</predicate>
	</vds> <equ>(type=2D)</equ>
	<transitions> </predicate>
	<t> <predicate>
	<id>2</id>	<start>1</start>
	<end>2</end> <equ>and(type=3D,graphics=Enable)</equ>
	<vdid>1</vdid> </predicate>
	</vds>	<events>UI</events>
	</t> <transitions>
	<t>	</transitions>
	</FSMv> <start>1</start>
	<end>2</end>
	<vdid>1</vdid>
	<?xml version='1.0'> <events>UI</events>
	</t>	<FSMv>
	<t>	<type>D</type>
	<?xml version='1.0'> <name>UserInterface_des</name> <start>1</start>
	<FSMv> <end>2</end> <states>
	<type>R</type> <s initial=true>1</s> <vdid>2</vdid>
	<name>UserInterface_req</name> <s>2</s> <events>UI</events>
	<states> </t>	</states>
	<s initial=true>1</s> <set_of_sets_of_final_states> </transitions>
	<s>2</s> </FSMv>	<group_of_final_states>
	</states>	<s>2</s>
	<set_of_sets_of_final_states> </group_of_final_state>
		Inria

RR n°8125

The right hand side refers to the standard communicating finite state machine composition.RR n°8125

In Des dl , the transition from the middle elliptical state to the round state labeled with P of f : Shif tOutOf P ark is incorrect; Φ( Auto, P of f ) = ∅. Removing this transition fixes the bug.Inria

RR n°8125 RESEARCH CENTRE SOPHIA ANTIPOLIS -MÉDITERRANÉE 2004 route des Lucioles -BP 93 06902 Sophia Antipolis Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

D Proof of Lemma 11

Given a valid configuration π d of D 1 D 2 , we can write it as π d 1 + π d 2 , where π d 1 , π d 2 are respectively valid configurations of D 1 , D 2 (Lemma 8). Since D 1 ≤ Φ1 R 1 and D 2 ≤ Φ2 R 2 , there exist valid configurations π r

. Since Φ has been computed, for every valid configuration

. This along with the observation that L(D

E Proof of Theorem 12

. . , i j }. Using Lemma 8 repeatedly, we can then say that

Given the above, we show that the QBF Ψ holds. The LHS of the QBF Ψ is the formula ϕ d 1,2,...,n , which is the conjunction ρ d S for all subsets S of {1, 2, . . . , n}. The forall quantifier outside would thus evaluate all configurations of

For the QBF to hold good, for all valid configurations of D 1 • • • D n that have been evaluated on the LHS, we must find some configuration of

By Lemma 8, this means that π can be written as π r 1 + • • • + π r n . Thus, for the QBF to hold, we must be able to find for each valid configuration


H G Feichtinger

D Onchis-Moaca

B Ricaud

B Torrésani

C Wiesmeyr

A METHOD FOR OPTIMIZING THE AMBIGUITY FUNCTION CONCENTRATION

In the context of signal analysis and transformation in the time-frequency (TF) domain, controlling the shape of a waveform in this domain is an important issue. Depending on the application, a notion of optimal function may be defined through the properties of the ambiguity function. We present an iterative method for providing such optimal functions under a general concentration constraint of the the ambiguity function.

At each iteration, it follows a variational approach which maximizes the ambiguity localization via a userdefined weight function F . Under certain assumptions on this latter function, it converges to a waveform which is optimal according to the localization criterion defined by F .

INTRODUCTION

In the context of time-frequency analysis (such as short time Fourier analysis or Gabor analysis), it is commonly agreed that best results are obtained when one uses window functions that are well localized in the time-frequency domain. In the mathematically idealized setting of continuous time, infinite support signals, i.e. functions on the whole real line R, the optimally localized waveforms in the TF domain are well known to be Gaussians [START_REF] Donoho | Uncertainty principles and signal recovery[END_REF]. The latter are the minimizers of the variance uncertainty inequality (Heisenberg uncertainty principle) as well as the Hirschman entropic inequality and the Lieb time-frequency inequalities [START_REF] Elliott | Integral bounds for radar ambiguity functions and wigner distributions[END_REF]. However, in other contexts, of importance for particular applications, the optimal function is not known; the localization criterion does not rely on such measures and the definition of optimality can be different. For example, in the discrete, finite time setting, the variance is not defined and the entropy point of view gives a "picket fence" signal as a minimizer. The latter is indeed optimally concentrated, has smaller entropy than the periodized discrete Gaussian for example, but is definitely not well localized. In addition, according to the components/information one wants to retrieve This work was supported by the FET-Open european project UNLocX, grant number 255931 and by the ANR project Metason ANR-10-CORD-010.

or visualize inside a signal, there exist more appropriate families of windows (Hann, Hamming, prolate spheroidal, etc...), optimal in a different sense.

In the framework of the short time Fourier transform (STFT), the ambiguity function (which also characterizes the reproducing kernel of the STFT), provides a sensible measure of the spreading of the analysis window in the time-frequency domain. This function plays an important role in the estimation of optimal localization properties in many different areas e.g. for operator approximation by Gabor multipliers [START_REF] Doerfler | Representation of operators in the time-frequency domain and generalized Gabor multipliers[END_REF] or for RADAR and coding applications [START_REF] Herman | High-resolution radar via compressed sensing[END_REF][START_REF] Alltop | Complex sequences with low periodic correlations[END_REF][START_REF] Costas | A study of a class of detection waveforms having nearly ideal range-doppler ambiguity properties[END_REF]. Depending on the application, the search for an optimal function emphasizes some particular property, e.g. support properties, peakiness, fast decay away from some reference point. Hence the ambiguity function must satisfy a set of constraints being stated by the user as well as its own inherent constraints.

We present here a method for designing optimally localized windows in the TF plane, based on the maximization of some measure of the ambiguity function concentration. Under general hypotheses and shape constraints, the proposed algorithm is able to provide an optimal function as the solution of a variational problem.

TIME-FREQUENCY CONCENTRATION:

CONTINUOUS TIME

The ambiguity function

We first consider the case of continuous time, infinitely supported signals, and denote by •, • the L 2 inner product. Let ψ ∈ L 2 (R) be a finite energy waveform, and denote by ψ z , with z = (τ, ξ) a time-frequency shifted copy of ψ with time and frequency shifts τ and ξ: ψ z (t) = e 2iπξt ψ(t -τ ) .

The ψ z will be termed Gabor atoms. Let us introduce the STFT V ψ f of f ∈ L 2 (R), and the ambiguity function A ψ of ψ:

V ψ f (z) = f, ψ z , A ψ (z) = V ψ ψ(z) . (1)
The ambiguity function for an arbitrary ψ ∈ L 2 (R) is bounded, continuous, decays at infinity, satisfies

A ψ 2 = ψ 2 2
and is the kernel of a positive semidefinite operator. Furthermore its modulus satisfies the symmetry relation |A(z)| = |A(-z)|, attains its maximum value at the origin and satisfies specific concentration constraint [START_REF] Demange | Uncertainty principles for the ambiguity function[END_REF]. This shows that not every function defined on the TF plane is the ambiguity function of a window. Therefore the design of windows such that their TF picture satisfies arbitrary properties is in general impossible. Still, one can try to find waveforms whose ambiguity function matches as closely as possible such prescribed localization properties (see e.g. [START_REF] Sussman | Least-squares synthesis of radar ambiguity functions[END_REF], [START_REF] Hlawatsch | Bilinear signal synthesis[END_REF]). The current paper considers a new localization criterion in the ambiguity domain, and proposes corresponding new optimization algorithms.

Concentration measures

Classical families of concentration measures are provided by L p -(quasi)-norms, for p ≥ 0

I ψ (p) = A ψ p p = R 2 | ψ, ψ z | p dz, (2)
which are closely related to Rényi entropies (for details see e.g. [START_REF] Baraniuk | Measuring time frequency information content using the renyi entropies[END_REF]), and the Shannon entropy measure:

S(A ψ ) = - R 2 |A ψ (z)| 2 log(|A ψ (z)| 2 ) dz = I ′ ψ (2) . (3)
For p < 2, maximizing the L p -norm (under unit L 2 norm constraint) favors spreading while for p > 2 this increases sparsity. Small values for the Shannon entropy is a sign of sparsity. In the continuous case, Lieb [START_REF] Elliott | Integral bounds for radar ambiguity functions and wigner distributions[END_REF] gives the following bounds on the L p -norm of the ambiguity function:

A ψ p p ≤ (2/p) ψ 2p 2 , p > 2 (4)
with a reversed inequality for p < 2. These bounds are sharp and all yield Gaussian functions (up to translations, dilations and rotations in the TF plane) as minimizers. Lieb also provides a lower bound for the entropy, with again the same family of Gaussians as minimizers

S(A ψ ) ≥ 1 , (5)
These cases are examples of a family of problems for which our method provides optimizers.

Optimization principle

We describe a general scheme for optimizing prescribed time-frequency localization properties. The rationale is to set the problem as a variational problem, and optimize a weighted L 2 -norm of the ambiguity function. The problem to solve reads

ψ opt = arg max ψ: ψ =1 F (|A ψ (z)|, z) |A ψ (z)| 2 dz , (6)
where the density function F : R + × R 2 → R + is chosen so as to enforce some specific localization properties. We shall consider here the two following specific cases, but the approach is not limited to these.

1. Find a ψ which optimizes the sparsity of A ψ , we choose F of the form

F (|A ψ (z)|, z) = |A ψ (z)| p-2 (p > 2)
and ( 6) becomes equivalent to finding the function which maximize A ψ p p . This will lead to the Gaussian here but our method clearly extends to more general settings than L 2 (R). We shall see in the next section that this also leads to discrete versions of the Gaussian function.

2. The other extreme case is to choose weight function of the form

F (u, z) = F (0, z) ,
i.e. a fixed weight in the ambiguity plane. In this case, the optimization ( 6) is expected to produce waveforms ψ whose ambiguity function is concentrated in TF regions where F takes large values. Given the constraints on ambiguity functions, we limit ourselves to weight functions concentrated around the origin and satisfying the symmetry property F (-z) = F (z). When F is an indicator of a ball the solution of the problem is the Gaussian function [START_REF] Flandrin | Maximum signal energy concentration in a time-frequency domain[END_REF].

Optimizing Eq. ( 6) does not lead to a closed-form solution. Alternatively, we shall search for approximate solutions, by recursive quadratizations.

Suppose a guess φ is available (fixed function in L 2 (R)), then we can maximize the following quantity (cost function) with respect to ψ:

Γ λ [ψ|φ] = F (|A φ (z)|, z)|V φ ψ(z)| 2 dz-λ( ψ 2 -1) (7)
where the constraint of unit norm was added via a Lagrange multiplier λ. This is equivalent to constraining the STFT of ψ (with window φ) to be localized in regions where F (|A φ (•)|, •) is concentrated. Let us denote by ψ 1 the function maximizing [START_REF] Demange | Uncertainty principles for the ambiguity function[END_REF] and

Γ (1)
λ the maximum. The next step is to replace φ by ψ 1 and solve the variational problem again. This yields a new optimal function ψ 2 , with maximum Γ

(2) λ . Iterating this procedure leads to a (possibly local) maximum for Γ λ . For special weight functions we have the following result: Proposition 1. For any function F bounded, positive and even with respect to z, maximizing [START_REF] Demange | Uncertainty principles for the ambiguity function[END_REF] is equivalent to solving the following eigenvalue problem

R 2 F (|A φ (z)|, z)V φ ψ(z)φ z dz = λψ , ( 8
)
where λ is the largest eigenvalue. Furthermore, the sequence Γ

(n)

λ converges to a (local) maximum for weight functions F independent of φ.

Sketch of proof:

Using the classical method for the calculus of variations, i.e. equating the functional derivative of Γ λ with respect to ψ to zero yields the linear equation [START_REF] Sussman | Least-squares synthesis of radar ambiguity functions[END_REF]. The cost function Γ λ converges for F real, positive, even, bounded and independent of φ since Γ λ is bounded, and at rank n

Γ λ [ψ n |ψ n-1 ] = Γ λ [ψ n-1 |ψ n ] ≤ Γ λ [ψ n+1 |ψ n ]. Remark 1. a). The convergence of Γ (n)
λ does not necessarily imply the convergence of the sequence ψ (n) . Conditions on F for the convergence of ψ (n) to ψ opt can be derived; this is the object of current research and will be developed elsewhere. b). When it exists, the limiting function ψ opt satisfies Eq. [START_REF] Sussman | Least-squares synthesis of radar ambiguity functions[END_REF], with φ = ψ opt and hence maximizes Γ λ with maximal value Γ λ [ψ opt |ψ opt ]. This turns out to match the expression of Eq. ( 6), and hence it is at least a local solution of the initial optimization problem.

Remark 2. a). When φ is the standard Gaussian and Daubechies showed in [START_REF] Daubechies | Time-frequency localization operators: a geometric phase space approach[END_REF] that the solution of (8) is φ. Hence it is a function which gives a (local) maximum for [START_REF] Costas | A study of a class of detection waveforms having nearly ideal range-doppler ambiguity properties[END_REF]. Moreover, she showed that the eigenvectors of the STFT-multiplier are the Hermite functions. b). In our iterative process, the diagonalization of the operator obtained in the last iteration yields an orthonormal basis which can be seen as a set of generalized Hermite functions.

F (|A φ (τ, ξ)|, (τ, ξ)) = F (0, τ 2 + ξ 2 ) is radially sym- metric,

ALGORITHM IN DISCRETE TIME

Discrete time considerations

In terms of localization, the finite discrete case is not just a discretization of the continuous one. Replacing integrals by finite sums yields a completely different world. For example, for signals of length N analogues of the Lieb inequalities can be obtained.

Proposition 2. Assume ψ ∈ C N is such that ψ 2 = 1. Then, assuming p < 2, A ψ p ≥ N 1 p -1 2 , (9) S(A ψ ) ≥ log(N ) . ( 10
)
The family of "picket fence" signals, translated and modulated copies of the following periodic series of Kronecker deltas:

ω(t) = 1 √ b b n=1 δ(t -an), ab = N ,
saturates the inequality.

Sketch of the proof:

The proof is directly adapted from the proof of Lieb's inequality for the continuous case [START_REF] Elliott | Integral bounds for radar ambiguity functions and wigner distributions[END_REF]. The ambiguity function is expressed as a finite Fourier transform, its L p -norm can be bounded using the Hausdorff-Young inequality. The resulting bound takes the form of a finite periodic convolution product which is itself bounded using Young's convolution inequality. Finally, the entropic inequality is obtained by a standard limiting argument. Note that the minimizer is not unique. Picket fence signals turn out to optimize many finite domain uncertainty principles (see e.g. [START_REF] Donoho | Uncertainty principles and signal recovery[END_REF]). This is quite different to the continuous case described in Sec. 2.2. In particular, picket fences are concentrated but not localized: they are not the most relevant windows for applications.

In this discrete setting, it is interesting to find an equivalent of the Gaussian function. One may define it as the optimal function of the following discretized version of ( 6):

ψ opt = arg max ψ: ψ =1 z F (|A ψ (z)|, z) |V ψ ψ(z)| 2 , ( 11
)
where

F (|A ψ (z)|, z) = |V ψ ψ(z)| p-2 for any p > 2.
This is made possible by the proposed algorithm.

Algorithm

As in the continuous case recursive quadratization, as described in Eq. ( 7) and below can be used to make the problem treatable. It leads to diagonalizing the STFT multiplier matrix: z F (|A φ (z)|, z) φ z , • φ z . All the given arguments for convergence apply in the discrete case also. Given any density function F , an initial window φ has to be specified to start with at the beginning. The steps are summarised in Algorithm 1. The stopping criterion is based on the L 2 -norm difference between functions issued from two successive iterations.

Algorithm 1 compute the optimal window ψ opt Input: φ -initial window, F -weight, eps. Individual Steps:

1: ψ 0 = 0, ψ 1 = φ 2: while ψ 1 -ψ 0 > eps do 3: ψ 0 ← ψ 1 4:
Compute the STFT-multiplier with weight F and window ψ 0

5:

Compute ψ 1 as the eigenvector to the largest eigenvalue 6:

Update F if necessary 7: end while 8: ψ opt = ψ 1

Results and convergence issues

Fixed weight (F (0, z)): For a radial symmetric weight function F as stated in Remark 2.a), the iterative proce-dure presented in Algorithm 1 converges to a Gaussianlike function. In Fig. 1 a plot of F (top right) and of the convergence rate (top left) is presented. Notice that it linearly decreases in log scale. The optimal function is plotted (middle) together with an example of another eigenvector of the operator given at the last iteration (bottom). We may define the discrete Hermite functions to be the eigenfunctions of such an operator, as pointed out in Remark 2. Weight functions which are constant along squares centered at the origin are another interesting example, see Fig. 2. Algorithm 1 leads to a square-shaped optimal function. Notice the generalized Hermite function which forms a square ring in the TF plane.

As stated in Remark 1.a), the sequence of ψ (n) may not converge although Γ does; this is the case when F has the shape of a cross in the TF plane for example. The algorithm is "hesitating" between convergence to one of the cross branch or the other. Weight depending on |A ψ | (F (|A ψ (z)|)): The main difference to the previous case is that the weight function evolves at each iteration and that the result depends on the initial window. The maximum of the objective function Γ λ is very degenerate (there are at least 2N solutions: N Kronecker deltas and N sine waves) and

CONCLUSION

We have proposed a novel approach for designing waveforms with controlled localization in the ambiguity plane. Our algorithm is able to provide optimally concentrated functions for a wide range of constraints/applications via a flexible weight function. It covers the intuitive spreading measure associated to L p -norms as well as the design of concentration masks in the TF plane. We recover the optimal functions given in the literature for particular choices of weight functions. Furthermore, by choosing a weight function F , one can define an application-tailored measure of localization and obtain the optimal window accordingly. For example a square-shaped window in the TF plane may be an interesting window for tiling the TF domain, when using a square lattice for the Gabor transform. It should be less redundant than the round-shaped Gaussian atoms.

The investigation of conditions of F which guarantee convergence is the object of ongoing work, together with the analysis of more general expressions for F . This procedure may also be of interest for other problems. Firstly, when diagonalizing the STFTmultiplier matrix with respect to the limiting window and the chosen weight F , one obtains a whole orthogonal basis, one of them being the optimal function. The other vectors have original shapes in the TF plane, looking like deformed rings around the origin. This could be seen as a generalization of the Hermite func-tions basis.

Fig. 1 .

 1 Fig. 1. Results in the case of a radial TF mask: F (|A ψ (z)|, z) = F (0, z). Top left: ψ n+1 -ψ n 2 , log scale. Top right: TF mask. Middle: optimal function in time (left) and in the TF plane through its ambiguity function (right). Bottom: an eigenvector of the last STFT-multiplier, the "generalized" Hermite function H 20 in time (left) and in the TF plane through its ambiguity function (right). The signal length is N = 420.

Fig. 2 .

 2 Fig. 2. Results in the case of a square-shaped TF mask: F (|A ψ (z)|, z) = F (0, z). Top left: ψ n+1 -ψ n 2 , log scale. Top right: TF mask. Middle: optimal function in time (left) and in the TF plane through its ambiguity function (right). Bottom: an eigenvector of the last STFT-multiplier, the "generalized" Hermite function H 20 in time (left) and in the TF plane through its ambiguity function (right). The signal length is N = 420.

Fig. 3 .

 3 Fig. 3. Results for the optimization of the L p norm of the ambiguity function (p = 3). Top: Cost function leading to the picket fence (dashed) and to the Gaussian-like function (crossed). Middle: initial delocalized function (left) and final function, i.e. twopicket fence (right). Bottom: initial localized function and final one, the Gaussian-like function.


Cesar Bernardini

Thomas Silverston

Olivier Festor

Towards Popularity-Based Caching in Content Centric Networks

I. INTRODUCTION

Today's Internet was created aiming to share resources. The chosen model was therefore a conversation mechanism between two machines: the messages are exchanged between two host according to source and destination addresses of IP datagrams. This led to a model with strong coupling between where and what, even when most of the users value the Internet for what content it contains. As well location dependence makes configuration and implementation of network services more complex. Alternative architectures such as CDN and P2P networks provide high availability and improve performance but they are not-supported natively by the current Internet. In order to solve these issues, Information-Centric Network architectures (ICN) have been proposed such as PSIRP [START_REF] Särelä | RTFM: Publish/subscribe internetworking architecture[END_REF], NetInf [START_REF] Dannewitz | OpenNetInf documentation design and implementation[END_REF], or CCN [START_REF] Van Jacobson | Networking named content[END_REF]. These architectures are thought as clean-state designs for the Future Internet.

Content Centric Networking (CCN) is a communication architecture based on named data where packet address name content, not location. The host notion does not exist anymore. The communication paradigm relies on two primitives: Interest and Data. A consumer requests content by broadcasting its interest all over the network; any node hearing the request and having the data can issue a response with a data message. In addition, CCN offers routing-by-name, caching, integrity checks based on signatures, encryption, multicast support, flow-control at each hop, protection against Denial of Service attacks.

Caching consists in storing data messages at a node. In CCN, data messages are cached at every intermediate nodes from a source to a destination. A content is therefore replicated and is available at a closer distance for future requests. An important feature for CCN is to manage the cache of nodes by defining replacement policy, cache policy and cache strategy [START_REF] Rossi | Caching performance of content centric networksunder multi-path routing (and more)[END_REF].

Most of the research about information centric networks, have been carried out on CCN. For instance, Kurose et al. [START_REF] Rosensweig | On the Steady-State of Cache Networks[END_REF] show that cache replacement policies can be grouped in the same equivalence class. Rossi et al. [START_REF] Rossi | On sizing ccn content stores by exploiting topological information[END_REF], [START_REF] Rossi | A dive into the caching performance of content centric networking[END_REF] study cache sizes and compare several caching strategies. They also argue that popularity of content have a strong impact on CCN performances [START_REF] Rossi | Caching performance of content centric networksunder multi-path routing (and more)[END_REF].

In this extended abstract, we propose a new caching strategy based on popularity. Section II describes our proposal in detail.

Then, Section III relates to our ongoing work and finally, we end up with future work at Section IV.

II. POPULARITY-BASED CACHING STRATEGY

As we explained before, every time a CCN node issues an interest message, it is broadcasted through the network until a node hearing the request is able to reply. Instead of the CCN caching strategy where all the nodes cache every content message that has passed by them, we believe that caching only popular content will help to save resources and to improve the overall performances of the CCN network. To this end, we propose a new caching strategy called Most Popular Content (MPC), where nodes will cache only popular content. Purging unpopular content from caches will help in several ways: more resources will be available for popular content; unpopular content will not increase the workload of replacement caching policies; Unpopular content will not be cached, and for these, CCN network will act as IP does in the current Internet where a request is forwarded to the node owning the content.

A content is defined as popular when it has been requested (through interest messages) a certain number of times reaching a popularity threshold. Every node maintains therefore a local popularity table and counts all the interest messages it receives for any particular content. When a content become popular, the CCN node holding the content suggests his neighbor nodes to cache the content. Besides, after receiving suggestion messages, neighbor nodes may accept to cache the content or not. Moreover, the popularity of a content can decrease with time, as it may be less popular in the future.

More precisely, our new caching strategy works as presented in Figure 1. Figure 1(I) describes a typical scenario, and the final state of cache at every node according to our strategy, Fig. 1(II), or CCN, Fig. 1

(III).

There is a popular content d1, initially stored at node D, and an unpopular content e1 at node E. In our scenario, the popular content d1 will be requested by three nodes A, B, C. The unpopular content e1 will be requested only once by node A.

Figure 1(II) shows how our strategy works with the proposed scenario. When node A sends an Interest Message for content e1, e1's popularity is increased in the popularity tables of every node along the path [A, C, D, E]; in other words, e1 content popularity at nodes A, C, D and E is now set to 1. In the same way, when node A sends an Interest Message for At this moment, node D is the only node to hold the content d1. D spreads suggestions messages to his neighbors C and E. Node C and E will therefore cache the content and will be able to transmit the content after upcoming requests. For instance, if there are interested nodes close from A, their request will be redirected directly to C and not D, reducing the number of hops to get the content.

Figure 1(III) describes the CCN case. When the first request is sent by node A, content e1 will be cached at every nodes along the path [A, C, D, E]. Then, according to our scenario, content d1 will be cached around [A, C, D] after the first request from A. The request from B will be directed only through C and d1 will be cached into B. Finally, node C has already the content since it has been stored from previous requests.

The main difference between our strategy and the CCN's one is that the CCN behavior caches all content, and it will overload resources at every node, even though that content is not popular. For instance on Fig. 1

III. ONGOING WORK

In the previous section, we presented MPC, our new caching strategy for CCN network. We are currently evaluating MPC by implementing it into the ccnSim simulator [START_REF] Rossi | Caching performance of content centric networksunder multi-path routing (and more)[END_REF]. Our implementation includes all the features to support our proposed strategy, as for example, popularity tables and suggestion messages. In order to evaluate our strategy properly, we are investigating its key parameters such as popularity threshold, replacement policy for popular content, or popularity table size. We are also refining our strategy according to the feedback we have from our simulations. For instance, we could adjust the behavior of nodes when receiving a suggestion message and define an acceptance policy if nodes cache the content or not.

We intend to analyze this strategy thoroughly with optimal parameters values and as well to compare it fairly to current cutting-edge CCN strategies. Thus, we will introduce new metrics such as the percentage of claimed cached elements, the number of hops between the content and the receiver, the number of replicas in the entire network, or the lifetime of a content cached in a node. By using ccnSim and our new strategy, we will be able to compare different caching strategies and to point out that popularity caching may outperform other strategies and is well suited with CCN.

IV. FUTURE WORK

Fig. 1 .

 1 Fig. 1. (I) represents an example of a network and a representative scenario; (II) depicts our proposed caching strategy with the scenario; (III) shows the normal CCN behavior with the same scenario.

  (III), content e1 is replicated at nodes A, C and D and content d1 is on nodes A, C and B. Differently, with our strategy on Fig 1(II), e1 is only present at node E and d1 is replicated but only to nodes C and E. Clearly, our proposed strategy (Fig.1(II)) is saving resources such as memory, bandwidth or the number of caching replacement operations compared with the CCN strategy.

We stand strongly for MPC, and we expect that it could be a startup for studying name-based routing. Since it is a suggestion based mechanism, it could be adapted to manage content among nodes, predict popularity and routing content to destination. Beyond, the popularity of content is also a piece of information that can be obtained from social networks. This feature may help improving the accuracy of our strategy.