D Foures
email: dfoures@laas.fr

V Albert
email: valbert@laas.fr

A Nketsa

A New Specification-based Qualitative Metric for Simulation Model Validity

Keywords: Experimental Frame, Abstraction, Input/Output Automata, Compatibility

Informal validation techniques such as simulation are extensively used in the development of embedded systems. Formal approaches such as model-checking and testing are important means to carry out Verification and Validation (V&V) activities. Model-checking consists in exploring all possible behaviours of a model in order to perform a qualitative and quantitative analysis. However, this method remains of limited use as it runs into the problem of combinatorial explosion. Testing and model-checking do not take into account the context of use objectives of the model. Simulation overcomes these problems but it is not exhaustive. Submitted to simulation scenarios which are an operational formulation of the V&V activity considered, simulation consists in exploring a subset of the state space of the model. This paper proposes a formal approach to assess simulation scenarios. The formal specification of a model and the simulation scenarios applied to that model serve to compute the effective evolutions taken by the simulation. It is then possible to check whether a simulation fulfils its intended purpose. To illustrate this approach, the application study of an intelligent cruise controller is presented. The main contribution of this paper is that combining simulation objectives and formal methods leads to define a qualitative metric for a simulation evaluation without running a simulation.

Introduction

Context

In [START_REF] Frantz | A taxonomy of model abstraction techniques[END_REF] it is stated that a model abstraction is valid if it maintains the validity of the simulation results with respect to the questions the simulation is supposed to address. Hence, the validity of a model should never be assessed in isolation but should always be envisaged in relation to the context in which the model is experimented, i.e. the purpose of the simulation. Traditional Modeling and Simulation (M&S) practices describe abstraction choices when building up a model to provide documentation of its "domain of use" as suggested in [START_REF] Weld | Reasoning about model accuracy[END_REF][START_REF] Frantz | A taxonomy of model abstraction techniques[END_REF][START_REF] Albert | Simulation validity assessment[END_REF]. These practices do not follow the same process for the intended purpose of the simulation. However, simultaneously conducting the same process for the model and its context would make it possible to define a priori the sufficient and necessary model required to reach an intended purpose and to check a posteriori whether a model can be used in various contexts. Thus, challenging issues in M&S are mostly related to their specification/documentation, the capabilities of the model and the properties expected from this model to achieve the simulation purpose.

Framework

We retained the Theory of Modeling and Simulation (TMS) developed in [START_REF] Zeigler | Theory of Modeling and Simulation[END_REF]. Zeigler established a framework which provides a precise definition of the entities involved in the process of modeling and simulation. We consider this framework as an excellent base for structuring modeling and simulation applications. It highlights relationships between the intended purpose of the simulation, the system which is represented and the simulations themselves. TMS is not the only existing framework available to describe dynamic system modeling. It can be compared with other work which has been published concerning the community of Verification, Validation and Accreditation (VV&A) of simulations as in [START_REF] Sargent | Verification and validation of simulation models[END_REF][START_REF] Brade | Vv&a ii: enhancing modeling and simulation accreditation by structuring verification and validationresults[END_REF]. The experimental frame is one of the entities that have been introduced in the TMS to make a distinction between the model and the experiment. The experimental frame can be viewed as a system which interacts with the model in order to answer the questions raised by the simulation purpose. Then it consists in stimuli injected into the model inputs, observation of the model outputs and constraints to determine whether the model outputs "fit" some acceptance conditions. The experimental frame concept has been used for the simulation of embedded systems engineering in [START_REF] Schulz | Towards an application of model-based codesign: An autonomous, intelligent cruise controller[END_REF], for ecology systems in [START_REF] Traoré | Capturing the dual relationship between simulation models and their context[END_REF][START_REF] Bonte | Recursive simulation and experimental frame for multiscale simulation[END_REF] and for environmental processes in [START_REF] Kops | The process of model building and simulation of ill-defined systems: Application to wastewater treatment[END_REF]. In [START_REF] Traoré | Capturing the dual relationship between simulation models and their context[END_REF], Traoré and Muzy pioneered a formal definition of the experimental frame. Our approach relies on this definition. However, this definition does not allow formal verification of the behavioural compatibility analysis between an experimental frame and a model. Such an issue is of paramount importance in order to know whether a model within an experimental frame can address the questions raised by the simulation purpose. Our approach is modelbased. Therefore the experimental frame and the studied system are represented by their models. In this paper to avoid repeating the model word for both the system and the experimental frame, we are going to use a model for the system under test and experimental frame for its model.

Novel concept and its benefits

The novel concept relies on building a simulation model which specifies the model behaviour under the conditions of the experiment. This model is obtained by composition of the system model of interest and the model of the context within which that system is studied, i.e. its experimental frame. In a simulation-based development methodology, the intended purpose of the simulation would usually be to check that some requirements on the real system are met. The simulation model and the simulation intended purpose can then be input into a model checker for quantitative analysis. This idea is illustrated in Figure 1. Metrics ( 1) and ( 2) can be measured by composition of the system model of interest and the model of the experimental frame, and metric (3) can be measured by checking the simulation model against the specification of the system of interest.

Formal specification languages

TMS also offers a specification language for models called Discrete Event System Specification (DEVS) using precise operational semantics thanks to an abstract simulator which establishes formal rules for executing a DEVS model. It is important to highlight that TMS is based on a general system theory. In this way, many types of systems can be modeled within TMS. TMS has given rise to many subclasses such as Cell-DEVS for cellular automata, DTSS for discrete-time systems and DESS for differential equation systems. However, DEVS is not used here as it does not support model checking because the state space of a DEVS model is infinite. State space exploration techniques and qualitative properties analysis can be supported by Finite and Deterministic DEVS (FD-DEVS). However as far as we know, there are no tools supporting FD-DEVS models and temporal logic.

Automata are a subset of DEVS. Automata theory is suitable for state space exploration and quantitative properties analysis with temporal logic and it supports well the composition of automata. With Input/Output Automata (IOA) we capture the temporal I/O behaviour of the model and the experimental frame. By composition we check whether the automaton which describes the trajectory injected into the model inputs can be accepted by the automaton describing the model of the system of interest and whether this set provides a path of interest observed on the model outputs. In [START_REF] Lee | Behavioural types for component based design[END_REF], the authors use synchronous products of automata for composition. Behavioural incompatibility is detected if the product is zero. However this approach does not allow the cause of that incompatibility to be detected. Our synchronous product is based on the work of [START_REF] Alfaro | Interface automata[END_REF] which relies on an "optimistic" view of composition and offers the possibility to detect illegal states leading to possible incompatibility. Our composition adds another dimension, i.e. while two components can be synchronized and therefore compatible, we can highlight which part of the model is overlooked thanks to the synchonous product. Composition results in a new automaton which describes the behaviour of the simulation model which is checked against the requirements that the system under study must fulfil. The latter are described with Linear Temporal Logic (LTL) [START_REF] Filiot | An antichain algorithm for ltl realizability[END_REF] properties. An LTL formula is interpreted on infinite words which do not include time as a first-class variable. State space exploration with linear temporal logic based on automata theory can be solved using UPPAAL [START_REF] Behrmann | A tutorial on UPPAAL[END_REF]. Moreover, UPPAAL supports timed automata and event-clock automata specifications.

This paper is organized as follows. Section 2 gives an overview of related work. Section 3 includes a description of the M&S framework, experimental frame and IOA. Section 4 states the main contribution, defining a trace inclusion property with Input/Output automata. Section 5 describes steps and an algorithm to conduct compatibility checks. Section 6 introduces an example of use of this approach. Section 7 gives a conclusion and anticipates future work.

Related work

Combining simulation with formal methods has been extensively investigated. We present our contribution in this context.

In [START_REF] Cavaliere | Model Checking Satellite Operational Procedures[END_REF], a model checker is used to automatically drive the SIMSAT simulator to check operational plans. In contrast to the verification of operational plans, our proposed approach has a general scope, being applicable to simulation models of any system and a set of requirements to be verified.

In [START_REF] Mancini | System level formal verification via model checking driven simulation[END_REF] the authors use a model checker to generate all possible simulation scenarios and then optimise the simulation of such scenarios by exploiting the ability of simulators to save and restore visited states. Our approach is quite different because we have defined some metrics for evaluating simulation without running it.

In [START_REF] Dill | Formal verification meets simulation[END_REF], the authors make the following observations: functional errors are not eliminated by synthesis and not detected by a formal verification based on test equivalence. These errors result from incorrect specifications, a misinterpretation of specifications, etc. They highlight the limits of formal verification (equivalence checking, model checking, theorem proving) in the context of validation. They use a semi-formal approach, initially proposed by [START_REF] Tasiran | A functional validation technique: Biased random simulation guided by observabilitybased coverage[END_REF], based on the notion of metric coverage coupled with simulation. The objective is to achieve understandable validation without duplication of effort. The approach combines symbolic simulation, model-checking and the generation of test vectors based on coverage analysis to minimize unwanted portions of the system. The authors advocate the definition of metrics at different levels of abstraction: on the code, the system structure, its state space, functionality and specifications.

In [START_REF] Karlson | Validation of embedded systems using formal method aided simulation[END_REF], the authors propose model checking to guide the simulation process and improve coverage. Coverage metrics are measured during the validation session and model checking is invoked when coverage is insufficient to reach uncovered parts of the state space more quickly. Invoking model checking is dynamically controlled during run-time.

We positioned ourselves relative to these works by considering two key differences:

• In current practice simulation, runs are actually performed: in contrast, our approach aims to verify before simulation whether a simulation behaviour (i.e. model + experimental frame) can be used for the intended purpose of the simulation which is derived from requirements on the real system.

• Using formal methods, all possible simulation scenarios are exhaustively explored: our approach makes use of the intended purpose of the simulation to investigate only that part of the behaviour of the simulation (that portion of the state space) which is of interest for the intended purpose.

Framework for the preparation of models and simulations

TMS

In [START_REF] Zeigler | Theory of Modeling and Simulation[END_REF], a new way of providing a model description is proposed and the question of knowing whether this model is a true representation of the dynamic behaviour of the system from a given perspective is asked. The basic principle of the M&S process described by Zeigler involves the separation of the model and the simulator. The basic entities of the M&S process are the system, the model and the simulator (Figure 2).

The system is the real or virtual element used as a source of observable data and subject to modeling. The model, also called system substitute, is a representation of the system. It usually consists of a set of instructions, controls, equations or constraints designed to generate its behaviour. The simulator is a computer system executing the model and generating its behaviour based on model instructions and injected inputs. This set is reorganised to integrate the experimental frame (EF). The latter is a specification of the conditions under which a system can be observed or experimented. It is an operational formulation of the objectives which the development of the M&S application supports. There may be several experimental frames for the same system and the same experimental frame may be applied to several systems.

Figure 2. M&S process and its entities

It should be pointed out that the experimental frame transforms the objectives used to focus model development on a particular point of view, into specific experimental conditions. A model must be valid for a system in such an experimental frame. An operational formulation of the objectives is produced by matching the output variables with measurements of the system's effectiveness in accomplishing its function. These measurements are called outcome measures.

Modeling is the relationship between a model, a system and an experimental frame. The validity of a model is the basic concept of the modeling relationship.

Experimental frame

An experimental frame features three components as shown in Fig. 3: a generator, which generates a set of input segments for the system; an acceptor, which selects the data of interest to the system while monitoring whether the desired experimental conditions are complied with, and a transducer, which observes and analyses the output of the system. Mapping between output variables and outcome measures is carried out by the transducer.

An experimental frame is given in [START_REF] Traoré | Capturing the dual relationship between simulation models and their context[END_REF] as a structure where:

EF = 〈T, I M , I E , O M , O E , Ω M , Ω E , Ω C , SU〉 • T is a time base,
• IM is the set of Frame-to-Model input variables, the set of model stimulation ports,

• IE is the set of Frame input variables, the control input set,

• OM is the set of Model-to-Frame output variables, the set of model observation ports,

• OE is the set of Frame output variables, the summary set,

• Ω M ⊆ (IM, T) is the set of segments injected into the model inputs,

• Ω E ⊆ (IE, T) is the set of admissible input segments for the experiment,

• Ω C ⊆ (OM, T) the set of segments observed on the model outputs,

• SU is a set of conditions, also referred to as summary mappings, which establishes relationships between inputs and outputs within the frame.

Figure 3. The experimental frame and its components

Typical experimental frame components can be found in [START_REF] Zeigler | Theory of Modeling and Simulation[END_REF] in chapter 14. For example, typical generator functions are sine wave, square wave, step ramp, periodic arrivals.Typical acceptor functions are steady state, transient. Typical transducer functions are throughput, turnaround times, elapsed times, rates, averages.

It has been seen that the experimental frame features data gathering (statistics, performance measurements, etc.) and behavioural control (initialization, termination, transient state removal etc.). Again, an experimental frame can be seen as a system that interacts with the system or the model to obtain data of interest under certain conditions. Hence, defining boundaries between the experimental frame and the model is essential to clearly distinguish between what drives the model, what can be observed as output, and the model itself. This has been illustrated in [START_REF] Albert | Simulation validity assessment[END_REF].

Input/Output Automata

We use input/output automata (IOA) [START_REF] Hopcroft | Introduction to Automata Theory, Languages, and Computation, 2ndEdition[END_REF] to describe the dynamics of models at a quite abstract level that is independent from an encoding language. Definition 1 (IOA). It consists of the following structure: A = 〈D, X, Y, dom, S, σ, Σ, δ, s 0 〉 where • D is a set of data types (integer, real, string, etc.),

• X is a finite set of names representing the set of input variables,

• Y is a finite set of names representing the set of output variables,

• dom : X ∪ Y → D is the typing function which allocates a type of data to each variable,

• S is the set of states,

• σ : S → ((X ∪ Y) → dom(X ∪ Y)) is the configuration function, i.e.

mapping of values with

the typed input/output variables for each state.

• Σ is the set of event names. These names are the state transition labels. e is the set of nonobservable events.

• δ ⊆ S × Σ × S is the transition relation, a transition identifies a change to the inputs, the outputs or the states.

•s 0 ⊆ S is the set of possible initial states, the states in which the automaton can be if no inputs have yet been transformed.

X ∪Y ∪ Σ is the vocabulary used to define the automaton. For the sake of simplicity, we will assume that the names used in the vocabulary are unique.

Example. Let us consider a communication system with a shared memory which implements a FIFO (First In First Out) scheme, the behaviour of which is described by the reachability graph in Figure 4. In this example, a variable queue is defined to describe a sequence of messages. This variable is declared as a table of length 2. Each place of the buffer is set to 1 if there is a message, or 0 if not. This automaton has an initial state s0, where the sequence is empty (e.g. σ (s0) = (0, 0)). The set of state S is {(0,0), (0,1), (1,0), (1,1) }. These states are connected by transition relations. These transitions are labeled by the events recv and send which respectively add a message to the head of the sequence and remove a message from the sequence. ). An IOA run is a sequence (finite or not) σ (s 0 ) →l 0 … σ (s i ) →l i … where s i is a state (s 0 is an initial state) and l i is an event name such that any (s i →l i s i+1 ) of a run is a transition of the automaton. A run can also be defined by a path taken from the computation tree of an automaton. "Run" can also be called "trace".

Our contribution on verifying trace inclusion

Objective of trace inclusion

Ω IEF are the simulation results that the experimenter wishes to observe, whereas ΩOEF are the stimuli injected into the simulation. Similarly, ΩIM are allowable inputs of the model and ΩOM are the possible simulation results.

Definition 3 (EF-Model behavioural compatibility). We state that an experimental frame can be applicable to a model if their behaviours are compatible, i.e.:

Ω OEF ⊆ Ω IM Ω OM ⊆ Ω IEF
The next section introduces a formal way for using IOA in order to check EF-Model behavioural compatibility.

Behavioural compatibility

A Temporal Interfacing Constraint (TIC) is an execution property defined with respect to a given vocabulary (names of events and input/output variables).

The properties of invariants are constraints on the configuration function. For example, let us consider altitude as an input variable of the automaton's vocabulary. The constraint "variable altitude is positive or zero" is an example of an invariant. The automaton that satisfies this invariant includes an integer input variable called altitude and a configuration function σ such that, for any state s, σ(s)(altitude) ≤ 0.

The temporal properties are constraints which link the configuration and the transitions. There are two separate types of time-dependent properties:

• linear versus computation tree: refers to the constraints on all executions of the automaton versus those on the computation tree taken from the automaton,

• past versus future.

For example, consider the Boolean output variable alarm in the vocabulary of an automaton: "If the value of alarm is true in one state of the execution, then there is a previous state in the execution where altitude ≤ 10" is a linear time and past property. "If altitude ≤ 10 in one node of the computation tree of an automaton, then we should be able to find a path and a subsequent node in the path which satisfies alarm = true" is an example of a computation tree and future property. Definition 4 (Runs set satisfied by a TIC). Let TIC be a constraint expressed on the vocabulary V and let A be an automaton that generates all the runs that can be constructed with the vocabulary V. Then we note TIC A the set of runs of A which satisfies the TIC.

Let us define a set of restrictions to reduce the set of execution traces of the model to the set of execution traces required by the experimental frame.

Definition 5 (Restriction of an automaton).

The restriction of an automaton 〈D, X, Y, dom, S, σ, Σ, δ, s 0 〉 to a subset X' ∪ Y' ∪ Σ' of its vocabulary is an automaton 〈D, X', Y', dom, S, σ / X' ∪ Y', Σ', δ / Σ', s 0 〉 in which the restricted configurations and the restricted transitions are defined below.

Definition 6 (Restriction of a configuration). The restriction σ

/ X' ∪ Y' of a configuration σ : S → ((X ∪Y) → dom(X ∪Y)) restricted to a vocabulary X' ∪ Y' such that X' ∪ Y' ⊂ X ∪Y is the configuration σ' / X' ∪ Y') : S → ((X' ∪ Y') → dom(X' ∪Y')) such that σ / X' ∪ Y' (s)(v) = σ (s)(v) for all v ∈ X' ∪ Y'.
The restriction of a configuration keeps for each state the value of a subset of variables of interest and puts aside the values of all other variables. • for all e ∈ Σ', for all (s, s' ) ∈ S × S, if (s, e, s' ) ∈ δ then (s, e, s' ) ∈ δ / Σ',

• for all e ∈ Σ -Σ', for all (s, s' ) ∈ S × S, if (s, e, s' ) ∈ δ then (s, e, s' ) ∈ δ / Σ'.

The restriction of a transition relation keeps the structure of a transition relation unchanged, but identifies the names of a subset of events of interest and masks the other names with non-observable events e.

Definition 8 (Restriction of a run).

A run restricted to a vocabulary is the initial run in which the initial configuration function and the initial function relation are replaced by their respective restrictions.

Let us define an EF by a TIC on the vocabulary XEF ∪ YEF ∪ ΣEF. Also, define a model of a system of interest by a TIC on a vocabulary XM ∪YM ∪ ΣM.

Definition 9 (Compatibility of vocabularies).

The model and experimental frame can be connected if they have compatible vocabularies:

• XEF ⊆ YM: all the results of interest required by the experimental frame are supplied by the model and the model may supply more results than necessary.

• YEF = XM: all stimulations planned by the experimental frame can be performed and all inputs necessary to perform simulation are defined by the experimental frame. Particular attention must be paid to the case YEF ⊂ XM. It is assumed that EF and M can be connected. However, in that case it is necessary to make sure that there is no dependency between a non-assigned input of the model and an observed output. In that case the simulation results could be biased. Dependency between inputs/outputs of a component may be a specific condition which is beyond the scope of this paper.

• ΣEF ⊆ ΣM: all events of interest in the experimentation can be observed during simulation, but the latter produces more events.

For simplicity it is assumed that the names used to designate EF and M inputs/outputs are identical.

Compatibility of vocabularies is a prerequisite for using simulation with respect to an experimental frame. We will now clarify how to check the behavioural compatibility of an experimental frame with a model by comparing traces fulfilled by the corresponding TICs.

If we have EF and M, two TICs for the respective vocabularies VEF = XEF ∪ YEF ∪ ΣEF and VM = XM ∪ YM ∪ ΣM such that these vocabularies are compatible.

Definition 10 (Full compatibility). EF and M are fully compatible if all traces of M restricted to the vocabulary of EF are traces of EF:

M VM/VEF = EF VEF (case 1 in Figure 5).

Definition 11 (Relaxed compatibility). Exact matching not being required, this means that:

• M VM/VEF ⊆ EF VEF : the behaviours of the model are in the envelope of significant behaviours with respect to the EF (case 2 in Fig. 5).

• EF VEF ⊆ M VM/VEF : all experimentations planned by the EF can be performed on the model (case 3 in Fig. 5).

When M VM/VEF ⊆ EF VEF is false, there are model executions which are not EF executions.

We identify two cases (Fig. 5):

• (case 2.1 in Fig. 5). There is a test coverage risk. This may be the case if the model considers input variables with other values than those planned by the EF. The EF does not therefore explore all executions of the simulation. This means that either the unexplored executions are not relevant for the experimentation, or that the EF is not comprehensive enough.

• (case 2.2 in Fig. 5). There is a bias in the simulation or in the reference definition. This may be the case as the model considers output variables with other values than those expected by the EF. This means either that the simulation results are incorrect or that the EF assumptions are false.

When EF VEF ⊆ M VM/VEF is false, executions are envisaged by the EF but are not model executions. Here again, two cases can be considered (Figure . 5):

• (case 3.1 in Figure . 5). Some experiments are outside the usage domain of the simulation model. This may be the case if the EF considers output variables with more values than those accepted by the model. The EF therefore plans to explore simulation executions outside the scope recommended by the model and the simulation results can no longer be guaranteed. The model or EF must be modified.

• (case 3.2 in Figure . 5).There is a risk concerning the completeness of the model. This may be the case if the EF considers the input variables with more values than those supplied by the simulation results. Thus, either there is something to be learnt from the simulation if we reduce the uncertainties of the EF, or the simulation overlooks the implementation of some cases.

Computing compatibility

A key step in our methodology is to ensure that a model provides meaningful input and output ports for a given experimental frame, i.e. a set of stimulation and observation points [START_REF] Albert | Signature matching applied to simulation/frame duality[END_REF]. In other words, we focus on the boundaries between the model and the experimental frame. Thus, we can clearly perceive what drives the model, what is observed as its output, and the model itself. It is worth noting that incorporating data-gathering facilities into the model must be avoided, since this would make the model not only more complex but also unsuitable for reuse or for association with different experimental frames. D.S. Weld [START_REF] Weld | Reasoning about model accuracy[END_REF] defines the scope of a model as the range of the system the model describes. A model has a larger scope than another if it gives a broader description of the system. Changing the scope of a model is equivalent to redefining the boundaries between the system (described by the model) and its environment. So, selecting the scope of the model implicitly includes selecting the exogenous parameters and determining their values. Then consider a system A which has a set of endogenous parameters and a set of exogenous parameters. By reducing the scope of the model of system A, we get a system B with a new (smaller) set of endogenous parameters and a new (larger) set of exogenous parameters. The new exogenous parameters then become parameters that can be controlled and/or observed by the simulation user to properly carry out his/her experimentation. They now belong to the experimental frame. New boundaries between the experimental frame and the model of the system of interest are defined. We thus define the scope of a simulation by the set of exogenous parameters of the system of interest.

In industrial practice, a simulation is developed to verify and validate a given set of system requirements. Therefore a test plan associated with those requirements is elaborated. We assume that a test plan requiring user specification leads to an experimental frame component annotated with specific constraints, i.e. a signature. We equally assume that the component model of that system is annotated with those constraints. We can then analyse a set of compatibility properties between the experimental frame and the model. There exist static and dynamic properties. Hence simple properties (scope, values, domain...) have been found to be correct and the modeler can therefore go further to include more complex properties (e.g. a minimum user specification is required for static properties). An incorrect property informs us that the simulation cannot be executed in the given situation, i.e. either the model or the experimental frame must be modified.

Steps of compatibility computation

A component-based approach is proposed to describe a simulation. We assume that an experimental frame and a system model of interest are two components as defined by [START_REF] Szyperski | Component Software: Beyond Object-Oriented Programming[END_REF]. A component features a set of ports and is coupled to another component through connectors via their respective ports. A component can either be coupled, i.e. it is the result of a composition of components, or it is atomic, i.e. it cannot be decomposed any further.

Then we assume that both the experimental frame and the model are specified and can be built using a component-based approach. The experimental frame successively affects values to the model inputs (generator), triggers events and observes the model outputs (transducer). Temporal logic may be used to specify the acceptor, i.e. a set of relationships between inputs and outputs within the frame.

Consider two components EF and M defined by two IOAs : EF = 〈D EF , X EF , Y EF , dom EF , S EF , σ EF , Σ EF , δ EF , S 0EF 〉 and M = 〈D M , X M , Y M , dom M , S M , σ M , Σ M , δ M , S 0M 〉.

Computing the compatibility of the experimental frame relative to a model involves several steps:

• • • • Step 1: Verifying scope compatibility
The ports of a component are defined by its automaton vocabulary (X, Y and S). Then an EF and M can be connected if (definition 9): XEF ⊆ YM, YEF =XM, ΣEF ⊆ ΣM.

• • • • Step 2: Computing the targeted state

A simulation achieves its intended purpose if the set of summary mappings given by the acceptor are satisfied by the interaction of the model with the generator and the transducer. Remember that a summary mapping can be seen as a set of constraints which links a configuration σ(v) with v ∈ SEF and a transition l ∈ δEF. v is a targeted state of the acceptor. We denote the set of targeted states given by the acceptor by Sacc ⊆ SEF.

This step consists in verifying that for all targeted states there exists a state in the model such that:

∀v ∈ Sacc ∃u ∈ SM  σ(v) = σ(u) • • • • Step 3:
Computing the synchronous product of the generator, transducer and model.

The generator, transducer and model share a set of events to satisfy the properties expected by the acceptor. The product allows an IOA to be built up from two IOAs. The synchronous product A of EF and M, denoted A = EF M is defined by: (SEF × SM, ΣEF ∪ ΣM, δEF × δM, S0EF × S0M) where -SEF × SM is the set of states, -ΣEF ∪ ΣM is the set of event names, -S0EF × S0M is the set of initial states, -δEF × δM is the transition relation defined by:

* ((v;u), l, (v', u'))  (v, l, v') ∈ δEF ∧ (u, l, u') ∈ δM ∧ l ∈ ΣEF ∩ ΣM * ((v;u), l, (v', u))  (v, l, v') ∈ δEF ∧ u ∈ SM ∧ l ∈ ΣEF \ ΣM * ((v;u), l, (v, u'))  (u, l, u') ∈ δM ∧ v ∈ SEF ∧ l ∈ ΣEF \ ΣM • • • • Step 4:
Verifying that EF M satisfies the set of properties P expected the acceptor: EF M    = P.

How to use trace inclusion

Using trace inclusion consists of evaluating a simulation based on the experimental frame approach and the steps of compatibility computation as shown in figure 6.

Figure 6. Simulation with trace inclusion approach

We assume that an evaluation of simulation is defined by the model of the system under test and de requirements to evaluate. We recall that our approach is model-based. Therefore the modeling of the experimental frame is built from the simulation requirements to obtain the following models: generator, transducer and acceptor as seen in Figure 6. Each used model in this approach has to be formally checked. It is worth remembering that an experimental frame successively affects values to the model inputs (generator), triggers events and observes the model's outputs (transducer). As mentioned in related work, errors not detected by formal verification are due to incorrect specifications or misinterpretation of specifications. In our approach specifications are taken into account and modeled as IOA that leads to test generation. The IOA can be checked by model checking to ensure its correctness in relation to specification and to detect different kinds of errors such as misinterpretation.

For the compatibility computation we assume the above mentioned models are formally checked and available. Compatibility can be splitted in type of metrics:

• Step 1: allows computation of scope metrics between the EF (i.e. its models) and the model under test. Scope metrics identify expected and required input/output ports of the model and the EF, respectively. These metrics are computed using the IOA of connected models.

• Steps 2 and 3: lead to the computation the compatibility metrics between model, generator and transducer thanks to synchronous product of IOA. Compatibility metrics are achieved by synchronous product between EF models and model under test to identify the applicability of event sequences between EF and model and verify the reachability of searched states given by the acceptor.

• Steps 4, 5 and 6: help to compute the coverage metrics. Coverage analysis is performed by the acceptor which provides acceptance criteria for trace inclusion. This analysis is based on the results of a verification tool as UPAAL. We compare the set of model traces, which meets the properties given by the acceptor, with the set of traces given by the generator and the transducer. With the trace inclusion approach, we can identify a priori (before simulation execution) whether a simulation can be executed indicating to the modeler whether the guarantees provided by the model will satisfy its simulation objectives of use. Coverage metrics can be defined using five quantities (figure 5): exact matching (case 1), test coverage risk (case 2.1), bias in the simulation (case 2.2), wrong usage of the model (case 3.1), and model completeness risk (case 3.2).

An example: Adaptive cruise controller

Our approach can be illustrated with the design of an embedded system, the control unit of an autonomous intelligent cruise controller (AICC) [START_REF] Palmquist | Intelligent cruise control and roadside information[END_REF][START_REF] Schulz | Towards an application of model-based codesign: An autonomous, intelligent cruise controller[END_REF]. The AICC is more than just a regular cruise controller which maintains speed as required by a driver, it adapts it according to the distance and speed of the vehicle in front. A safe speed is the maximum speed required to maintain the vehicle safely away from the other vehicles in front of the vehicle. The expected speed is the one requested by the driver. The control unit must keep the speed within ±2km/h of the safe speed or expected speed, whichever is lower.

Adaptive cruise controller simulation

The structural definition of the simulation is given in Figure 7 below. Remember that it is an important step since it allows to define the boundaries between the model and the experimental frame. Selecting the scope of the model implicitly includes selecting exogenous parameters. All other components of the global system (e.g. AICC vehicle) now belong to the experimental frame needed to represent the environment of the cruise controller. Some of these elements can be abstracted or simplified if their contributions are not relevant to the experiment.

The system of interest consists of the cruise controller calculation module which computes a throttle setting according to data from the driver and sensors. Those data include brake command, coast and acc controls to respectively decrease and increase the required speed. The safe speed and actual speed are retrieved from speed sensors.

In this context, the experimental frame consists of scenarios for brake, and required speed and a function to compute the safe speed according to the distance and speed of the leading vehicle. This is accomplished by the generator. The transducer monitors the throttle setting and updates the vehicle speed accordingly. The acceptor continually tests the run control segments to satisfy a set of constraints, e.g. the speed of the vehicle must remain within ±2km/h of the safe speed or expected speed.

Adaptive cruise controller model

Consider a model of the AICC for which Figure 8 gives all possible executions. This model has several variables: s, ws, ss, which are the speed of the vehicle, the expected speed given by the driver, and the safe speed given by a sensor, respectively. These variables can only take the values 10 or 20. A variable status indicates whether the cruise controller is OFF or ON. A variable cs is employed to know whether the controller must maintain the safe speed or the expected speed, whichever is lower. incTh and decTh are used to adjust the throttle valve angle. The set of states S is then given by S = {status ∈ {ON, OFF}, cs ∈ {ws, ss}, ss ∈ {10, 20}, ws ∈ {10, 20}, s ∈ {10, 20}}.

The set of events is given by Σ = {acc, coast, brake, s < ws, ws ≤ ss, incDst, decDst}. When the cruise controller is OFF, if a coast event occurs, it switches to the ON state and the speed is maintained. In this state, having a coast event leads to decreasing the driver expected speed, while having an acc event results in increasing the driver's expected speed. A brake event turns the cruise controller OFF. The s < ws event will occur when the speed (s) decreases below the wanted speed (ws). The ws ≤ ss event will occur if the wanted speed decreases to the safe speed or a speed lower than the safe speed. The incDst and decDst events respectively increase or decrease the safe speed value.

Figure 8. Reachability graph of the cruise controller

Let us now formally describe the "observable" version of the model. The state variables which are not controllable and/or observable are masked. This causes state aggregation over the model's state space. Fig. 9 shows an abstraction of the previous reachability graph. The cs variable is hidden and the states which share the same combination of values for status, ws, s and ss are aggregated. The transition relations are kept.

Adaptive cruise controller experimental frame

Consider then the following intended purpose: when the safe speed is lower than the expected speed, the controller must keep the speed of the vehicle at the safe speed.

There are two scenarios for which the safe speed becomes lower than the expected speed:

1. the safe speed is greater than or equal to the expected speed and an acc event increases the expected speed which becomes greater than the safe speed.

2. the safe speed is greater than or equal to the expected speed and a decDst event decreases the safe speed which becomes lower than the expected speed.

Behavioural compatibility

Given below are examples of relaxed compatibility as given in definition 11. Case 1:

Consider the model given in Figure . 9 and an experimental frame scenario which simply stimulates an acc event, then it observes ss < ws and finally s=ss. The set of targeted states are all states where s < ss: Sacc = {s2, s5, s7}

The product EF M satisfies the property    →  < ws ss s = ss. The algorithm used to verify that an automaton satisfies a temporal property is not given here. It can be found in [START_REF] Alfaro | Interface automata[END_REF]. In the model given in Figure 9, three execution traces satisfy this property: If properties A◊ speed ≥ curr_speed-2 and A◊ speed ≤ curr_speed+2 are true, the speed of the vehicle always remains within ±2km/h of the current speed.

M VM = 1. s0   →  acc s2    →  < ws ss s2 2. s0    →  incDst s1   →  acc s3    →  incTh s5    →  decDst s4    →  < ws ss s4    →  decTh s2 3. s0   →  acc s1    →  incDst s3    →  incTh s5    →  decDst s4    →  < ws ss s4    →  decTh s2
If the property E◊ curr_speed==expected_speed is true, there is a sequence of alternating delay transitions and action transitions where the current speed equals the required speed. Scenario 1: ΩYM ≠ ΩXEF and ΩXM < ΩYEF (Fig. 14) This scenario occurs when the execution trace of the experimental frame is not an execution trace of the model (case 3.1 in Figure 5). Some experiments lie outside the usage domain of the model, i.e. the model cannot reach the ON state from the OFF state with the event brake. Indeed, the transducer state OK will never be reached (case 2.2 in Figure 5). 15 This scenario occurs when the experimental frame does not explore all execution traces of the model (case 2.1 in Figure 5). The generator is applicable to the model, i.e. the end state is reached but does not allow to support the simulation intended purpose, i.e. the transducer state OK will never be reached (case 2.2 in Figure 5). Indeed, the left side transition of the UpdateData module is never fired. 16) This scenario occurs when the experimental frame execution traces are also execution traces of the model. The generator is applicable to the model, i.e. the end state is reached and the simulation intended purpose is met, i.e. there is an execution trace in which the transducer state OK will be reached.

Conclusion and future work

This paper has introduced an approach to formally validate and define a context of ongoing simulation using behavioural compatibility between a model and its intended purpose. The concept of experimental frame, proposed in the M&S theory, has been employed to address the problem within a well-founded methodological framework. It has also allowed us to treat a recurring problem in that the intended purpose of the simulation is often not well-defined. We have shown that the model is not the only cause of bias to simulation, but that the experimentation performed with this model may also have been poorly defined.

The issue of matching relies on the principle that an intended purpose and a model are two components, in the formal meaning of the term, i.e. interacting through their interfaces and only through them. We turned to component-based engineering techniques to iteratively enhance the concept of an experimental frame of "symbolic concepts" and determine the system behaviours to be included in the model.

The generator defines the logical order of the stimuli injected into the simulation. The transducer defines the logical order of the observations. We specified these two components using input/output automata. The acceptor, specified using temporal logic, consists in verifying whether a requirement has been verified based on stimulus/observation pairs. As for properties related to the applicability check between the experimental frame and the model, we also defined temporal logic properties for EF states to determine which applicability case we found ourselves in. While this approach is consistent, an effort remains to be made to find more systematic applicability properties. We have defined and compute three types of metrics: scope metrics between the EF and the model, compatibility metrics and coverage metrics within the state space. Furthermore, with this approach, coverage analysis can be performed either from scratch with the development of a simulation necessary and sufficient to satisfy an intended purpose, or with the reuse of an already existing simulation model to satisfy an intended purpose. Developers are free to associate a model with different experimental frames, each corresponding to a particular simulation objective of use.

Figure 1 .

 1 Figure 1. Novelty of the concept A simulation scenario consists of a trajectory injected into the model inputs and a path of interest observed on the model outputs. Typically a simulation is not comprehensive in the sense that it does not explore all possible trajectories of the model. A simulation scenario restricts the model to a subset of evolutions the model may produce. Then the simulation requires metrics which capture (1) the applicability of a scenario to a model, i.e. a set of stimuli can be accepted by the model and the model produces expected outputs, (2) the reliability of the simulation results, i.e. to what extent the state space of the model has been explored by the simulation, and (3) whether certain requirements of the real system are met by the simulation model.Metrics (1) and (2) can be measured by composition of the system model of interest and the model of the experimental frame, and metric (3) can be measured by checking the simulation model against the specification of the system of interest.

  Validity refers to the degree to which a model faithfully represents a system in an experimental frame of interest. The relation between a model and a simulator is simulation. The correctness of the simulator is the basic concept of this relation. A simulator correctly simulates a model if it guarantees a faithful generation of model output values given the model state and the input values. This relation refers to the principle of separating concerns about model design and its implementation.

Figure 4 .

 4 Figure 4. Reachability graph of a shared memory communication system Definition 2 (Run (or trace)). An IOA run is a sequence (finite or not) σ (s 0 ) →l 0 … σ (s i ) →l i … where s i is a state (s 0 is an initial state) and l i is an event name such that any (s i →l i s i+1 ) of a run is a transition of the automaton. A run can also be defined by a path taken from the computation tree of an automaton. "Run" can also be called "trace".

Definition 7 (

 7 Restriction of a transition).The restriction δ / Σ' of a transition relation δ ⊂ S × Σ × S restricted to a vocabulary Σ' ⊂ Σ is the transition relation δ / Σ' ⊂ S × Σ' ∪ {ε} × S such that:

Figure 5

 5 Figure 5 below illustrates these four cases.

Figure 5 .

 5 Figure 5. Level of EF/Model behavioural compatibility

Step 5 :Step 6 :

 56 Computing the IOA of the model restricted to the IOA of the experimental frame (Comparing execution traces (definition 12).

Figure 7 .

 7 Figure 7. Adaptive cruise controller simulation

Figure 9 .

 9 Figure 9. Abstract version of the previous reachability graph

Figure 11 .Figure 12 .

 1112 Figure 11. IOA 2 of the model: UpdateSpeed

Figure 13 .

 13 Figure 13. Left to right: generator for scenarios 1, 2 and 3

Figure 14 .Scenario 2 :

 142 Figure 14. Temporal logic verification for scenario 1 Scenario 2: ΩYM ≠ ΩXEF and ΩXM >ΩYEF (Figure15This scenario occurs when the experimental frame does not explore all execution traces of the model (case 2.1 in Figure5). The generator is applicable to the model, i.e. the end state is reached but does not allow to support the simulation intended purpose, i.e. the transducer state OK will never be reached (case 2.2 in Figure5). Indeed, the left side transition of the UpdateData module is never fired.

Figure 15 .Scenario 3 :

 153 Figure 15. Temporal logic verification for scenario 2

Figure 16

 16 Figure 16 Temporal logic verification for scenario 3

We have two directions for the future work:

• we would refine coverage quantities and explore other gauges for metrics.The latter are ordered, i.e. measuring trace inclusion implies that ports and event sequences are compatible,

• we would like to focus on establishing equivalence classes between execution traces, e.g. traces that rise to the same conclusion can be aggregated. This would allow to reduce the number of simulation scenarios and to avoid the duplication of tests.

Result:

The experimental frame covers the first model's execution trace but does not explore traces 2 and 3. This corresponds to case 2.1 in Figure 5.

There is a test coverage risk.

Case 2: Consider a model which overlooks the implementation of execution traces 2 and 3 shown above. Consider an experimental frame which stimulates a decDst event, then it observes ss < ws and finally s=ss.

The product EF M does not satisfy the property    →  < ws ss s =ss, i.e. the event decDst of the experimental frame is not synchronizable with M. The synchronous product step failed. Therefore we don't need to compare execution traces.

Result:

The experimental frame plans to explore simulation executions are outside the scope recommended by the model. This corresponds to case 3.1 in Figure 5.

The experimental frame and model are not compatible.

Verifying trace inclusion with UPPAAL

UPPAAL is a tool environment for the modeling and verification of real-time systems modeled with timed automata. It uses Linear Temporal Logic (LTL) to encode requirements and analyse qualitative properties of models.

The behaviour of the AICC calculation module is given by the automaton in Figure 10. The second automaton in Figure 11 implements a module called UpdateSpeed used to continually check which speed must be used for cruise control, i.e. safe speed or expected speed. Observe that we have used the synchronization mechanism offered by UPPAAL to ensure that the product of the model and experimental frame satisfy the properties given by the acceptor.

Figure 10. IOA 1 of the model: calculation module

The intended purpose consists in validating the speed selection process (module UpdateData): if the safe speed is lower than the required speed, the cruise controller must maintain the speed equal to the safe speed. Otherwise, it must maintain the speed equal to the required speed. The transducer, as illustrated by the IOA Figure 12, updates the vehicle speed according to the throttle setting, and continually checks the property curr_speed == expected_speed, i.e. the cruise controller maintains the speed equal to the required speed.


Omar Krichen
email: omar.krichen@irisa.fr

Nathalie Girard
email: nathalie.girard@irisa.fr

Eric Anquetil
email: eric.anquetil@irisa.fr

Mickaël Renault
email: mickael.renault@irisa.fr

Real-time interpretation of geometric shapes for digital learning

Keywords: On-line Recognition, Hand-drawn stroke analysis, Digital learning

In the context of the ACTIF project that aims for active and collaborative learning promotion, this paper presents a pattern recognition and analysis system for Geometry learning in middle school. The goal is to allow students to draw geometric shapes on a touch-tablet, given a teacher's instruction. To make the student active, the system have to recognize and analyze on the fly the student's productions in order to produce realtime visual, corrective, and guidance feedback. We base our work on the visual grammar CD-CMG [1] (Context Driven Constraints Multi-set Grammar), to model the domain prior knowledge and interpret the hand-drawn sketches on the fly. Our first contribution lies in adapting this grammar to the Geometry domain to cover the geometric objects taught in middle school curriculum. Although being expressive enough to model this large scope, the formalism could not cope with the exigence of real-time analysis, given that the multiple interactions between geometric objects generate combinatorial issues. Our second contribution lies in extending the formalism which resulted in having an acceptable performance for a real-time user interaction system. The first experiments show that the proposed approach allows complexity and interpretation time reduction.

I. INTRODUCTION

Our work is in the context of ACTIF project, which aims to use pen-based tablets in an educational context, mainly in French middle schools, to foster active learning [START_REF] Chickering | Implementing the seven principles: Technology as lever[END_REF]. In this paper, we focus on learning Geometry by drawing freely on a touch-tablet. Dynamic Geometry Software products are now an important part of teaching geometry. Their goal is to make geometric concepts understanding easier for the student by graphical construction, manipulation and visualization of figures. To our knowledge, the tools used in middle schools, such as Geogebra [START_REF] Bhagat | Incorporating GeoGebra into geometry learning -A lesson from India[END_REF], rely on a drag-and-drop approach to manipulate geometric objects. Indeed, in order to compose a figure, a student must choose from a graphical panel the object he wants to create then has to place its components in the interface. This tends to limit the creative process of the user. In [START_REF] Fiorella | Learning as a generative activity: Eight learning strategies that promote understanding[END_REF], Fiorella and Mayer demonstrate that "generative drawing", i.e learning by drawing, has a positive impact on students learning abilities in the classroom. In [START_REF] Kluger | The effects of feedback interventions on performance: A historical review, a meta-analysis, and a preliminary feedback intervention theory[END_REF], Kluger and DeNisi show the impact of feedback intervention on learning performance. These two points represent the pedagogical foundation of our project. We propose a pen-based system that simulates the traditional pen and paper figure sketching and enriches it by real-time visual, corrective and guidance feedback. This paper presents the first works done in the project, and focuses on the online recognition method of the system. In the literature several works have been done for hand-drawn sketches recognition, the following Sec. II presents an overview of existing approaches. Based on this overview and the application domain, we introduce the formalism and the modelling of the geometric knowledge in Sec. III. Since the system has to recognize hand-drawn sketches in realtime, some optimizations are needed, Sec. IV describes the formalism extension and its impact on the analysis process. Sec. V presents our experiments and results while conclusion and perspectives are given in Sec. VI.

II. RELATED WORKS

In this work, we are interested in on-line recognition of handwritten structured documents. We distinguish between two types of handwritten documents interpretations methods: lazy [START_REF] Ghorbel | Interactive interpretation of structured documents : application to the recognition of handwritten architectural plans[END_REF] and eager [START_REF] Lank | On-line recognition of UML diagrams[END_REF]. Lazy interpretation means that the analysis process begins after completion of the user's production. Eager interpretation means that the handwritten strokes are analyzed on the fly, which is more relevant to our objective of having real-time corrective and guidance feedback to prevent error propagation. There are two major approaches for document analysis: statistical and structural. Statistical approaches [START_REF] Delaye | Hbf49 feature set : A first unified baseline for online symbol recognition[END_REF] rely on learning on large labelled databases to discriminate between symbols and are well suited for isolated shapes recognition. However, they do not allow the modelling of the document's structure. Since we are in Geometry context, the system has to recognize not only the geometric shapes, but also the structural relations between the objects. Structural approaches consider a symbol in terms of its constituents, the graphical primitives, and the structural relations between them. For instance, a triangle is considered as three segments related by spacial relations. Structural approaches rely on modelling prior domain knowledge by visual grammars. We distinguish between two classes of structural recognition methods. The former is based on graph grammars. For example, Zannibi et al. [START_REF] Zanibbi | Evaluating structural pattern recognition for handwritten math via primitive label graphs[END_REF] use labelled graphs to recognize handwritten mathematical expressions. One problem with graph-based methods is that they are complex to manipulate for the designer, especially if the production rules number is high. The latter is based on bi-dimensional grammars. For example, in [START_REF] Hammond | LADDER, A Sketching Language for User Interface Developers[END_REF] Hammond and Davis proposed Ladder, a generic description language, and applied it for the interpretation of Truss diagrams in a digital learning context [START_REF] Atilola | Mechanix : A natural sketch interface tool for teaching truss analysis and free-body diagrams[END_REF]. In [START_REF] Muñoz | Recognition of on-line handwritten mathematical expressions using 2D stochastic context-free grammars 48 and hidden Markov models[END_REF], a bi-dimensional extension to the Stochastic Context Free Grammar is proposed for handwritten mathematical expressions analysis. In this work, to model the geometry domain knowledge, we prefer to use Context Driven Constraints Multi-set Grammar (CD-CMG) [START_REF] Macé | Eager interpretation of on-line hand-drawn structured documents: The DALI methodology[END_REF], a generic formalism for eager interpretation of hand drawn documents. Indeed, in this grammar, the context is explicitly specified in the production rules, which reduces the search space. Moreover, this formalism is the combination between a statistical approach (to locally recognize a shape) and a structural approach (to model the global structure of the document). Finally, CD-CMG has been applied on various types of documents such as architectural plans [START_REF] Pecot | Interprétation interactive de plans d'architecture composés à main levée[END_REF] or electrical sketches [START_REF] Macé | Eager interpretation of on-line hand-drawn structured documents: The DALI methodology[END_REF]. All these features show these formalism is well adapted for our purpose. Thereafter, our contribution lies in two folds: adapting this grammar to the Geometry domain for e-education (see Section III), and extending this formalism to match the constraint of real-time analysis of geometric productions (see Section IV).

III. GEOMETRY DOMAIN MODELLING

In this section, we present the formalism, and illustrate it through its adaptation to the Geometry domain.

A. Context Driven Constraints Multi-Set Grammar

As an extension of the well-known grammar CMG [START_REF] Marriott | Constraint multiset grammars[END_REF], CD-CMG is formally defined as follows: Definition 1. A CD-CMG is a tuple G=( V N , V T , S, P) with:

• V N : the set of non terminal symbols = symbol classes; • V T : the alphabet, here V T = {stroke}; • S: the first symbol, or axiom; • P: the set of production rules.

And where a production rule p ∈ P is composed of three blocks allowing different levels of vision on the document. The precondition and the postcondition blocks stand for the global vision of the document while the constraint block stands for the local vision of the analyzed strokes. Therefore, a production rule p is denoted as follows:

α → β      Preconditions Constraints Postconditions      | α ∈ V N + , β ∈ (V T ∪ V N ) +
Preconditions and postconditions are based on the concept of Document Structural Context, which models a zone in the document and the awaited elements in it, defined as follows:

Definition 2. A DSC is defined by (λ)[position](γ)[part]
where:

• λ is a set of reference elements;

• position is a zone (i.e a position) related to λ;

• γ is a set of awaited symbols in this zone;

• part is a part of the awaited symbol that has to intersect the zone.

The preconditions are a set of DSC that have to be satisfied and represent the context in which β can be replaced by α. The postconditions are a set of DSC that represent the objects that can be created from the new reduced elements α. This formalization enables to drive the analysis process by the context. Indeed, the preconditions represent the verification step while the postconditions represent the prediction step. The constraints model a local vision on the analyzed elements β. They have two purposes: checking that the shape of β is consistent with the production, and decide if it is pertinent to reduce β into α

B. Adaptation of CD-CMG to Geometry

We consider the main geometric objects taught in French middle schools: segments, arcs, circles, angles, all the types of triangles and quadrilaterals. We defined around 20 productions rules to model these objects productions as well as the interactions between them (e.g intersection and orthogonality). Let's illustrate this with two production rules. Fig. 1 presents a part of a segment production rule, while Fig. 2 and Fig. 3 illustrate a segment composition. In this example, the red stroke in Fig. 2 is transformed into a segment if the precondition block and the constraint block are satisfied. The postcondition DSC (green rectangle in Fig. 1) models the fact that a bisector production rule will be triggered if a straight d intersects the center zone of the new created segment (res). The precondition block is composed of one precondition which is a conjunction of three DSC modelling the fact that each segment intersects a zone related to the other two. The constraint here is structural, such that it verifies that the three Triangle: res → segment: s1, s2, s3 with:

Preconditions: (S1) [Zone] (s2) [one] & (S2) [Zone] (s3) [one] & (S3) [Zone] (s1) [one]
Constraints: LinkedSegments(s1, s2, s3) Fig. 4: Triangle production rule segments are linked by their extremities. Since the structural context is the same for all types of triangles (and quadrilaterals as well), we established a hierarchy between production rules, from general to specific, in order to prune the search space and speed up the analysis process. For example, a triangle can be reduced into an isosceles triangle if two of its sides are equal.

C. Analysis process associated to CD-CMG

The analysis process, extensively explained in [START_REF] Macé | Eager interpretation of on-line hand-drawn structured documents: The DALI methodology[END_REF], is a combination of a bottom-up strategy (guided by the reduced elements) and a top-down strategy (guided by the postconditions DSCs). For each new element, the parser searches the DSC it satisfies and vice versa. Consequently, a production is triggered if its β elements contain at least a new element and its precondition block contains at least a new DSC. Let's consider the scene illustrated in Fig. 5 composed of a new stroke t (in red) and 3 segments (s1, s2, s3).

Fig. 5: Stroke analysis process

The analysis of t leads to the construction of the analysis (or derivation) tree presented in Fig. 6. The root represents the stroke t. The nodes and the leaves represent the triggered rules, while the blue path is the sequence of reduced production rules, i.e the analysis result. As shown in Fig. 6, t is first reduced into a segment, denoted thereafter s4. Then, several rules are tested among which the production rules that led to the correct interpretation of the user's drawing. As we can see in Fig. 6, the triangle production rule is triggered three times for each possible combination of segments: (s4, s1, s2), (s4, s1, s3) and (s4, s2, s3), even if there is no coherent context for creating a triangle in this scene. This is due to the fact that these productions contain a new element (s4) and one of their preconditions DSC is satisfied (c.f Fig. 5). Only the preconditions block is checked in this case, since not all DSC are satisfied. The impact on the combinatorics is not important here, but when the document is complex, the analysis becomes costly. Even though the formalism is generic and expressive enough to model the prior geometry knowledge, the multiple possible interactions between geometric objects, e.g creating sub-figures from existing ones (c.f Fig. 7), also generate combinatorics problems in the analysis process. Let's consider the triangle production rule (c.f Fig. 4). A direct consequence of adapting CD-GMC to the geometry domain is that the β elements (here the 3 segments) are not really replaced by the α elements (here the triangle). They contribute to create the triangle but they remain considered in the analysis process in order to create other new elements. This has a big impact on the applicable rules search space size. We distinguish two factors producing the combinatorics explosions: the format of the DSCs, and the computation of equivalent interpretations. We will explicit these factors and our proposed solutions in the next section.

IV. REVISION AND FORMALISM EXTENSION

In this section, we present the problems we faced in terms of analysis process complexity and our proposed solutions.

A. The DSC problematic

The expressivity of the formalism in terms of describing the document structure with the DSC allows to formalize that all the components of a polygon are linked by their extremities. Unfortunately, as we have seen in Section III.C, the fact that a production can be triggered even if only one of its preconditions DSC is validated generates a combinatory problem. Indeed, the more segments a polygon contains, the more DSC there are in the polygon production. Fig. 8 illustrates the composition of a new stroke t in the context of three already interpreted segments. t will be recognized as a new segment called thereafter s2. The fact that s2 is linked to [AB] (blue zone in Fig. 8) will activate the DSC: ) instead of once. Thus, the analysis time can be very long, especially if the document is complex. In fact, this issue relies on a CD-CMG limitation. The formalism does not allow to have more than one zone in a DSC, which would enable positioning many awaited elements in relation to one reference element. To resolve this problem, we propose to refine the constraints on the zones such that a zone can cover all the awaited symbols in the same DSC. The DSC related to the triangle production rules will then be:

[AB] [InitialExtremity] s2 [one] =⇒ triangle → [AB],s2,s3.
[AB] [T otalLengthSegment] s2, s3 [one],
where T otalLengthSegment is the zone that covers the length of [AB] (in blue in Fig. 9). This formulation allows to have a contextual information on all the segments composing a triangle. The loss in focus of the zone (from covering an extremity to covering all the segment) is balanced in the Constraint block by verifying that the segments are structurally linked by their extremities. For the scene illustrated in Fig. 9, the triangle production rule is triggered only once, which reduces the analysis complexity.

B. Equivalent interpretations problematic and formalism extension

Since we are in Geometry learning context, it is important know the dependence links between the elements, e.g the connections between several segments. These links are modeled in the preconditions DSCs. Fig. 10 presents a focus on the precondition block of the segment production rule. It is composed of a dis-junction of three preconditions. They model the fact that there are three possible contexts for a segment creation. The stroke can be linked to two existing segments The F irstP recondition operator, introduced in [START_REF] Pecot | Interprétation interactive de plans d'architecture composés à main levée[END_REF], establishes an order between the preconditions, e.g from specific to general, and forces the parser to stop the context research at the first valid precondition. Fig. 11: FirstPrecondition limits Fig. 11 illustrates a scene in which a stroke t is recognized as a segment. F irstP recondition forces the parser to consider the stroke as linked to two segments, considering only the first precondition. Without this operator, the three preconditions, which are valid in this case, will be tested as hypotheses and the parser will choose the one with the highest score. A limit to this operator is that the verification of the first precondition can also be complex. Indeed, in this example, there are six contextually valid hypotheses: t can be linked to the couples (s1, s5), (s1,s6), (s1, s7), (s4, s5), (s4, s6), (s4, s7). Hence, six equivalent branches will be created in the analysis tree multiplying the analysis complexity by six. To tackle this problem, we propose to extend the formalism by creating a new operator F irstContext. This operator forces the parser not only to stop the research at the first valid precondition, but also at the first valid context within a precondition. That means that the search is stopped when the first reference elements that are coherent with the precondition are found. In the example (Fig. 11), the parser will choose the first couple of segments that satisfies the DSCs of the preconditions, e.g it will choose the couple (s1, s7) without considering the other combinations. This will drastically reduce complexity, without losing information about connections. In use, we have noticed a limit to this new operator, which occurs when the segments are not exactly connected, but have overlapping zones (see the example in Fig. 12) . Without the F irstContext operator, the system computes the membership degree of the stroke's extremity in each zone of the segments to choose the best possible interpretation. With F irstContext operator, it has to Fig. 12: Zones overlap problem choose the first valid interpretation, which is not necessarily the best. However, the robustness of this extension lies in the interaction with the user since he has the possibility to implicitly validate the interpretation by continuing his drawings, or to delete the segment and redraw it more precisely. This is a trade-off between interpretation precision and analysis process. We will detail the impact of our contributions in the next section.

V. EXPERIMENTS AND RESULTS

A. Quantitative study

To evaluate the impact of our contributions on the system performance, we established several criteria:

• Iterations: number of reduced productions rules • Interpretations: number of branches in the analysis tree • Time: Analysis time • Triggered: Number of triggered rules The evaluation is realized on one complex drawing benchmark, illustrated in Fig. 13.

Fig. 13: Benchmark

We study the impact of our contributions on three critical steps of the drawing scenario of this figure, illustrated in Fig. 14, Fig. 15, and Fig. 16. We compare the performance of our system with DALI, the framework based on CD-CMG and its associated parser. In the following, the term ZoneOpt refers to the constraints refinement on the zones while F irstContext refers to the formalism extension by the addition of the new operator.

1) First step of the scenario: The scene (Fig. 14) illustrates a drawn stroke that will produce an analysis process. The stroke will be first interpreted as segment [AD]. This segments will trigger the production of a rectangle.

Drawn stroke

Analysis result 2) Second step of the scenario: The scene (Fig. 15) illustrates a more complex production. The drawn stroke will be first interpreted as segment [EB]. This segments will trigger the production of two triangles, one being isosceles and the other rectangle.

Drawn stroke

Analysis result Fig. 15: Second step of the scenario

The impact of our contributions on this step is illustrated in TABLE II. With the classic Dali methodology, the performance is not acceptable since analysis time takes 6.4 seconds. This is due to the number of triggered rules (1057) and equivalent interpretations [START_REF] Delaye | Hbf49 feature set : A first unified baseline for online symbol recognition[END_REF]. By modifying the format of the DSCs, ZoneOpt improves the analysis time (2s) by reducing the number of triggered rules. F irstContext operator forces the parser to consider only one interpretation. In consequence, the number of triggered rules decreases from 1057 to 356, and the analysis time is down to 4.2 seconds, which is still not acceptable in a context of real-time interaction with a user. However, the coupling of Opt1 and Opt2 enables to have an analysis time of 0.62 which is acceptable.

3) Third step of the scenario: In this final step of the scenario (illustrated in Fig. 16), the drawn stroke will be first interpreted as segment [DF]. This segment will trigger the production of rectangle triangle, a trapezes and a parallelogram.

Drawn stroke

Analysis result and TABLE III, the more complex the scene gets, the greater the impact of our contributions on the performance gets. Thus, taking into account the desired real-time user interaction, the proposed optimizations allow the design of a system with acceptable performance.

B. Qualitative study 1) Edition mode: In the traditional pen and paper setup, we often use symbols or codes to explicit geometric properties such as orthogonality or equality. We extend this notion by designing command that not only display properties, but also modify physically the objects, with respect to these properties. These gestures are integrated in the grammar as strokes triggering production rules, therefore modifying the geometric objects. The orthogonality command gesture is illustrated in Fig. ??. Our system allows also to modify the length of a segment by dragging one of its extremities. The same principle is applied for angle modification. In this paper, we propose a pen-based system that interprets in real-time geometric figures in order to give visual and corrective feedback, given an instruction. We optimize and extend the CD-CMG formalism to adapt the DALI methodology to geometry. Our contributions have a consequent impact on the system performance which is now acceptable for realtime user-interaction. Our future work consist in improving even more the analysis time, one possible solution being the modification of the analysis process in terms of triggering rules. We will also work on an author mode, where the teacher can create customized exercises. The goal will be to generate automatically the solver procedure from the teacher's drawings. The system will also have to generate all the alternative procedures in order to give personalized corrective feedback to each student. The successive versions of our prototype will be tested in pilot middle schools, and we will benefit from the studies of LP3C and LOUSTIC laboratories in usage psychology and ergonomics to design visual and corrective feedbacks that are well suited for the students.

Fig. 1 :

 1 Fig. 1: Segment production rule in CD-CMG

Fig. 6 :

 6 Fig. 6: Analysis tree

Fig. 7 :

 7 Fig. 7: Sub-figures creation

Fig. 8 :

 8 Fig. 8: Strict DSC

  Segment: res → stroke t with: Preconditions: F irstP recondition: (Segment:S1) [Zone] (t) [first]& (Segment:S2) [Zone] (t) [last] or (Segment: S1) [Zone] (t) [extremity] or (Document) [in] (t) [all] ...

Fig. 10 :

 10 Fig. 10: Precondition block for segment production

Fig. 14 :

 14 Fig. 14: First step of the scenario

Fig. 16 :

 16 Fig. 16: Third step of the scenario

Fig. 17 :

 17 Fig. 17: Prototype interface

TABLE I

 I presents the analysis results for this step. Since the document is still simple, the performance is good (around 0.20 seconds). However, our contributions have no real impact on the analysis time. With ZoneOpt, the number of triggered rules decreases from 43 to 23. F irstContext operator has no effect since there is no equivalent interpretations to consider.

TABLE I :

 I First step analysis result

	Approach	Iterations Interpretations	Time	Triggered
	DALI	4	1	0.23 s	43
	ZoneOpt	4	1	0.20 s	23
	F irstContext	4	1	0.20 s	43
	ZoneOpt+ F irstContext	4	1	0.19 s	23

TABLE II :

 II Second step analysis results

	Approach	Iterations Interpretations	Time	Triggered
	DALI	15	3	6.4 s	1057
	ZoneOpt	15	3	2 s	330
	F irstContext	5	1	4.2 s	356
	ZoneOpt + F irstContext	5	1	0.62 s	113

TABLE III :

 III Third step analysis results

	Approach	Interpretations Analysis time Triggered rules
	CD-CMG	6	30 s	2472
	Extended zones	6	7 s	962
	F irstContext	1	5 s	412
	Extended zones + F irstContext	1	1.5 s	167

ACKNOWLEDGMENT

"ACTIF" project is funded by the French government and the region of Brittany. The authors would like to thank the academic partners and the LP3C and LOUSTIC laboratories.


B Dufay

A Esper

E Portalier

C Dolabdjian

J Gieraltowski

Long-time fluctuations of off-diagonal GMI-based magnetometers

Keywords: Giant magneto-impedance, magnetometers, noise, long time fluctuations

This paper presents the measurement of long-time equivalent magnetic field fluctuations. It was obtained with a low noise off-diagonal GMI magnetometer. Acquisitions are conducted with a dedicated acquisition system. The GMI sensor principle and associated noise sources are reminded. Furthermore, the noise model is extended to include the impact of the very low frequency drift of the associated GMI impedance. The homemade GMI magnetometer and the used high dynamic analog to digital converter board are described. The obtained performances show a peak to peak fluctuations of 10 nTpp and a drift of 20 nT/h during 4.5 hours after a transient response. Results are compared, in real time, to a commercial flux gate magnetometer.

I. INTRODUCTION

The giant magneto-impedance (GMI) effect is based on the large variation of the impedance of a soft magnetic conductor, driven by a high frequency current, when submitted to a change of the external magnetic field applied parallel to the current [START_REF] Knobel | Giant magnetoimpedance[END_REF] [START_REF] Phan | Giant magnetoimpedance materials: Fundamentals and applications[END_REF]. Since its rediscovery in the 90s [START_REF] Mohri | Magneto-inductive effect (MI effect) in amorphous wires[END_REF] [START_REF] Beach | Sensitive field-and frequencydependent impedance spectra of amorphous FeCoSiB wire and ribbon[END_REF], it has attracted considerable attention due to its potential in high sensitive magnetometry. To develop a highly sensitive magnetometer, attention must be paid on the equivalent magnetic noise level, which describes the undesired fluctuations of the output signal, since it ultimately limits the lowest detectable magnetic field. Usually, equivalent magnetic noise spectral densities of GMI-based devices shows white noise for upper frequency bands (above few kHz), mainly originating from the electronic conditioning circuitry [START_REF] Dufay | Characterization of an optimized off-diagonal GMI-based magnetometer[END_REF]. At lower frequency, an excess noise arises, exhibiting a 1/f behavior, due to intrinsic noise of the sensor related to low frequency fluctuations of the magnetization direction [START_REF] Dufay | Low frequency excess noise source investigation of offdiagonal GMI-based magnetometers[END_REF].

At even more lower frequency, the characteristics of interest is not the noise power spectral density but the quantification of the long time drift of the output signal. This paper presents preliminary investigation of the long time drift of an optimized GMI-based magnetometer, operating in a field-locked loop.

The paper is organized as follows. Section II recalls the basis of GMI effect, in the context of using it as a sensing element, along with few recalls about noise sources. Section III is dedicated to the description of the experimental setup. Both the electronic conditioning circuitry constituting the magnetometer and the measurement setup are described. Section IV shows the obtained results which is followed by a general conclusion given in section V.

II. THEORETICAL BASIS

A. Principle of the sensing element

The used sensing element is constituted of a CoFeSiB amorphous wire exhibiting GMI effect, strongly coupled to a 450-turns thin pick-up coil. This configuration is usually known as off-diagonal GMI [START_REF] Dufay | Characterization of an optimized off-diagonal GMI-based magnetometer[END_REF] or fundamental mode orthogonal fluxgate [START_REF] Paperno | Suppression of magnetic noise in the fundamental-mode orthogonal fluxgate[END_REF]. It allows to magnify the intrinsic sensitivity of the device according to the number of turns of the pick-up coil. In the case of a classical setup for off-diagonal configuration, the sine wave excitation current, of amplitude Iac and frequency fc, drives the GMI wire which in turn induces a voltage at the pickup coil ends. This voltage is proportional to the off-diagonal term, Z21, of the associated impedance matrix and so, reflects its dependence upon external magnetic field. As GMI effect is strongly non-linear versus the applied magnetic field, we usually consider that the sensor operates in a field locked loop. In an open loop, the output signal after demodulation and low-pass filtering, Vs, has been defined previously [START_REF] Portalier | Noise behavior of high sensitive GMI-based magnetometer relative to conditioning parameters[END_REF]. It yields

≈ + , , … + (1)
where Bp is the static field working point of the closed loop, b(t), the sensed small signal variation. The term ∂Z21/∂B defines the intrinsic sensitivity, SΩ, of the sensing element expressed in Ω/T and the factor kd is the demodulation gain related to the employed demodulation technique. The terms en(t) and zn(t) are the output noise from the electronic conditioning circuitry and the intrinsic noise, respectively. The latter is expressed as an equivalent impedance variation and could depend on external parameters, like the temperature, and could contain terms showing long time drifts. Their corresponding power spectral densities are en(f) and zn(f) expressed in V/√Hz and Ω/√Hz, respectively.

B. Noise Model

As presented in [START_REF] Dufay | Characterization of an optimized off-diagonal GMI-based magnetometer[END_REF], the equivalent magnetic noise level in the white noise region is mainly due to the electronic conditioning circuitry, en. In such a case, the equivalent magnetic noise level is given by the ratio of the output voltage noise to the magnetometer/sensor sensitivity. So that, increasing the sensitivity is usually a way to improve white noise performances.

At lower frequency, the equivalent magnetic noise spectral density exhibits a 1/f behavior. We have recently proposed that the intrinsic fluctuations of the magnetization direction are responsible of this excess noise [START_REF] Dufay | Low frequency excess noise source investigation of offdiagonal GMI-based magnetometers[END_REF]. These fluctuations could appear in the term zn(t) as long as the sensitivity of the GMI impedance to the magnetization direction is known. In our case, the quantity of interest is the equivalent magnetic noise spectral density which relies on the imaginary part of the magnetic susceptibility, χ'' as previously detailed [START_REF] Dufay | Low frequency excess noise source investigation of offdiagonal GMI-based magnetometers[END_REF]. It yields

⁄ ≈ ′′ ( 2
)
where kB is the boltzmann constant, T the temperature, MS the saturation magnetization of the material, Hint the internal stiffness field, and V the GMI wire volume. Notice that this model is still valid in locked loop mode as noise performances are not modified by the feedback as long as the feedback field loop is properly done. Furthermore, at even lower frequency, long time fluctuations of the sensing element may affect the output response. Obviously, such fluctuations may also be included in the term zn whatever is the physical mechanism responsible of them. Such fluctuations could be due to slow degradations (variations) of the material properties in time or of external influence factors such as the temperature for instance.

III. EXPERIMENTS

A. GMI-based Magnetometer

Measuring long-time fluctuations of a GMI based device requires to use a "true magnetometer" (in the meaning of an instrumentation device) based on a GMI sensing element. This is done when the sensing element is operated in a field locked loop. In such a case, static working point is set and locked by the feedback loop so that the sensing element virtually work in a non-varying magnetic field which is the result of the sum of the external magnetic field to be sensed with the feedback field generated by the feedback loop. Overall principle schematic of the magnetometer is given in Fig. 1. It is based on a classic direct chain essentially relying on an excitation stage and a demodulation stage. The first one feeds the GMI wire with a sine wave excitation current of 10 mApk at an excitation frequency, fc, of 1 MHz. Practically, the excitation signal is generated thanks to a direct digital synthesizer (DDS -AD9102), embedded on the magnetometer board. The demodulation stage is made of a diode peak detector, preceded by an amplifier for impedance adaptation regarding the coil impedance at the excitation frequency. The feedback loop incorporates an operational amplifier in pseudo-integrator configuration insuring that the DC error is removed. It is followed by a resistor and a feedback coil. The latter induces the feedback magnetic field. For integration purpose, the field feedback is done directly through the pick-up coil. The excitation frequency of the sensing element being much higher than the upper limit of the magnetometer band pass ensures correct spectral separation of both signals involved through the pick-up coil. A description of the electronic circuitry is given in [START_REF] Dufay | Characterization of an optimized off-diagonal GMI-based magnetometer[END_REF]. In such setup, noise performances only depend upon those of the direct chain whereas the field feedback sets the linearity range as well as the band pass of the magnetometer. In our case, overall performances of the homemade magnetometer are summarized in Table I.

B. Measurement setup

Long time fluctuations of the magnetometer are monitored by performing acquisition of the output signal during an important amount of time. In our case, we specifically designed a four-channels data acquisition system based on four 24-bits, low-noise, successive approximation register, analog-to-digital converters (ADC) LTC2380, synchronously clocked at a sampling frequency of 735 kHz. The resulting data flow is preformatted by a programmable logic chip (FPGA Xilinx Artix7), achieving the hard real-time constraints, in order to be transferred to a laptop through USB-3.0 protocol without loss of data. With an averaging factor of 1024, the resulting sampling frequency is 718 Hz, with a corresponding data flow of 11 kB/s on the computer hard disk drive. Further data analyses are then performed on the stored data in differed time by postprocessing. Block diagram of the acquisition system is given in Fig. 2. Each ADC is preceded by a low-noise instrumentation amplifier with a programmable gain as to match with several kinds of signals. To validate the setup, the Fig. 3 shows, as an example, the noise power spectral density of our magnetometer obtained from data measured with our acquisition system compared with that obtain thanks to a spectrum analyzer HP3562A (16 bits).

Long time acquisitions are performed in a controlled environment mainly build on a 6-layers magnetic shielded room placed in a tempered area. Simultaneously, the external magnetic field is measured with a commercial fluxgate magnetometer (Bartington MAG03) located near from the GMI magnetometer. Both are battery powered.

IV. RESULTS

Acquisition was performed for a duration time longer 4.5 hours. A reference signal was applied at the beginning and at the end of the acquisition sequence to ensure that the overall experimental setup still properly operates. During the rest of the acquisition time, no magnetic signal was applied. Temporal plot of the acquired data is given in Fig. 4, expressed in units of magnetic induction (T). One can note that the output signal of the GMI magnetometer shows peak-peak fluctuations of 10 nT during this time period. Variations of the surrounding magnetic field are not involved in these fluctuations as the output of the flux-gate magnetometer doesn't exhibit similar behavior.

V. CONCLUSION

A fully embedded GMI-based magnetometer has been designed and characterized. Its performances are fairly comparable to those of its main competitors for low frequency, room temperature, high sensitive magnetometry (particularly fluxgate magnetometers). A dedicated setup has been presented which allows long time acquisition of simultaneous voltage signals with high sampling frequency and dynamic range, suitable for low-noise applications. This setup has been validated against commercial instruments. Finally, acquisitions of long time fluctuations of GMI-based magnetometer has been performed, showing the relative good performance of GMI-based magnetometer. Remaining fluctuations of the output signal is under investigation. Particularly, the effect of the electronic components drift will be explored as well as physical mechanisms involved in the degradation of the GMI material and the effect of the surrounding temperature variations. Furthermore, longer acquisitions are required, such as weeks or months, to fully qualify this magnetometer compared to the state of the art. This would require specific facilities such as magnetic observatory.

Fig. 1 .

 1 Fig. 1. Block Diagram of the magnetometer.

Fig. 2 .

 2 Fig. 2. Block diagram of the acquisition system.

Fig. 3 .

 3 Fig. 3. Equivalent magnetic noise spectral density of the GMI magnetometer. Curve (a) is obtained from spectrum analyzer HP3562A whereas the curve (b) is computed from acquired data with the homemade acquisition system.

Fig. 4 .

 4 Fig. 4. Long time recording of the magnetometer output signal. Curve (a) and (b) are the GMI-based and fluxgate magnetometer outputs respectively and are expressed in Tesla (T) relying on the left axis.

TABLE I .

 I MAGNETOMETER SPECIFICATIONS

	Parameters	Value	Units
	Band-pass	300	Hz
	Sensitivity	241	kV/T
	White noise level	3	pT/√Hz
	Noise level at 1 Hz	100	pT/√Hz
	Dynamic range	± 50	µT