Camille Constant
email: camille.constant@irisa.fr

Bertrand Jeannet
email: bertrand.jeannet@inrialpes.fr

Thierry Jéron
email: thierry.jeron@irisa.fr

AUTOMATIC TEST GENERATION FROM INTERPROCEDURAL SPECIFICATIONS

Keywords: Model-based testing, push-down systems, reactive systems, test selection Test à partir de modèles, automates à pile, systèmes réactifs, sélection de tests

This paper adresses the generation of test cases for testing the conformance of a black-box implementation with respect to its specification, in the context of reactive systems. We aim at extending the principles and algorithms of model-based testing à la ioco for recursive specifications that can be modeled by Push-Down Systems (PDS). Such specifications may be more compact than non-recursive ones and are more expressive.

The generated test cases are selected according to a test purpose, a (set of) scenario of interest that one wants to observe during test execution. The test generation method we propose in this paper is based on program transformations and a coreachability analysis, which allows to decide whether and how the test purpose can still be satisfied. However, despite the possibility to perform an exact analysis, the inability of test cases to inspect their own stack prevents it from using fully the coreachability information. We discuss this partial observation problem, its consequences, and how to minimize its impact.

I R I S A 1 Introduction

We address the generation of test cases in the framework of conformance testing of reactive systems [START_REF]Conformance Testing Methodology and Framework[END_REF]. In this context, a Test Case (TC ) is a program run in parallel with a blackbox Implementation Under Test (IUT ), that stimulates the IUT by repeatedly sending inputs and checking that the observed outputs of the IUT are in conformance with a given specification S. In case the IUT exhibits a conformance error, the execution is immediately interrupted. Moreover, in addition to checking the conformance of the IUT , the goal of the test case is also to guide the parallel execution towards the satisfaction of a test purpose, typically a set of scenarii of interest. The test selection problem consists in finding a strategy that maximizes the likehood for the test case to realize the test purpose. This problem has been previously addressed in the case where the specifications, the test cases and the test purposes are modeled with finite Labelled Transition Systems (LTS) [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF][START_REF] Jard | TGV: theory, principles and algorithms[END_REF]. It was more recently addressed in the case where the same objects are modeled with Symbolic Transition Systems (STS), which extend LTS with infinite datatypes and can model non-recursive imperative programs [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF]. The aim of this paper is to address the test selection problem in the case where the specification is modeled as a Push-Down System (PDS), which extends LTS with a stack over a finite alphabet and can model recursive programs manipulating finite datatypes, which are more expressive than single procedure programs. Fig. 1 summarizes the different models.

Contributions. The contribution of this paper is twofold. First we describe a test selection algorithm that takes as input a recursive specification and a non-recursive test purpose and that returns a recursive test case. This algorithm is based on program transformations and (co)reachability analysis of recursive programs. Technical choices are guided by theoretical properties of the underlying PDS and LTS models, but the generation is defined in term of programming language concepts. Second, we analyze the partial observation problem, due to the inability of test cases to inspect their own stack. We compare its consequences on the generated test cases with the impact of using a non-exact, overapproximated coreachability analysis as done for test selection based on symbolic STS models [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF].

LTS STS

PDS

Introductive Example

We illustrate in this section the concepts we will develop and our testing methodology on a running example, before formalizing it in the next sections.

Specification. In our testing theory, the IUT is considered as a black box reactive system, and its observation points are the messages exchanged with its environment. The specification we consider as an example is the small recursive program of Fig. 4. Its control flow graph is given on Fig. 2(a). Double circles denote the observation points. Inputs and outputs are distinguished by the symbols ? and ! (inputs and outputs alphabets are disjoints). The behavior of this specification program is the following: the main function calls the function F (), which either emits the output !z and returns, or emits the output !x, calls the function G(), then receives the input c and returns to its caller. According to its first input, the function G() has two different behaviors: if the input is ?a, it returns to the caller, whereas if the input is ?b, the function G() is called again (recursively) and after it returns, the output !y is emitted.

What is really important is the traces recognized (or generated) by the specification, which is here

Traces(S) = {!z} ∪ {!x • (?b) n •?a • (!y) n • c? | n ≥ 0}.
The (non-)conformance of an IUT w.r.t. a specification S will be only based on Traces(S). Intuitively, an IUT will be defined as conformant to S if after any execution trace which is a prefix of Traces(S), it emits only outputs that S can emit as well. For instance, the IUT besides (where [] stands for the non-deterministic choice operator) is not conformant to S. After the execution trace !x, it may emit !y, whereas S specifies that no output may be emitted at this point: one or more ?b and then one ?a should be received first).

The global variable t has no influence on Traces(S), its usefulness will be explained later (see Sect. 6).

Canonical Tester. A tester, called canonical tester can be generated from S very straightforwardly, according to the (yet intuitive) definition of conformance. The program transformation consists in mirroring inputs into outputs and vice-versa, and to emit a failure verdict PI n1835 when the transformed program receives an unexpected input at an observation point. Fig. 5 gives the canonical tester Can(S) associated to S. A new type and a global variable verdict have been introduced for storing the verdict. Can(S) stimulates the IUT by sending to it input messages, and checks that the outputs of the IUT , which correspond to its own inputs, are conformant w.r.t. S.

If this canonical tester is run in parallel with the non-conformant program of Fig 3, and if the conformant program chooses to emit !x and then !y, the tester will perform the execution m 0 τ -→ f 0 ?x -→ f 1 τ -→ g 0 and will reach location g 0 , where it will receive an unexpected ?y input and will abort.

Notice that not only the (canonical) tester, but also the example IUT accept any input at an observation point. For the tester, the reason is that it should check any output from the IUT for conformance. For the IUT , this allows to prevent deadlocks.

The name canonical tester stems from the fact that it can detect any non-conformant execution of the implementation. It is actually the most general tester, from which any sound test case can be derived.

Test purpose. For large specifications, the canonical tester is too general. It tests the IUT in a completely random way. One is often more interested in guiding the execution of the IUT so as to realize a specific scenario that may reveal an error, and to stop the test execution successfully when the scenario has been completed without conformance error.

In this context, a test purpose is a (set of) scenario one wants to observe during a conformant test execution. The test purpose depicted as an automaton on Fig. 2 specifies that one is interested in detecting conformance errors occuring along the traces in Traces E (TP ) = xb * ayc. The symbol * means "all other elements in the alphabet" and the double circle denotes the final state E. This test purpose indicates that we want to test the case where the IUT emits !x at control point f 0 and where it performs one recursive call of G from G.

The aim of test selection is to transform the canonical tester so that it is more likely to produce the execution trace xb * ayc until completion when executed in parallel with the IUT . When performing such a selection, we anticipate the possible behaviors of a conformant IUT. If a conformance error occurs, the tester aborts immediately with a fail verdict. For instance, the first time the tester enters in function G(), it should first emit a !b, because a matching ?y should be later received to realize the scenario. Moreover, the second time it enters (recursively) in function G(), it should emit an !a, because only one ?y message should be observed before !c.

On the other hand, if an IUT starts its execution by emitting one !z (which is conformant to S), the scenario cannot be completed. The tester should detect such a case and abort gracefully with an inconclusive verdict.

Selected test case. Fig. 8 depicts the test case we obtain with the method we will develop in the paper. Compared to the canonical tester of Fig. 5, we have first inserted at each observation point a call to the function TP() (after having checked the absence of conformance Irisa Constant, Jeannet & Jéron error at this point). The function TP() defined on Fig. 6 takes as input the last message exchanged and implements the automaton of Fig. 2(b). If the final state is reached, it emits the pass verdict.

There are two other modifications to the canonical tester. At control point f 0 , when a ?z is received, the inconclusive verdict is emitted. Last, at control point g 0 , the condition for emitting a message has been enforced: !a is emitted iff the variable t is true. Indeed, t allows to distinguish if G() is called for the first time from f 1 , in which case t is false, or if it is called recursively from g 2 , in which case t is true. Hence, the knowledge of the value of t allows the test case to realize exactly the scenario defined by the test purpose (once ?x has been received from the IUT ).

The next sections describe the theoretical fundations of this test selection scheme sketched on the running example. Sect. 3 reminds classical definitions related to LTS and PDS. Sect 4 recalls the testing theory we use and the corresponding test selection algorithm on LTS models. We define in Sect. 5 a small programming language and define its semantics in term of PDS. We also describe how specifications, canonical tester and test purposes are defined. Sect. 6 describes the selection algorithm and discuss the issues related to partial observation, and Sect. 7 draws some conclusions and perspectives.

Labelled Transition Systems and Push-Down Systems

A Labelled Transition Systems (LTS) is defined by a tuple M = (Q, Q 0 , Λ, →) where Q is a set of states, Q 0 is the set of initial states, Λ = Λ v ∪ {τ } is an alphabet of visible (Λ v
) and internal ({τ }) actions and →⊆ Q × Λ × Q is a set of labelled transitions. The notation p a → q stands for (p, a, q) ∈→, and p a → for ∃q : p a → q. An execution is a sequence q 0 a0 → q 1 a1 → . . . q n+1 with q 0 ∈ Q 0 . Traces(M ) ⊆ Λ * v denotes the projection of the set of executions of M onto visible actions. For a subset X ⊆ Q of states, Traces X (M ) denotes the projection of the set of executions of M ending in a state q ∈ X onto visible actions. It is also named the set of traces accepted by X. The set of prefixes (resp. strict prefixes) of a set of traces Y is denoted by pref

≤ (Y ) (resp. pref < (Y )). M is deterministic if Q 0 has a single element q 0 , if p α → q ∧ p α → q =⇒ q = q and if p τ → q =⇒ ¬(∃α ∈ Λ v : p α →). M is complete for A ⊆ Λ, if ∀a ∈ A, ∀p ∈ Q, p a →.
A labelled Push-Down System (PDS) is defined by a tuple P = (G, Γ, Λ, c 0 , →) where G is a finite set of locations, Γ is a finite stack alphabet, c 0 ∈ G×Γ * is the inital configuration, Λ = Λ v ∪{τ } is a finite set of visible (Λ v ) and internal ({τ }) actions, and →⊆ (G×Γ )×Λ×(G×Γ * ) is a finite set of labelled transitions. Such a labelled PDS P generates an infinite LTS

M = (Q M , Q M 0 , Λ, → M ) where Q M = G × Γ * , Q M 0 = {c 0 }
, and →is defined by the rule:

(g, γ) α → (g, γ ) ∧ ω ∈ Γ * =⇒ (g, ω • γ) α → (g, ω • γ )
The notions of deterministic and complete PDS are defined in term of LTS.

Irisa 4 Testing Theory

The testing theory we consider is based on the notions of specification, implementation, and conformance relation between them [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF]: the specification is a deterministic LTS S = (Q S , Q S 0 , Λ, → S ), and the Implementation Under Test (IUT ) is assumed to be an LTS IUT = (Q IUT , Q IUT 0 , Λ, → IUT ) which is unknown except for its alphabet, which is assumed to be the same as that of the specification. Moreover, it is assumed that the IUT is input-complete, which reflects the hypothesis that the IUT cannot refuse an input from its environment.

In this context, a test case for the specification S is a deterministic LTS TC = (Q TC , Q TC 0 , Λ, → TC ) which is able to interact with an implementation and to emit verdicts:

-its alphabet is the mirror of that of S (Λ TC ? = Λ S ! and Λ TC ! = Λ S ? ) -it is input-complete (outputs of IUT are not refused) except in verdict states; -it is equipped with 3 disjoint subsets of sink, verdict states Pass, Fail, Inconc ⊆ Q TC .

Intuitively, Fail means rejection, Pass that some wanted behavior has been realized (this will be clarified later), and Inconc that a wanted behavior cannot be realized any more.

The conformance relation defines which implementations are considered correct w.r.t. the specification. We will consider the following conformance relation:

Definition 1 (Conformance relation). Let S = (Q S , Q S 0 , Λ, → S ) and IUT = (Q IUT , Q IUT 0 , Λ, → IUT ) be two LTS with same alphabet. A trace σ of IUT conforms to S, denoted by σ conf S, iff pref ≤ (σ) ∩ [Traces(S)•Λ ! \ Traces(S)] = ∅
IUT conforms to S, denoted by IUT conf S, iff all its traces are conformant:

Traces(IUT ) ∩ [Traces(S)•Λ ! \ Traces(S)] = ∅.
Intuitively, IUT conf S if after each trace of S, IUT may emit only outputs that S can emit as well, while its inputs are unconstrained. Except for the notion quiescence (absence of outputs), conf corresponds to the ioco relation of [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF]. The set of traces Traces(S)•Λ ! \Traces(S) is the set of minimal (with respect to the prefix ordering) non-conformant traces, which is characterized by a test case called the canonical tester, which is obtained from the specification S by inversion of inputs and outputs, followed by an input-completion, where each unspecified input leads to Fail. Definition 2 (Canonical Tester). Let S = (Q S , Q S 0 , Λ, → S ) be the deterministic LTS of the specification. The canonical tester of S for conf is the deterministic LTS

Can(S) = (Q S ∪ Fail, Q S 0 , Λ Can , → Can ) such that -Fail = {q Fail }, with q Fail ∈ Q S a new state; -its alphabet is the mirror of that of S (Λ Can ? = Λ S ! and Λ Can ! = Λ S ? ) -→ Can is defined by the rules: q, q ∈ Q S q α -→ S q q α -→ Can q q ∈ Q S α ∈ Λ S ! = Λ Can ? ¬(q α -→ S ) q α -→ Can q Fail PI n1835
Constant, Jeannet & Jéron

We have the following equalities:

Traces(Can(S)) = pref ≤ (Traces(S)•Λ ! ) Traces Fail (Can(S)) = Traces(S)•Λ ! \ Traces(S)
Can(S) is already a test case. However, it is typically too large and is not focused on any part of the system. It is more interesting in practice to test what happens in the course of a given scenario (or set thereof), and if no error has been detected, to end the test successfully when the scenario is completed. Definition 3 (Test Purpose). A test purpose TP for a specification S is a deterministic LTS TP = (Q TP , Q TP 0 , Λ, → TP ) equipped with a subset Accept ⊆ Q TP of accepting sink states. TP is complete except in Accept states. TP defines a set ATraces(S, TP ) of accepted traces of S which induces a set RTraces(S, TP ) of refused traces (traces of S that cannot be extended to accepted traces):

ATraces(S, TP ) = Traces Q S ×Accept (S ×TP ) = Traces(S) ∩Traces Accept (TP ) (1)
RTraces(S, TP ) = Traces(S) \ pref ≤ (ATraces(S, TP ))

The completeness assumption allows not to constrain S in the product S × TP (unless the execution trace is accepted). Observe that both accepted and refused traces are conformant.

The test case should now not only detect conformance errors, but also try to satisfy the test purpose. For this, it has to take into account output choices of the specification (observable non-determinism) and to detect incorrect outputs of the IUT w.r.t. the test purpose. The following definition formalizes the meaning of the verdicts of a test case. TC belongs to S (it is conformant) but is refused by TP . The test execution can thus be interrupted, as Pass cannot be emitted any more. In addition, the test case is optimal if: (4) Traces Inconc (TC ) = Traces(TC ) ∩ RTraces(S, TP ) ∩ pref < (ATraces(S, TP ))•Λ ! : Inconc is emitted as soon as possible; (5) Traces(TC ) ∩ Λ * • Λ ? ⊆ pref ≤ (ATraces(S, TP )): TC emits only outputs (inputs of S) which maintain the current trace in the accepted traces. The Fail and Pass verdicts are uniquely defined, so that they are emitted appropriately and as soon as possible, whereas the Inconc verdict is not uniquely defined. We have adopted this definition because checking whether a trace is refused is not always possible, either because it is undecidable, for instance with infinite-state symbolic model [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF], or because of partial observation issues as discussed in Sect. 6. Last, we refer to [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF] for details about the conditions (4) and ( 5) defining optimal test cases.

Irisa

Test selection for LTS. We briefly recall how to generate an optimal test case from a specification S and a test purpose TP given as finite LTS [START_REF] Jard | TGV: theory, principles and algorithms[END_REF]. One first builds the canonical tester Can(S) using Def. 2. One then builds the product P = Can(S) × TP combining the information about conformance given by Can(S) and the information about the wanted scenario given by TP . One defines the set Pass of verdict states as Pass = Q S × Accept TP . P as a test case satisfies conditions (1)-( 2 where coreach(Pass) = {q ∈ Q P | ∃q ∈ Pass : q → * q } denotes the set of states that may reach a state in Pass. Recalling that RTraces(S, TP ) = Traces(S) \ pref ≤ (ATraces(S, TP )), a valid test case TC is obtained from P by adding a new state Inconc and by modifying → P as follows:

q α -→ P q q ∈ coreach(Pass) q α -→ TC q q α -→ P q α ∈ Λ Can(S) ? q ∈ coreach(Pass) q α -→ TC Inconc
The first rule keeps only transitions maintaining the execution in coreach(Pass), in order to stay in pref ≤ (ATraces(S, TP )). In particular, it selects the appropriate outputs w.r.t. TP that should be sent to the IUT . As TC should remain input-complete, the second rule redirects the input transitions not selected by the first rule to the Inconc verdict, which is thus emitted as soon as the execution leaves the prefixes of accepted traces by a conformant input. The resulting test case TC satisfies all the conditions of Def 4.

Modeling Recursive Specifications and Test Purposes

The previous section recalled our framework for model-based testing, based on the lowlevel semantics model of LTS. We already extended these principles and designed sound algorithms for infinite-state symbolic transition systems in [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF]. Our aim here is to do the same for recursive specifications which can be compiled into (input/output) pushdown automata, PDS. Such specifications manipulate finite data but may have an infinite control due to the recursion, hence they are more expressive than finite LTS. In terms of traces, which is a relevant notion for the conformance relation, they generate context-free languages instead of regular languages. Moreover, even if there are cases where the recursion is bounded and the specification may be flattened into a LTS (by inlining), such a process may result in a huge LTS.

A small programming language. The syntax and semantics of the small language we used in the example of Sect. 2 is inspired by Bebop [START_REF] Ball | Bebop: A symbolic model checker for boolean programs[END_REF], an input language of the Moped tool, which is a model-checker for linear-time temporal logic on pushdown systems [START_REF] Esparza | A BDD-based model checker for recursive programs[END_REF].

Bebop uses a classical imperative language syntax. We assume for the sake of simplicity that control structures have been transformed into test and branch intructions, and that parameter passing and returns for procedures are emulated by using dedicated global variables. This results in the syntax given in Fig. 9. The features added to Bebop are the communication instructions, and the non deterministic choice operator between them. Emission and reception instructions use a special global variable p which contains the message, and which may be used only in the condition and in the block associated to these instructions. We assume that emission and reception are not nested. The operator [] is the non-deterministic choice operator. It may be used only for communication instructions. The reason is that while we allow non-determinism, it should remain observable, so that to any trace of the program corresponds an unique execution.

Control point k ∈ K Global environment g ∈ GEnv = GVar → Val Local environment l ∈ LEnv = LVar → Val Configuration (g, σ) ∈ C = GEnv × (K × LEnv ) +
Its semantics as a Push-Down System (PDS). We assume that the special variable p takes its values in the alphabet Λ. The semantics of this language is defined using the domains defined on Fig. 10. It is given as a labelled PDS P = (G, Γ, c 0 , Λ, →) where G = GEnv , Γ = K × LEnv , c 0 = (g 0 , (k 0 , l 0 )) is the initial configuration, and → is defined by the following inference rules, using the control flow graph associated to the program. We just sketch the standard inference rules and we refer to [START_REF] Esparza | A BDD-based model checker for recursive programs[END_REF] for more details, as we focus more precisely on the semantics of the emission and reception instructions.

-An atomic instruction generates a rule of the form

k atom ---→ k (g, (k, l)) τ → (g , (k , l ))
with a condition on (g, l) in the case of a test and branch instruction.

-A procedure call generates a rule

k proc() ----→ k (g, (k, l)) τ → (g, (k , l) • (s proc , l 0 ))
Irisa where s proc is the start point of the caller. Such a transition means that a new activation record is pushed onto the stack, with an initial local environment l 0 , which reflects the assumption that the variables are uninitialized. A procedure return generates a rule ------------------→

k ∀v = p : g (v) = g(v) (g, (k, l)) p → (g , (k , l)) if expr (g , l) = true (g, (k, l)) τ → (g , (k , l)) if expr (g , l) = false
One first forgets the previous value of p when introducing g , in order to make it uninitialized, as its real scope is the condition and the block associated to the emission. Then, if the current environment (g, l) satisfies the condition, p is emitted and the control passes to the beginning of the block k . Otherwise, the control passes to k . Notice that an non-deterministic choice is performed here: the instruction may emit any message p which satisfies the condition.

The semantics of the reception is identical to the emission. Emission and reception need to be distinguished only w.r.t. the conformance relation.

All instructions generate internal transitions labelled by τ , except emission and reception instructions. The observation points of a program are defined as the control points at the beginning of communication instructions. They are the only control points from which a message may be exchanged. Such observation points may be separated by (sequences of) ordinary control points linked by internal τ -transitions. Notice that we do not use the term "observation point" in the sense given to it in the testing community, when refering to the testing architecture.

Interprocedural specification and its canonical tester. An interprocedural specification S (c.f. Fig. 4) is a program defined with the language of Fig. 9, which is deterministic, in the sense that the allowed non-determinism should be observable, so that to a trace corresponds a unique possible execution ending in an observation point. A choice can still exist between two emissions and/or receptions, but we cannot have a choice between two internal instructions (generating τ -transitions).

This deterministic assumption allows to build easily the canonical tester of S, which is an executable, hence deterministic observer of Traces(S) • Λ S ? \ Traces(S). The canonical tester Can(S) is obtained from S using the following program transformation at each observation point: We will exploit nice theoretical properties of PDS for computing coreach. These properties justify the choice of PDS as the semantic model of our language, and the restriction to finitestate variables. Given a PDS For receptions, at location k r , after having checked the conformance, ¬cond co(k) is a sufficient condition to leave the prefixes of accepted traces (γ(¬cond co(k) ) ⊆ coreach(k)). So if it is satisfied we emit Inconc. For emissions, cond co(k) is a necessary condition to stay in prefixes of accepted traces (γ(cond co(k) ) ⊇ coreach(k)).

PI n1835

P = (G, Γ, c 0 , Λ, →), a set of configurations X ∈ ℘(G × Γ * ) = G → ℘(Γ * )
The obtained program is a sound test case, satisfying conditions (1)-(3) of Def. 4. There is a strong similarity between this test selection algorithm and the test selection algorithm for symbolic infinite-state transition systems defined in [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF]. Here partial observation may prevent us to perform an optimal selection, but if we distinguish perfectly coreachable configurations, we have, despite the partial observation, an optimal selection. Indeed, in this case, the obtained program satisfies conditions (4)-( 5) of Def. 4. In [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF], it is the impossibility to compute the exact coreachability set, and the need to resort to an overapproximation.

Improving selection with reachability information. One can improve the selection algorithm using reachability information. Let reach denote the set of reachable configurations of the program P . At a point k, we can exploit the knowledge that the current configuration is anyway included in reach(k), and testing the inclusion in γ •α(reach(k)∩coreach (k)) instead of γ • α(coreach(k)). 1 The problematic case identified by Eqn 4) is not true for k = g 0e , thus the selection is optimal at this point. Fig. 8 depicts the test case obtained by this improved selection algorithm. It should be noted that the presence of the variable t helps to perform an accurate selection at location g 0 , because it allows to distinguish whether G() has been called from f 1 or from g 2 . If we remove this variable, which does not change the semantics of S w.r.t. the conformance relation, one could not select optimally the output a or b to send to the IUT.

Fig. 1 .ConstantFig. 2 .

 12 Fig. 1. Test selection on various models

Fig. 5 .

 5 Fig. 5. Canonical tester associated to the specification of Fig. 4

Fig. 3 .

 3 Fig. 3. Non-conformant IUT

Definition 4 (

 4 Soundness of test cases). The verdicts of a test case TC are sound w.r.t. S and TP whenever the following properties are satisfied: (1) Traces Fail (TC ) = Traces(TC ) ∩ (Traces(Can(S))): Fail is emitted iff TC observes an unspecified output after a trace of S; (2) Traces Pass (TC ) = Traces(TC )∩ATraces(S, TP ): Pass is emitted iff TC observes a trace of S accepted by TP ; (3) Traces Inconc (TC ) ⊆ RTraces(S, TP ): Inconc may be emitted only if the trace observed by

  ) of Def.4. Adding the Inconc verdict is done by observing that pref ≤ (ATraces(S, TP )) = pref ≤ (Traces Pass (P )) = Traces coreach(Pass) (P )

Fig. 9 .

 9 Fig. 9. Language Syntax

Fig. 10 .

 10 Fig. 10. Language Semantic domains

  -→ k e proc return ---→ . . . (g, (k , l ) • (e proc , l)) τ → (g, (k , l ))where the activation record is popped and the control goes back to the caller.-An emission instruction generates a rule k emit(p) when expr {k :block}

Fig. 11 . 7 .

 117 Fig. 11. Analysis of the program of Fig.7. The configurations are composed of the values of global variables (t, verdict , pc, p) and the stack (-means any value, and ω = K * ).As p is "active" only at observation points, its value is not precised elsewhere.

4 )

 4 (3) becomes γ • α(reach(k) ∩ coreach(k)) ∩ γ • α(reach(k) ∩ coreach(k)) = ∅ (It is clear that Eqn. (4) implies Eqn. (3) but that the converse if false. Coming back to our example, Fig. 11(b) gives the reachability set of P projected on observation points, and Fig. 11(c) the intersection reach(k) ∩ coreach(k) for these points. If cond co(k) (g, l) denotes now a formula characterizing α(reach(k) ∩ coreach(k)), we now have cond co(g0a) = (pc = B) ∧ (t ∧ p = b ∨ ¬t ∧ p = a) instead of just (pc = B). One can check that Eqn. (

  is regular if it associates to each global state a regular language. The first result is that the coreachability (resp. reachability) set of a PDS is regular if the final (resp. initial) when true{ if (not expr r ) { verdict = fail; abort() } kr : if not (cond co(kr ) ) { verdict = inconc; abort() } TP (p); block r } [] emit(p) when expr e andcond co(ke) {ke : TP (p); block r }

	˛receive(p) when true{	˛receive(p)
	if (not expr r )
	{ verdict = fail; abort() }
	kr :
	TP(p); block r	⇒
	}
	[]
	emit(p) when expr e
	{ke : TP(p); block e }
	PI n1835

As reachability and coreachability sets are regular, so is their intersection.PI n1835

This work was partly supported by France Telecom R&D, contract

This operation mimics the corresponding operation defined for LTS in Sect. 4. Here, it could be done on the PDS generated by the program, but we prefer to proceed directly by program transformations.

Test purpose. When performing test generations from LTS, the test purpose is an LTS that is taken into account by computing the product Can(S) × TP (c.f. Sect. 4). Now, Can(S) is a PDS. It is known that the product of two PDS is not a PDS, hence we cannot specify test purposes using PDS if we do not want to manipulate more expressive computational models. However, as the product of a PDS with an LTS is still a PDS, we can consider test purposes defined by finite LTS. We can compute the synchronous product of Can(S) with TP to add the Pass verdict to the canonical tester. However, our goal is to proceed by program transformations. This excludes to work directly on the underlying LTS and PDS models. The solution consists:

-in implementing the LTS TP (which should satisfy Def. 3) by a procedure TP(p) that takes as input the last exchanged message and implements the LTS, c.f. Figs. The call to TP is performed after having checked the conformance, because accepted traces are conformant. The procedure TP is in charge of emitting the Pass verdict. This transformed canonical tester will be denoted by P , which satisfies conditions (1)-(2) of Def. 4. Fig. 7 depicts the obtained program for our running example.

Test Selection on Recursive Canonical Tester

Test selection is based on the same principle as for LTS, c.f. Sect. 4. In particular we will exploit the identity pref ≤ (ATraces(S, TP )) = Traces coreach(Pass) (P ) to recognize (conformant) traces that may be accepted in the future by the test purpose.

Irisa

Constant, Jeannet & Jéron set of configurations is regular [START_REF] Caucal | On the regular structure of prefix rewriting[END_REF]. The second result is that in this case, the coreachability (resp. reachability) set is computable with polynomial complexity [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems[END_REF][START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model checking[END_REF]. The Moped tool implements efficient symbolic algorithms to compute these sets, using a model of symbolic PDS where the relation transition → is represented with BDDs [START_REF] Esparza | A BDD-based model checker for recursive programs[END_REF].

As the set Pass is regular, we can provide to Moped the PDS generated by our recursive program and the set Pass, and we obtain the regular set of coreachable configurations. Coming back to our running example, the table of Fig. 11(a) indicates, for every location, the configuration from which we can reach the final configuration (-, pass, E), ω . As there are no local variables in the example, the stacks contain only control points.

The problem of partial observation. The selection consists in adding tests in the program P , using coreachability information, for selecting the outputs to emit, and for detecting the inputs which makes P leaves the set of accepted traces. However, in an usual imperative language like ours, a program can only observe the top of the stack, whereas deciding whether the current configuration is coreachable or not may require the inspection of the full stack.

Let us define the observation function

extended to sets, and γ = α -1 the corresponding inverse function. (α, γ) forms a Galois connection. At some location k of the program, given a set of configurations X, and

))} its projection on location k, the program can only decide if the current valuation of variables (g, l) is included in α(X(c)). This means that in term of configurations, one can only test inclusionship in γ • α(X) ⊇ X. In particular one may be in a case with

where one cannot decide, using only the observable part of the configuration, whether the configuration is coreachable or not. For instance, in Fig. 11(a), in location g 0e , α(coreach(g 0e )) = (p ∈ {a, b} ∧ pc = B) and α(coreach(g 0e )) = tt.

Selection rules. Because of the partial obervation phenomenon, we have to be conservative in the selection. Let cond co(k) (g, l) be the logical characterization of α(coreach(k)). We transform the program P as follows:

Irisa Constant, Jeannet & Jéron

Concluding Remarks

We have not yet implemented the selection algorithm of Sect. 6. We need to extend the Moped tool for this purpose. Indeed, Moped acts as a model-checker returning a Boolean answer, possibly with a counter-example. For our application, we need to get the sets of configurations computed by Moped, to intersect reachability and coreachability sets, to project this intersection on the visible part, and to convert the result in terms of a programming language expression. This requires extensions of Moped.

It is interesting to note the similarity of the two combinations: partial observation and exact analysis w.r.t. full observation and approximated analysis. In case of partial observation, the observation function α we introduced acts exactly as an abstraction (approximation) function. This means that one could apply our method to general recursive programs, on which the analysis would be in general approximated. The non-optimality of the selection would then be a consequence of the combination of partial observation and inexact analysis. One gets the diagram of Fig. 1.

Alternative methods. Our selection method described in Sect. 6 is based on (i) an exact analysis computing full configurations (instead of just visible parts of configurations), and (ii) on pure program transformations. These two choices could be revised. Concerning (i), one could use a less precise, classical interprocedural analysis method, which could still be exact for the observable part of the stack (for instance using the Bebop tool [START_REF] Ball | Bebop: A symbolic model checker for boolean programs[END_REF]). However it would lead to a less precise selection scheme. In particular, intersecting the coreachabe set with reachable set would filter out less values. Concerning (ii), one could instrument the program so as to get more knowledge about the invisible part of the configuration. For instance, one could add a data-structure maintaining a stack of procedure return points, and using it when testing if one is still in a coreachable configuration. Although the resulting test case could not be any more transformed into a PDS, the analysis would still be performed on the same intermediate program P as in Sect. 6. Test case execution would be however slower, as testing for coreachability would involve more complex datatypes.


P Sévillano
email: sevillano@celia.u-bordeaux1.fr

G Machinet

R Dubrasquet

P Camy

J.-L Doualan

R Moncorgé

P Georges

F Druon

D Descamps

E Cormier

Sub-50 fs, Kerr-lens mode-locked Yb:CaF 2 laser oscillator delivering up to 2.7 W

By means of a high-brightness optical pumping scheme with a fiber laser, we demonstrate Kerr-lens mode locking (KLM) with an Yb:CaF 2 laser crystal. Stable 48 fs pulses are produced at an average power of 2.7 W.

Introduction

Calcium fluoride has raised a great interest in the laser community since its revival in 2004 when it has been doped with ytterbium ions. Indeed, since its first laser operation in 2004 [1,2], Yb:CaF 2 have been among the most studied crystals for the development of high power, short-pulsed solid state lasers. Thanks to its broad emission bandwidth, its good thermal properties and its strong energy-storage ability, Yb:CaF 2 is particularly suitable for high-energy, high-power femtosecond laser systems [2,3]. Nevertheless, development of ultra-short pulsed oscillators with Yb:CaF 2 has revealed certain exertion. In fact, due to the very long lifetime of Yb:CaF 2 (τ =2.4 ms) and its low nonlinear refractive index (1.6 10 -20 m 2 /W), the stable sub-100-fs mode-locking operation (ML) of Yb:CaF 2 remains challenging and very few works have reported operation in this regime [4]. Up to now, the ML of Yb:CaF 2 oscillators has only been achieved using a saturable absorber mirror to produce stable femtosecond pulses. In this paper we report, to the best of our knowledge, on the first demonstration of a high average power sub-50 fs pulses Kerr Lens Modelocked oscillator in Yb:CaF 2 by means of a high-brightness pump source [5].

Experimental setup

The laser cavity and pumping geometry is sketched in figure 1. We use a 6-mm-long, 4 x 4 mm² Brewsterangle cut 4.5 at % Yb:CaF 2 crystal mounted in a water-cooled copper holder. The Yb:CaF 2 crystal is positioned between two R = 100 mm spherical mirrors (M 1 , M 2 ) in a standard X-fold cavity configuration. To compensate the astigmatism due to the Brewster-angle incidence, these mirrors are tilted with an angle of 8°. On one side, the cavity is delimited by a high reflection (HR) mirror (M 5 ) where a pair of SF10 60° prisms (P 1 , P 2 ) is inserted as an intracavity dispersion control. The cavity is closed on the other side by a 20% output-coupler (M 4 ). The mirrors of the cavity are specified to introduce a low group-velocity dispersion (GVD). The cavity is nearly symmetric and its length of 2.05 m corresponds to a repetition rate close to 73 MHz. The Yb:CaF 2 crystal is longitudinally pumped by a high-brightness fiber pump source through the M 1 dichroïc mirror (HT for wavelength below 980 nm and HR above 1020 nm). The pump source (ALS-IR 15W model) consists in an Yb-doped fiber laser emitting up to 12 W of linearly polarized radiation at 979 nm with a spectral bandwidth of 200 pm and is characterized by a high spatial quality with a M² of 1.1. The pump radiation is focused into the Yb:CaF 2 crystal by a 60 mm focal-length lens. The high spatial quality of the pump beam allows us to obtain a spot radius at the focal plane of 20 µm (at 1/e²) leading to a confocal parameter equal to 2.3 mm and a maximum pump intensity of 1 MW/cm 2 . Hence, the absorption of the Yb:CaF 2 is saturated when the pump focus is positioned in the middle of the crystal leading to an unabsorbed power of 8 W. Under this pump intensity and without lasing effect, the inverted population on-axis is estimated to be 48 %.

Results and discussion

At first, we characterize the CW performance of the high-brightness fiber-pumped Yb:CaF 2 oscillator. At 12 W of incident pump power, a maximum output power of 3.7 W is obtained at the central wavelength of 1046 nm. In this configuration, the unabsorbed pump power measured after the dichroïc mirror M 3 is 4 W leading to an opticalto-optical efficiency of 31 %.The laser threshold has been measured to be 950 mW with a 20% output coupler. It only correponds to the losses introduced by the coupler. Moreover, even if the pump intensity is very strong into the cristal, a weak thermal birefringence has been measured (Prisms losses ~ 100 mW and Brewster Yb:CaF 2 losses ~ 20 mW). Since the pump source used in this setup is characterized by a low M 2 value, a very good spatial overlap between the laser beam waist and the gain channel is achieved over the 6 mm crystal length and leads to a high optical-to-optical efficiency [6].

In order to discriminate the CW and ML regimes in the oscillator, we adjust the M 2 curved mirror position a configuration where the CW regime is less stable. The CW output power drops down to 2.2 W. Then a stable Kerrlens mode-locking is initiated by simply translating the prism P 2 . In a daily operation, when the KLM starts, a small fraction of the power remains in the CW regime however suppressed with a small displacement of the prism P 1 . In an optimal configuration (3 mm of P 2 is inserted in the beam path), the oscillator delivers 60 fs (FWHM) at the 73 MHz repetition rate with an average power of 2.73 W. We estimate the GDD introduced by the prisms to be -2600 fs 2 . The spectrum of the femtosecond pulses is centered at 1046 nm with a 28 nm bandwidth (see figure 2.a) and corresponds to a Fourier-Transform limited duration of 47 fs (FWHM). Indeed, the temporal pulse profile from the oscillator has been characterized through a SHG-FROG device and a quadratic phase has been measured and compensated by an external compressor requiring 6 bounces on -100 fs² chirped mirror (global transmission of 99.2%). Figure 2.b shows the retrieved pulse characteristics at the external compressor output from SHG FROG measurement. A 48 fs pulse duration (FWHM) has been retrieved in close agreement with the independently measured autocorrelation width of 73 fs. At the external compressor output, the time-bandwidth product of the pulses reaches 0.36. These parameters correspond to a peak power of 770 kW. In addition, we have investigated the influence of the pump power level on the stability of the KLM regime. We have recorded the output power and the compressed pulse duration at different pump powers. Results are displayed in figure 3. The best performances (pulse duration and output power) are obtained for the maximal pump power of 12 W but the KLM regime persists with a pump power down to 7 W. As pump power decreases, the spectral broadening from self-phase modulation in Yb:CaF 2 becomes less efficient and leads to longer pulse durations. However the Kerr-lens effect is efficient enough to discriminate ML and CW until 7 W of pump power. In this pumping condition, the oscillator delivers at least 1.6 W of average power with 65 fs pulse duration. Below 7 W of pump power, a continuous peak appears in the spectrum of the output pulses. In conclusion, we have presented the first experimental demonstration of a high-average power pure KLM femtosecond oscillator based on an Yb:CaF 2 crystal optically pumped by a very high-brightness fiber pump laser. The oscillator delivers, at 73 MHz repetition rate, pulses of 48 fs duration which is the shortest pulse duration ever obtained in Yb doped material at 2.7 W average power level.

Figure 1 :

 1 Figure 1 : Experimental setup

Figure 2 :

 2 Figure 2 : a) Experimental spectrum, b) SHG FROG retrieved temporal pulse profile

Figure 3 :

 3 Figure 3 : Performances of the ML Yb:CaF 2 oscillator as a function of the pump power.

Aknowledgement

We acknowledge the support from the Direction Générale de l'Armement et de la Recherche, the European Community through the I3 LASERLAB II JRA2 Happie, the Conseil Régional d'Aquitaine with the "Lougre Brillant" program, Aquitaine Valorisation, the CNRS national networks FEMTO and CMDO+ through the entitled HABRY program, and the Agence Nationale de la Recherche (ANR) through the FEMTOCRYBLE (ANR 2010 BLANC 0421) and PAMPERO (ANR-12-B509-0033) projects.


Laboratoire

Maxime Meilland

Andrew I Comport

SIMULTANEOUS SUPER-RESOLUTION, TRACKING AND MAPPING

Keywords: super-resolution, SLAM visuel, localisation, cartographie, suivi 3D super-resolution, visual SLAM, localisation, mapping, 3D tracking 1 Simultaneous super-resolution, tracking and mapping

Cet article propose une technique nouvelle de SLAM visuel qui intègre non seulement le pose en 6ddl et la structure 3D de façon dense, mais il intègre simultanément les informations de couleur contenues dans les images au fil du temps. Il s'agit de développer un modèle inverse pour la création d'une carte de super-résolution à partir de plusieurs images à basse résolution. Contrairement aux techniques classiques de super-résolution, notre approche tient pleinement compte de la translation et rotation 3D dans une formalisme de localisation et cartographie dense. Cela permet non seulement de prendre en compte toute la gamme des déformations de l'image, mais permet également de proposer des critères nouveaux pour combiner les images à faible résolution ainsi que sur la base de la différence de résolution entre les images différentes dans l'espace 6D. Plusieurs résultats sont donnés montrant que cette technique fonctionne en temps réel (30 Hz) et est capable de cartographier les environnements à grande échelle en haute résolution tout en améliorant la précision et la robustesse du suivi.

I. INTRODUCTION

The problem of dense real-time localisation and mapping within complex environments is a challenging problem for a wide range of applications ranging from robotics to augmented reality. In this paper the aim is to be able to interact in realtime with the surfaces of the environment so dense approaches are necessary. This work is undertaken as part of a French DGA Rapid project named Fraudo which requires dense localisation and mapping in real-time so as to allow path planning for a mobile robot to traverse uneven ground and surfaces autonomously. Another objective is to allow remote observation of the complex scenes for the operator. The goal is therefore to develop an efficient, accurate and robust dense visual models for localisation and mapping. As in all SLAM problems, in order to estimate the unknown maps using a moving sensor, it is necessary to simultaneously estimate the pose of the sensor.

The objectives here require real-time computational efficiency so several bodies of literature are not considered in this short review but are noted to have some overlapping approaches. In particular, the large volume of literature associated with off-line techniques such as Structure From Motion (SFM) and video post-production techniques [START_REF] Seitz | A comparison and evaluation of multi-view stereo reconstruction algorithms[END_REF], [START_REF] Renaud | Modelling dynamic scenes by registering multi-view image sequences[END_REF], [START_REF] Merrell | Real-time visibility-based fusion of depth maps[END_REF], [START_REF] Furukawa | Accurate, dense, and robust multiview stereopsis[END_REF] have similar problems but perform lengthy calculations using all the data simultaneously. 3D volumetric approaches from the computer graphics literature are also very relevant [START_REF] Curless | A volumetric method for building complex models from range images[END_REF]. Equally, we focus on approaches which look at full 6D transformations including rotation and translation since we consider this to be essential. Even so there are many interesting works which have looked at dense approaches in 2D including optic flow [START_REF] Baker | Super resolution optical flow[END_REF] or piecewise dense models such as affine [START_REF] Hager | Efficient region tracking with parametric models of geometry and illumination[END_REF] or planar geometry [START_REF] Silveira | Unified direct visual tracking of rigid and deformable surfaces under generic illumination changes in grayscale and color images[END_REF]. Some real-time stereo algorithms have also been around for quite some time [START_REF] Yang | Multi-resolution real-time stereo on commodity graphics hardware[END_REF], however, only stereo matching is performed and full poses are not estimated.

In the past ten years a lot of work has been carried out to perform robust real-time 6D localisation and mapping. In particular we can note that most visual SLAM approaches have used feature-based techniques combined with depth and pose estimation [START_REF] Nistér | Visual odometry[END_REF], [START_REF] Davison | Simultaneous localisation and mapbuilding using active vision[END_REF], [START_REF] Chiuso | Structure from motion causally integrated over time[END_REF], [START_REF] Mouragnon | Real time localization and 3d reconstruction[END_REF]. Unfortunately these approaches are still based on an error prone feature extraction step and are not suited to interact with surfaces since they only provide a sparse set of information and do not provide any information about the dense structure of the surface. Amongst the various RGB-D systems, feature based methods include [START_REF] Henry | Rgb-d mapping: Using depth cameras for dense 3d modeling of indoor environments[END_REF], [START_REF] Engelhard | Real-time 3d visual slam with a hand-held rgb-d camera[END_REF], [START_REF] Sturm | 3d pose estimation, tracking and model learning of articulated objects from dense depth video using projected texture stereo[END_REF]. All of these methods rely on an intermediary estimation processes based on detection thresholds. This feature extraction process is often badly conditioned, noisy and not robust therefore relying on higher level robust estimation techniques. Furthermore, it is necessary to match these features between images over time which is another source of error (feature mapping is not necessarily one-toone).

More recently, dense techniques have started to become popular and several groups have demonstrated real-time performance with commodity hardware. In particular, an early work performing dense 6D SLAM in real-time over large distances [START_REF] Comport | Accurate quadrifocal tracking for robust 3d visual odometry[END_REF] was based on minimising an intensity in image key-frames. Other photometric approaches include [START_REF] Meilland | A spherical robot-centered representation for urban navigation[END_REF] which looks at fully dense omnidirectional spherical RGB-D sensors. Alternatively, other approaches have focused only on geometry [START_REF] Zach | A globally optimal algorithm for robust tv-l1 range image integration[END_REF], [START_REF] Newcombe | Live dense reconstruction with a single moving camera[END_REF]. In the later truncated signed distance functions (TSDF) are used to define depth integration in a volumetric space and a classic Iterative Closest Point (ICP) is used to estimate the pose. Recent contributions have included using a moving TSDF with ICP [START_REF] Whelan | Kintinuous: Spatially extended KinectFusion[END_REF]. Uniquely geometric approaches are also common to time-of-flight range sensors [START_REF] Schuon | Lidarboost: Depth superresolution for tof 3d shape scanning[END_REF]. Unfortunately the techniques described here either limit themselves to photometric optimisation in the former case and in the later only geometric information is used. Neglecting one or the other means that important characteristics are overlooked in terms of robustness, efficiency and precision. It can be noted, however, that in [START_REF] Steinbruecker | Real-time visual odometry from dense rgb-d images[END_REF], a benchmark test was used to compare both approaches and it was shown that the photometric approach is more precise.

Few techniques have considered optimising an error on both intensity and depth images. In [START_REF] Tykkala | Direct iterative closest point for real-time visual odometry[END_REF] a direct ICP technique was proposed which does this simultaneously using an image-based approach. Alternatively, in [START_REF] Damen | Egocentric real-time workspace monitoring using an rgb-d camera[END_REF] both errors were minimised but using a volumetric approach based on Octomap. There are several arguments for and against each approach. In the image based case the resolution of the map is a function of the path taken to acquire it, whereas the volumetric approach is invariant to the path used. In that way the volumetric approach is unable to easily capture the nonlinear variation of the image resolution which depends on a particular camera trajectory. More importantly, it should be noted that none of these techniques have tried to "integrate the photometric intensity information", i.e. only pose and depth parameters have been estimated.

To investigate models to integrate the image intensity function we turn to super-resolution (SR) approaches. In this field a great amount of research has been carried out in the past, however, this has mainly been focused on applications such as photography or surveillance so as to obtain better 2D images. More particularly, super-resolution is the art of reconstructing higher resolution images, from a set of lower resolution images. In the most general case, these images are captured from different viewpoints, under different lighting conditions and with sensors of varying resolutions. See Figure 1 (a) for an overview of the image degradation pipeline reconstruction pipeline. Since the paper of [START_REF] Huang | Multiple frame image restoration and registration[END_REF], super resolution has been extensively studied in the computer vision community, however, most of the research only considers small relative motion between the input images and the major contributions are focused on how to fuse the registered images [START_REF] Baker | Limits on super-resolution and how to break them[END_REF], [START_REF] Bascle | Motion deblurring and superresolution from an image sequence[END_REF], [START_REF] Baker | Super resolution optical flow[END_REF]. Furthermore, the registration techniques are mainly 2D and do not take into account knowledge about the dense depth maps of the scene. Several tutorials of these approaches are available which give basic underlying models and principles [START_REF] Capel | Computer vision applied to super resolution[END_REF], [START_REF] Park | Super-resolution image reconstruction: a technical overview[END_REF] and more recent approaches aim at extending them such as [START_REF] Su | Spatially adaptive block-based super-resolution[END_REF] who perform spatially adaptive block-based superresolution.

In this paper we propose an approach to not only simultaneously estimate the 6D pose along with the dense depth map but also the photometric images in a super-resolution format. This is achieved by considering an inverse compositional approach which is efficient for real-time performance since it allows a maximum of pre-computations to be performed. This differs from the classic super-resolution pipeline as is shown in Figure 1. In the model proposed here, dense tracking is used to align the images in 6D while several low resolution images are combined together and integrated to form the highresolution image (SR). The low resolution (LR) images are combined by minimising their distance to a "virtual image" which is translated and rotated in such a way that it has the same resolution as the high-resolution image. In this way low resolution images are considered better if they are closer to the the same resolution as the target images.

The remainder of the paper is set out as follows. In

Section II an overview is first given for the super-resolution process. In Section III the dense SLAM algorithm is defined.

In Section IV-B a simulator is used to obtain a ground truth and evaluate the approach. In Section IV-C real-time images are used to perform super-resolution.

II. OBSERVATION MODEL

Consider a RGB-D sensor with a color brightness function I(p, t) and a depth function D(p, t), where p = (u, v) are pixel locations within the image acquired at time t. It is convenient to consider the set of measurements in vector form such that I ∈ R nm and D ∈ R nm . Consider now a RGB-D image, denoted also an augmented image [START_REF] Meilland | A spherical robot-centered representation for urban navigation[END_REF], to be the set containing both brightness and depth I = {I, D}. v = {p, D} ∈ R 3×n are then the 3D vertices of the surface associated with the image points p and the depth image. I will be called the current image and I * the reference image. A superscript * will be used throughout to designate the reference view variables. Now consider a set of low resolution augmented images {I 1 , I 2 , . . . , I N }, which observe the same scene from different 3D poses, the super-resolution process consists in simultaneously registering and fusing the images onto an augmented super-resolved image I * sr such that:

   I * sr = f N i C I i I i w T i , v i ; K, S + η, B -1 D * sr = f N i C D i D i w T i , v i ; K, S + η, B -1
(1) where the matrices T = ( R, t) ∈ SE(3) are the true poses of the RGB-D cameras relative to the reference position. Throughout, R ∈ SO(3) a rotation matrix and t ∈ R(3) the translation vector. The matrix S ∈ R 3×3 is the up-sampling matrix, K ∈ R 3×3 is the intrisic matrix of the real camera, C ∈ Rnm × nm is the combination matrix and B is the blur or inverse blur of a given radius. These variables and the warping function will be now explained in detail.

Note that in practice affine illumination parameters are also estimated as in [START_REF] Capel | Computer vision applied to super resolution[END_REF]: I ′ = αI + β along with vignetting parameters but to improve the clarity of the equations we omit this part of the pipeline.

1) Geometric warping: Consider the Figure 1 which shows the processing pipeline. From the first processing block, the motion model w(T i , v i ; K) is a 3D warping function, which is related to the 3D pose T of the camera and to the scene vertices v:

p w = K(Rv + t) e T 3 K(Rv + t) , (2)
where e 3 is a unit vector with the third component equal to 1.

2) Image up-sampling : The next block in Figure 1 involves the up-sampling of the LR image to the SR image. Usually this is done by creating intensity values at sub-pixel increments, however, for ease of notation and programming, here we consider the SR image pixels to be smaller than the LR pixels by a scaling factor s. This consists in warping the reference low resolution image by a diagonal homography scaling matrix

S =   1 0 0 0 1 0 0 0 s -1   , ( 3
)
where s is the desired scale factor. Note, however, that this means that we must transform between SR pixel units and LR pixel units in the equations.

A pixel in the SR image is then obtained from the LR image by performing a homographic warping as:

p sr = Sp lr e T 3 Sp lr , (4)
where p lr are the corresponding low-resolution pixels in normalized coordinates. The equivalent intensity and depth upsampling are done via warping as in [START_REF] Curless | A volumetric method for building complex models from range images[END_REF] given further.

3) Intensity and depth warping: The super-resolution image I * sr and depth-map D * sr of dimensions sm × sn are finally obtained by warping the corresponding low resolution images such that

I * sr = I * lr w S -1 , p w D * sr = D * lr w S -1 , p w (5)
where p w are the geometrically warped pixels from (2). The corresponding warped intensities are obtained by interpolation (nearest-neighbour, bi-linear or bi-cubic). In practice the depth warping function is optimised and computed differently as in [START_REF] Tykkala | Direct iterative closest point for real-time visual odometry[END_REF] and bi-linear interpolation is used. 4) Blur: The function f (I w , B -1 ), is a filter which performs image deconvolution. This will be assumed to be a post-processing step of the reconstructed SR image, that can be achieved using for example a Wiener filter [START_REF] Gonzalez | Digital Image Processing[END_REF].

5) Combination matrix:

The matrices C I i and C D i are normalized diagonal "combination" matrices ( N i C i = I) that allow to correctly combine the input depth-map and images into a consistent high resolution one. This will be shown to minimise the difference in image resolution and will be detailed in the next Section.

A. Image resolution distance function

One of the main contributions of this paper is based on how the low resolution images are combined to form a high-resolution image. Classic techniques mainly average the aligned images using a smoothing point-spread function. This naive approach has the effect of simply considering the combination matrices to be C I = I. Clearly, this results in a simple average of the input warped images. This often yields a blurred reconstruction since the images taken with a highly different resolution than the SR image and treated the same as those which contain as much detail as those taken by the SR camera. In reality though, the images undergo full 3D transformation and non-linear light field sampling effects are hard to model. To solve this, the aim is to define a distance function with allows to minimise the effective resolution of the LR image with the SR image.

The following will show that a LR camera can undergo a 3D transformation with respect to the SR image such that it sees the same effective light rays in space (i.e. the same resolution). This also means that we can compute an "optimal virtual image" with the same resolution as the LR image such that it intersects the same viewing cones as the SR image. This can be seen intuitively as moving the camera toward the scene so that it sees an effective higher resolution (even if it does not cover the same total area as the SR camera).

To better understand, consider the Figure 2. The SR image is defined by the frame T. The current LR image which must be used to generate a part of the SR image is defined in Frame T c . Both the LR and SR images observe a vertex v ∈ R 3 of the scene. The light reflected of the surface at v forms cones in space that are projected onto the SR and LR images respectively. Now consider moving a virtual camera defined by the frame T o and with the same resolution as the LR image. This camera can move in 3D via its homogeneous transformation matrix

T o = (R o , t o ).
The first goal is to determine the position in 3D space of the virtual camera such that it has the same effective resolution as the SR image. For each viewing cone, this is equivalent to minimising the area between the SR image's pixel size and the intersection between the virtual image plane and the cone. This area is minimised by computing the following equality:

S -R o -d -1 t o n T = 0, ( 6
)
where S is the scaling homography defined in Section II-2 and the right hand side is the parametrised homography describing the equivalent transformation in 3D. The viewing cone intersects the 3D surface at vertex v with a certain radius. This forms a plane with the surface with the normal n, and n T n = 1. This normal is known from the dense 3D map, and is obtained by a local cross product on the image grid. t o is the translation vector of the virtual camera and d is the distance between the camera centre of projection and the plane:

d = |n T v * |. (7)
To reduce the number of solutions we first set R o = I and solve (6) for the translation vector as:

t o = d(I -S)n. ( 8
)
Since the scale is invariant to rotations around the Z axis, only the other two axes need to be set. In practice, the rotation is set such that the optical axis of the virtual camera is in the direction of the viewing ray of each pixel. This has the effect of ensuring that we minimise the distance in both translation and rotation between the virtual image and the LR image. This also means that the virtual camera is centred on each pixel in the image which helps avoid optical lens distortion effects and (see Figure 2). This matrix can be computed by

   r oz = v * v * , r ox = r y ∧ r oz , r oy = r oz ∧ r ox . (9)
Note that the computation of the virtual camera for each pixel and subsequently its distance, is not computationally expensive.

Following the definition of the optimal pose, it is now possible to define the error metric between the LR pixel and the ideal LR pixel. This transforms directly into a weighting coefficient for each vertex v * and each LR pixel intensity, both defined with respect to the current estimated pose T c :

C I (v * ) = (T c -T o )v * + ǫ -1 , ( 10
)
where ǫ is a noise constant and v * is the homogeneous vertex coordinates. It can be seen from this error that it constrains the 5 degrees of freedom (i.e. not the rotation around Z). Also if the current image (LR) moves towards the optimal resolution then the error is zero whilst as it moves away the error increases. The scale factor which combines the rotational and translation components is determined by the vertex v * on the surface.

B. Depth weighting coefficients

For the depth weighting, a theoretical random error model proposed by [START_REF] Khoshelham | Accuracy and resolution of kinect depth data for indoor mapping applications[END_REF] can be used. The depth weighting coefficient is then

C D = f b mσ d diag(D) -2 (11)
where m is a constant, f is the focal length of the camera, b is the baseline and σ d is the disparity standard deviation.

III. SUPER-RESOLUTION VISUAL SLAM A. Cost function

The super-resolution visual SLAM problem is defined here to be that which estimates, incrementally, the set of camera poses T i (x i ) whilst simultaneously estimating the superresolved depth image D * sr and the super-resolved intensity measurements I * sr a set of low resolution images. This is achieved by considering the following photometric and depth errors:

e I = N i C I i I * sr -I i w T i T(x i ), D i , p, S , (12)
e D = N i C D i D * sr -D i w T i Tx i , D i , p, S . (13)
where it is supposed that for each pose there exists an incremental pose that combines homogeneously with the global pose to give the true transformation: ∃x i : T i T(x i ) = T i . The full state vector representing the variables is then

[I * sr , D * sr , x 1 , . . . , x N ] . (14)
Non-linear optimization of this error can then be decomposed via marginalization into three separate non-linear minimization phases which are performed iteratively for each low resolution input image: i.e. pose estimation, depth estimation and intensity estimation. This is the optimal formulation for the joint problem assuming that the initial super-resolution depth and intensities measurements are locally close to the solution.

B. 3D image registration and tracking

For each current image, the unknown motion parameters x ∈ R 6 are defined as:

x = 1 0 (ω, υ)dt ∈ se(3), (15)
which is the integral of a constant velocity twist which produces a pose T. The pose and the twist are related via the exponential map as T = e [x]∧ with the operator [.] ∧ as:

[x] ∧ = [ω] × υ 0 0 ,
where [.] × represents the skew symmetric matrix operator. Thus the pose cost function is then obtained by simultaneously minimising the errors of equation ( 12) and ( 13) in a robust least square procedure

C(x) = λ 2 I e I T W I e I + λ 2 D e D T W D e D , (16)
where λ (.) are weighting scalar gains and where W (.) are diagonal weighting matrices obtained by M-estimation [START_REF] Huber | Robust Statistics[END_REF]. The unknown x is then iteratively estimated using

x = -(J T WJ) -1 J T W e I e D T T ← TT(x), (17)
where J contains the stacked Jacobian matrices of the errors and W contains the stacked weighting matrices. More details on such a minimisation can be found in [START_REF] Tykkala | Direct iterative closest point for real-time visual odometry[END_REF].

Minimising both errors provides a lot of advantages since photometric and depth informations are complementary. First the depth error term usually offers a larger domain of convergence and a fast minimisation. It also allows to track textureless areas, but it is sensitive to noise and not efficient with symmetric objects or with unconstrained scenes. On the other hand, the photometric term allows to track any textured areas with a better precision [START_REF] Steinbruecker | Real-time visual odometry from dense rgb-d images[END_REF].

C. Super-resolution

Since the matrices C I i are diagonal, minimising equation [START_REF] Chiuso | Structure from motion causally integrated over time[END_REF] with respect to the photometric parameter I * sr can be done incrementally as new low resolution images I(t) are registered and warped onto the super-resolved frame, leading to the following update rule

C I sr (t) ← C I sr (t-
where C I sr (t -1) is the global intensity cost at time t -1 and I w (t) is the current image, warped from the registration process of Section III-B.

IV. EXPERIMENTS

A. Real-time implementation

A real-time implementation of the super resolution tracking and mapping algorithm has been made on GPU using the OpenCL library. The algorithm runs at 30 Hz with low resolution input images of size 640 × 480 pixels and a 4× super-resolution factor on a Nvidia GTX 670 card. For the pose estimation minimisation, a coarse to fine multi-resolution approach is employed. The minimisation begins at the lower resolution, and the result is used to initialize the next level repeatedly until the higher resolution is reached. In this way, larger displacements are minimised at low cost on smaller images. Since the RGB-D sensor usually provides noisy depth measurements, a bilateral filtered is applied to remove noise whilst preserving discontinuities. The filtered depth-map is only used for pose estimation, whilst the raw depth-map D is used for depth integration, in order to preserve details in the integration process.

B. Simulated results

The algorithm has been tested on a synthetic sequence of images with ground truth poses, generated from the sponza atrium model [START_REF] Dabrovic | Sponza atrium model[END_REF]. The sequence is a 30 meters corridor with textured surfaces. The input images were downscaled to an input resolution of 160 × 120 pixels. The reference image is taken at the beginning of the sequence and then the camera moves along the corridor. Two experiments were conducted: first a simple tracking is applied to each current image without using super-resolution integration. Then the same sequence is tracked with super-resolution integration, with a scale factor s = 4. For both methods, we set the gain which controls the depth error λ D = 0, in order to only compare the influence of the photometric integration in the tracking process. The plot reported on Figure 3 shows the absolute translation error with respect to the distance to the reference frame for both approaches. It can be seen that the super-resolution approach clearly improves the localisation error, by integrating new information as the camera moves along the trajectory.

C. Experimental results

The visual SLAM algorithm has been successfully tested on a number of real scenes. The images of Figure 4 reports the results of an experiment performed in an office containing a desk, with different objects and books. The RGB-D camera used for this experiment is an Asus Xtion Pro Live, capturing low resolution images of 640×480 pixels at 30Hz. The superresolution SLAM is performed in real-time with a scale factor s = 4. The original reference image is shown on Figure 4(c). The camera was then moved around the desk with different motions. The image of Figure 4(d) shows the photometric image obtained at the end of the sequence. The Figures 4(e) and 4(f) show a region of interest. We can visually see that the super-resolved image is highly detailed compared to the original one. The Figures 4(a) and 4(b) show the Phong shaded surfaces computed from the depth-maps and the surfaces normals. We can see that compared to the original depth-map, the super-resolved depth-map is much more detailed and less noisy. Other aspects of our visual SLAM method, such as the ability to track during very rapid motion, or its robustness to camera occlusions are illustrated in our submitted video 1 .

V. CONCLUSION

In conclusion, this paper has proposed a new visual SLAM technique which integrates 6DOF pose and dense structure simultaneously with the color information contained in the images over time. A novel inverse model has been provided for creating a super-resolution map from many low resolution images based on a 3D distance criteria which minimises the difference in resolution between the low resolution image in 3D and integrates the super-resolution image. Experimental results are given showing that this technique runs in real-time (30Hz) and is able to map large scale environments in highresolution whilst simultaneously improving the accuracy and robustness of the tracking.

Future research in this direction will be focused at using the resolution distance criteria proposed here to better choose the position of the key frames in space. It would also be interesting to use this approach to take into account illumination changes on the surface within a dynamic model.

Fig. 1 .

 1 photometric warping

Fig. 2 .

 2 Fig.2. Super-resolution camera poses. The optimal pose To projects the vertex v on the low resolution camera with the same resolution as the superresolved image.

Fig. 3 .

 3 Fig. 3. Absolute translation error with respect to the distance to the reference image. The super-resolution algorithm reduces the localisation error.

  (a) Original 3D surface with phong shading. (b) Super-resolved 3D surface with phong shading. (c) Original image. (d) Super-resolved image. (e) Original image, area of interest. (f) Super-resolved image, area of interest.

Fig. 4 .

 4 Fig. 4. On left column, the original LR augmented image of resolution 640 × 480 pixels. On the right column the SR augmented image with a resolution of 2560 × 1920 pixels. The first row shows a Phong shaded surface computed from the depth-map of the images. The second row is the photometric map of the images, and the last row is a zoom on an interesting area. It can be seen that the super-resolution SLAM algorithm greatly improves depth measurements as well as intensity measurements.

  1)+C I (t)

	I sr (t) ←	C I sr (t) sr (t-1)Isr(t-1)+C I (t)I w (t) C I	,


published or not. The documents may come   L'archive ouverte pluridisciplinaire

The "Math for Biology" c--book unit is produced by the French Community of Interest (CoI) gathering mathematics teachers, teacher educators, computer scientists and researchers in mathematics education. It proposes a sequence of activities within a biomathematics context aimed at enhancing CMT using a wide range of widgets useful in biology. Hany and El--Demerdash (2015) assert that biomathematics is a good educational medium context to enhance CMT. The c--book consists of four sections: The first is an introduction to biomathematics, its meaning and its study fields. In the second section, mathematics is used to model biological traits, leading to a reflection on magnitudes. Golden ratio is studied in the third section, its occurrences in nature, paintings, architecture and Fibonacci numbers. The c--book unit ends with the analysis of spiral images uploaded by students themselves, and allowing them to build their own artwork.

This c--book unit embeds many widgets that propose open--ended activities to train a high degree of CMT such as reflecting on models, modelling spirals and code tweaking in a half--baked logo microworld. In this poster, three examples of these widgets are presented.

[1] DGS widgets enabling students to upload their own spiral pictures and try out some formulae that fit them.

CADGME 2016

[2] The cross widget communication between Cinderella 1 and EpsilonWriter 2 (DAS) allows sending messages between the two software factories (a widget factory is a software system --often developed independently of the c--book environment over many years --allowing to produce sophisticated parameterizable c--book widgets easily. This widget sends the measurements from Cinderella widget to EpsilonWriter where users can write text and mathematical content, as well as doing calculations, in particular comparing the ratio of values.

[3] The digital golden ratio compass tool is a DGS widget enabling users to discover proportions seemingly like golden ratios in other context such as in insects, and in plants, artwork, etc. Users look for a picture of an object, upload it and check with the digital compass whether its dimensions satisfy the golden ratio.

Using these widgets, users have the opportunity to look for many different and varied examples of spirals to look for models and formulas. CMT is fostered mainly in the direction of fluency and elaboration because the students have to come up with many different trials that go deeper into refined details.

Digital Resources to Enhance Creative Mathematical Thinking in a Biomathematics Context

Introduction The Math for Biology c--book Unit Widget Instances and CMT Enhancement References Mohamed El--

Demerdash 1,2 , Nataly Essonnier 1 , Jana Trgalova 1 and Christian Mercat 1 1 S2HEP EA4148 Université Claude Bernard -Lyon 1, France, 2 Menoufia University, Egypt

	Promoting Creative Mathematical Thinking (CMT) to enable
	innovation is a central goal of European Union. CMT is a highly
	valued asset in industry and addresses current and future
	economic challenges. It is seen as an individual and collective
	construction of mathematical meanings, norms and uses in novel
	and useful ways, which can be of relevance to a larger (academic,
	learning, professional, or other) community. Exploratory and
	expressive digital media created by new designers are providing
	users with access to and potential for engagement with CMT in
	unprecedented ways.

A new kind of digital resource, a c--book unit ("c" for creative) designed within the MC Squared project (http://mc2--project.eu) is a digital book produced within a socio--technological environment called "C--book technology". It allows meshing narratives with interconnected interactive dynamic digital artefacts, called widgets, to promote students' CMT.

Hany, M., & El--Demerdash, M. (2015). The effectiveness of a proposed unit in Bio--Mathematics for developing secondary stage students' deep understanding skills --in Arabic. Egyptian Association for Science Education Journal, 18(5).1 http://www.cinderella.de 2 http://www.epsilonwriter.com