Clément Poncelet
email: clement.poncelet@ircam.fr

Florent Jacquemard
email: florent.jacquemard@inria.fr

Test Methods for Score-Based Interactive Music Systems

Score-Based Interactive Music Systems (SBIMS) are involved in live performances with human musicians, reacting in realtime to audio signals and asynchronous incoming events according to a pre-specified timed scenario called a mixed score. This implies strong requirements of reliability and robustness to unforeseen errors in input.

In this paper, we present the application of formal methods for black-box conformance testing of embedded systems to SBIMS's. We describe how we have handled the 3 main problems in automatic testing reactive and realtime software like SBIMS: (i) the generation of relevant input data for testing, including delay values, with the sake of exhaustiveness, (ii) the computation of the corresponding expected output, according to a given mixed score, (iii) the test execution on input and verdict. Our approach is based on formal models compiled from mixed scores. Using a symbolic checker, such a model is used both for (i), by a systematic exploration of the state space of the model, and for (ii) by simulation on a given test input. Moreover, we have implemented several scenarios for (iii), corresponding to different boundaries for the implementation under test (black box). The results obtained from this formal test method have permitted to identify bugs in the SBIMS Antescofo.

INTRODUCTION

Interactive music systems (IMS) presented in [START_REF] Rowe | Interactive Music Systems: Machine Listening and Composing[END_REF] are involved in live music performances with human musicians. They work by coupling functionalities of artificial listening, in particular score following and tempo detection, and of reactive systems, for synchronizing their outputs to musician inputs. In the case of SBIMS, all these activities are performed in realtime following a pre-specified timed scenario called a mixed score, written in a domain specific language (DSL).

During an instrumental performance, when a musician does a mistake, the piece must and will continue. However, IMS practitioners know that a crash or misbehavior of an IMS can jeopardize a mixed instrumental-electronic performance. In order to avoid unforeseen errors of an IMS at runtime, and meet listeners' expectations, it is important to be able to explore, statically, its reactions to possible musician's interpretations, and check that they conform to the behavior specified in the given mixed score. This difficult task is complicated by high unpredictability of musicians' inputs and hard temporal constraints (due in particular to the strong requirements of audio computing platforms).

A traditional and manual approach is to rehearse with musicians. However time is precious during a rehearsal, and its purpose is usually more to solve musical questions than to fix bugs. It is also possible to listen to an IMS playing with some recordings of musicians, checking that the system is not crashing and that the result sounds in a satisfiable way. The problem with this approach is that, on the one hand, the test input is not complete (it just represents one or a few particular performances), and on the other hand the verification of the outcome is not rigorous. Several formal methods have been developed for automatic conformance testing of critical embedded software, see e.g. [START_REF] Krichen | Black-box conformance testing for real-time systems[END_REF]. The principle (Figure 1) is to execute a real implementation under test (IUT) in a testing framework. When the source code of the IUT is not known and only its input and output are observed, we call it black-box testing. In conformance model-based testing (MBT), a formal specification, or model M of the system is written (in general manually) and used to generate automatically some test data. This comprises input test data t in , sent to the IUT, and theoretically expected output test data t out , computed from t in using M. The latter t out is then compared to the real output test data t out , obtained from the IUT when it receives t in , in order to produce a test verdict. This procedure is iterated on a large base of pairs t in , t out , which is generated, for exhaustiveness purposes, according to a user specified covering criteria, expressed as a formula referring to elements of M. This provides a rigorous mathematical framework, increasing the confidence in the tested systems and reducing test costs. For realtime systems such as communication protocols, transportation control etc, like for IMS, time is a semantical issue (not just a measure of performance), and it must be included in test data, which become timed traces.

This paper presents a study of the application of MBT methods to the SBIMS Antescofo, developed at Ircam and used regularly in concerts. This system shares several characteristics of the reactive and realtime systems usually targeted by MBT, but also has its own specificities. In particular, the formal specification of the IO behavior of the system is produced automatically from a given mixed score, using a front-end compiler into an ad hoc intermediate representation (IR). This is in contrast with usual MBT case studies where the specification has to be written manually by an expert in formal methods. After a brief presentation of Antescofo and its score DSL (Sections 2.1 and 2.2), the test data is presented in Section 2.3. Then we describe some test scenarios that we have used for Antescofo (Section 2.4). Some are running in real time, some running in a fast forward mode thanks to implementation of virtual clocks in Antescofo. The automatic construction of formal model, using IR, is presented in Section 3. In particular, we show how we used the symbolic model checker Uppaal [START_REF] Hessel | Testing Real-time systems using UP-PAAL[END_REF] based on timed automata model, and its extension CoVer [START_REF] Blom | Specifying and generating test cases using observer automata[END_REF] for the production of test input data with covering criteria.

The test outcome permits us to prepare concerts, by simulation of covering sets of fake musician performances (the test input t in ) derived from a given mixed score. Moreover, it increases the guarantee on the reliability on the system, with a systematic analysis of test outcome, exploited for debugging.

TEST FRAMEWORK FOR A SBIMS

We present in this part the principles of a testing framework that we have developed for the SBIMS Antescofo 1 , following the approach depicted in Figure 1.

Antescofo

Collective music performance involves several complex and sometimes implicit activities. The system Antescofo aims at acting as an electronic musician interacting with human musicians, implementing these behaviours. For this purpose, the system takes as input a mixed score which describes in the same file some musician and electronic parts. During a performance, the system synchronizes the electronic parts to the musician's ones: it aligns in realtime the performance of human musicians to the score, handling possible errors, detects the current tempo, and plays the electronic part, following the detected tempo. Playing is done by passing by messages to an external audio environment such as MAX or PureData. A popular particular case of this behavior is automatic accompaniment [START_REF] Cont | Correct Automatic Accompaniment Despite Machine Listening or Human Errors in Antescofo[END_REF].

Antescofo is therefore a reactive embedded system, interacting with the outside environment (the musicians), under strong timing constraints; the output messages must indeed be emitted at the right moment, not too late but also not too 2 shows the Antescofo architecture. Our electronic musician is composed of two units. A listening machine (LM) receives an audio or midi stream from a musician and detects in realtime his position in the mixed score. This score following feature is coupled with a function of tempo inference based on Large's algorithm [START_REF] Cont | A coupled duration-focused architecture for realtime music to score alignment[END_REF]. The positions and instantaneous tempo detected by the LM are sent to a reactive engine (RE) which schedules the electronic actions to be played and emits on time messages to the audio environment. Note that the information exchange between LM and RE is discrete, as well as the output of the system (messages sent).

Mixed Scores DSL

The mixed scores of Antescofo are written in a textual reactive synchronous language describing the electronic accompaniment as reaction to the detected instrumental events. A simplified extract of the score of Einspielung I 2 by Emmanuel Nunes is presented in Figure 3. This piece for violin and electronics will be used as a running example in this paper.

We give here an abstract syntax corresponding to a small part of this language, following our needs for presenting our test framework. The reader can find more complete descriptions in [START_REF] Echeveste | Operational semantics of a domain specific language for real time musician-computer interaction[END_REF][START_REF] Echeveste | A Dynamic Timed-Language for Computer-Human Musical Interaction[END_REF]. Formally, an Antescofo mixed score is a finite sequence of input events e 1 , . . ., each event being bound to a finite An event e i is a tuple i , c, d, g made of the unique identifier i (event number), some event data c, the event's duration d (also denoted dur (e i )), expressed either in number of beats of tempo or milliseconds (ms), and group g triggered by e i . The event data contains information such as the event kind (note, chord, trill...), and pitch values. An important point here is that on detection of an event, the LM will return the id i to the RE (and not simply the pitch). Note that all values in Antescofo, including durations, are expressions which can possibly contain variables (global or local to groups) and functions. An action is a pair a = d, g where d is a delay (in beats or ms) and g can be either an atom or a group. An atom is a control message sent to an external audio system -MAX or PureData or a computation of the form x := exp where x is a variable and exp an expression. Note that with the above recursive definition, the groups can be nested arbitrarily, in order to reflect some musical intention. Moreover, every action is contained in a group, called its container.

The delay d in a = d, g is the time to wait before starting to play g, after the trigger of a has been detected (if it is an event) or started (if it is an action). The trigger of an action a with container g is defined as follows. If a is not the first action of g , then its trigger is the action preceding a in g . Otherwise, either g is a top-level group act(e i ) and the trigger of a is e i , or g is in an action a = d , g called parent of a and the trigger of a is the trigger of a . Some high-level attributes can be added to groups to express an expected behavior for musician-electronic synchronization and error handling, corresponding to a particular musical situations [START_REF] Cont | Correct Automatic Accompaniment Despite Machine Listening or Human Errors in Antescofo[END_REF]. In this paper, we shall consider, for illustration purposes, a small sub-set of attributes : two synchronisation attributes: loose: Synchronization on tempo. Only the tempo is used to compute the delays of the group's actions.

tight: Synchronization on events. Every action in the group is bound to the closest event.

and two error management attributes. In Antescofo, an error is a missing event (note), either because the musician did not play it or else because the LM did not detect it (e.g. because it is not well tuned).

local: Skip. If the triggering event is missing, the actions of the group are skipped.

global: Immediately. The actions are started immediately at the detection that the triggering event is missing.

Roughly, the synchronisation attribute expresses how smoothly (for loose) or not (for tight) the electronic part should be played. The error management specifies the importance of the actions. Figure 4 illustrates Antescofo's behavior for various compositions of attributes for the group in the extract of mixed score of Figure 3. Note that in the score, the attributes loose and global have been chosen.

Test Input and Output Data

What is the form of the input data send to the SBIMS for testing its behavior, as well as the output data collected for analyzing the results of tests?

Basically, a test input is a trace of events representing a musician performance and an output is a trace of actions representing the electronic accompaniment generated in reaction to the input. For reactive and realtime IMS, time is a semantics property, and the dates at which events and actions are played must be included in test input and output data (timestamps). This is in contrast with functional programs, computing output from the given input, for which it is sufficient to consider, for testing, untimed data values. A grand challenge for the design and implementation realtime embedded systems (including IMS) is to reconciliate two time units [START_REF] Henzinger | Two challenges in embedded systems design: predictability and robustness[END_REF]: the time of the environment and the time of the platform. The first is the physical time, expressed in milli-seconds. The second is a logical time used by the system in its computations. For IMS, the logical time unit is the number of beats, it is called relative time in the rest of the paper. Hence, in IMS, reconciliation of the times of environment and platform is done through tempo. A test input trace t in is a finite sequence of triples i, d, T made of an event identifier i (pointing to an event e i in a given mixed score), a duration value d expressed in relative time (like in the score), and the instant tempo T between e i and the next event in the trace, expressed in beat per minute. Note that missing events can be specified, by absence, in t in : the event e i is missing in a t in of the form . . . , i -1,

d i-1 , t i-1 , i + 1, d i+1 , t i+1 , . . .
As an example, from a mixed score e 1 , e 2 , . . . we can directly generated the so called ideal trace 1, dur (e 1 ), T , . . ., where T is the tempo specified in the score 3 (see Figure 5). This trace corresponds to the performance of a robot, playing exactly the notes and durations specified. An expected output trace t out (resp. real output trace t out )

1, 1/7, 144 • 2, 1/7, 144 • 3, 1/7, 144 • ... • 7, 1/7, 144 a0,0 • a1, 0 • a2, 1/7 • a3, 2/7 • ... • a7, 6/7
Figure 5: Ideal input and expected output for Fig. 3 is a finite sequence of pairs a, d made of an atom (as de-fined in Section 2.2) and its date d expressed in relative time (resp. in physical time). A test case (see Figure 1) is a pair made of an input trace t in and the corresponding expected output trace t out .

Related models of performances

Time-warps [START_REF] Dannenberg | Abstract time warping of compound events and signals[END_REF], Time-Maps (Jaffe 1985), Time-deformations (Anderson and Kuivila 1990), are continuous and monotonically increasing functions used to define either variations of tempo or variations of the duration of individual notes (time-shift). Some models of performance [START_REF] Dannenberg | Abstract time warping of compound events and signals[END_REF][START_REF] Honing | Structure and interpretation of rhythm and timing[END_REF] are defined by combination of these two transformations, defined independently. Our input test trace format is a discrete version of such models, where the tempo variations and time-shifts are defined respectively in the third and second component of entries i, d, T . An important difference with [START_REF] Dannenberg | Abstract time warping of compound events and signals[END_REF][START_REF] Honing | Structure and interpretation of rhythm and timing[END_REF] is the possibility to have missed notes in input traces.

Input trace fuzzing and generation

Thanks to these models, generating input traces scripting musical performances is not difficult. One can start with the ideal trace, generate arbitrary tempo values (e.g. defined by a tempo curve) and add some fuzz to events durations (time shifts) and missing events. The obtained traces are well suited for testing in the preparation of concerts. Another method for generating more exhaustive sets of input traces, suitable for debugging, is presented in Section 3.4.

Generating the corresponding expected output traces t out is a more difficult problem: it wouldn't make sense to use the system under test for this purpose, and we need instead a formal reference of the timed behavior expected for the system. As explained in introduction, we follow a modelbased approach (MBT) to tackle this problem, where a model M is used to compute t out from t in (M is also used to generate t in ); this is detailed in Section 3.

Test Execution

How can we execute given test cases on the SBIMS?

The execution of a test case t in , t out is somehow a monitored simulation of a performance. It consists in sending the events in the input trace t in to the SBIMS, with their durations, and collect a real output trace t out by monitoring and time-stamping (in physical time) all output emissions of the SBIMS during the execution. The latter is then automatically compared to t out to produce a test verdict.

The problem is more tricky that it seems due to the data flow in Antescofo, its modular nature (Figure 2) and the relative time unit used in test cases. We present below several scenarios for testing different parts of the system. precisely, it does not physically wait, but instead notifies a virtual clock in the RE that the time has flown of d ms. This way the test does not need to be executed in realtime but can be done in fast-fordward mode. This is very important for batch execution of huge lists of test cases.

The messages sent by RE are traced in t out , with timestamps in physical time (this functionality is built in the current RE). Finally, the timestamps in t out are converted from relative time to physical time using the tempo values in t in , in order to be comparable to t out .

In this scenario, the IUT is the RE (the LM is idle). In this second scenario the tempo values T are not read in t in by the adapter but instead inferred by the LM (the adapter is calling an appropriate method in LM). The rest of the scenario is similar to Section 2.4.1. The values of detected tempo are stored by the adapter and used later to convert the dates in the expected trace t out from relative to physical time. In this case, the IUT is somehow the RE plus the part of the LM in charge of tempo inference.

Testing the whole SBIMS as a Blackbox

This scenario is the most general. It is executed in a version of Antescofo embedded into MAX (as a MAX patch), using an adapter which is another MAX patch. The adapter iteratively reads triples i, d, T in a file containing t in , and plays them as MIDI events, using the duration d converted to physical time with T . The audio stream generated is then sent to the LM, and the output of the RE is traced in t out as before. Note that here, the RE uses the tempo values detected by the LM, which will differ from the tempo values in t in [START_REF] Cont | A coupled duration-focused architecture for realtime music to score alignment[END_REF]. Therefore, the former are saved by the adapter (in MAX the detected tempo is available as an outlet of the antescofo˜patch), and used later to convert the dates in t out from relative to physical time like in Section 2.4.2. In this realistic scenario, the IUT is the whole SBIMS.

In an alternative scenario, the adapter ignores the tempo values in t in and uses tempo detected by the LM, similarly to Section 2.4.2. Note that in these scenarios, the tests are executed in realtime and not in a fast-forward mode like in Sections 2.4.1, 2.4.1.

Test Verdict

How can we check that the real output trace t out is correct? When t out is not known, we are left to listen the execution of the IMS on t in , in extenso, for instance using the framework presented in Section 2.4.3, and decide subjectively whether we are satisfied with it. This manual solution is not rigorous and also tedious when one need to consider many different t in for covering purposes. When t out is known, we just need to compare pointwise the conversion of t out to physical dates to t out , with a fixed error bound δ to dealing with latency, and report differences. This raises the following important question: How can we systematically compute the expected t out from t in ? This is going to be answered in the next part of the paper.

MODEL BASED CONFORMANCE TESTING

We report here the use of state-of-the art MBT models, techniques and tools for testing the SBIMS Antescofo in the framework presented in previous Section 2.

Generalities on Model Based Testing

Figure 9 depicts in its higher half a reactive system's IUT interacting with an environment RealENV, and in its lower half, two formal specifications of the latter, resp. S and E.

The behavioral specification S of the system is a formal description of its reactions to the outside environment. In our case, it is the function producing t out given t in .

The environment model E is a formal description of what can be expected from the environment. In our case, it is the definition of the set of all possible t in , i.e. all the potential interpretations of musicians to be tested.

Note that since IMS are realtime systems, we need to express time in E and S, like in: "one message m has to be emitted one beat after the first event e 1 of the musician".

The conformance of the IUT to the specification S wrt E is defined as the inclusion of the set of real output traces t out , obtained by the execution of all t in ∈ E against the IUT, into the set of expected output traces t out = S(t in ) with t in ∈ E. As time values are included in the traces, conformance ensures the time safety of the IUT on the test cases.

Antescofo Intermediate Representation

How can we write formal specifications E and S for testing the SBIMS Antescofo on a given mixed score s? Actually, this is the exact purpose of the score! Therefore, in our test framework we generate automatically from a score two formal specifications E and S of the expected behavior of the musicians and Antescofo, exploitable by testing tools. This prevents us opportunistically from the burden of an initial phase of manual specification by experts, generally needed for the testing and verification of embedded systems. Hence the automatic production of E and S is a convenient feature, typical of IMS testing. We use a front-end compiler transforming an Antescofo mixed score s into a medium level executable intermediate representation IR(s). The model IR(s) will be furthermore translated into the timed automata formalism in order to use tools dealing with such models (Sections 3.3, 3.4). This approach is similar to the use of Ecode for the Giotto language [START_REF] Henzinger | The Embedded Machine: Predictable, Portable Real-time Code[END_REF] in order to ensure portability and predictability (determinism), both in timings and functionality. We present here a simplified graphical version of the IR designed for Antescofo [START_REF] Jacquemard | Antescofo Intermediate Representation[END_REF]. An IR is a finite set (called network) of finite state machines extended with variables and durations (EFSM), communicating synchronously with some symbols taken from a finite alphabet Σ. Some example of EFSMs can be found in Figures 10 and13. We let Σ = Σ in Σ out Σ sig where Σ in and Σ out are respectively the sets of the event ids and atomic messages of s (as described in Section 2.2), and Σ sig contains internal signals presented below. Every transitions of the EFSMs is labelled by one of σ! (emission of a symbol σ ∈ Σ), σ? (reception of a symbol), a computation x = exp or a delay d (in relative or physical time). The communication with the external environment are represented by σ? with σ ∈ Σ in (reception of events) and σ! with σ ∈ Σ out (emission of messages).

Moreover, all branching (multiple outgoing transitions from a single state) must have the form depicted in Figure 11 4 : A transition is fired from the state r as soon as 4 IR can also contain conditional branchs that we do not describe here. We consider a synchronous model of time (following [START_REF] Echeveste | A Dynamic Timed-Language for Computer-Human Musical Interaction[END_REF]):

RealEN

The time can flow only in source states of branchings. The other transitions, labeled by σ! or x = exp are instantaneous (i.e. a logical time 0 is spend in the source state).

The EFSMs composing a network are run concurrently: at each instant, every EFSM is in one control state. Initially, every EFSM starts in its initial state, which is unique.

Compiling Scores into IR (construction of the models)

The EFSM network IR(s) is produced from a given score s by traversing the hierarchical structure of s. Intuitively, it contains one EFSM for each group in s and a fixed number of auxiliary EFSMs. An EFSM called error proxy defines the notion of errors in the flow of musician events. To each i ∈ Σ in we associate a unique new signal ī ∈ Σ sig , meaning that the event of id i (in the score s) is missing. The transitions of the error proxy are labeled by i? (the event i has been detected) or ī! (to signal that the event i is missing). Various definitions of the notion of missing events are allowed, and specified using parameters of the compilation command.

Next, we generate one EFSM for each group in the score. To a group g we associate 2 symbols denoted ǧ and ḡ. If g is a toplevel group, triggered by e i , then ǧ = i ∈ Σ in and ḡ = ī ∈ Σ sig . Otherwise, ǧ and ḡ are new signals of Σ sig . The generic form of the EFSM of group g is depicted in Figure 12, where init is the initial state and the sub-EFSMs fsm(g), mfsm(g) are defined according to the strategies for g (see examples in Figures 10 and13).

Additionally, an EFSM E modeling the environment is constructed, in order to bound the space of possible interpretations of musicians considered for testing and avoid explosion during test input generation. Figure 13: IR of the beginning of a tight and global group with a unique action d, α . We have 4 execution modes, corresponding to the 4 lines: normal, earlier, missed-earlier and missed. In states s 0 , s 3 and s 2 , the automaton is waiting for an event or group symbol. If this symbol is missed, it switches to the missed mode (resp. states s 1 , s 4 ). In normal mode (state s 1 ), the automaton waits for a delay d before sending the action α. In missed mode (state s 1 ), the automaton sends α without waiting. Moreover, in state s 1 , the automaton waits concurrently for a delay d and for the detection of the next event e i+1 (at the current score position). If e i+1 , respectively e i+1 , arrives before the expiration of d, then the automaton switches to mode earlier (state u 2 ), resp. missed-earlier (state u 2 ). In both cases, the action α bound to the previous event e i is sent without delay and then the automaton switches to normal or missed mode (s 4 or s 4 ).

Timed Automata and Uppaal

Timed automata (TA) [START_REF] Alur | A theory of timed automata[END_REF] are finite state automata extended with a finite set of real-valued variables called clocks. Every TA transition is labeled by a symbol (in a finite alphabet), and a linear constraint (guard) on the clock values: the transition can be fired only if the current values of the clocks satisfy the associated constraint. Moreover, every clock can be independently reset to 0 during a transition and keeps track of the elapsed time since the last reset. Some linear constraints (guard) on the clock values called invariants can also be attached to states, such constraint must be satisfied as long as the control stays in the state.

In a TA, all the clock values are expressed in a unique abstract time unit, the model time unit (mtu), i.e. all the clocks evolve at the same rate. The IR of a score s can be converted into an equivalent TA, under the restriction that: (i) all the delays are expressed in relative time in the score (like in all traditional scores) and (ii) the score contains no variables or all the variables can be evaluated statically.

Uppaal5 is a symbolic model checker which permits users to write, simulate and verify timed automaton networks. The set of configurations of a TA A is infinite (it is the Cartesian product of the finite set of states of A and the infinite set of valuations of the clocks of A). However, it is possible to transform a TA into a finite state automaton recognizing the same (untimed) sequences of symbols, using a finite equivalence on configurations (region construction) [START_REF] Alur | A theory of timed automata[END_REF]. This fundamental technique gives a PSPACE algorithm for deciding reachability properties, implemented efficiently in Uppaal.

Given an input trace t in for testing and a TA model S of a score, it is possible to compute the corresponding output t out , according to S. A deterministic environment model E is first computed from t in as in Figure 14. Then, a simulation is performed with Uppaal, on the automata network E∪S, and t out is obtained by tracing output during this simulation. The environment can be modified slightly in this process (from E presented in Figure 14), by introducing intervals on delays in transition's guards, in order to prevent state-space explosion in the generation of test cases (Section 3.4). Testing does not prove that Antescofo is crash-free, but the more test-case we have checked, the bigger guarantee we have. As we cannot test exhaustively for all possible performances on a given mixed score, a strategy is to consider a relevant set of test-cases (including extreme ones!) that covers in some sense the possible behavior of the IUT on the score. It is possible to generate automatically such sets of test-cases based on the formal specification of the system, and this problem has been extensively studied [START_REF] Broy | Model-Based Testing of Reactive Systems[END_REF]. For this purpose, we use an Uppaal extension called Co-Ver [START_REF] Blom | Specifying and generating test cases using observer automata[END_REF], which has been used for testing Ericsson's industrial size networking systems [START_REF] Hessel | Testing real-time systems using uppaal[END_REF]. It allows to generate test cases sets according to a user-written coverage criteria, defined as a finite state automaton called observer monitoring the execution of S. The transitions of observers are labeled by Boolean predicates validated when some states or transitions in the TA model S have been reached. The model checker Uppaal is used to generate the input traces t in enabling to reach a final state of a given observer for S. This modular approach permits to target a specific group, or a specific problem such as error handling for testing, with a focus on Antescofo debugging.

Note that the traces t in generated by CoVer do not contain tempo values, but only durations in relative time. They refer to a clock in the TA model which is not yet specified, and can be instantiated using an arbitrary time-map (for execution scenario of Section 2.4.1 or 2.4.3, first case), or by the detected tempo (Section 2.4.2 or 2.4.3, second case). Let us consider the generation of a test case on our running example (Figure 15). First, CoVer returns a couple of notes e 3 (E ) and e 4 (D ), with respective durations 0.27 (a little less than 2 7 ) and 0.4 (a little less than 3 7 ) beats. They represent time-shifts over the durations in the score. The other notes are assumed missing. Next, some arbitrary tempo values are generated: 60 bpm for e 3 and 114 bpm for e 4 , completing an input trace t in . The output trace t out associated to t in is then computed by Uppaal. out . An execution with Antescofo on t j in , 1 ≤ j ≤ k, following one of the scenarii of Section 2.4, will return real output traces t j out . A step by step comparison of the t j out and t j out will permit to draw a test verdict (see Section 2.5). A fixed error bound (approx. 0.1ms) is applied when comparing the delays, for dealing with latency.

The crucial point here is that when observers express that we cover all the edges of E and S, then success on all the test cases generated by CoVer guarantees the conformance of the IUT to the model S of the score, wrt E. This completeness result is obtained thanks to the use of the region construction in CoVer.

CONCLUSION

We have presented model based conformance testing approaches and their application to the SBIMS Antescofo.

The generation of test input data and computation of the corresponding expected output is based on a formal model compiled from a mixed score, and done with the help of the symbolic model checker Uppaal.

The results obtained with these approaches, with real scores or small case studies, have permitted to identify and fix bugs in Antescofo. For instance, an erroneous cast of Antescofo's detected tempo caused the computation of wrong values of action delays. The small variation was detected when comparing t out against t out .

The generation of input can be done automatically with CoVer, following covering criteria expressed as observers. This approach is oriented towards software engineering and debugging. Alternatively, the input can be produced manually by adding some fuzz to an ideal trace (using timemaps describing tempo variations and time shifts) as described at the end of Section 2.3. This gives no guaranty of coveredness but the input produced is musically more relevant (it corresponds to a performance). This approach is more oriented towards the preparation of concerts and can be helpful at composition time.

Another possible application of our framework is nonregression testing: An expected trace t out can be simply recorded by monitoring an execution on a given t in with a former reliable version of the SBIMS. Then one can compare with the trace t out produced on t in by the new version under test. Of course, unlike model based approaches, this technique gives no guarantees that the execution t out is correct, it only permits to check automatically whether the new version behaves like the old one on t in .

One limit of the approach is related to the input test data generated by CoVer, which tends to chose shortest delays for t in inside regions. As a consequence, the tempo computed on this input can increase exponentially (since delays in t in are expressed in relative time, refering to the current tempo). To avoid this problem, some other input delays (not the shortest) should be chosen in regions. A second limitation is due to the expressiveness of TA. TA can have several clocks but they all run at the same frequency (the mtu). Hence, multirate is not supported in TA models whereas it is possible in Antescofo DSL. Moreover, in Antescofo DSL and IR, delays can be expressions with variables which cannot always be evaluated statically (e.g. when they depend on input). Some extensions of TA with variables are supported by Uppaal and remain to be studied in the context of IMS model-based testing.

The approach presented in Section 3 generates the test cases offline: the whole traces t in and t out are generated before test execution, which can be space consuming. Equivalent online approaches exist, with 'on the fly' generation and execution of traces. This is developed as Uppaal extension and named TRON. However it could not be used in our case due to a technical issue in the conversion from relative to physical time values. An interesting alternative could be to follow an approach similar to [START_REF] Bounimova | Billions and billions of constraints: Whitebox fuzz testing in production[END_REF] combining fuzz testing and a white box approach. It consists in executing an online test loop, with on the fly random generation of test input from the code and, in parallel, the incremental developpement a propositional constraint (checked for satisfiability with a SAT solver), ensuring a form of coveredness.

Finally, a visualization of the output traces, with a graphical representation e.g. in Ascograph 6 would greatly benefit Antescofo's users, for composition assistance purposes. It would be useful e.g. to compare respective temporal positions of groups for different performances.

Figure 1 :

 1 Figure 1: Principles of Model Based Testing

Figure 4 :

 4 Figure 4: Attribute specification (e1 and e4 missed)

2. 4 . 1 Figure 6 :

 416 Figure 6: Testing scenario of Section 2.4.1.

2. 4 . 2 Figure 7 :

 427 Figure 7: Testing scenario of Section 2.4.2.

Figure 8 :

 8 Figure 8: Testing scenarios of Section 2.4.3.

Figure 11 :

 11 Figure 11: Generic IR branching

Figure 12 :

 12 Figure 12: EFSM associated to group g

Figure 14 :

 14 Figure 14: An environment automaton

tFigure 15 :

 15 Figure 15: Test input generation for the running example

  Simplified extract of Einspielung in Antescofosequence of triggered actions called act(e i ). In the following, a finite sequence of actions is called group, and act(e i ) is called top-level group triggered by e i .

	2 http://brahms.ircam.fr/works/work/32409/
	bpm 144
	note D4 1/7 event1
	0 a0
	group 0 g1 @loose @global
	{
	0	a1
	1/7 a2
	1/7 a3
	1/7 a4
	1/7 a5
	1/7 a6
	1/7 a7
	}
	chord ( B3b D4 ) 1/7 event2
	chord ( E4 D4 ) 1/7 event3
	chord ( D5# D4 ) 1/7 event4
	chord ( A4 D4 ) 1/7 event5
	chord ( C4b D4 ) 1/7 event6
	chord ( G4 D4 ) 1/7 event7
	Figure 3:

  Figure10: IR of a loose and local group. In the initial state s 0 , the automaton is waiting for the trigger symbol ǧ. Once this symbol is read, it waits (in state s 1 ) for a delay d 1 , and sends action α 1 . Then it continues from state s 2 with the rest of the group.

	V t s0 E output input t in s1 u1 s2 sn ǧ? d1 α1! r . . . d 1 dn σ 1 ? . . . σ m ?	IU T S

out

Figure 9: Specification : reality (top) and models (down)

If the tempo changes in the score, then it is changed accordingly in the ideal trace.

http://www.uppaal.org

Acknowledgments

The authors wish to thank Antoine Rollet for his advises on MBT, and the team Ircam's Mutants for their help.


A soft dynamic programming approach for on-line aircraft 4D-trajectory optimization

Patrick Hagelauer, Felix Mora-Camino


Thom Frühwirth

Pascal Brisset
email: pascal.brisset@recherche.enac.fr

Optimal Planning of Digital Cordless Telecommunication Systems *

Digital mobile communications comes to company sites. No cabling is required and the employees can be reached at any time at any place. However, planning of wireless digital networks is quite different from planning traditional wire-based systems. Small, local radio transmitters (senders) have to be installed to provide the wireless devices with signals. The specifics of radio wave propagation at the installation site have to be taken into account.

POPULAR is an advanced industrial prototype that allows to compute the minimal number of senders and their location given a blue-print of the building and information about the materials used for walls and ceilings. It does so by simulating the propagation of radio-waves using ray tracing and by subsequent optimization of the number of senders needed to cover the whole building. Taking advantage of state-of-the-art techniques for programmable application-oriented constraint solving, POPULAR was among the first practical tools that could optimally plan cordless communication systems. In this paper, we introduce the basics of this real-life application and show how easy it is to implement the necessary constraints to solve the problem.

Introduction

Mobile communication has become literally ubiquitous these days. According to a press release of British Telecommunications Plc (BT) and MCI Communications Corp of September 1996, there are 600 Mill. phones worldwide, 60 Mill. of them mobile (compare this figure to the world's 50 Mill. fax numbers and 40 Mill. email addresses).

With the introduction of the European standard for digital cordless telecommunication (DECT) [ETS92] cordless local area networks are possible. The DECT standard integrates a number of telecommunication services. The wireless services include the Telepoint service (wireless public phones in cities), wireless Local Area Networks (LAN) for data transfer and wireless Private Automatic Branch Exchange (PABX) for in-house communication. The PABX service is the one we are concerned with in this article. PABX enables the installation of Cordless Business Communication Systems (CDBS). PABX systems (fig. 1) have turned out to be a major market which is growing even faster than the wireless communication market in general [START_REF]Cordless Telecommunications in Europe[END_REF].

Of course, selling such systems is not enough, the service that comes with it makes the difference. A vendor will also plan, install and maintain the system. Especially the planning phase is of importance, since a vendor that can offer to cover a company site with a smaller number of base stations will be ahead of its competition.

The DECT standard allows for a cellular structure of the radio network. A cell is the space that is covered by a single base station (a transmitter). Today, the number and positioning of base stations is estimated by an experienced sales person. The specifics of radio wave propagation at the installation site have to be taken into account. The size of a cell is usually in the tens of meters. For buildings, multi-cellular systems are required, because walls and floors absorb part of the radio signal. To help the sales person, Siemens has compiled a set of guidelines based on typical scenarios. However, a scenario may not always apply and the approach does not work well when it comes to position the base stations.

Computer-aided planning promises to ease some of the difficulties encountered. The idea is: Given a blue-print of the building or company site, together with information about the materials used for walls and floors, compute the minimal number of base stations and their location by simulation and subsequent optimization.

An advanced prototype, POPULAR (Planning of Picocellular Radio), was developed in collaboration with industry and research institutions in Germany: The Siemens Research and Development Department (ZFE), the Siemens Personal Networks Department (PN), the European Computer-Industry Research Center (ECRC) and the Institute of Communication Networks at the Aachen University of Technology.

The authors implemented a protoype version while working at ECRC -nick- named the "phone-demo" -in a few months in the constraint logic programming language ECL i PS e [MS*95]. The language includes a library for Constraint Handling Rules (CHR) [START_REF] Frühwirth | Chapter on Constraint Handling Rules[END_REF][START_REF] Frühwirth | Constraint Handling Rules, Chapter in Constraint Programming: Basics and Trends[END_REF], which are a high-level language extension to implement arbitrary constraint systems. The CHR library was essential for a rapid, flexible and efficient implementation of the geometric constraints that appear in this optimization problem. The prototype is part of the demo suite of ECL i PS e 3.4. Based on this prototype, J.-R. Molwitz from the University of Aachen implemented the tool POPULAR [START_REF] Molwitz | Entwicklung eines Werkzeugs zur Planung picozellularer Funknetze für die drahtlose Kommunikation[END_REF] within one man-year while at Siemens.

In the next section, we introduce the physical model of radio wave propagation used in our application. Then we describe the implementation giving details about the constraint solving involved in the optimization. Finally, we conclude the paper with an evaluation of our tool. This work is a companion paper to [START_REF] Frühwirth | Planning Cordless Business Communication Systems[END_REF] which does not describe the implementation, but concentrates on the model used and its features (here section 2). For a general survey on constraint logic programming see [START_REF] Jaffar | Constraint Logic Programming: A Survey[END_REF], for a survey on its applications [START_REF] Wallace | Survey: Practical Applications of Constraint Programming[END_REF].

Radio wave propagation suffers mainly from the following effects:

• attenuation (weakening) of the signal due to the distance,

• shadowing (absorption) through obstacles,

• multipath propagation due to reflection and diffraction. Figure 2 shows an example of the resulting path loss over distance on a logarithmic scale. At 6m and 9m walls are weakening the signal. The COST 1 Subgroup 'Propagation Models' proposed the following path loss model [START_REF]Propagation Models' Subgroup. Building Penetration Losses[END_REF]:

L P = L 1m + 10 n log 10 d + i k i F i + j p j W j (1)
where L P : total path loss in dB, L 1m : path loss in 1 m distance from transmitter, n : propagation factor, d : distance between transmitter and receiver, k i : number of floors of kind i in the propagation path, F i : attenuation factor of one floor of kind i, p j : number of walls of kind j in the propagation path, W j : attenuation factor of one wall of kind j.

The model is based on the power balance of wireless transmission. It combines a distance dependent term with correction factors for extra path loss due to floors and walls of the building in the propagation path. So far the path loss model does not take reflection and hence multipath effects into account. Even with sufficient receiver sensitivity a radio link could fail due to fading and too many bit errors that result from it. Thus a fading reserve (fade margin) is introduced. Furthermore, we also extended the model to take the directional effect of an antenna into account, since antennas do not beam with the same energy in every direction.

Planning in POPULAR

Given a blue-print of the building and information about the materials used for walls and ceilings, POPULAR computes the minimal number of senders and their location by simulating the propagation of radio-waves using ray tracing and subsequent optimization of the number of senders needed to cover the whole building.

To get a description of a building one scans in a blue-print. From the scanned image, the walls and ceilings are redrawn. Each wall and ceiling gets its own attenuation factor.

Simulation of Radio Cells by Ray-Tracing

The characteristics of the building are computed using of test points. Each test point represents a possible receiver position. The test points are placed on a 3-dimensional grid inside the volume that should be covered. At each floor of the building, there is one such layer of test points (fig. 3). For each test point the space where a sender can be put to cover the test point, the "radio-cell", is calculated. If the test grid is sufficiently small (several per squaremeter), we can expect that if two neighbouring test points are covered, the space inbetweenhence the whole building -can also be covered.

Ray tracing simulates the propagation of radio waves through the walls and ceilings of the building. To get to the point of minimal sensitivity (i.e. maximal permissible path loss), each path must be followed through the whole building (fig. 4). The values of antenna attenuation in the direction of the path, the path loss due to the distance and the insertion losses due to intersections of the path with walls and floors are added up to the maximal permissible path loss. The resulting end points are used to describe the hull of the radio cell. We use binary (dichotomy) search to find the threshold location for each ray to speed up the simulation. For each test point, 128 rays are computed in POPULAR.

Note that the radio-cell will usually be a rather odd-shaped object, since the coverage is not a smooth or even differentiable function. The received power at a single point may exhibit discontinuities because of tiny changes in the sender location -for example, a move around the corner can cause an entirely different pattern of transmitted rays. This is the reason, why the path loss formula cannot be directly expressed as a constraint and why ray-tracing has to be used. Also note that the coverage that can be computed is noisy, i.e limited in accuracy, otherwise we would have to calculate the effect of e.g. every piece of furniture.

In practice, the base stations are installed at the same height at each floor, on the ceiling or on the walls. This means that on each floor, the possible space of locations for base stations is on a single plane. This plane is intersected with the radio cells, reducing them from a polyeder to a series of connected polygons (one for each floor) (fig. 5).

Constraint-Based Optimization

For each of the resulting polygons a constraint is set up that there must be (at least) one location of a sender (geometrically speaking, a point) somewhere in that space. Then, we try to find locations that are in as many polygons at the same time as possible. This means that a sender at one of these locations will cover several test points at once. Thus the possible locations are constrained to be in the intersections of the polygons covered. In this way, a first solution is computed. Next, to minimize the number of senders, we use a branch-and-bound method. It consists in repeatedly searching for a solution with a smaller number of senders until the minimal number is found.

The result of covering a medieval monastery is shown in figure 6, where four senders are needed. If more than one sender covers a region, it is attributed to In a first attempt restricted to two dimensions, we approximated a polygon by a single rectangle. The 2-D coordinates are of the form X#Y, rectangles are orthogonal to the coordinate system and are represented by a pair, composed of their left lower and right upper corner coordinates. For each polygon, simply a constraint inside(Sender, Rectangle) is imposed, where Sender refers to a point that must be inside the Rectangle.

The constraint solver was implemented using Constraint Handling Rules (CHR) [START_REF] Frühwirth | Chapter on Constraint Handling Rules[END_REF][START_REF] Frühwirth | Constraint Handling Rules, Chapter in Constraint Programming: Basics and Trends[END_REF], which are our proposal to allow for more flexibility and applicationoriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. The CHR code for the inside constraint is simply:

% inside(Sender, LeftLowerCorner -RightUpperCorner) not_empty @ inside(S,A#B-C#D) ==> A<C,B<D. intersect @ inside(S,A1#B1-C1#D1),inside(S,A2#B2-C2#D2) <=> A is max(A1,A2), B is max(B1,B2), C is min(C1,C2), D is min(D1,D2), inside(S,A#B-C#D).
The first rule (named not empty) says that the constraint inside(S,A#B-C#D) is only valid if also the condition A<C,B<D is fulfilled, so that the rectangle has a non-section test point

Figure 5: Typical radio coverage areas in a building empty area. The intersect rule says that if a senders location S is constrained by two inside constraints to be in two rectangles at once, we can replace these two constraints by a single inside constraint whose rectangle is computed as the intersection of the two initial rectangles.

To compute a solution, after we have set up all the inside constraints, we try to equate as many senders as possible. (This is called the "labeling phase" of the constraint computation). A simple way to do this is the following recursive procedure:

equate_senders([]) <=> equate_senders([S|L]) <=>

(member(S,L) or true), % equate S with another sender or not equate_senders(L).

For each sender S, the piece of code (member(S,L) or true) nondeterministically equates S with one of the remaining senders in the lest L using member or does not do so (true). Equating senders causes the intersect rule to fire with the constraints associated with the senders. As a result of this labeling procedure, a senders location will be constrained more and more and thus the intersect rule will be applied again and again until the rectangle becomes very small and finally empty. Then the not empty rule applies, causes failure and so initiates chronological backtracking that will lead to another choice.

A good heuristic for equating senders takes advantage of the geometric nature of the problem and equates senders from polygons associated with nearby test Figure 6: Covering a medieval monastery points first. The result of the optimization is a few senders constrained to be located inside some small rectangle.

It took just 10 minutes to extend this solver so that it works with union of rectangles, that can describe the polygon more accurately, actually to any desired degree of precision. This corresponds to a disjunctive constraint of the form inside(S,R1) or inside(S,R2) or ... or inside(S,Rn) which is more compactly implemented as inside(S,[R1,R2,...,Rn]). "Geom" stands for "geometrical object". % inside(Sender, GeomList) intersect @ inside(S, L1), inside(S, L2) <=> intersect_geoms(L1, L2, L3), L3 = [_|_],

% at least one geom left inside(S, L3). intersect_geoms(L1, L2, L3) <=> setof(Geom, intersect_geom(L1,L2,Geom), L3).

intersect_geom(L1, L2, rect(A#B,C#D)) <=> member(rect(A1#B1,C1#D1), L1), member(rect(A2#B2,C2#D2), L2), A is max(A1,A2), B is max(B1,B2), C is min(C1,C2), D is min(D1,D2), A<C, B<D. % not empty

The above solver can be adapted quickly to work with other geometric objects than rectangles by changing the definition of intersect geom/3. Also, the lifting to 3 dimensions just amounted to adding a third coordinate and code analogous to the one for the other dimensions. The simplicity of the solver does not mean primitiveness or triviality, it rather illustrates the power of CHR, since it would be quite hard to implement the functionality in a hard-wired black-box solver:

Already in the initial non-disjunctive case there are problems: Finite domains are in principle applicable, however coordinates would have to be rounded to integers. Also, we found that for our application the built-in finite domain solver of ECL i PS e was slightly slower than the CHR implementation. Using linear polynomial constraints would be an overkill and thus inefficient, too. Interval arithmetic as in CLP(BNR) [START_REF] Benhamou | Interval constraint logic programming[END_REF] or Newton [START_REF] Benhamou | CLP(Intervals) Revisited[END_REF] can express the required constraints more adequately -even when we move from rectangles to other geometric objects that are described by non-linear equations. However, the actually used disjunctive geometric constraints would require recasting using auxiliary variables, which is expensive, error-prone and limits the amount of propagation. The cardinality constraint of cc(FD) [START_REF] Van Hentenryck | Constraint processing in cc(fd)[END_REF] could be used to express the disjunction. But to the best of our knowledge, a glass-box system combining interval reasoning and cardinality is not available.

Evaluation and Conclusions

While we worked on POPULAR, without knowing from each other, the WISE tool [FGK*95] was developed with exactly the same functionality. WISE is written in about 7500 lines of C++. For optimization WISE uses an adaptation of the Nelder-Mead direct search method that optimizes the percentage of the building covered. A recent paper [START_REF] Stamatelos | Spectral Efficiency and Optimal Base Placement for Indoor Wireless Networks[END_REF] uses the Nelder-Mead method for continuous space and Hopfield Neural Networks for a modelling in discrete space. The authors shortly mention a tool called IWNDT which is programmed in C.

POPULAR is a state-of-the-art tool. For a typical office building, an optimal placement is found by POPULAR within a few minutes. This is impressive since everything (including ray tracing and a graphical user interface) was implemented in a CLP language. The CLP code is just about 4000 lines with more than half of it for graphics and user interface. The overall quality of the placements produced is comparable to that of a human expert. The precision of the placements is within 0.7 meters. It is influenced by the underlying path loss model with its the fading reserve, the number of rays used in the simulation and the approximation of radio cells by unions of rectangles.

While the simulation phase has linear complexity in the number of test points, the optimization phase has a theoretical exponential complexity. Our practical experience shows, however, that the actual complexity is much lower. Ray tracing is fast by limiting the number of rays to 128 and by using binary (dichotomy) search for the threshold of each ray. The labeling benefits from heuristics that take the geometric nature of the problem into account. The average run-time on a SUN SPARCStation 10 was almost linear in the number of walls and test points, with about 25ms per wall and per test point. In a big building, this number may reach several thousands, resulting in computation times of about a minute and placing up to 25 base stations.

The necessary constraints were expressed and implemented with ease in CHR. Simplicity, flexibility, efficiency and rapid prototyping were the advantages of using CHR: The application was extended from rectangles to unions of rectangles, from 2-D to 3-D. Also, restricting allowed senders locations to walls or near ceilings or to aisles for ease of installation and maintenance was just a matter of constraining the sender positions to the union of the allowed spaces.

Figure 1 :

 1 Figure 1: Wireless Private Automatic Branch Exchange (PABX) with Base Stations (BS) and Public Switched Telephone Network (PSTN)

Figure 2 :

 2 Figure 2: Path loss with additional attenuation at 6m and 9m due to walls

Figure 3 :

 3 Figure 3: Grid of test points in a building

Figure 4 :

 4 Figure 4: Path from transmitter intersecting a ceiling and a wall


Christophe Macabiau
email: macabiau@recherche.enac.fr

Willy Vigneau
email: vigneau@m3systems.net

Dominique Houzet
email: dominique.houzet@enseeiht.fr

EVIL WAVEFORM TEST-BED DESIGN

I. INTRODUCTION

Several types of failures can occur in the GPS satellites that transmit the ranging signals to the users. Among them, a specific type of failure in the signal generation process aboard the satellite may result in an anomalous waveform being transmitted, called an 'evil waveform'.

Evil waveforms are GPS signals that have a distorted PRN code modulation waveform. The main impact is a rupture of the symmetry of the cross-correlation peak inside the tracking channel, therefore inducing a different measurement error for two receivers that would not have the same architecture. As a consequence, there is a potential for evil waveforms to induce large tracking errors of differential systems if left undetected.

Simulations of the impact of these evil waveforms using simplified GPS receiver simulators with harmonized assumptions have been conducted by several teams. This includes simulations of the performance of the ground monitoring techniques and tracking errors induced by these waveforms [START_REF] Macabiau | Signal Quality Monitoring for Protection of GBAS Users Against Evil Waveforms[END_REF]. Only a small number of practical results were reported about the behavior of real receivers tracking evil waveforms [START_REF] Macabiau | Signal Quality Monitoring for Protection of GBAS Users Against Evil Waveforms[END_REF].

ESTEC has decided to develop a test-bed to increase the knowledge on the true effect of evil waveforms on real receivers since few results exist on the subject. The test set-up will allow to :

• understand how real receivers behave when tracking evil signals (deformation of correlation function, acquisition and tracking points), • find-out if their behavior is conform to what can be predicted using receiver simulators,

• analyze what exactly is the performance of the different ground monitoring techniques.

This test-bed is developed jointly by M3SYSTEMS, ENAC and ENSEEIHT.

II. EVIL WAVEFORM MODEL

Evil waveforms are GPS signals that have a distorted PRN code modulation waveform. The deformation is modeled by a lead or a lag of the rising or falling edges of the modulation code, and/or by a second-order filtering of this waveform.

The main impact is a rupture of the symmetry of the cross-correlation peak inside the tracking channel, therefore inducing a different measurement error for two receivers that would not have the same architecture.

As a consequence, there is a potential for evil waveforms to induce large tracking errors of differential systems. This potential danger pushed the Global Navigation Satellite System Panel (GNSSP) of the International Civil Aviation Organization (ICAO), and the RTCA SC-159, to propose sections in the standards that would guarantee the safe operation of differential GPS.

Several teams gathered their efforts to tackle that problem, and it was proven from simulation results that an adequate ground monitoring technique exists and that constraints on the airborne receiver could be proposed to make sure the differential tracking error does not exceed the required accuracy level.

The evil waveform is a GPS signal that has a distorted PRN code modulation waveform. The failure giving birth to an evil waveform occurs in the code modulation generation channel only, therefore the transmitted carrier is not affected. Two types of failure can occur that result in an evil waveform being radiated. A failure in the digital code chip generation module can alter the synchronization of some of the C/A code chip edges. A mismatch of the analog bandlimiting filter can distort the physical waveform being transmitted.

As a consequence, the model proposed in [START_REF] Enge | Detecting Anomalous Signals from GPS Satellites[END_REF] is a PRN signal affected by one or both of the following effects: 1. All the falling edges or all the rising edges of the code modulation are delayed or advanced by an amount of ∆ seconds. If there is a lag, then ∆ is positive, if there is a lead, ∆ is negative. ∆ is usually expressed in chips, as a multiple of the chip length T c =1/1.023⋅10 6 s.

2. The modulation is filtered by a 2 nd order filter characterized by two parameters:

• σ=δω n where δ is the damping factor and ω n /2π is the frequency.

• 2 1 2 δ π ω - = n d F is the resonant frequency.
Usually, σ and F d are expressed in MHz.

Several types of threat models are considered: • Threat model A: this type of evil waveform contains only the lead/lag effect. In that case, σ=0, F d =0 and the accepted range of values for ∆ is: -0.12 T c ≤ ∆ ≤ 0.12 T c . • Threat model B: this type of evil waveform contains only the 2 nd order filtering effect.

III. IMPACT OF EVIL WAVEFORM ON RECEIVERS

Model A evil waveforms add a periodic line spectrum to the nominal C/A code power spectrum density. This additive line spectrum has a

( ) ∆ ∆ f f π π sin envelope.
Moreover, model A evil waveforms raise the DC component of the code modulation by an amount close to 2 ∆ due to the near balance of 0s and 1s in each C/A code.

As indicated in [START_REF] Enge | Detecting Anomalous Signals from GPS Satellites[END_REF], the cross-correlation between model A evil waveforms and a nominal C/A code shifts the top section of the triangle by ∆/2, and introduces a plateau of width ∆.

Model B evil waveforms raise all the frequency components of the code spectrum located around F d ,. As a result, the cross-correlation function is also filtered by the 2 nd order filter.

Model C evil waveforms are a combination of the lead/lag effect with the 2 nd order filtering effect.

IV. TEST-BED ARCHITECTURE

The General test bed architecture can be broken down into the following building blocks :

• Baseband IF Signal generator: This generator is designed to output the baseband evil waveform signal. It includes a digital unit providing analog undisturbed baseband GPS signals with two different C/A code (PRN1 and PRN2) .

One of these signals is crossing a module that provides the lead/lag effect on the rising edge of chips, the output is the model A evil waveform. This signal is fed to a 2 nd order filter designed to add model B evil waveform generation capability. The output of this baseband IF Signal generator is the sum of the undisturbed signal and the model C evil waveform (or model A or B according to the modules' parameters), both in baseband. The whole signal generator functions are provided by a numeric card (FPGA) described in Section V. • RF Signal generator:. This is an Off The Shelf signal generator performing the modulation of the L1 carrier by the baseband modulation signal. The selected equipment is Vector signal generator -SMIQ -Rohde & Schwarz. • Receiver: For determining the measurement error induced by evil waveforms, the receiver can be any GPS receiver providing raw data output. For testing the performance of evil waveform monitoring techniques, the receiver selected is a NovAtel Millenium receiver with specific multi-correlator software (Cf. Section 6). This receiver will also be extensively used for range error analysis due to its large RF bandwidth and its capability to have various chip spacings and discriminator types. • Evil waveform events monitoring : The system is composed of the NovAtel Millenium receiver with the multicorrelator software, whose outputs are collected in real time with a LabView module running on a PC, implementing an SQM technique.

The Test Bed architecture is illustrated in figure 1

V. EVIL WAVEFORM GENERATOR

The board is using a set of a digital unit delivering model A evil waveforms, and the 2 nd order filter. The digital unit is designed to output the analog baseband GPS signal including rising or falling edge shifts corresponding to model A evil waveforms. This unit is a FPGA circuit reading memories containing valid navigation messages and the PRN to be generated. The FPGA will also have the capability to delay the rising or the falling edges of the bit transitions by triggering counters driving latches.

This output will then have to be fed to a 2 nd order filter implemented in the second digital unit. The combination of the module adding the delays on the bit transitions and the 2 nd order filter allows the generation of any GPS evil waveform.

Two PRNs signals are generated in baseband: one of them is not affected by the evil waveform, the second one is affected. This is done so that the GPS receiver can provide two pseudorange measurements than can be differenced to yield directly the pseudorange measurement error induced by the evil waveform.

The entire generator needs to be tied to a common clock. That common clock is the 10 MHz reference synchronization signal that is output by the SMIQ OCXO. The FPGA board uses that 10 MHz reference signal to trigger the generation of the C/A code chip edges. That 10 MHz reference is also internally used by the SMIQ itself to generate the L1 carrier. Such a synchronization is required so that the receiver can track signals for which the dynamics on the carrier is identical to the dynamics on the code modulation.

The general architecture of the board used to generate the evil waveform is given in figure 3

VI. MULTICORRELATOR RECEIVER

The receiver used in the test-bed is a Novatel Millenium receiver. That receiver can provide as much as 48 correlator output pairs (48 on I, 48 on Q), where all correlators are slaved to the punctual determined by one tracking pair in one tracking channel.

The first software has a single tracking channel providing 48 correlator output pairs with 5 distributions (evenly spaced correlator, leading or trailing edge only, peak intensive distribution, and ultra wide spacings). Correlator ouputs observed with the first configuration with nominal signal conditions are shown in figure 5. The second software is a multiple correlator outputting 12 correlator pair values (12 I and 12 Q) for 4 tracking channels.

In each channel, all the correlators are slaved to the tracking pair and placed at the location (in each of the 4 channels) as illustrated in figure 6. This software version is designed to implement the SQM candidate 2b described in [Ref. 11].

Finally, the third software version has a single tracking channel and allows 4 chip spacings (0.05, 0.1, 0.2, 0.5, 1.0) with traditional dot-product discriminator (figure 7), and 3 chip spacing sets (0.05-0.1, 0.1-0.2, 0.2-0.4) with double delta discriminator. As we can see from these 2 figures, the main effect of the oscillations is predicted with good accuracy although a deviation is visible. That deviation has a maximum value of 0.03, and is globally lower than 5% in the interval [-0.5; 0.5] chip of the correlation function.

VII. CODE TRACKING ERROR

Another task included in the test plan is to observe the tracking error induced by evil waveforms. That analysis is done to determine what exactly is the influence of evil waveforms on a receiver tracking loop and to compare the predicted values with the observed values. The linear evolution of the tracking error seen on these 2 figures can be explained by the predicted effect of a model A evil waveform on the correlation peak. In the case of an infinite bandwidth receiver, a model A evil waveform creates a plateau of width ∆ on the correlation function and shifts the correlation function by ∆/2. Therefore, as the receiver used has a wide bandwidth (BW2=16 MHz), the tracking error grows as ∆/2 as long as ∆ is lower than the chip spacing. Some distortions to that simple value are introduced when ∆ is larger than the chip spacing.

The software used to predict the measurement error takes all this into account, but we can see that the predicted value deviates from the observed value as ∆ grows (0.8 m for ∆=0.12 Tc for a 0.05 chip DLL in figure 11, 0.6 m for ∆=0.12 Tc for a 0.2 chip DLL in figure 12). That behaviour may be due to several factors: first of all, the ∆ value affecting the PRN modulation may have a few percent incertitude. Secondly, as the DLL chip spacing is smaller than ∆, the DLL locks on a point that is difficult to predict because of the flatness of the discrimination function in those cases.

Globally, the error is lower than 0.8 m for all configurations tested, which is satisfying. Figure 13 represents the evolution of the observed tracking error as a function of F d and σ. As we can see, for a specific σ, the error decreases when Fd increases. This is due to the combinations of two effects: first of all, as Fd increases, the tracking error decreases in the case of an infinite bandwidth receiver. Then, the filtering effect applied by the receiver front-end filter reduces the amount of high-frequency components entering the tracking loops. As we can see, the effect of model B evil waveforms is quite constant starting from Fd=9 MHz.

We can see from the contour plot in figure 14 that the deviation between the observed and predicted tracking errors is maximum when F d is lower than 8 MHz. In that region, the maximum deviation is -1.9 m (observed 9.6 m / predicted 11.5 m) for Fd=4 Mhz and σ=3.8 MHz. The deviation here may be due to the implementation of the second order filter that was done on the FPGA and to our capacity to model the RF front-end filter. The waveform is encoded on 8 bits, which is perhaps too small a number of bits to represent the waveform. Then, the true RF front-end filter differs from our best model. That deviation represents an 18% accuracy, which we feel is quite large. Current efforts aim at understanding whether this deviation is due to the model B evil waveform implementation in the EWF generator or to an inadequate receiver filter model.

VII. CONCLUSION

A test-bed for evaluation of the effect of evil waveforms on real receivers is in development for ESA. That test-bed is designed to provide knowledge on the true impact of evil waveforms on the correlation function and on the tracking error, as well as to test the performance of SQM techniques.

The test-bed is composed of a baseband generator that can generate all evil waveforms in models A, B and C, delivering a signal to a vector signal generator to which a real receiver can be connected.

Initial correlation function observations show a good consistency between the predicted and observed deformations (less than 5% error in the [-0.5; 0.5] chip region.

The pseudorange error measurements in most of the possible cases have been done. The first analyses of the observed and predicted errors that were conducted are satisfying for model A evil waveforms (0.8 m max deviation between observations and predictions). Those analyses are not completely satisfying for model B evil waveforms (1.9 m max deviation), and efforts will are made to determine whether this deviation may be due to the EWF generator or to the receiver filter model.

Further efforts will aim at testing the SQM performance using the evil waveform generator and using live GPS signals.

Figure 1 :

 1 Figure 1: Test Bed ConfigurationFigure2shows the test bed that has been developed. The baseband signal generator block is provided by the electronic card -metallic box-, the RF signal generator is the SMIQ 02B at the bottom-left of the picture, events monitoring are assumed by the computer, and the receiver is the black box on the generator. The additional equipment used for development and validation phases is a frequency meter and an oscilloscope (on the SMIQ).

Figure 2 :

 2 Figure 2: Evil Waveform Test Bed

Figure 4 :

 4 Figure 4: Nominal tracking error in absence of evil waveforms.

Figure 5 :Figure 6 :

 56 Figure 5: Nominal correlator outputs with the 1 st software configuration.

Figure 7 :Figure 8 :Figure 9 :Figure 10 :

 78910 Figure 7: Possible E-L tracking pairs with 3 rd SW version

Figures

  Figures 11 and 12 show the evolution of the observed and predicted tracking errors induced by a model A evil waveform on an E-L 0.05 chip DLL and a 0.2 chip DLL.

Figure 11 :

 11 Figure 11 : Comparison between observed and predicted effect of model A EWF on an E-L 0.05 chip DLL

Figures

  Figures 13 and 14 show a comparison between the observed and predicted tracking errors induced by a model B evil waveform on an E-L 0.1 chip DLL.

Figure 13 :

 13 Figure 13: Evolution of the observed tracking error in presence of a model B evil waveform.Figure 14: Deviation between the observed and the predicted tracking error (model B evil waveform).

Figure 14 :

 14 Figure 13: Evolution of the observed tracking error in presence of a model B evil waveform.Figure 14: Deviation between the observed and the predicted tracking error (model B evil waveform).

  Therefore, ∆=0 and the possible range of values for σ and F d is: 0.8 MHz ≤ σ ≤ 8.8 MHz, 4 MHz ≤ F d ≤ 17 MHz. • Threat model C: this type of evil waveform contains both effects. The possible range of values is: -0.12 T c ≤ ∆ ≤ 0.12 T c , 0.8 MHz ≤ σ ≤ 8.8 MHz, 7.3 MHz ≤ F d ≤ 13 MHz.

  :

													Clock 10 Mbps
			PRN2 code			1.023 Mbps
			generator			(1 ms/cycle)
									Modulo
									2 adder
			Navigation Data
			stream Generator		50 bit/s (12,5 min/cycle)
									Modulo 2 adder		Ligne Lead /Lag retard Effect			2nd order Filter						D/A converter	I	SMIQ
	RS232																									Q
			PRN2 code generator			1.023 Mbps (1 ms/cycle)
	Downloading
										CONTROL
	0,15
	0,1
	0,05
	0
	1	5	9	13	17	21	25	29	33	37	41	45	49	53	57	61	65	69	73	77	81	85	89	93	97	101 105 109 113 117
	-0,05
	-01

Figure 3: Evil Waveform Generator Architecture Figure 4 shows an example of the code tracking error that can be observed with a nominal signal when no evil waveforms are applied.

Presented at NAVITEC'01, ESTEC, Noordwijk


Wen Chi Lu

Felix Mora-Camino

Karim Achaibou

A new flight guidance approach based on differential flatness

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