Shengyu Shen
email: syshen@nudt.edu.cn

Ying Qin

Sikun Li
email: skli@nudt.edu.cn

A Faster Counterexample Minimization Algorithm Based on Refutation Analysis

It is a hot research topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. The BFL algorithm is the most effective counterexample minimization algorithm compared to all other approaches. But its time overhead is very large due to one call to SAT solver for each candidate variable to be eliminated. The key to reduce time overhead is to eliminate multiple variables simultaneously. Therefore, we propose a faster counterexample minimization algorithm based on refutation analysis in this paper. We perform refutation analysis on those UNSAT instances of BFL, to extract the set of variables that lead to UNSAT. All variables not belong to this set can be eliminated simultaneously as irrelevant variables. Thus we can eliminate multiple variables with only one call to SAT solver. Theoretical analysis and experiment result shows that, our algorithm can be 2 to 3 orders of magnitude faster than existing BFL algorithm, and with only minor lost in counterexample minimization ability.

Introduction

Model checking technology is widely employed to verify software and hardware system. One of its major advantages in comparison to such method as theorem proving is the production of a counterexample, which explains how the system violates some assertion.

However, it is a tedious task to understand the complex counterexamples generated by model checker. Therefore, how to automatically extract useful information to aid the understanding of counterexample, is an area of active research [START_REF] Ravi | Minimal assignments for bounded model checking[END_REF][START_REF] Jin | Fate and free will in error traces[END_REF][START_REF] Gastin | Minimization of counterexamples in spin[END_REF][START_REF] Groce | Making the most of bmc counterexamples[END_REF].

At the same time, many important verification algorithms need to analyze counterexample (or witness). Some of them are: abstraction-refinement model checking [START_REF] Clarke | Sat based abstraction-refinement using ilp and machine learning[END_REF][START_REF] Glusman | Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation[END_REF] and SAT based image computation [START_REF] Chauhan | Using sat based image computation for reachability analysis[END_REF][START_REF] Mcmillan | Applying sat methods in unbounded symbolic model checking[END_REF][START_REF] Kang | Sat-based unbounded symbolic model checking[END_REF]. In these algorithms, if we can extract a subset of variables that are suf-ficient to lead to counterexample, then these variables can express a large number of counterexamples, not just the individual one generated by model checker. In the remainder of this paper, we call this variable subset as minimization set, and call the algorithm that extract minimization set as counterexample minimization.

Now we demonstrate the concept of counterexample minimization with following example:

For AND gate z = a&b, let the assertion be "z always equal to 1", then there are three counterexamples: {a ⇐ 0, b ⇐ 0, z ⇐ 0}, {a ⇐ 1, b ⇐ 0, z ⇐ 0}, and {a ⇐ 0, b ⇐ 1, z ⇐ 0}. We need nine bits to store these counterexamples.

However, from an intuitive viewpoint, a ⇐ 0 is sufficient to lead to counterexample. So b is an irrelevant variable in this case. At the same time, b ⇐ 0 is also a sufficient condition of counterexample. So a is also an irrelevant variable when b equal to 0. Then we can minimize above three counterexamples, and obtain 2 minimization sets: {a ⇐ 0, z ⇐ 0} and {b ⇐ 0, z ⇐ 0}. We only need four bits to store them.

McMillan [START_REF] Mcmillan | Applying sat methods in unbounded symbolic model checking[END_REF] and Chauhan et al. [START_REF] Chauhan | Using sat based image computation for reachability analysis[END_REF] point out that , directly storing and processing the minimization set, can be exponent efficient than storing and processing the corresponding set of counterexamples.

Thus, a minimized counterexample is easier to be understood, and will significant boost the performance of many verification algorithms.

Ravi and Somenzi [START_REF] Ravi | Minimal assignments for bounded model checking[END_REF] propose a counterexample minimization algorithm called Brute Force Lifting algorithm. We will refer to it as BFL in the remainder of this paper. For every free variable v, BFL construct a SAT instance SAT(v), to determine if v can prevent the counterexample. If result of SAT(v) is UNSAT, then v is irrelevant to counterexample, and can be eliminated. Ravi compares BFL with other counterexample minimization approaches, and concludes that BFL is the most efficient one, it can often eliminate up to 70% free variables.

However, the time complexity of BFL is much larger than all other existing approaches due to one call to SAT solver per candidate variable to be eliminated.

So the key to reduce time overhead of BFL is to eliminate multiple variables after every call to SAT solver Therefore, we propose a faster counterexample minimization algorithm based on refutation analysis in this paper, which employ refutation analysis for UNSAT instances of BFL, to extract all relevant variables and eliminate all irrelevant variables simultaneously.

We implement our algorithm based on zchaff [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF] and NuSMV [START_REF] Cimatti | Nusmv 2: An opensource tool for symbolic model checking[END_REF], and perform experiment on ISCAS89 benchmark suite. Theoretical analysis and experiment result shows that, our algorithm can be 2 to 3 orders of magnitude faster than BFL algorithm, and with only minor lost in counterexample minimization ability.

The remainder of this paper is organized as follows. Section 2 presents background material. Section 3 presents the counterexample minimization algorithm based on refutation analysis. Section 4 presents experiment result of our algorithm and compare it to that of BFL. Section 5 reviews related works. Section 6 concludes with a note on future work.

Preliminaries

Bounded Model Checking

We first define the Kripke structure: Definition 1 Kripke structure is a 6-tuple M = (S, I, W, T, A, L), with a finite set of states S, the set of initial states I ⊆ S, the input variable set W , transition relation between states T : S × W × S → {0, 1}, and the labeling of the states L : S → 2 AP with atomic propositions set AP .

Bounded Model Checking (BMC) [START_REF] Biere | Symbolic model checking using sat procedures instead of bdds[END_REF] is a model checking technology that considers only limited length path. We call this length as the bound of path. We denote the state of the i-th and i+1-th cycle as S i and S i+1 , and transition relation between them as T i (S i , W i , S i+1 ), with input variable set of i-th cycle denoted by W i .

Then we can unfold the transition relation k times, and obtain the following equation:

[[M ]] k = I ∧ 0≤i<k T i (S i , W i , S i+1 ) (1)
Let the safety assertion under verification be ASSERT , the goal of BMC is to find a state S that violate ASSERT , that is to say, ¬ASSERT ∈ L(S). In remainder of this paper, we denote ¬ASSERT as P , and will not refer to ASSERT any more.

Let P at i-th cycle as P i ,then BMC problem can be express as:

F = [[M ]] k ∧ 0≤i<k ¬P i ∧ P k
Because BMC always searches for shortest counterexample, so 0≤i<k ¬P i always holds true. Therefore we can reduce above equation into following equation ( 2):

F = [[M ]] k ∧ P k (2)
Reduce equation ( 2) into SAT instance, and solve it with SAT solver, then a counterexample can be found if it exists.

BFL Algorithm

BFL algorithm proposed by Ravi and Somenzi [START_REF] Ravi | Minimal assignments for bounded model checking[END_REF] can eliminate much more free variables than all existing algorithm, often up to 70% free variables can be eliminated.

We give some terminology below: Definition 2: Assume the bound of counterexample is k, and denote the set of free variables as

F ree = I ∪ 0≤i≤k W i . The assignment to variable v in counterex- ample is denoted by Assign(v), the assignment to vari- able set V in counterexample is denoted by Assign(V ) = {Assign(v)|v ∈ V }.
Obviously, the set F ree includes input variables at all cycle and initial state variables.

For a free variable v ∈ F ree, v is an irrelevant variable if and only if the following statement hold true: "no matter what value does v take on, it can't prevent the counterexample from happen. That is to say, it can't prevent P k of equation (2) from equal to 1". Formal definition of irrelevant variable is given below:

Definition 3 Irrelevant Variable: for v ∈ F ree, v is an irrelevant variable iff: ∀c ∈ {0, 1}.[[M ]] k ∧ (v ⇐ c) ∧ A → P k which is equal to ¬∃c ∈ {0, 1}.[[M ]] k ∧ (v ⇐ c) ∧ A ∧ ¬P k ( 3
)
where

A = F ree -{v} ⇐ Assign(F ree -{v}) (4)
From equation ( 3) and ( 4) we can conclude that:

v is ir- relevant variable iff SAT instance [[M ]] k ∧ A ∧ ¬P k is Un- satisfiable.
Thus, the BFL algorithm [START_REF] Ravi | Minimal assignments for bounded model checking[END_REF] that extracts minimization set from counterexample is show below:

Algorithm 1:BFL Algorithm 1 F " = [[M ]] k ∧ ¬P k a) F = F " ∧ (F ree -{v} ⇐ Assign(F ree -{v})) b) if(SAT Solve(F )==UNSAT)
i F ree = F ree -{v} 3 F ree is the minimization set To make it more distinct, we give the following two definitions:

Definition 4 Model Clause Set: all clauses generated from F" in step 2a) of algorithm 1.

Definition 5 Assignment Clause Set: all clauses generated from (F ree -{v} ⇐ Assign(F ree -{v})) in step 2a) of algorithm 1

We call the former as model clause set, because F " represents inverted model checking problem of equation [START_REF] Chauhan | Using sat based image computation for reachability analysis[END_REF]. We call the latter as assignment clause set because they are used for assigning to all variables their value in counterexample, except v. For every v ∈ F ree -{v}, its assignment clause contain only one literal. If Assign(v ) == 1, then assignment clause of v is {v }, otherwise it is {¬v }. SAT solver will assign these values to them by BCP when solving this instance.

Counterexample Minimization with Refutation Analysis

As stated before, the key to reduce time overhead of BFL is to eliminate multiple variables after every call to SAT solver.

In algorithm 1, when SAT instance F is Unsatisfiable, a variable subset R ⊆ F ree can be extract from it by refutation analysis, which is the sufficient condition of counterexample. Then all variables in F ree-R can be eliminated immediately. Thus we can eliminate multiple variables in this way.

In this section, we first describe the overall algorithm flow in subsection 3.1, and then describe the most important part -refutation analysis in subsection 3.2. We will prove its correctness in subsection 3.3. At last, we will analyze the complexity of this algorithm in subsection 3.4.

Overall algorithm flow

Overall flow of our algorithm is shown by algorithm 2. Algorithm 2 BFL algorithm with refutation analysis Compare it to algorithm 1, steps in 2b) of algorithm 2 are newly inserted steps, which are highlighted with bold font. In step 2b)i, we perform refutation analysis to extract the variables set R that leads to UNSAT. And then in step 2b)ii, we eliminate all variables not belong to R. After that we terminate the whole algorithm by going to step 3 directly.

1 F " = [[M ]] k ∧ ¬P k 2 foreach v ∈ F ree a) F = F " ∧ (F ree -{v} ⇐ Assign(F ree -{v})) b) if(SAT Solve(F )==UNSAT) i R =

Refutation Analysis

As stated by last subsection, we perform refutation analysis to extract the variable set R that leads to UNSAT.

For SAT instance F of algorithm 2, we denote its model clause set by F ", and its assignment clause set by A. After SAT solver finished running, denote its conflict clause set as C.

Refer to last paragraph of section 2.2 of L.Zhang's famous paper about unsatisfiable core extraction [START_REF] Zhang | Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications[END_REF], we have the following theorem 1.

Theorem 1 : If F is unsatisfiable, then there must be a conflict clause at decision level 0, we denote it by c. Because the decision level is 0, so there are no decided variables, any variables can only take on their value by implication.

With this theorem, it is obvious that there must be an implication graph root at unit clauses and target at all literals of conflict clause c. We show this implication graph in figure 1.Every rectangle denote a unit clause, and S is the set of unit clauses that makes all literals of conflict clause c to be 0.

Staring from clause c, we can traverse the implicate graph in reverse direction, to obtain the set of unit clauses S that lead to conflict. We denote the assignment clauses in S by S ∩ A, then the set of variables that lead to con-flict is R = {v|{v} ∈ S ∩ A} ∪ {v|{¬v} ∈ S ∩ A}. This is the key idea of our refutation analysis algorithm. Now we present the refutation analysis algorithm below.

Algorithm 3 Refutation Analysis

1 set S = ∅ 2 queue Q = ∅ 3 foreach literal l ∈ c a) push antecedent clause of l into Q b) mark antecedent clause of l as visited 4 while(Q is not empty) a) cls=pop first clause from Q b) if(cls is a unit clause) i S = S + {cls} ii If(cls is a learned unit clause) return R = F ree -{v} c) else i foreach literal l ∈ cls 1 assume ante(l) is antecedent clause of l 2 if(ante(l) has not being visited) a) push ante(l) into Q b) mark ante(l) as visited 5 R = {v|{v} ∈ S ∩ A} ∪ {v|{¬v} ∈ S ∩ A} are

variables that lead to UNSAT

There is a special case in step 4b)ii, when cls is a learned unit clause, we can't backtrack further because the SAT solver has not record the clauses involved in resolution to construct cls. In this case, we abandon the effort to extract R, and simply return R = F ree -{v}. This means that we can eliminate only one variable v in this case.

Fortunately, we have not met with this special case in experiments. I suspect that this is because of the 1UIP conflict learning mechanism, which seldom generate learned unit clause.

Correctness Proof

We prove the correctness of algorithm 2 and 3 with following theorems: Theorem 2: F " ∧ cls∈S cls is an Unsatisfiable clause subset of F Proof: it is obvious that F "∧ cls∈S cls is a clause subset of F , so we only need to prove that it is Unsatisfiable.

Assume C ⊆ C is the set of learned clauses met with by algorithm 3 while traversing implication graph. Thus, F " ∧ cls∈S cls ∧ cls∈C cls is Unsatisfiable. Then if we can remove cls∈C cls from it, and still retain its unsatisfiability?

For every learned clause cls ∈ C , assume NU(cls) and U (cls) are non-unit clauses set and unit clauses set that involved in resolution to construct cls.

It is obvious that NU(cls) ⊆ F ". And according to [START_REF] Zhang | Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications[END_REF], unit clauses never involve in resolution, so U (cls) is empty set. So we can remove cls∈C cls from F " ∧ cls∈S cls ∧ cls∈C cls, and still retain its unsatisfiability Thus this theorem is proven.

Theorem 3: F " ∧ v ∈R (v ⇐ Assign(v )) is an Un- satisfiable clause subset of F Proof: it is obvious that F " ∧ v ∈R (v ⇐ Assign(v )
) is an clause subset of F . Thus we only need to prove that

F " ∧ v ∈R (v ⇐ Assign(v )) is Unsatisfiable.
According to algorithm 3, v ∈R (v ⇐ Assign(v )) is equal to cls∈S∩A cls. So we only need to prove that F " ∧ cls∈S∩A cls is Unsatisfiable. According to theorem 2, F " ∧ cls∈S cls is Unsatisfiable, which can be rewritten as F " ∧ cls∈S∩A cls ∧ cls∈S-A-F " cls. Lets discuss it in two aspects:

1. If S -A -F " is empty set, then F " ∧ cls∈S∩A cls is Unsatisfiable 2.
Otherwise, S -A -F " isn't empty set. In this case, algorithm 3 will meet with a learned unit clause. According to step 4b)ii of algorithm 3, it will abandon the effort to extract R, and eliminate only one variable v. In the case, F " ∧ cls∈S∩A cls is Unsatisfiable Thus this theorem is proven.

Complexity Analysis

Because our algorithm depends heavily on SAT solver, so we don't analyze its complexity directly. Instead, we compare our algorithm with SAT solver.

Lets first analyze space complexity of our algorithm. Comparing algorithm 2 and 1, the only difference is that algorithm 2 adds a refutation analysis step. Therefore, difference of space complexity between them resides in refutation analysis algorithm. We know that the space overhead of refutation analysis mainly resides in set S and queue Q. Lets analyze them as below:

• We add a tag to each clause in clause database of SAT solver, to indicate that if this clause belongs to set S. Therefore, space overhead of S is linear to size of clause database.

• For queue Q, it may contain conflict clauses. Because conflict analysis algorithm of SAT solver also need to perform similar implicate graph traversing, so space overhead due to Q is not larger than that of SAT solver.

Next, we will analyze the time complexity of our algorithm.

In algorithm 3, the most complex part is the if statement in step 4c)i2. for every clause that has been in Q, this statement will be run once. Because the size of Q is smaller than clause database, so time overhead of algorithm 3 is smaller than that of conflict analysis.

In step 2b) of algorithm 2, one call to refutation analysis algorithm will eliminate many irrelevant variables, thus prevents them from calling SAT solver. This will significant reduce time overhead.

Experiment Result

Ravi and Somenzi [START_REF] Ravi | Minimal assignments for bounded model checking[END_REF] only presents the circuits that used to generate counterexample, but has not presented the assertion used. Therefore, we can't compare our algorithm with his one directly. So we implement his algorithm and ours in zchaff [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF], such that we can compare them with same circuits and assertions.

We use NuSMV [START_REF] Cimatti | Nusmv 2: An opensource tool for symbolic model checking[END_REF] to generate deep counterexample in the following way:

1. Perform reachability analysis to generate state sequence {S 0 , . . . , S k }.

2. Use "S k can't be reached" as an assertion, and put it into bounded model checking package of NuSMV [START_REF] Cimatti | Nusmv 2: An opensource tool for symbolic model checking[END_REF],

we can obtain a counterexample with length smaller than k.

We perform counterexample minimization with BFL [START_REF] Ravi | Minimal assignments for bounded model checking[END_REF] and ours. The timeout limit is set to 20000 seconds.

Experiment result is presented in table 1. The 1st column is the circuits used to generate counterexample. The 2nd column presents the length of counterexample. The 3rd column presents number of free variables.

The 4th column shows the numbers of irrelevant free variables eliminated by K Ravi's BFL [START_REF] Ravi | Minimal assignments for bounded model checking[END_REF]. Divide this column with the 3rd column, we can get the minimization rate shown in 5th column. Run time of BFL is shown in 6th column.

The numbers of irrelevant free variables eliminated by our algorithm are shown in the 7th column. Divide this column with the 3rd column, we can get the minimization rate shown in 8th column. Run time of it is shown in 9th column. The speedup compared to BFL is shown in last column.

From this table, we can conclude that:

1. As shown by last column, our algorithm can be 2 to 3 orders of magnitude faster than BFL;

2. Compare the 4th and 7th column, the number of irrelevant variables eliminated by BFL and our algorithm are of almost the same.

Related Works

Our work is somewhat similar to that of SAT-based image computation [START_REF] Chauhan | Using sat based image computation for reachability analysis[END_REF][START_REF] Mcmillan | Applying sat methods in unbounded symbolic model checking[END_REF][START_REF] Kang | Sat-based unbounded symbolic model checking[END_REF].

McMillan [START_REF] Mcmillan | Applying sat methods in unbounded symbolic model checking[END_REF] propose an SAT solution minimization approach, to extract a partial assignment from SAT solution. His approach needs to construct an alternating implication graph root at input variables. With this graph, he eliminates many irrelevant variables from SAT solution.

Kang and Park [START_REF] Kang | Sat-based unbounded symbolic model checking[END_REF] assign lower decision priority to next state variables, such that when the transition relation is satisfied, as many as possible next state variables are undecided.

Chauhan et al. [START_REF] Chauhan | Using sat based image computation for reachability analysis[END_REF] employ an ATPG-like approach to analyze the dependence relation between input variables and transition relation. And try to eliminate as many as possible next state variables from final solution.

Minimization of counterexamples is useful in the context of abstraction-refinement [START_REF] Clarke | Sat based abstraction-refinement using ilp and machine learning[END_REF][START_REF] Glusman | Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation[END_REF]. Refinement is often more effective when it is based on the simultaneous elimination of a set of counterexamples rather than on elimination of one counterexample at a time.

There are also other approaches to minimize counterexample.

Gastin et al [START_REF] Gastin | Minimization of counterexamples in spin[END_REF] propose an length minimization approach for explicate state model checker SPIN, which try to generate smaller counterexample with respect to their length.

Groce and Kroening [START_REF] Groce | Making the most of bmc counterexamples[END_REF] propose an value minimization approach for CBMC tools, which target at bounded model checking of C language. His approach tries to minimize the absolute value of typed variables of C language.

Conclusions

To make the counterexample easier to be understood, irrelevant variables must be eliminated. At the same time, minimized counterexamples can significant improve the performance of many important verification algorithms.

BFL is the most effective counterexample minimization algorithm. However, its time overhead is too large.

Therefore, we propose a faster counterexample minimization algorithm based on refutation analysis in this paper. Our algorithm can be 2 to 3 orders of magnitude faster than BFL, and with only minor lost in minimization ability.

In this paper we only due with safety assertion, we would also like to address minimization algorithm for loop like counterexample of liveness property in future work.

Acknowledgements

Figure 1 .

 1 Figure 1. implication graph root at unit clauses and target at all literals of conflict clause c

  Supported by the National Natural Science Foundation of China under Grant No. 90207019; the National High Technology Development 863 Program of China under Grant No.

Table 1 . Experiment Result

 1

	2002AA1Z1480

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05)


Alexandre Chureau

Yvon Savaria

El Mostapha Aboulhamid
email: em.aboulhamid@umontreal.ca

The Role of Model-Level Transactors and UML in Functional Prototyping of Systems-on-Chip: a Software-radio Application

Developing a functional prototype of a system-on-chip provides a unifying vehicle for model validation and system refinement. Keeping the prototype executable across several abstraction levels, clock domains and design tools is a key requirement to effective prototyping. This paper presents how model-level transactors address design heterogeneity by unifying event-based and cyclebased worlds from specification to implementation. Transactors are used to build a functional prototype of a software-radio component. An executable UML model is bridged to a hardware abstraction of a radio stream developed with Simulink to implement a realistic and working prototype. Model validation and performance measurements are realized through prototype execution and real-time monitoring.

Introduction

The development of complex systems on chip (SoC) faces a paradox. Developing a system of a reasonable scale requires an extensive analysis and design phase before implementation. But the very nature of these systems is dynamic and intricate, thus requiring some sort of implementation to carry out a knowledgeable and effective design. Hence, it has been accepted that design and implementation are two activities that are profitably carried out at once.

Leveraging this association between design and implementation, the concept of functional prototype has emerged as a means to handle the rising complexity of design. A functional prototype is a machine-executable specification of the system and its operating environment that is used for early system validation. More generally, a prototype is a primitive but working version of the system that can be executed and observed in real-time using real world stimuli.

In electronic design, the prototyping activity ranges from a software specification of the final product to an implementation on a FPGA-based prototyping board. What differentiates a prototype from a simulated model is the ability of the former to work in real-time, maybe at some low but useful performance, and to allow different blocks to execute seamlessly while the system appears as a coherent whole.

The concept has been around since top down methodologies took over ASIC design. Early prototypes have been used for formal specifications and model validation [START_REF] Kemp | The role of functional prototyping in model validation[END_REF][START_REF] Habra | A transformational method for functional prototyping[END_REF]. The functional virtual prototype recently presented by Cadence is at the heart of its proprietary verification methodology [START_REF] Lev | It's about Time: Requirements for the Functional Verification of Nanometer-Scale ICs[END_REF]. This virtual prototype is used as a unifying vehicle expressed at the transaction abstraction level. So far, functional prototyping has been hardware-centric, and meant to represent hardware systems at high level of abstraction. This is becoming inefficient and unnatural, as software plays an increasing role in systems-on-chip. In this paper we make extensive use of the software-centric UML-RT (Unified Modeling Language -Real-Time) to build a more neutral, yet executable, functional prototype of a SoC.

This paper presents a transaction mechanism that enables several levels of abstraction to be represented in a functional prototype built around UML. This leads to:

Matching the expressiveness of a language with the desired level of details across the prototype.

Distributing the development effort among different experts working with different tools.

Providing an executable and unifying specification built in a well accepted modeling language, UML. Model level transactors are used to couple asynchronous components such as behavioral description with synchronous components. Multiple abstraction levels coexist and collaborate through a unifying software backplane described in UML-RT. The resulting prototype is executable, observable and compatible with hardware descriptions and verification environments.

The first section of the paper describes the functional prototype and the role of UML-RT in its development. The next section presents the details of model transactors and their exact role in the prototype. The final section presents how a complete functional prototype was built for a software-defined radio component. Some observations and recommendations conclude the paper.

Prototyping and the Real World

Concept

The functional prototype of an electronic system is an unambiguous executable specification of the system coupled with a realistic test environment. It is built from the paper specification in collaboration with design and verification engineers, as well as application specialists. The executable specification is a model that iterative refinement will transform into a network of collaborating objects, much like the final system. The test environment provides realistic data right from the beginning of the design cycle to allow model observation and validation. It can be put together in the most efficient manner with fourth generation languages and verification IPs. If the proper tools are used, the model will gradually become the system, and the test environment will be reused all along the development, increasing design reuse and productivity [START_REF] Omg | MDA Guide Version 1[END_REF][START_REF] Mcgroddy | SOC -The IBM Microelectronics Approach, Chapter 6, Winning the SoC Revolution[END_REF].

An important aspect of the functional prototype has been purposely left out of this discussion so far: the communication mechanisms between the different parts of the prototype. These mechanisms play a crucial role in preserving the executability of a prototype. One mechanism is necessary to transfer test data between the test environment and the executable model. Another similar mechanism is used by the model to communicate with lower-abstraction components introduced during the refinement, e.g. hard IP cores. The next two sections will describe these important mechanisms in more detail, while the rest of the paper is devoted to their implementation and analysis.

Connecting the World Around

The primary role of the test infrastructure in functional prototyping is to act as the world around the system being developed. The test infrastructure has the following characteristics: 1. It must provide realistic data to the executable model. 2. It is described at high-level of abstraction for speed of development and convenience. 3. It improves controllability and observability over the test scenarios. 4. In some cases, the test infrastructure must act as a placeholder for the analog circuitry that will convey the signal to the system. It is in the context of an executable specification that the importance of testing arises so early: besides the extensive verification that will be performed along the design cycle, test is used early to validate the model. The executable model will respond to stimuli, encouraging test reuse from the executable specification down to implementation.

The connection mechanisms between the test environment and the model should be minimally intrusive in order to stay clear of the model execution and refinement. Extensive interaction between the test and the model might be necessary to feed a model that is dataflow dominated. To allow large amounts of data to be processed, the communication mechanisms should use fast transfer techniques such as shared memory, memory mapped files and sockets.

Connecting the World Below

As model refinement progresses, several clocked components expressed at lower levels of abstraction or described in different models of computations may get involved in model execution. Some hardware components may be used to enhance performance of critical parts or to reuse some existing hardware IP. Eventually, the executable model will reach implementation, meeting all temporal constraints of the application.

Although this is a powerful property of functional prototyping, model heterogeneity raises a communication issue: most hardware functions are synchronized on a clock signal, while the initial model behavior is described in UML using asynchronous operation calls, which leads to some sort of globally asynchronous locally synchronous system. In all cases, preserving the model integrity and executability after the inclusion of these clocked components is a priority. This is part of the challenge of seamlessly connecting the executable model to the world below with model level transactors.

Somewhat similar concepts are found in the Ptolemy project, where a framework enables collaboration of executable models built under different models of computations [START_REF]Overview of the Ptolemy Project[END_REF]. The framework uses domainpolymorphic actors to wrap executable entities and has its own design entry interface. In contrast, model-level transactors live at the boundary of real-time and simulated-time domains, which encompasses model-ofcomputation boundaries. In that sense, model-level transactors are closer to existing design and implementation tools.

The MASCOT methodology [START_REF] Bjuréus | MASCOT: A Specification and Cosimulation Method Integrating Data and Control Flow[END_REF] implements a communication protocol between control and dataflow domains, defined in SDL and Matlab respectively. This co-simulation method is also bound to models of computations, which is an issue efficiently addressed by tool vendors. Mathworks has since launched an integrated tool that manages state machine and dataflow models transparently. The primary issue addressed by model level transactors is how components developed in different time domains (real vs. simulated) can cooperate to form a complete functional prototype. The specificity of tools and vendor methodologies prevent this kind of interaction.

Event-Based UML and SoC prototyping

UML for the Executable Model

The Unified Modeling Language (UML) offers all the objects and diagrams needed to build an unambiguous specification of a SoC. Originally a software modeling tool, UML has recently been extended to model real-time systems, an extension we will refer to as UML-RT [START_REF] Omg | UML Profile for Schedulability, Performance, and Time Specification[END_REF]. Its usage in SoC design is an active field of research [START_REF]UML for SoC Design Workshop at DAC'04[END_REF]. The usage of UML-RT allows building a model of a SoC that is not biased towards a hardware or software implementation. The basic architectural unit is a capsule and its associated state machine, which describe the structure and the behavior of a system respectively.

A capsule is a stereotype of a class that is the equivalent of a VHDL entity, a SystemC SC_MODULE or an independent software execution thread. Some vendors of UML editing tools have implemented efficient model to code translation, which will be used in this paper [START_REF] Harel | Statecharts: A visual formulation for complex systems[END_REF]. Populating the capsule's state machine with platformindependent C++ code produces a complete executable model of the system under development, which can be executed and profiled on different CPUs. In that regard, this approach differs from the Seamless co-verification environment [START_REF] Seamless | [END_REF], which runs software over an instruction-set-simulator (ISS) of the target CPU.

As introduced earlier, this executable model is the entity that must be connected to the test infrastructure as well as to the hardware implementation components used during the refinement. In both cases, the communication mechanism must resolve real-time events vs. cycle-based events, which are two totally different ways to describe the dynamic aspect of a system.

Real-time Events and Cycle-based Events

UML-RT offers state machines inspired from Harel's statecharts [START_REF] Harel | Statecharts: A visual formulation for complex systems[END_REF] to model the behavior of a capsule. These state machines have the following characteristics:

Concurrent: state machines in different capsules can be executed concurrently. Reactive: transitions occur when an event is raised on the capsule's communication ports. Hierarchical: state machines can be nested to simplify behavior modeling Through code generation, these state machines become executable software, where events are operation calls processed in real-time. Although a UML-RT state machine has many advantages to model a system's dynamic aspects, some caveats are observed when interacting with components described in a cycle-based environment. For instance, some cycle-based components rely on registered inputs that are sampled on clock ticks (typical to the discrete-time and discrete-events models of computation). In UML-RT state machines, information is transferred during punctual operation calls and therefore the communication link retains no information. On the other hand, toggling a signal in a cycle-based system does not generate an event by default: an observer must listen passively on the line to capture the state of the signal and react upon a change (defined as the sensitivity of a process). In UML, state machine transitions are actively triggered by a calling system in a one-shot manner.

The test infrastructure will manifest itself to the executable model under a cycle-based form. Since the primary role of the test infrastructure is to represent the world outside, it will include the role of the analog-todigital and digital-to-analog processing happening on the outskirts of the SoC. On a smaller-scale, the test infrastructure can also act as some clocked co-processor available in an IP library and used during system refinement. In either case, it is safe to assume that the real world will communicate with the executable model via clocked samples.

To enable both worlds to communicate efficiently, cycle-based data must translate to active events interpreted by the model's statecharts. We will present a communication mechanism based on a simple clientserver model that solves this problem. In SystemC, transactors are used for transaction-level modeling and verification. They enable transactions from one level of abstraction to the other, inside the same simulated-time environment. A SystemC transactor is a hardware device that, on the software side, communicates at the transactional level, and, on the hardware side, at the signal level [START_REF] Alquier | Co-Simulation Between SystemC and New Generation Emulator[END_REF].

Role of Transactors in Prototyping

This usage of transactors is very hardware-biased, as are models issued from SystemC. Moreover, these transactors are dependent on the SystemC scheduler that controls the timing and order of process execution [START_REF] Osci | SystemC 2.0.1 Language Reference Manual[END_REF]. By contrast, model-level transactors are high abstraction entities with built-in synchronization standing between real-time and simulated time domains. Their implementation handles transactions between a working prototype, running in real-time without the support of a simulator, scheduler or ISS, and another component running under one of these constraints.

As a side note, transactors do not exist in the final implementation of the system. Iterative refinement will transform them into one of the following forms that are relevant in systems-on-chip: drivers or interrupt service routines for softwarehardware interaction; bus slaves and masters or custom signals for hardware-hardware interaction; Application Programming Interface (APIs) for software-software interaction.

Client-Server Model

A server is an entity that responds to a client's requests. Likewise, an embedded application is a processing entity offering a service to clients. If the processing entity is disabled, client requests are denied. If client requests stop, the server will go idle or do some internal business. In this paper, the server is the executable model and the client is the cycle-based test environment. From a hardware refinement perspective, the executable model becomes the client of multiple hardware accelerators seen as servers. This case is a conjugate of the first one and will not be covered here.

The transactor that will enable the communication between these two entities is divided into a server half and a client half that live in the executable model and the cycle-based model respectively. Of course, each half is itself divided in a front-end that is compatible with the model and a back-end that implements the client-server signaling. From this standpoint, different communication scenarios are described in Table 1. Dataflow synchronization between cycle-based and event-based domains relies on the identification of atomic processes in the capsule's state machines. An atomic process is a chain of events occurring between two interactions of the executable model with the clocked model. These interactions may occur every cycle (as assumed in this paper) or span across n clock periods. Determining the value of n can be used as a partitioning metric, which is left as a topic of future research.

Implementing Transactors with Sockets

The Berkeley sockets are an efficient communication mechanism that can be used to implement the back-end of a model-level transactor. On the UML side, the transactor is a capsule connected to the ports of the design, hiding the socket implementation from the model. On the client side, the same socket mechanism is implemented using a client compatible front-end. In Simulink, for example, the client transactor is implemented in a user-defined block called a C++ S-function. This is a special block that can be inserted in a Simulink model to execute custom C++ code during a simulation. When the Simulink scheduler executes the S-Function block, the custom code is executed and all the transactions with the UML-RT model relevant to this cycle are performed. The characteristics of this socket mechanism are:

Communication between the executable model and the clocked component is synchronous and interactive. A socket can act as a signal observer similar to a latch, enabling fine resolution feedback and realistic execution scenarios. The communication overhead is still significant from a real-time perspective, and therefore the capsule transactor must be easy to remove for proper model refinement. Reset signal sent from Simulink to UML

Table 1. Communication Scenarios between Event-Based (Server) and Cycle-Based (Client) Behavior

Server (no handshaking)

Data is sent to the client transactor that monitors the line. The cycle at which data is expected must be known precisely, or an observer must be implemented on the client side.

Processed data returned back to the test environment after n client cycles 2. Server Client

Client (with handshaking)

When the conditions apply, the clocked module that needs data activates a request line on the transactor. A request event is sent to the server and data is returned at a known time.

Simulink retrieves the value of a state register in the executable model

Sporadic signals such as a reset signal expose a limit of a UML-RT model. The delay produced by the translation of the toggle on the line into an event for the capsule state machine is less deterministic than in hardware (c.f. scenario 1.2 in Table I). The granularity of events in the capsule world is a lot coarser than in the cycle-based world and it is the role of the transactor to act as a buffering and recovery mechanism. This leads to an important observation in the usage of UML-RT for integrated systems: a statechart is a high-level construct that cannot profitably imitate the timing granularity of clocked hardware components. Knowing this limit, unnecessary modeling efforts can be avoided.

Case Study

Prototyping of a Software Radio Component

Model-level transactors have been used in the functional prototyping of an adaptive equalizer for a software radio. The prototype will be presented here as a case study. The tool used to build the executable model is Rose-RT from IBM-Rational, which offers efficient model-to-code translation. The UML-RT state machines are detailed using C++ code, which is essential to obtain a complete behavioral model. The generated C++ code is compiled into an executable file and runs on a host station.

The test infrastructure is developed in parallel with Simulink to produce test stimuli and analyze test results. Simulink has numerous pre-built components to generate and analyze radio signals, like QPSK encoders, channel models and constellation scope. The test infrastructure and the executable model of the equalizer, coupled with the appropriate transactor, constitute the first version of a functional prototype, which was up and running in a matter of days.

Experimental Results

The adaptive equalizer has been completely specified using UML-RT capsules, state machines and C++ code realizing the dataflow. Its development is influenced by the fact that the equalizer will eventually be part of a larger software-defined-radio system. A complete test environment has been set up in Simulink by a different team to produce realistic data and to analyze the processing results. Figure 3 presents the block diagram of the complete functional prototype.

The execution of this functional prototype is a two-step process. The UML-RT model is first launched to act as the server. The transactor capsules are created and the server completes its initialization procedure. Then the Simulink test environment is launched and its client transactor issues a connection request to the server transactor. Once the connection is established, the Simulink fixed-step solver starts the cyclic execution of the test environment blocks, producing the test data we need. The diagrams of Figure 4 illustrate the structure of the UML-RT half of the transactor and its connection to the rest of the model.

Figure 5. Test environment in Simulink

A reliable solution to interconnect the client and server halves of the transactor is to implement basic handshaking between the clock-based and event-based domains (c.f. scenario 1.1 in table I). To this end, a ready signal is sent by the executable model when it is ready to receive new data. Blocking TCP sockets were needed to ensure proper synchronization, because of the sensitivity of the prototype to variable speed of execution on different hosts. Indeed, on one type of computer, Simulink waited at each cycle for the executable model to send the ready signal as illustrated in scenario 1 of Figure 6. On a faster computer though, the model ran faster than a Simulink cycle, producing a "ready" signal before the completion of the Simulink cycle, as illustrated in scenario 2. In the first scenario, the clocked transactor socket blocks the execution of Simulink until the "ready" signal is received. In the second scenario, the same socket keeps the "ready"

Figure 6. Execution scenarios on two different computers

The execution of this functional prototype on a Pentium 4 CPU running at 1.7 GHz on a non real-time OS has allowed us to reach a sample period of 32 µs for basic BPSK modulation, or 62.5 kbps. Although the code could be optimized to reach a higher rate or the modulation changed to higher density, this rate would be enough to handle digital voice communication over a radio channel.

Figure 7 was traced dynamically by Simulink with data gathered on the fly from the executable model. It represents the evolution of mean square errors (MSE) vs. time in an adaptive equalizer. This kind of analysis was extremely useful in the validation and refinement of the specification of the system.

Observations and Conclusion

Transactors allow breaking tool barriers and implementing functional prototypes that can be tested in a virtual simulated environment, and then run under realistic conditions. To achieve an accurate stimulation of the system, a Simulink model was used as a test environment to produce realistic radio channel data. The coupling of a UML-UML model to the Simulink tool with model level transactors allowed a functional and inter-active prototype of a system to be built.

The hardware implementation components that can be introduced in a UML-RT model will eventually use different communication means such as an AMBA-AHB bus, interrupt pins or custom protocols. Somehow, the transactor should be transformed into one of these hardware implementations, like a bus protocol. Modeling such communication infrastructure is left for future investigation. Another interesting issue is the exchange of fixed-point data with clocked components. Fixed-point data format are used in hardware systems where data lines have finite widths. The translation from fixed-point to floating point is another functionality which could be implemented in the model-level transactors.

This work opens a variety of opportunities to bring high-level modeling and functional prototypes closer to hardware implementations.

Figure 1 Figure 1 .

 11 Figure 1. Overview of the functional prototype

4. 1 .

 1 Model-Level Transactors vs. Transaction-Level ModelingIt is first important to define what a transactor is in the context of our work, and how it relates to other usage of the concept. A transactor enables communication between simulated-time and real-time components. Model-level transactors are used in the UML-RT model as capsules that communicate with clocked or cycle-based models running in simulators. Figure2depicts the location of transactors in the functional prototype.

Figure 2 .

 2 Figure 2. Location of transactors (Tr)

  requires information from a client, it sends a message on its transactor. A client transactor is observing this trigger on the cycle-based side. The information is sent back to the server UML capsule ready to receive tick, the client transactor checks for a change in a given signal state. If a change is detected, a message is sent to the server through the transactor. The transaction requires polling or interruption on the server side.

Figure 4 .

 4 Figure 4. Key UML structure diagrams On the Simulink side, the client transactor is implemented in a user-defined S-function block, as shown by the model snapshot of Figure. 5.

6 Figure 7 .

 67 Figure 7. Mean-square error vs. time

Simulink Top UML-RT Top Capsule

		Test Environment		Executable Model
		SDR Receiver
	BPSK Source	Rummler Model Channel	C	Sink	S	Equalizer
		Ref eq	Ref dec		Legend: C/S	Client / Server Transactor
						TCP Connection
	Figure 3.

Functional prototype built with Simulink, UML-RT and transactors signal

  in a queue until it is sampled at the beginning of a cycle. It is interesting to note that only the first scenario will provide continuous real-time bit rates, since the executable model runs at its maximum speed. In the second scenario, the bit rate is artificially slowed down by the unrealistic execution time of Simulink, which prevents measurement of a continuous real-time bit rate.

		Scenario 1 : Simulink runs		Scenario 2 : the model runs
		faster than the model		faster than Simulink
	::ClockBasedTransactor	::EventBasedTransactor	::ClockBasedTransactor	::EventBasedTransactor
	Cycle					READY
	Tick	IDLE	READY	Tick Cycle	DATA	IDLE
			DATA		RESULT
			RESULT		READY
	Cycle
	Tick	IDLE	READY	Cycle Tick	DATA	IDLE

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Acknowledgements

Academic licenses of tools provided by IBM and Mathworks enabled this research. Philippe Dumais, Stéphane Cormier, Olivier Munger, members of the MAME team at École de Technologie Supérieure in Montréal, developed the Simulink test environment under the guidance of Professor François Gagnon, team leader of the Prompt project that supports this research.


Petri Kukkala

Jouni Riihimaki

Marko Hannikainen

Timo D Hamalainen

Klaus Kronlof

Jouni Riihimäki

Marko Hännikäinen

Timo D Hämäläinen

Klaus Kronlöf

UML 2.0 Profile for Embedded System Design

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The development of modern embedded systems requires reducing the gap between traditional hardware and software designs. Unified Modeling Language (UML) is widely used in software development, but now it is emerging in embedded system design. Especially the latest release of the language, UML 2.0 with its extension proposals, brings several advanced features to support also this domain. UML 2.0 holds a promise of a general design language that can be understood by system designers as well as software and hardware engineers.

This paper presents a new UML 2.0 profile, called TUT-Profile. TUT-Profile defines a set of stereotypes for extending UML metaclasses as well as design practices to describe applications, platforms, and mapping of them. It is especially targeted to automated system implementation using only UML 2.0 description. For this reason, TUT-Profile is used with a set of tools as depicted in Figure 1. Tools include Telelogic TAU G2 and a new custom UML profiling tool. Currently the physical target hardware platform is composed of Altera NIOS soft core processors and HIBI interconnection network [START_REF] Salminen | HIBI v.2 Interconnection for Systemon-Chip[END_REF] on single FPGA. However, the profile will not limit the type of platform and its components.

In this paper, we focus on the TUT-profile and demonstrate its use with a real implementation. In the next section, we start with highlighting the use UML 2.0 in embedded system design and give a brief review of related research. In addition, the TUT-Profile based design flow is briefly presented. Section 3 gives a detailed description about the stereotypes of TUT-Profile. Section 4, in turn, demonstrates the TUT-Profile in the design and profiling of a Wireless Local Area Network (WLAN) terminal. Finally, Section 5 concludes the paper.

UML 2.0 in Embedded System Design

A set of UML key properties can be identified for embedded system design [START_REF] Martin | UML for Embedded Systems Specification and Design: Motivation and Overview[END_REF]. One of the major advantages is that UML is not only a single language, but it allows the creation of languages for different purposes. To adapt UML 2.0, for example to different application and platform domains, sophisticated extension mechanisms are provided by the language.

Extension mechanisms in UML 2.0 can be roughly divided into first-class and second-class extensibility. The first-class extensibility is handled through the Meta Object Facility (MOF). This approach allows modifications on the existing metamodels and creating new metamodels with no restrictions.

The second-class extensibility does not allow modifications on existing metamodels. Instead, it enables adapting metamodels on specific purposes by extending existing metaclasses. The adaptations are defined using stereotypes, which are grouped in a profile. A profile contains constructs that are specific to a particular domain, platform, or method.

TUT-Profile utilizes only the second-class extensibility, which is considered to be powerful enough for applying UML 2.0 for embedded system design. Compared to the first-class extensibility, the use of stereotypes is a more lightweight mechanism, as it maintains the basic concepts and properties of the standard UML 2.0. Consequently, this leads to better tool support.

Related Research

A number of extension proposals have been presented for real-time and embedded system design. The proposals can be roughly divided into three categories: system and platform design, performance modeling, and behavioral design. Next, the main related proposals are presented.

The Embedded UML [START_REF] Martin | Embedded UML: a Merger of Real-Time UML and Co-design[END_REF] is a UML profile proposal suitable for embedded real-time system specification, design, and verification. It represents a synthesis of concepts in hardware/software co-design. It presents extensions that define functional encapsulation and composition, communication specification, and mapping for performance evaluation.

A UML Platform profile is proposed in [START_REF] Chen | UML for Real: Design of Embedded Real-Time Systems[END_REF], which presents a graphical language for the specification. It includes domain-specific classifiers and relationships to model the structure and behavior of embedded systems. The profile introduces new building blocks to represent platform resources and services, and presents proper UML diagrams and notations to model platforms in different abstraction levels.

The ACCORD/UML profile [START_REF] Tessier | A Component-based Methodology for Embedded System Prototyping[END_REF] defines a methodology for model mappings during the different development stages. ACCORD/UML proposes a real-time modeling based on the real-time active objects. The modeling features introduced by the ACCORD/UML method define a set of modeling rules involving model transformation techniques.

The UML Profile for Schedulability, Performance and Time (or the Real-time UML Profile) is standardized by OMG [START_REF] Omg | UML Profile for Schedulability, Performance, and Time Specification[END_REF]. The profile defines notations for building models of real-time systems with relevant Quality of Service (QoS) parameters. The profile supports the interoperability of modeling and analysis tools. However, it does not specify a full methodology, and the profile is considered to be very complex to utilize.

The UML-RT profile [START_REF] Selic | Using UML for Modelling Complex Real-Time Systems, White Paper, Rational[END_REF] defines execution semantics to capture behavior for simulation and synthesis. The profile presents capsules to represent system components, which internal behavior is designed with state machines. The capabilities to model architecture and performance are very limited in UML-RT, and thus, it should be considered complementary to the Real-time UML profile. HASoC [START_REF] Green | The Modelling of Embedded Systems Using HASoC[END_REF] is a design methodology that is based on UML-RT. It proposes also additional models of computation for the design of internal behavior.

These proposed profiles contain several features for utilizing UML in embedded system design, but they miss the completeness for combining application and platform.

TUT-Profile Approach

TUT-Profile extensions are used to define the structure and parameters of an application and platform as well as their mapping. Correspondingly, the system design is divided into three parts: application description, platform description, and mapping. Both the application and platform descriptions can be developed independently of each other.

TUT-Profile mainly concerns the structure of an application and platform. The application is seen as a set of active classes with an internal behavior. The platform is seen as a component library with a parameterized presentation in UML 2.0 for each library component. The profile does not restrict the behavioral modeling, and by default, it utilizes standard UML 2.0 concepts for this.

TUT-Profile classifies different application and platform components by defining various stereotypes and strict rules how to use them. The objective is to enhance the support of external tools for automatic analyzing, profiling, and modifying the UML 2.0 description of an embedded system. The classification also assigns defined parameters to proper components.

In practice, the profile is applied in a tool framework depicted in Figure 2. The platform mapping can be explicitly performed by the designer, or assisted with tools. For the latter, we have developed a UML profiling tool that combines the UML 2.0 description (model parsing) and simulation statistics (simulation log-file) that is obtained during the verification phase. Based on the profiling, also the application description can be modified for example to fulfill real-time constraints. When the verification is completed, executable application for the implemented platform is automatically generated from the UML 2.0 description.

TUT-Profile Stereotypes

TUT-Profile contains several stereotypes to support embedded system design. The structure of the TUT-Profile is presented in Figure 3. An application is composed of application components, which are instantiated as application processes. Next, application processes are grouped into process groups.

Correspondingly, a platform is composed of platform components, which are instantiated as platform component instances. Finally, process groups are mapped to platform component instances using platform mapping. The summary of the profile stereotypes is presented in Table 1.

Application Description

Application stereotypes are applied to an application description containing a platform independent structure and behavior of an application. The application stereotypes mainly concern the structure and parameterization, as the TUT-Profile does not extend the behavioral modeling.

The application stereotypes classify the different types of classes and parts used in an application description. The parameterization of an application is performed using tagged values. The parameters may be manually added by a designer, or automatically derived from the behavioral part of the application description by the profiling tool. Process grouping is a part of an application description and it defines the structure for an application. The structure is implementation-oriented and may thus differ from the composite structure of an application. However, the grouping is platform independent as process groups do not represent any specific platform components.

The grouping can be performed according different criteria, such as the preliminary scheduling of application processes, workload distribution, communication between process groups, dependencies between process groups, and size of a process group (code size, memory requirements). The grouping is used for the analysis and architecture exploration, which can be performed using simulations or static analysis. The composed groups are mapped to platform components specified later.

The grouping can be fixed either at the level of a single process, or at the level of a process group. In the latter case, processes cannot be added or removed from a group. Currently, the grouping is done manually by the designer, but tools for automatic grouping according to the profiling information and process types will be implemented.

Platform Description

The platform description is more abstracted compared to the application description. The platform description is not targeted for functional synthesis of hardware, but it is used for composing a platform containing components using an existing platform library. In TUT-Profile, properties, capabilities, and limitations of a component are parameterized. The summary of tagged values in platform stereotypes is tabulated in Table 3.

The parameterized description models are used to perform a high-level hardware/software co-simulation. In that case, the execution of application processes is guided with the properties of the platform components.

The stereotype <<Platform>> is applied to define the top-level class of a platform description, composed of available platform components. Platform components and their parameterization can be refined by the further specialization of platform stereotypes.

In the platform description, the communication between active platform components, called processing elements, is performed via communication elements. Communication elements are implemented as communication wrappers that are used to connect processing elements to communication segments.

Mapping

When both an application and platform description have been defined, each group of application processes is mapped to a platform component instance. Mapping is performed by defining a dependency between a process group and a platform component instance. In order to account performance issues, the performance related parameterizations specified in the application and platform descriptions are combined.

The stereotype <<PlatformMapping>> is applied to describe how a process group is mapped to a platform component. When the mapping is fixed (indicated by a tagged value), it cannot be changed automatically by profiling tools during the design process. This can be used when a designer knows that a certain process group has to be placed into a certain processing element.

TUT-Profile Case: WLAN Terminal

This section presents TUT-Profile utilization with the design of a custom WLAN terminal. The examples show how UML 2.0 diagrams are used with TUT-Profile, and how the stereotypes are applied in design.

The application is a custom Medium Access Control (TUTMAC) protocol [START_REF] Kukkala | UML 2.0 Implementation of an Embedded WLAN Protocol[END_REF] of a proprietary WLAN (TUTWLAN) [START_REF] Hännikäinen | TUTWLAN -QoS Supporting Wireless Network[END_REF]. The TUTMAC protocol has been modeled with UML 2.0 meeting the TUT-Profile, and the software parts of the protocol have been implemented with the automatic code generation for the platform. The platform is Altera Stratix FPGA with NIOS soft processor cores. In addition, the platform library contains implementations of some time critical algorithms, such as Cyclic Redundancy Check (CRC), that can be used for hardware acceleration of protocol functions.

TUTMAC Application Description

The design of an application description starts from the definition of the class hierarchy. The top-level application class and its components are created, and the associations between components are defined. A TUTMAC class diagram is presented in Figure 4.

The Tutmac_Protocol class is the top-level class of the application. Thus, it is stereotyped as <<Application>>. The class is composed of five classes. The

Management, RadioManagement

and RadioChannelAccess classes are functional components containing behavior, and can be instantiated as application processes. Thus, they are stereotyped as <<ApplicationComponent>>. The UserInterface and DataProcessing classes are structural components having composite structure without behavior. Consequently, they can not be instantiated as application processes, and are not stereotyped. Table 3. Tagged values of platform stereotypes. In Figure 5, the mng, rmng and rca parts are instances of the functional components stereotyped as <<ApplicationComponent>>.

Tagged values Description

Stereotype <<PlatformComponent>>

Type

They represent the processes of the application, and are thus stereotyped as <<ApplicationProcess>>. ui and dp parts are instances of the structural components, and therefore they do not represent processes.

The structural components are hierarchically modeled using class diagrams and composite structure diagrams, until the behavior of the functional components can be expressed. The behavior of the functional components in TUTMAC is described using statechart diagrams combined with the UML 2.0 textual notation. TUTMAC statecharts are modeled as asynchronous communicating Extended Finite State Machines (EFSM).

The TUTMAC application description is finished by grouping the main processes as depicted in Figure 6. The objective in grouping has been to minimize the communication between process groups, which enhances the performance if groups are mapped to different processing element.

TUTWLAN Platform Description

When describing hardware the designer selects suitable components from the TUT-Profile library and connects components together. Figure 7 presents a platform description for the TUTWLAN terminal containing four processing elements connected with three communication segments. Three of the processing elements are similar NIOS processors. The fourth is a hardware accelerator for CRC-32 calculation.

The employed communication channel is a HIBI bus [START_REF] Salminen | HIBI v.2 Interconnection for Systemon-Chip[END_REF]. For HIBI, the platform stereotypes are specialized, thus including more detailed information of the platform specific communication elements. The specialized stereotypes are <<HIBIWrapper>> from <<CommunicationWrapper>>, and <<HIBISegment>> from <<CommunicationSegment>>. The specialized information contains sizes of buffers, bus arbitration, and addressing.

The communication between processing elements is carried out through a hierarchical bus structure. As presented in Figure 7, processor1 and processor2 are connected to the same bus segment called hibisegment1, which is connected to a bridge segment. The remaining two processing elements, processor3 and accelerator1, are connected to hibisegment2, which is also connected to a bridge segment.

Mapping of TUTMAC to a Platform

The mapping in Figure 8 integrates the TUTMAC application description and the platform description of a TUTWLAN terminal. As seen, two process groups, group1 and group3, are mapped to processor1. This indicates that the designer prefers the processes of the two process groups to be implemented on the same processor, although they were divided into separate process groups in the application description. group4 has processes that can be implemented on an existing hardware accelerator, and thus, the process group is mapped to accelerator1.

Profiling TUTMAC Description

The profiling tool implemented for TUT-Profile contains three main stages that are implemented as TCL scripts. First, the XML presentation of the UML 2.0 model is parsed to gather process group information from the model. Next, the automatically generated application code is complemented with custom C functions to create simulation log-file during simulations. These phases are shown in the design flow presented in Figure 2.

Finally, after simulation, the profiling data in the simulation log-file and the process group information are combined and analyzed. The results are gathered to a profiling report. An example profiling report based on the TUTMAC simulations on the workstation processor is presented in Table 4. The report contains the execution times of the process groups (a), and the amount of communication between the groups (b). In addition, other metrics, such as transfers between individual application processes, are also available.

The report is used for improving the application description. The process groups and mapping are modified to improve performance including amount of communication and the division of workload between application processes. Further, the profiling report can be used to refine the parameterization of the application description as the performance information is gathered with simulations on a reference platform, such as a PC workstation.

Conclusions

This paper presents the TUT-Profile for embedded system design with UML 2.0. The TUT-Profile concentrates on the structure and parameterization of an application and platform, and the mapping of these.

The case design with a TUTWLAN terminal demonstrated the use of TUT-Profile in practice. The example illustrated the use of UML 2.0 diagrams, and the applying of the stereotypes. TUT-Profile and the profiling tool were used to improve performance of TUTMAC by minimizing the communication between process groups.

In the future, the TUT-profile will further be developed by the specialization of the stereotypes and the improvement of parameterization. The profile will also be evaluated for multiprocessor System-on-Chip co-design environment. In addition, real-time operating system will be used in system processors, which will also be accounted in the TUT-Profile.

Figure 1 .

 1 Figure 1. Design flow with TUT-Profile.

Figure 2 .

 2 Figure 2. TUT-Profile design and profiling flow.

Figure 4 .

 4 Figure 4. TUTMAC class diagram of an application description.

Figure 5 .

 5 Figure 5. Composite structure diagram of Tutmac_Protocol class in the TUTMAC application description.

Figure 6 .

 6 Figure 6. TUTMAC process grouping using composite structure diagram.

Figure 7 .

 7 Figure 7. Stereotyped composite structure diagram for an example TUTWLAN platform.

Table 2

 2 tabulates the tagged values for each application stereotype in TUT-Profile.The stereotype <<Application>> is applied to define the top-level class of an application description. The toplevel class has a class hierarchy defining different classes of an application. The active classes having behavior are called functional components. Passive classes are structural components, which do not have behavior, but instead, define composite structures and data structures storing application data.

Table 1 .

 1 TUT-Profile stereotype summary.

	Stereotype name	Description
	(extended Metaclass)
	Application (Class)	Top-level application class
	ApplicationComponent	Functional application component
	(Class)	(active class, has behavior)
	ApplicationProcess	Instance of a functional application
	(Structural feature)	component
	ProcessGroup	Group of application processes
	(Structural feature)
	ProcessGrouping	Dependency between an application
	(Dependency)	process and a process group
	Platform (Class)	Top-level platform class
	PlatformComponent	Defines features of a platform
	(Class)	component
	PlatformComponentInstance	Instantiated platform component
	(Structural feature)
	CommunicationWrapper	Defines wrapper parameters of a
	(Dependency)	communication agent
	CommunicationSegment	Interconnection structure of
	(Structural feature)	communicating agents
	PlatformMapping	Dependency between a process group
	(Dependency)	and a platform component instance

Table 2 .

 2 Tagged values of application stereotypes.

	Tagged values	Description
		Stereotype <<Application>>
	Priority	Execution priority of an application
	CodeMemory Required memory for application code
	DataMemory	Required memory for application data
	RealTimeType Type of real-time requirements (hard/soft/none)
		Stereotype <<ApplicationComponent>>
	CodeMemory Required memory for application component code
	DataMemory	Required memory for application component data
	RealTimeType Type of real-time requirements (hard/soft/none)
		Stereotype <<ApplicationProcess>>
	Priority	Execution priority of application process
	CodeMemory Required memory for application process code
	DataMemory	Required memory for application process data
	RealTimeType Type of real-time requirements (hard/soft/none)

ProcessType

Type of process (general/DSP/hardware)

Stereotype <<ProcessGroup>>

Fixed Defines if the group is fixed (true/false) ProcessType Type of processes in a group (general/DSP/hardware)

Stereotype <<ProcessGrouping>>

Fixed Defines if the grouping is fixed (true/false)

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05)

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Acknowledgements

The research work for the TUT-profile and custom tools has been carried out as part of ITEA (Information Technology for European Advance) project "Prompt2Implementation" (ITEA 010009) at Tampere University of Technology (TUT).


Célestin Matte

Mathieu Cunche

Vincent Toubiana

Does disabling Wi-Fi prevent my smartphone from sending Wi-Fi frames?

Keywords: Wi-Fi, tracking, Android, iOS, iPhone, privacy Wi-Fi, traçage, Android, iOS, iPhone, vie privée

No. For Android, we show that another option, called "Always allow scanning", when activated, makes a device send Wi-Fi frames which can be used to track this device, even if the Wi-Fi switch is off. This option is not clearly described in all Android versions, and sometimes very hard to find. Besides, the Google Maps application prompts the user to activate this option. Similarly, for iOS 11, the Wi-Fi switch in the control center does not prevent Wi-Fi frames from being emitted by some services.

Est-ce que la désactivation du Wi-Fi empêche mon smartphone d'émettre des trames Wi-Fi?

Introduction

Wi-Fi signals emitted by mobile smartphones can be exploited to passively track users' mobility [START_REF] Musa | Tracking Unmodified Smartphones Using Wi-fi Monitors[END_REF][START_REF] The | How stores use your phone's WiFi to track your shopping habits[END_REF]. Turning off the Wi-Fi interface of the device is often presented as a mean to evade those tracking systems 1 . As a matter of fact this method is sometime suggested by the actors of the Wi-Fi tracking industry as a way to opt-out from those systems2 .

The Android system features an option to enable or disable Wi-Fi on the device. However, disabling Wi-Fi through this option is not sufficient to prevent all Wi-Fi activity of the device [START_REF]Stop android 4.3 from always scanning for wi-fi networks[END_REF]. Similarly, iOS possesses a control center allowing to quickly switch Wi-Fi on or off. In iOS 11, this switch does not prevent the phone from scanning anymore3 . We performed several measurements that confirm this behavior on a range of Android and iOS devices.

2 Wi-Fi on Android

Android Wi-Fi scans

The Android system supports Wi-Fi in order to provide network connectivity. As any other Wi-Fi-enabled system, Android relies on Wi-Fi service discovery mechanisms to detect Wi-Fi access points in range. Unlike what is commonly expected [START_REF]Android scan forum[END_REF], as most mobile systems, Android rely on active service discovery, a mechanism in which the device actively searches for nearby access points. To do so, the device perform scans during which it sends wireless inquiries called probe requests containing its own -and often unique -MAC address. Access points reply to those requests through probe responses, revealing themselves to the device.

Nowadays, Wi-Fi service discovery is also used to get location information. Wi-Fi access points, identified by their unique BSSID (a MAC address), are used as landmarks. Aided by a Wi-Fi-based location engine, a location can be derived from a list of access points detected during a Wi-Fi scans. In Android, Wi-Fi scans are used to enable both network connectivity, and location [START_REF]Android location strategies[END_REF].

However, Wi-Fi scans are not only used by the device to derive its location, analytics companies now leverage the Wi-Fi probe requests to estimate the number of visitors in stores and malls and to record customer mobility. Indeed, by counting the number of unique MAC addresses broadcast in probe requests, retailers can derive the number of smartphone carriers in their store. Location tracking of these customers is performed by following these MAC addresses as they are heard by antennas located in different spots.

Wi-Fi-related settings in Android

The Android system includes a number of configuration options that can impact the Wi-Fi activity of the device. The most obvious one is the Wi-Fi switch (see Figure 2a). When this switch is activated, the Wi-Fi interface can be fully used by the operating system and the application (provided that they have sufficient permissions). When the switch is off, network connection through Wi-Fi is unavailable and application cannot access the result of Wi-Fi scans.

A second option called "Always allow scanning" (see Figure 2b), or "scanning always available", allows the device to perform Wi-Fi scans even if the Wi-Fi switch is off. The description of this option is the following: "Let Google Location Service and other applications scan for Wi-Fi networks, even when Wi-Fi is off" (see Figure 2b). On the Android 4.4.4 of a Samsung Galaxy S3 and the Android 4.3 of a Nexus S, this option is located in System → Wi-Fi → Advanced whereas on the Android 7.0 of a Lenovo Moto G 5, this option is located in Settings → Location → Scanning. On the Android 6.0.1 of a OnePlus One, this option is very hard to find 4 . In order to deactivate it, users have to go to Settings → Location, then click on the small dots on the upper right of the screen (see Figure 1), then click on Scanning → Wi-Fi scanning. Tests described later in the paper indicate that the option is activated.

Wi-Fi in iOS 11

On iOS 11, the Wi-Fi switch in the Control Center does not deactivate Wi-Fi anymore. Similarly to the Android case, Wi-Fi remains active for some applications, including location services. This behaviour is officially documented 5 . In order to actually disable Wi-Fi, users have to turn it off in the parameters (see figure 3).

Analysis of generated Wi-Fi activity

A total of 8devices covering a Android versions ranging from 2.2.1 to 6.0.1 . The devices considered in this study are the following:

• Galaxy S3: Samsung Galaxy S3 (GT-I9...), Android 4.4.4

• Galaxy Tab E: Samsung Galaxy Tab E (SM-T560), Android 4.4.4 We also tested an iOS device:

• iPhone 6 model MG472ZD/A, iOS version 11.0.3.

Inria

Experimental protocol

We monitored the Wi-Fi traffic generated by each smartphone in different configurations and under different types of activities. Devices were never associated to an access point. Monitoring was performed using a Wi-Fi interface set in monitoring mode and capturing the traffic on a fixed channel. The source MAC address of the collected Wi-Fi frame was used to detect traffic generated by a device. Indeed, all Wi-Fi frames emitted by those devices include their MAC address in the frame header 6 . Several configuration options have been considered:

• Wi-Fi switch: the option controlling the activation of Wi-Fi.

• Always allow scanning: the option allowing Wi-Fi scans when the Wi-Fi is off.

• Location: the option controlling the location feature. In some devices, the option is divided into 2 options: GPS geolocation and cellular/Wi-Fi geolocation. We only considered the latter.

Several activities, reflecting a typical usage were considered:

6 These devices do not support MAC address randomization.

RR n°9089

• Screen on: the screen is on and the device is kept in this state by switching between panels for a few minutes.

• Idle: the device is left untouched for at least 5 minutes after the screen has automatically turned off.

• Leaving idle: the device is put out of idle mode by touching the power key.

• Google Maps: the Google Maps application is running on the device.

• Starting Google Maps: the Google Maps application is started by the user.

• Uncorrelated: when the event happens without any obvious correlation with the user activity.

For each device and for each combination of the previous options, the Wi-Fi traffic was captured while the device was put through the different type of activity.

All devices except the OnePlus One and the Galaxy S3 had no other source of Internet connection.

Measurement results

Results of the measurements are presented in Tables 1, 3, 4, 5 and 6. During those measurements, only frames of probe request type were generated by the device.

Galaxy S3

The measurements show that the Wi-Fi activity depends on all three parameters: "Wi-Fi switch", "Always allow scanning" and "Location". Obviously, when Wi-Fi is activated, the device sends Wi-Fi frames at any time and in particular when leaving the idle mode.

Starting Google Maps also triggers the emission of probe requests, but only if Location is activated. Probing is observed both when Google Maps is running or not.

An important observation is that disabling Wi-Fi does not necessarily prevent Wi-Fi activity. For instance, if "Always allow scanning" and Location are both activated, Wi-Fi traffic will be generated when Google Maps is used. This is likely due to the use of Google Wi-Fi-based location engine.

Total lack of Wi-Fi activity was observed in only two configurations when both Wi-Fi and "Always allow scanning" were disabled, regardless of the Location option.

When both Location and Wi-Fi are disabled but not Always allow scanning, we observed Wi-Fi scan events for which we were unable to associate any specific activity on the device. In other words, those scan events seems to happen regardless of the activity on the phone. It is not clear what the purpose of those scans is.

OnePlus One

Results for the OnePlus One, presented in Table 3 are similar to the ones of the previous device. One difference subsists: when both the Wi-Fi switch and the location option are off, the device still sends a burst of probe requests each time it leaves idle mode. Reasons for this behavior aren't clear.

Inria

Wi-Fi switch off off off off on on on on Always allow scanning off off on on off off on on Location off on off on off on off on Summary

× × Screen on × × × Idle × × × × Leaving Idle × × × × Google Maps × × × Starting Google Maps × × × × × Uncorrelated
Table 1: Wi-Fi activity generated in various settings for the Galaxy S3 (with SIM Card).

Wi-Fi switch off off off off on on on on Always allow scanning off off on on off off on on Location off on off on off on off on Summary

× × × Screen on × × × × Idle × × × × × × Leaving Idle × × × × Google Maps × × × × × Starting Google Maps × × × × × × Uncorrelated
Table 2: Wi-Fi activity generated in various settings for the Galaxy Tab E (without SIM Card).

Wi-Fi switch off off off off on on on on Always allow scanning off off on on off off on on

Location off on off on off on off on Summary × × Screen on

× × × × Idle × × × Leaving Idle × × Google Maps × × × Starting Google Maps × × × × × × × ×
× × × Idle × × × × Leaving Idle × × × Google Maps × × × Starting Google Maps ×* × ×* × × × × ×
Table 4: Wi-Fi activity generated in various settings for the Nexus S. *Device immediately prompts for the user to activate location. Clicking "OK" does so. **The device, however, sends a burst of probe requests upon activating or deactivating the "always allow scanning" option.

Nexus S

Results for the Nexus S, presented in Table 4, only reveal minor differences with the Galaxy S3. One notable behavior is that, even with Wi-Fi switch and location option turned off, the device sends a burst of probe requests every time the "always allow scanning" option is toggled.

HTC WildFire and Galaxy Spica

Results for the HTC WildFire, presented in Table 5, are not surprising. In this early version of Android where the "always allow scanning" option did not exist, probe requests are sent if and only if the Wi-Fi switch is on. Results for the Samsung Galaxy Spica are not included because very similar, with the only difference that the device was not seen sending probe requests in idle mode or when leaving it.

Moto G5 Plus

Results for the Lenovo Moto G5 Plus are presented in Table 6. It uses a slightly customized version of Android 7.0 and randomization behavior is surprising: the device seems to randomize the MAC address only when probing in idle mode. The "Always allow scanning" is accessible through the Wi-Fi settings but only when Wi-Fi is off and permanently through the "Location settings".

× × × × Screen on × × × × Idle × × × × Leaving Idle × × × × Plans × × × × Starting Plans × × × × × ×
Table 8: Wi-Fi activity generated in various settings for the iPhone 6.

Moto G5S Plus

Results for the Motorola Moto G5S Plus are presented in Table 7. It uses a slightly customized version of Android 7.1.1. We note that, with this model, launching Google Photos systematically causes a burst of probe requests, in more cases than the "Starting Google Maps" one.

iPhone 6

Results for the iPhone 6 are presented in table 8. It appears that, as officially documented by Apple, the Wi-Fi switch in the control center does not prevent the device from sending probe requests, provided Wi-Fi is activated in the parameters. It is also true when location is turned off. If Wi-Fi is switched off in the parameters, no probe request is detected.

Summary of the measurements

All devices send Wi-Fi frames when Wi-Fi is activated, which is expected. When the Wi-Fi is deactivated, we observed two different behaviors depending on the version of Android. On older versions (2.2.1 and 2.3.7), no frames were observed when the Wi-Fi is turned off. On most recent versions (4.3 and above), Wi-Fi activity depends on whether the "Always allow scanning" option is activated. Wi-Fi frames are emitted if the "Always allow scanning" is activated no matter what is the status of the Wi-Fi switch. To fully prevent emission of Wi-Fi frames it is necessary Inria to disable both the Wi-Fi and the "Always allow scanning" options. We note that on OnePlus One, the "Always allow scanning" is very hard to find even when actively searching for it. On iOS, probe requests the state of the Wi-Fi switch in the control center does not affect the ability of the device to emit probe request frames in most cases.

Probing frequency

Probing frequency varies across devices, configurations and situation. While this work does not aim to review these behavioral differences, it can still be noted that devices in some situation can be lead to send signals at a high frequency. In such case, the possibility of tracking these devices is raised to a fined-grained level. For instance, the OnePlus One sends probe requests every 5 seconds when the Google Maps application is open if either the Wi-Fi switch or the location option is on.

Prompting for location activation

On some versions of Android, devices in which location is not activated will immediately prompt the user to activate it upon launching Google Maps. On the HTC Wildfire, the user is redirected towards the related parameters section. On the OnePlus One, simply replying "OK" to the prompted message immediately activates the option. If the user ignores the message, it is not prompted again in later Google Maps startups. It is, however, prompted again if the user clicks on the location button (top button in the bottom right corner in Figure 4). On the Nexus S, we notice two possible outcomes (see Figure 4):

• If the Wi-Fi switch is deactivated and both location and the "always allow scanning" option are deactivated as well, the device will prompt the user to activate both and do so if the user replies "Yes".

• If the Wi-Fi switch is activated and both location and the "always allow scanning" option are deactivated, the device will only prompt the user to activate location, and remain the "always allow scanning" option untouched.

Airplane mode

In airplane mode, devices are supposed not to emit any radio-frequency transmissions. We tested both an Android and an iOS devices (Motorola G5S Plus and iPhone 6) on airplane mode using the most permissive configurations (all switches on). As a result, we did not detect any transmission, suggesting that this mode works properly on both operating systems. However, on Android, while the airplane mode switch automatically turns the Wi-Fi switch off when activated, the latter can manually be turned back on while the airplane mode is active. As a consequence, Wi-Fi frames can be emitted while the phone is in airplane mode, provided the user allows it.

Conclusions

On both Android and iOS, disabling Wi-Fi is not necessarily sufficient to prevent the device from sending Wi-Fi frames as some devices still generate Wi-Fi frames after Wi-Fi has been disabled. Therefore, disabling Wi-Fi is not enough to escape data collection by Wi-Fi tracking systems. To prevent an Android device from sending Wi-Fi frame, it is necessary to disable two features on the device: both Wi-Fi and the "Always allow scanning" option must be disabled in order to have a silent device. On some devices this option is very hard to find, meaning that the user has to actually know how to deactivate this behaviour to prevent their phone from sending Wi-Fi frames. On iOS, Wi-Fi must be turned off in the parameters.

Although most recent versions of Android and iOS include MAC address randomization [START_REF]Android 6.0 changes[END_REF][START_REF] Skinner | Privacy and your app[END_REF], there are still a number of devices that are not supporting this feature. The MAC address randomization feature has been introduced in version 6.0 of Android, and as of April 2018 38.6% of Android devices are still using an older version [START_REF]Android dashboards: Platform versions[END_REF]. Furthermore, on Android, MAC randomization is activated provided that the hardware supports it, which was rarely the case as of 2017 [START_REF] Martin | A study of mac address randomization in mobile devices and when it fails[END_REF]. On iOS, the situation is better, as 95.7% of devices run a version of iOS greater or equal to 9 [10]. It is unknown how many of them actually use MAC address randomization, as hardware support is also required.

Recent news have brought hints of behaviours similar to the one observed in this document for other interfaces on Android: Bluetooth7 and NFC8 .

[10] David Smith.

Inria

RESEARCH CENTRE GRENOBLE -RHÔNE-ALPES

  (a) Wi-Fi switch option (b) Wi-Fi switch option (c) Wi-Fi switch option

Figure 1 :

 1 Figure 1: Locating the "Always allow scanning" option on the OnePlus One. User has to click on the three dots (circled on Figure (a)), then on the Scanning option appearing in the related menu to access a rather hidden option page.

  (a) Wi-Fi switch option (b) "Always allow scanning" option

Figure 2 :

 2 Figure 2: Wi-Fi related options in Android 4.4.4.

Figure 3 :

 3 Figure 3: Wi-Fi deactivation methods in iOS 11.0.3.

  (a) "Always allow scanning" activated (b) "Always allow scanning" deactivated

Figure 4 :

 4 Figure 4: Google Maps prompting for Wi-Fi activation on the Nexus S

  Inovallée 655 avenue de l'Europe Montbonnot 38334 Saint Ismier Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

  Android Wi-Fi scans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Wi-Fi-related settings in Android . . . . . . . . . . . . . . . . . . . . . . . . . . . Experimental protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 Measurement results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.1 Galaxy S3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Probing frequency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	Contents
	1 Introduction
	2 Wi-Fi on Android
	2.1 3 Wi-Fi in iOS 11
	4 Analysis of generated Wi-Fi activity
	4.1 5 Prompting for location activation
	6 Airplane mode
	7 Conclusions

4.2.2 OnePlus One . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.3 Nexus S . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.4 HTC WildFire and Galaxy Spica . . . . . . . . . . . . . . . . . . . . . . . 4.2.5 Moto G5 Plus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.6 Moto G5S Plus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.7 iPhone 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.8 Summary of the measurements . . . . . . . . . . . . . . . . . . . . . . . . 4.3

Table 3 :

 3 Wi-Fi activity generated in various settings for the OnePlus One. *Device immediately prompts for the user to activate location. Clicking "OK" does so.

	Wi-Fi switch	off	off	off	off on on on on
	Always allow scanning	off	off	on	on off off on on
	Location	off	on	off	on off on off on
	Summary	×** × ×**
	Screen on	×

Table 5 :

 5 Wi-Fi activity generated in various settings for the HTC WildFire. The "Always allow scanning" option does not exist in the early version of Android running on this device.

	Inria

Table 6 :

 6 Wi-Fi activity generated in various settings for the Moto G5 Plus. * When the device is idle, it keeps probing but with randomized MAC addresses, otherwise the real MAC address is used

	Wi-Fi switch	off off	off	off	on on on on
	Always allow scanning off off	on	on	off off on on
	Location	off on	off	on	off on off on
	Summary	×	×
	Screen on	×	×	×
	Idle	×	×	×		×		×
	Leaving Idle	×	×	**	**
	Google Maps	×	×	×		*		*
	Starting Google Maps ×	×	×	×	×	×	×	×
	Google Photos	×	×

Table 7 :

 7 Wi-Fi activity generated in various settings for the Moto G5S Plus. *In this case, the scanning rate is lower than when location is activated. Scans may not be initiated by the Google Maps application. **Unconsistently Wi-Fi switch (parameters) off off off off on on on on Wi-Fi switch (control center) off off on on off off on on Location off on off on off on off on Summary

RR n°9089

http://lifehacker.com/how-retail-stores-track-you-using-your-smartphone-and-827512308,https:// nakedsecurity.sophos.com/2014/06/12/apples-ios-8-will-help-keep-out-wi-fi-marketers-and-snoops-but-not-totally/

https://twitter.com/adhavet/status/891693199424729092

https://support.apple.com/en-us/HT208086 Inria

In a previous version of this report, we stated that this option could not be found. The fact that we did not find it even though we were actively looking for it suggests how hard to find this option can be.

https://support.apple.com/en-us/HT208086 RR n°9089

https://qz.com/1169760/phone-data/

https://www.xda-developers.com/future-android-smartphones-nfc-to-work-disabled/ Inria