Eugene Pamba Capo-Chichi

David Martins
email: dmartins@lifc.univ-fcomte.fr

Hervé Guyennet
email: hguyennet@lifc.univ-fcomte.fr

Violeta Felea
email: vfelea@lifc.univ-fcomte.fr

A Dynamic Clustering Construction for Wireless Sensor Networks

Keywords: wireless sensor networks, clustering, security, energy-efficient algorithms

Research in sensor networks has focused on development of energy efficient and secure infrastructures. In this article, we introduce a new approach to organize sensor networks in clusters in order to reduce energy dissipation. Our contribution is an heuristic to define the number of clusters and also an efficient manner to choose cluster heads by minimizing the distance between the cluster heads and its cluster nodes. Inspired from LEACH, a well-known TDMA cluster-based sensor network architecture, we introduce a new method for building and maintaining clusters using the paradigm of a soccer team. In this work, a new algorithm called OH-Kmeans, based on the Kmeans algorithm, is used to find dynamically the number of clusters and form them guaranteeing direct transmission between the cluster heads and cluster nodes.

I. Introduction

Facilities of deployment and reduced costs have encouraged the use of wireless sensor networks in many applications. Advances in processor, memory and radio transmission technology have also enabled the possibility to develop distributed networks with sensors. However this kind of networks is limited by the critical problem of the energy consumption [START_REF] Akyildiz | Wireless sensor networks: a survey[END_REF].

Because sensors have reduced sizes, their batteries are small and are thus limited in energy. We have to minimize energy consumption in order to guarantee the lifetime of the network. The most consuming activity of sensors is radio communication [START_REF] Hansen | Energy-efficient cluster formation for large sensor networks using a minimum separation distance[END_REF]. Two main methods are used in solving the problem of energy consumption: data aggregation and mode states scheduling (switch to sleeping mode for example) because these methods reduce energy spent in radio communications. Data aggregation is any process in which information is gathered and expressed in a summary form with minimum information loss [START_REF] Krishnamachari | The impact of data aggregation in wireless sensor networks[END_REF]. This method is also used in order to reduce energy consumption in wireless sensor networks by eliminating redundant data transmissions.

In this article, we introduce another approach of hierarchical organization of sensors. Indeed, to reduce the number of radio communications, we have to organize the sensor field in clusters. In the context where sensors are geographically close to each other, there is a strong probability that they sense the same information, so it is interesting to send minimum redundant information to the sink to save energy in the network.

Clustering is the classification of objects into groups, known as clusters, based on similarity. This similarity is often the proximity according to some defined distance measure. The objects, that are being clustered here, are sensor nodes. In each cluster, a sensor, called cluster head, gathers data from the others. In this paper, we define an algorithm to choose the number of clusters and form them as to minimize the distance between the cluster heads and the other cluster nodes. This approach uses the barycenter concept and a new algorithm named OH-Kmeans based on the K-means algorithm. This work is inspired from LEACH but according to [START_REF] Beth | Application-specific protocol architectures for wireless networks[END_REF], LEACH offers no guarantee about placement and/or number of cluster head nodes; the aim of this article is to give these guarantees.

This paper is organized as follows: Section 2 is the related work focused on the presentation of a well known clustering algorithm for wireless sensor networks named LEACH and its versions such as LEACH-F and LEACH-C. In Section 3 we present a new model of energy management in wireless sensor networks based on the paradigm of the soccer game using a new algorithm inspired from the K-means algorithm called as OH-Kmeans. Section 4 shows simulation results of the OH-Kmeans algorithm. Finally, we conclude.

II. Related work

Several works in sensor networks intend to solve the problem of energy waste in sensor networks. One of these approaches is a protocol known as LEACH (Low-Energy Adaptive Clustering Hierarchy) [START_REF] Beth | Application-specific protocol architectures for wireless networks[END_REF] which proposes energy-efficient communications.

LEACH is a protocol based on clustering: a node elects itself to be cluster head with some probability and broadcasts an advertisement message to all the other nodes in the network. A node is selected to join a cluster based on the power radio signal received from the cluster head. Being cluster head is more energy consuming than not being one. All nodes in the network may be cluster head during some period of time. The protocol is a two-phase model: the set-up and the steady-state phase. The set-up phase allows to organize the clusters. The steady-state phase consists of several cycles where all nodes have their communication slots periodically. The nodes send their data to the cluster head that aggregates data and sends it to the base station at the end of each cycle. After a certain amount of time, the TDMA round ends and the network re-enters the set-up phase. Experimental results show that the hierarchical architecture of LEACH [START_REF] Beth | Application-specific protocol architectures for wireless networks[END_REF] optimizes communication cost compared to direct communication.

A version of LEACH called LEACH-C (LEACH-Centralized) [Hei00] uses a centralized cluster formation algorithm to form clusters.

Centralized approaches allow to have a global view of the network and consequently identify relevant cluster heads and number. Even though all information is available in this kind of approaches, determining an adequate value of the number of clusters is still a NPhard problem.

LEACH-C uses simulated annealing to search for a near-optimal number of clusters. The protocol uses the same steady-state protocol as LEACH. During the setup phase, the base station receives information from each node about their current location and energy level. After that, the base station runs the centralized cluster formation algorithm to determine cluster heads and clusters for that round. LEACH-C chooses cluster heads randomly but the base station makes sure that only nodes with "enough" energy are participating in the cluster head selection. Once the clusters are created, the base station broadcasts the information to every network node.

There is another version of LEACH named LEACH-F (LEACH with Fixed clusters) [START_REF] Beth | Application-specific protocol architectures for wireless networks[END_REF] which forms clusters and then fixes them. There is no set-up overhead at the beginning of each round; this is an interesting advantage because overhead is one of the reasons for energy waste in sensor networks. To form clusters, LEACH-F uses the same centralized cluster formation algorithm as LEACH-C. The fixed clusters in LEACH-F do not allow new nodes to be added to the system and as such, do not adjust their behavior in case of nodes failure.

K-means is a well known algorithm that solves the clustering problem. The aim of this algorithm is to organize a given data set into a certain number of clusters (assume K clusters). The number of K is fixed at the beginning. The algorithm is composed of the following steps:

1) Place K points into the space represented by the objects that are being clustered. These points represent initial group centroids. 2) Assign each object to the closest centroid using a distance metric. 3) When all objects have been assigned, compute the positions of the new K centroids as barycenters of the clusters resulting from the previous step. 4) Repeat Steps 2 and 3 until the obtained centroids are the same as in the previous iteration. Since choosing centroids is very important, the best option is to place them, as much as possible, far away from each other. Indeed, in LEACH, node elects itself to be cluster head and consequently, we may obtain close centroids. This clustering method needs improvement in order to assure shrewd choice of the cluster heads and of their number.

III. System model

In this approach, we assimilate a sensor network to a soccer team and we use soccer principles to organize the network so as to minimize the energy consumption. In this model, the network is called team, sensors are the players, the sink is the goal and the information to send to the sink is the ball. To explain further in details, the team needs to be organized around some particular players who can facilitate ball exchanges. A good method for an interesting deployment of sensor networks is the clustering which reveals already interesting in [START_REF] Rabiner Heinzelman | Energy-efficient communication protocol for wireless microsensor networks[END_REF]. Clustering permits to avoid sending redundant information to the sink because nodes geographically close collect the same information with strong probability and by clustering, the cluster head can aggregate redundant data. Clustering used in LEACH [START_REF] Rabiner Heinzelman | Energy-efficient communication protocol for wireless microsensor networks[END_REF] reveals to be effective but on the other hand, LEACH does not offer any guarantee about placement and number of cluster head nodes. Our contribution is meant to introduce another clustering method which gives these guarantees. In the following lines we present this new clustering method for sensor networks.

A. Our clustering method

Generally, clustering is carried out in the following way: nodes are divided into clusters and in each cluster, one node, named cluster head is responsible not only for the cluster formation but also for its maintenance. In this way, several decisions need to be made: determination of the number of cluster heads, the choice of the cluster heads between the network nodes and the cluster organisation. In our model, a cluster's head is named captain. The choice of the number of captains in the network is very important but not easy. If we consider K the number of captains, there may be several methods to choose K:

• K is fixed according to the knowledge of the field and the application, • K is fixed in an empirical way: testing various values of K may help choosing K in order to optimize a validity and quality of the regrouping.

In this work, a criterion of quality is minimization of energy consumption by minimizing the distance between the captain and the cluster nodes. In this article, we propose a new way to choose K. Sensors are characterized by a Sensing Range (SR) and a Communication Range (CR). According to [START_REF] Gallais | Localized sensor area coverage with low communication overhead[END_REF], the Sensing Range is the monitored area of a sensor which is modeled as a disk of radius SR, centered on the node itself. Two sensors are communicating neighbours, or simply neighbours, if and only if the distance between them is at most CR.

In order to be able to relay information, nodes must communicate with their neighbours. In this way, we will compare the deployment area to a rectangle whose surface is equal to length*width. Let CR be the transmission range, an interesting K seems to be:

K = rounded(length/(CR * 2)) * rounded(width/(CR * 2))
where CR*2 is the diameter of the circle formed with the radius CR.

After having determined K, we can apply the Kmeans algorithm with some modifications like the choice of K presented previously. To form clusters, we introduce a new algorithm called OH-Kmeans (One Hop Kmeans) which uses the K-means algorithm. In this work, we consider that the sink has an unlimited energy power and a good computing power to run the OH-Kmeans algorithm. The aim of this algorithm is to guarantee one hop exchange between captain and players. The following lines define the different algorithms used by the OH-Kmeans algorithm.

The first function named Kmeans is an implementation of the K-means algorithm.

The second function, named OneHop, counts the number of nodes, one hop at most of the cluster head and returns this number.

The third function TestKInf verifies that it is possible to decrease K keeping one hop between a cluster head and its cluster nodes and returns null if it is impossible to do so.

The OH-Kmeans algorithm uses these previous functions and changes K dynamically.

This algorithm inspired from K-means named OH-Kmeans (One Hop Kmeans) allows to find a number of K clusters which guarantees a direct information transmission (one hop) between captains and players. The sink needs to know the position of all players at Algorithm 1 Kmeans: TableofCluster Kmeans(int K)

Step 1 -Choose K points randomly into the space represented by the network that are being clustered. These points represent initial captains (they may be virtual).

Step 2 -Assign each player to the closest captains using the euclidian distance metric.

Step 3 -When all players have been assigned, compute the positions of the new K captains as barycenters of the clusters resulting from the previous step.

Step

K ← K -1 newtable ← TestKInf(K) if (newtable = null) then T ableof Cluster ← newtable else out ← true end if end while end if
Once the initial captains are selected, they send messages to players to create clusters. Nodes choose the closest captain (at one hop) and send to it the information (position and energy level). These positions enable to maintain the cluster organisation (details will be given in the next paragraph which is related to the captain rotation).

Becoming captain is a very energetic task because the captain receives all information that is why it is very important to change the captain after a period.

B. Captain rotation

Because all balls in the network are sent through the captain, the latter is an energy consuming node, which makes its choice very important. At the end of each period the captain aggregates information before sending it to the goal. In this section we define the manner in which a captain is chosen.

When a captain receives messages from players which want to join clusters at the beginning of a period, it receives their positions and their energy level to choose the future captain. The captain chooses the best future captain among them depending on the criterion which follow:

• The energy level

This energy level corresponds to the level of sensor's battery because captains must exchange information with the other nodes which are not captain of cluster and this operation requires a considerable level of energy.

• The number of times that it was captain

In order to spare the captain's energy, we need to consider the number of times a node has already been captain.

• The density of nodes in a given range

To have several nodes in a given range can facilitate the exchange of information. If nodes are close to the captain, information is sent easily, in one hop transmissions.

• Proximity compared to the sink Information collected by the cluster's captain must be, after their aggregation, sent to the sink thus it would be less expensive to choose a captain close to the sink. This work is a mixture between LEACH-C and LEACH-F because at the beginning the system is centralized but when OH-Kmeans stops and the good clusters are formed, the system becomes stable. LEACH-F does not allow new nodes to be added but in this model, we can add new nodes if they send their position to the nearest captain. In this model, compared to LEACH-C, it is not the sink which chooses the future captain but the previous captain. After having created the clusters, it is important to use collective intelligence of all players in order to organize the game. After cluster construction, the steady state phase is the same as in LEACH.

IV. Experimental results

OH-kmeans and K-means have been simulated using Java platform. Results of simulations are presented here. All experiments have been done on a 100*100 surface with sensor's communication range equal to 15. We obtained Figure 3 for 1000 nodes deployed on a 100*100 surface. We can see that when the number of captains, K, in the network increases, the number of nodes, with a distance greater than one hop, decreases. Then we decided to implement an algorithm which allows to modify K dynamically. This new algorithm, called OH-Kmeans, allows to find the adapted value of K which guarantees one hop exchange between each captain and nodes in its cluster. In Figure 4, we varied the communication range between 5 and 30, for 100, 500, 1000 deployed nodes on a 100*100 surface and we remarked that when the communication range increases, the number of captains K (cluster-heads) which allows to have one hop exchange decreases.

This graphics shows that CR is an important factor just like K, the number of cluster heads, in the clustering technic. In Figure 5, we can see that for different networks with 1000 nodes or 100 nodes, the number of iterations with OH-Kmeans which guarantees one hop exchanges converges rapidly. According to the previous section, an interesting K seems to be: K = rounded(length/(CR * 2)) * rounded(width/(CR * 2))

In this example, we obtain: K = rounded(100/(15 * 2)) * rounded(100/(15 * 2)) = 9

According to Figure 5, for 100 proposed nodes and K = 9, the number of iterations, for the OH-Kmeans algorithm, is between 12 and 20 iterations but the simulated annealing used in LEACH, which allows to find the optimal number of clusters, converges in 200 to 500 iterations for a network of 100 nodes.

V. Conclusion

In conclusion, this paper introduces a new method to organize sensor networks, guaranteeing one hop exchange between cluster head and cluster nodes. This approach is based on an algorithm named OH-Kmeans. This algorithm gives an heuristic to find dynamically the number of clusters. OH-kmeans is inspired from the K-means algorithm and introduces a new manner to choose the number of clusters dynamically. Experimental results show that OH-Kmeans, for 100 nodes or 1000 nodes, converges more quickly than simulated annealing (used in LEACH). So, for any values of Communication Range (CR) or number of clusters K, with OH-kmeans, the number of nodes at more than one hop of its cluster head always equals zero. Future work concerns the integration of this new clustering method into the LEACH communication approach.

Fig. 1 .

 1 Fig. 1. LEACH: protocol based on clustering [HK05]

Fig. 2 .

 2 Fig. 2. Cluster construction using the K-means algorithm with K=3

Fig. 3 .

 3 Fig. 3. Number of nodes at more than one hop for different values of K using the K-means algorithm

Fig. 4 .

 4 Fig. 4. Variation of K with different values of communication range using the K-means algorithm

Fig. 5 .

 5 Fig. 5. Number of iterations for different values of K using the OH-Kmeans algorithm


F Bouquet
email: bouquet@lifc.univ-fcomte.fr

P.-C Bué

J Julliand
email: julliand@lifc.univ-fcomte.fr

P.-A Masson
email: masson@lifc.univ-fcomte.fr

Test Generation Based on Abstraction and Test Purposes to Complement Structural Tests

Keywords: Model-Based Testing, Abstraction, Test Purpose

This paper presents a computer aided model-based test generation method. We propose this approach as a complement to the LTG (Leirios Test Generator) method, which extracts functional tests out of a formal behavioral model M by means of static (or structural) selection criteria. Our method computes additional tests by applying dynamic (or behavioral) selection criteria (test purposes called TP). Applying TP directly to M is usually not possible for industrial applications due to the huge (possibly infinite) size of their state space. We compute an abstraction A of M by predicate abstraction. We propose a method to define a set of abstraction predicates from information of TP. We generate symbolic tests from A by using TP as a dynamic selection criterion. Then we instantiate them on M, which allows us play the tests on the implementation the same way as we play the functional ones. Our experimental results show that our tests are complementary to the structural ones.

I. INTRODUCTION

Model-Based Testing (MBT) is a test generation approach that automatically computes, from a behavioral model of a system and selection criteria, a set of tests to be executed on an implementation of that system (the implementation under test, IUT). There are model based test generation suites available as commercial products, such as LTG [START_REF] Jaffuel | LEIRIOS Test Generator: Automated test generation from B models[END_REF] and TD1 , Conformiq2 , SpecExplorer [START_REF] Barnett | The spec# programming system: An overview[END_REF], or as research prototypes, such as TGV [START_REF] Jard | TGV: theory, principles and algorithms[END_REF] and STG [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF], AGATHA [START_REF] Rapin | Behavioral unfolding of formal specifications based on communicating extended automata[END_REF], etc. One advantage of MBT is to have with the behavioral model an oracle to predict the outputs of the IUT. Another one is the possibility to achieve different kinds of coverage of the model (such as state coverage, decision coverage, path coverage) by varying the selection criteria. But writing the behavioral model and the concretization layer is costly, and ideally a large variety of test cases, i.e. achieving a large spectrum of coverage, should be computed from them.

An MBT tool-supported method, the LTG technology [START_REF] Jaffuel | LEIRIOS Test Generator: Automated test generation from B models[END_REF], has been developed in our research team and is now commercialized by the Smartesting company. It ensures structural coverage of the model by means of static (i.e. structural) selection criteria. Additionally, we intend to generate test cases issued from dynamic selection criteria [START_REF] Julliand | Generating tests from B specifications and dynamic selection criteria[END_REF], [START_REF] Julliand | Generating security tests in addition to functional tests[END_REF]. A test engineer (the tester) specifies a set of executions that he finds interesting to test by means of a test purpose (TP). The TP is specified in a language [START_REF] Julliand | Generating security tests in addition to functional tests[END_REF] that allows the tester to describe which actions to call and which states to reach. Some of the action calls can be left unspecified, which provides flexibility to the tester for expressing his test intention, but requires later these calls to be made explicit. This is performed by a research amongst the possible instantiations allowed by the model of the unspecified action calls, and it can possibly blow up with huge size models.

We propose in this paper to define, based on information extracted from the TP, a set of predicates from which we compute an abstraction A (of small size) of a behavioral model M. We first compute its synchronized product SP with the TP, and then a set of traces that cover every transition of SP. Each trace is a symbolic test for which we search an instantiation on M. This results in a new (w.r.t. the structural ones) set of instantiated tests IT, that can be executed on the IUT through the same concretization layer.

Our contributions are to define the set of abstraction predicates based on information of the TP. This makes the resulting abstraction related to what the tester intends to observe. Also, M provides an oracle for our new tests, and it is reused as well as the concretization layer to execute the tests on the IUT. We have an experimental validation of the method.

We detail our process for generating tests from abstractions and test purposes in Sec. II. Section III presents the "Qui-Donc" example that illustrates our approach. We define labelled transition systems (LTSs, for short) in Sec. IV and give the syntax of our behavioral models, whose semantics are LTSs. The abstractions and the test purposes are also defined as LTSs in Sec. V, where their synchronized product is defined.

The definition from the TP of a set of abstraction predicates is detailed in Sec. VI. This set is the basis for the computation of the abstraction, as explained in Sec. VII, where we also explain how to generate symbolic tests out of it. Experimental results are presented and discussed in Sec. VIII. Section IX concludes the paper, compares our approach to related works and gives some future research directions.

II. TEST GENERATION PROCESS FROM DYNAMIC SELECTION CRITERIA AND ABSTRACTIONS

Let us present our motivations, and our process for generating tests from dynamic selection criteria and abstractions.

A. Problem and Motivations

In our approach, the validation engineer describes by means of an hand-written test purpose TP how he intends to test the system, according to his know-how. We have proposed in [START_REF] Julliand | Generating security tests in addition to functional tests[END_REF] a language based on regular expressions, to describe a TP as a sequence of actions to fire and states to reach (targeted by these actions). The states are described as state predicates. The actions can be explicitly called by their name, or left unspecified by means of a generic name. This genericity allows the tester to describe a situation to reach without specifying how it should be reached. A regular expression repetition operator can be applied to the unspecified action call. This means in the tester's mind: leaving all possibilities to the system to reach a target state. The drawback is a combinatorial explosion of the number of executions of M in which to look for an instantiation of the action calls that reach the target state. The search should be guided to avoid that problem.

B. Test Generation Process by Abstraction

A small size state-transition graph, that symbolically models the executions of the system, can be obtained by computing an abstraction A of M. We propose to perform a synchronized product between A and the automaton that is the semantics of the TP, and to use paths of the synchronized product as guides for the instantiation of the TP on M. Our approach is depicted in Fig. 2. From a behavioral model M and the state variables of a TP, we define a set SD of abstraction predicates. SD stands for sub-domains (of the state variables). The details of this definition are given in Sec. VI. The GeneSyst tool [START_REF] Bert | Genesyst: a tool to reason about behavioral aspects of B event specifications[END_REF] produces an abstraction A of M based on the predicates of SD. The synchronized product, defined in Sec. V-B, of A with the TP results in a model SP. The executions of SP are the executions of A

(State = put down ⇔ HandSet = hang) ∧ (State = put down ⇒ TryCounter = 0) init = HandSet = hang ∧ TryCounter = 0 ∧ State = put down Call = HandSet = hang ∧ HandSet ′ = unhook ∧ TryCounter ′ = TryCounter ∧ State ′ = welcome HangUp = (HandSet = unhook ∨ State = busy) ∧ (HandSet ′ = hang ∧ TryCounter ′ = 0 ∧ State ′ = put down)
Fig. 3. A fragment of the Behavioral Model of the Qui-Donc System that match the TP. An implementation [START_REF] Thimbleby | The directed chinese postman problem[END_REF] of the Chinese Postman algorithm is applied to SP to cover its transitions. The result is a set of abstract symbolic tests AST. These tests are instantiated from M, which allows for re-using the same test execution environment (i.e. the concretization layer CL and the test execution tools) as of Fig. 1: the new instantiated tests IT (of Fig. 2) complement the ones of Fig. 1. Notice the dashed arrow in Fig. 2 from SP to the "instantiation" box. This is because, to instantiate the abstract symbolic tests, we use the reflexive transitions of SP that were ignored to generate AST. This point is explained in Sec. VII-B.

III. THE QUI-DONC EXAMPLE Our approach is illustrated by means of the Qui-Donc example [START_REF] Utting | Practical Model-Based Testing[END_REF]. It is a reverse phone book service. When the user contacts the service, he gets a welcome message followed by an invitation to enter the number he searches for. When he has done so, the service possibly answers that the number is an emergency one, or is invalid, or is unknown, otherwise the answer is the name and address of the owner of the number. In case the user forgets to provide an input, or provides an unexpected one (such as an unauthorized key), the service invites up to twice the user to provide its input again and finally closes the communication if needed.

We have designed a behavioral model of the Qui-Donc. Let us introduce its variables and some actions, which appear in a forthcoming example of test purpose. The Call and HangUp actions allow respectively to call the service and to close the communication. The Delay action simulates that the user remains inactive during a fixed delay. The HandSet ∈ {hang, unhook} variable stands for the state of the handset. The TryCounter ∈ {0, 1, 2} variable counts how many times the user has provided an unexpected (or void) input. The State variable indicates in which state the service is. Amongst the six possible State values are welcome (when the service is ready to listen to a new input from the user) and put down (when the communication has been closed). A fragment of its model is expressed w.r.t. the syntax of Def. 4 in Fig. 3.

IV. BEHAVIORAL MODELS AND THEIR SEMANTICS

We define Labelled Transition Systems (LTSs) and present a syntax, inspired from the guarded commands [START_REF] Dijkstra | Guarded commands, nondeterminacy, and formal derivation of programs[END_REF], [START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF], to describe the behavioral models.

A. Labelled Transition Systems

The state transition graph of the behavioral models, their abstractions as well as the test purposes are formalized as LTSs (see Def. 1). Notice that we only consider LTSs with finite state spaces in this paper, which is usual with models for the test.

Definition 1 (Labelled Transition System): An LTS is defined by a tuple O, Q, Q 0 , ∆, AP, L, Q f , where

• O is a finite set of action names,

• Q is a finite set of states,

• Q 0 (⊆ Q) is a set of initial states, • ∆(∈ Q × O × Q) is a labelled transition relation, • AP is the set of atomic propositions, • L(∈ Q → 2 AP
) is a state labelling function which maps each state to the set of atomic propositions that hold in this state,

• Q f (⊆ Q) is a set of final states.
We write q o → q ′ instead of (q, o, q ′ ) ∈ ∆ for the sake of simplicity. An execution σ of an LTS is a finite sequence of transitions represented by a sequence of pairs σ = (⊥, q 0 ), (o 1 , q 1 ), . . . (o n , q n ) where o i is an action name and q i a state. σ is such that q 0 is an initial state of Q 0 and for every i in [0, n-1], q i oi+1 → q i+1 and q n ∈ Q f . The set of atomic propositions AP is defined over a set of state variables X and their domains by relational operators. Any x ∈ X has a domain denoted by D(x). Let v be a value of D(x) and V be a sub-domain of D(x) (V ⊆ D(x)). An atomic proposition is either in the shape of x = v in a concrete LTS where the states are valuated, or in the shape of x ∈ V in an abstract LTS where the states are symbolic. Notice that we unify the notations and denote x = v by x ∈ {v}. When necessary, we use an upper-script notation to indicate the name of the LTS to which we refer.

An LTS A is compatible with an LTS M (see Def. 2) if its action names are in M, its set of state variables is included into that of M, and the atomic propositions of AP A partition the domains of the variables of the subset of state variables of M that also are state variables of A into several sub-domains.

Definition 2 (Compatible LTSs): Let M and A be two LTSs. A is compatible with M if:

• O A ⊆ O M (A uses only actions of M), • the set of variables X A on which is defined AP A is a subset of X M on which is defined AP M , • for any atomic proposition x ∈ V M in AP M such that
x is in X A , there exists a proposition x ∈ V A in AP A such that V M ⊆ V A . Two states q A and q M are compatible (see Def. 3) if q A is an abstract state that includes the more concrete state q M . Definition 3 (Compatible States): Let A be an LTS compatible with an LTS M. A state q A is compatible with a state q M if for any atomic proposition

x ∈ V A in L A (q A ) there exists a proposition x ∈ V M in L M (q M ) with V M ⊆ V A .
We say that (q A , q M ) is a compatible pair when q A is compatible with q M .

B. Model syntax and semantics

Our work does not necessitate that we specify a particular modelling syntax. We only consider a model as being defined on a set of variables, and as being specified by means of an initial condition and a transition relation. They are specified syntactically as first-order logic predicates. The relation symbols form the atomic predicates. The expressions are defined in the data set theory, as it is for example the case in B [START_REF]The B Book[END_REF]. The main data structures are sets, functions and relations. Some relation and function symbols may have fixed interpretations, such as =, =, ≤, ∈, +, etc.

Definition 4 (Behavioral Model): A behavioral model is defined by a tuple X, I, init, O, OP where:

• X is a finite non-empty set of state variables. Each variable x ∈ X has a finite or infinite domain of values, denoted by D(x), • I is an invariant specified as a predicate on X,

• init is an initial condition specified as a predicate on X such that init ⇒ I, • O is a set of guarded action labels,

• OP is the transition relation, specified by the definition of every guarded action (labelled by o) by an equation o

= T o (X, X ′ ), where T o (X, X ′ ) is a before-after predicate on X∪X ′ . X ′ is a set of "next-state" variables that is in 1- 1 correspondence with X. It is such that I ∧T o (X, X ′ ) ⇒ I ′
, where I ′ denotes the invariant in which the variables of X ′ replace the ones of X. The semantics of a behavioral model is an LTS. Q is the subset of the cartesian product of the domains of the variables X that satisfy the invariant condition I. The value of a predicate e in a state q is denoted by e(q). It can be defined by induction on the syntax of the predicates. A state q is an initial state in Q 0 iff init(q) = true. The transition relation is defined as follows: there is a transition q o → q ′ iff T o (q, q ′ ) is true. The state labelling function L is defined as follows: for each atomic predicate x = v, we have that x ∈ {v} is in L(q) iff v is the value of x in q. Any state is a final state:

Q f = Q.
Figure 3 models a fragment of the Qui-Donc example 3 . Each action in a behavioral model is made of one or many elementary guarded actions (EGA) in the shape of G ∧ X ′ = f (X), that assign all the state variables of X when a guard G is true. Each of the two actions Call and HangUp in Fig. 3 is made of only one EGA, but there can be several of them in an operation, as it is the case for the Delay operation. We denote by T oi (X, X ′ ) the i th EGA of an action o.

V. ABSTRACTION, TEST PURPOSE, SYNCHRONIZATION

In this section, we define the abstractions, the test purposes and their synchronization as LTSs.

A. Abstraction, Test Purpose

An abstraction A of a behavioral model M is an LTS defined on a subset of the variables of M, X A ⊆ X M . It is compatible with the semantics of M. It uses the same set of action names as M. Each variable of X A has an abstracted domain of values which is a partition of its domain in M. The state space Q A is the subset of the cartesian product of the set of the abstracted domains of the variables X A that satisfy the invariant condition I M . Any state is a final state. AP A is the set of atomic predicates defined on X A and their abstracted domains. An atomic proposition on A is denoted by x ∈ V A where V A is one of the elements of D A (x) which is a subdomain of D M (x). Figure 5 shows an example of abstraction of the Qui-Donc model.

A test purpose TP defined w.r.t. a behavioral model M (whose abstraction is A) is an LTS, where there is only one initial state in Q P 0 . This LTS is defined as follows. The labels of the transitions are actions names of M. With L P , any state of the set Q P is labelled by a set of atomic predicates defined w.r.t. a subset of the variables of X M . The set of final states Q P f is a subset of Q P which is defined by the tester. We assume that the tester defines test purposes that are compatible (see Def. 2) with the LTS semantics of M.

In our context, the sets of atomic predicates of a TP compatible with the semantics of M are subsets of atomic predicates of the abstraction A of M. By construction in our method, the set of symbolic states of A is a partition of the set of symbolic states of TP (see definition of SD in Sec. VI).

Figure 4 shows the automaton representation of a TP for the Qui-Donc. Its aim is to test that the try counter, once incremented, gets back to 0 in case of a correct entry from the user. For readability purposes, in the graphical representations of the LTSs of Fig. 4 and5, some transitions are labelled with a set of labels: this means that there are as many transitions in the LTS as there are labels in the set. Notice that the tester does not have to draw the automaton to express a TP: he would rather use the language of [START_REF] Julliand | Generating security tests in addition to functional tests[END_REF]. The automaton would be its semantics. In our example, TP is compatible both with the semantics of M and with A. By construction, A is also compatible with the semantics of M. The sets of action names satisfy the conditions O P ⊆ O A and O A = O M . The set of state variables X M = {HandSet, TryCounter, State}, X A = {TryCounter, State} and X P = {TryCounter} are such that X P ⊆ X A ⊆ X M . The set of atomic propositions

AP P = {TryCounter ∈ {0}, TryCounter ∈ 1..2} is included in AP A = {TryCounter ∈ {0}, TryCounter ∈ 1..2, State ∈ {welcome}, State ∈ {put down}, State /
∈ {welcome, put down}}. Thus TP is compatible with A and A is compatible with M.

{} {} {TryCounter = 0} {} {TryCounter = 0} {} q 0 q 1 q 2 q 3 q 4 q f Call O M O M \ {HangUp} O M \ {HangUp} HangUp O M \ {HangUp} O M \ {HangUp}

B. Synchronization of an Abstraction and a Test Purpose

We synchronize two compatible LTSs as in [START_REF] Jéron | Test generation derived from model-checking[END_REF]: an abstraction A and a test purpose TP. This synchronization is a particular synchronized product of LTSs (see Def. the transitions that have the same label are synchronized when their source and target states are compatible and when they are not reflexive in the abstraction. The reflexive transitions of A are not considered for the synchronized product because they do not help in progressing towards a target state of the TP. But they are essential for the instantiation of the abstract tests. Consequently, the input SP of the instantiation function of Fig. 2 is defined as in Def. 5, except that this time the reflexive transitions of A are taken into account. It is defined from Def. 5 by suppressing the condition q A = q ′A of the fourth item.

Definition 5 (Synchronized Product of two compatible LTSs):

The synchronized product between a test purpose

O M , Q P , Q P 0 , ∆ P , AP P , L P , Q P f with a compatible LTS O M , Q A , Q A 0 , ∆ A , AP A , L A , Q A f of an abstraction is an LTS O M , Q, Q 0 , ∆, AP A , L, Q f , where: • Q(⊆ Q P × Q A )
is the subset of compatible pairs (q P , q A ) of the cartesian product

Q P × Q A , • Q 0 (⊆ Q P 0 × Q A 0 )
is the subset of compatible pairs of the cartesian product Q P 0 × Q A 0 , • for any state (q P , q A ) ∈ Q, L((q P , q A )) = L A (q A ),

• for any pair of pairs of compatible states ((q P , q A ), (q ′P , q ′A )), (q

P , q A ) o → (q ′P , q ′A ) if q P o → q ′P , q A o → q ′A and q A = q ′A , • Q f = {(q P , q A ) | (q P , q A ) ∈ Q ∧ q P ∈ Q P f ∧ q A ∈ Q A f }. Notice that Q P 0 = {q P 0 }.
The state q P 0 is always compatible with any state of Q A 0 because L P (q P 0 ) = {}.

VI. SET OF ABSTRACTION PREDICATES DEFINITION

In this section, we present how we define a set of abstraction predicates from a test purpose TP and a behavioral model M. To compute the abstraction, we use GeneSyst [START_REF] Bert | Genesyst: a tool to reason about behavioral aspects of B event specifications[END_REF]. It requires that a set of symbolic states is defined by a set of predicates. This is a kind of predicate abstraction [START_REF] Graf | Construction of abstract state graphs with pvs[END_REF], [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF], [START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF] that uses a first-order theorem prover on the set theory.

We consider in this section a test purpose TP defined as an LTS and a behavioral model M defined as a guarded action system according to Def. 4. We call state predicate of TP a set of atomic propositions that labels a state of TP.

The set of abstraction predicates is defined w.r.t. the state predicates and the actions appearing in TP. We propose to define this set of in two steps:

• extraction of the subset X A of the variables of X M that are used in the state predicates of TP or modified by the actions explicitly fired in TP, • partition of the domains of these variables according to their use in the state predicates and in the actions of TP. The set of abstraction predicates is defined from a TP that is an LTS compatible with the semantics of M. In our example, the action names in the TP of Fig. 4 are Call and HangUp. The state predicates are about the state variable TryCounter.

A. Extraction of the Variable Names

We define O P (⊆ O M ) as the set of the actions explicitly fired in TP, i.e. the ones that appear at least once in the labels of the graphical representation of TP without being subtracted from O M . We have O P = {HangUp, Call} with Fig. 4.

The set of variables X A ( = X A sp ∪ X A op ) of the abstraction A is the union of the set of variables of M that are used in the state predicates of TP, denoted by X A sp , and the set of variables modified by all the actions of TP, denoted by X A op :

• X A sp = q∈Q P {x | x ∈ V is in L P (q)}, • X A op = {x| for any o in O P the definition T M o (X M , X ′M ) contains a predicate x ′ = e where e = x}.
For the example of Fig. 4, the set of variables abstracting the Qui-Donc is X A = {TryCounter, State}. TryCounter (∈ X A sp ) is used in the state predicates and State (∈ X A op ) is modified by both Call and HangUp (see Fig. 3) in the TP of Fig. 4.

B. Partition of the Variable Domains

To define the set of sub-domains of the variables of X A , we define (i) the set of sub-domains issued from the state predicates of TP and (ii) the sub-domains of the symbolic states targeted by the actions of TP. Then we split these subdomains into parts so as to realize the smallest partition of domains of each variable of X A .

The set SD x sp for item (i) is the union of the atomic predicates, on the variable x, that label the states of TP:

SD x sp = q∈Q P {x ∈ V | x ∈ V is in L P (q)}.
We obtain for example the two following sub-domains for the variable TryCounter of the TP in Fig. 4 4 :

SD TryCounter sp = {TryCounter = 0, TryCounter = 0}.
Let X be a set of variables. To distinguish between a variable x and the others in X, we define Z = X \ {x}.

The set of sub-domains issued from the actions (item ii) for a variable x is the set of strongest postconditions of every EGA a of every action used in TP (∈ O P ) from the precondition

p = x ∈ D M (x). It is denoted by sp(p, a) with sp(x ∈ D M (x), a) = x ′ ∈ V such that x ′ ∈ V ⇔ ∃x • ∃Z • ∃Z ′ • ( z∈Z (z ∈ D M (z) ∧ z ′ ∈ D M (z)) ∧ a ∧ x ∈ D M (x)).
4 Notice that we have simplified the writing of the predicates that should have been denoted by TryCounter ∈ {0} and TryCounter ∈ 1..2.

Let n o be the number of EGA of the action o. The set of sub-domains SD x op is defined as:

SD x op = o∈O P ,i∈1..no {x ∈ V | x ′ ∈ V = sp(x ∈ D M (x), T M oi (X M , X ′M ))}.
= {x ∈ V 1 , x ∈ V 2 , . . . , x ∈ V n }.
When the sub-domains V i intersect, we partition them. If the set of sub-domains do not overlap the whole domain of x, we add as the last sub-domain the complement of the union of the sub-domains. So the set of sub-domains SD x of any variable x of X A is the smallest partition of D M (x) w.r.t. the set SD x sp ∪ SD x op whose cardinal is n. Let F 1 (1..n) be the set of non empty finite parts of the set 1..n and ∁ J be the complementary set of J in 1..n. The partition is defined as:

SD x = J∈F1(1..n) {x ∈ ( j∈J V j \ i∈∁J V i )} ∪ {x ∈ (D M (x) \ j∈1..n V j )}.
Finally, the set of sub-domains is defined as:

SD = x∈X A SD x
For example, the We can obtain the predicates that define the sub-domains by constraint solving. This requires all the domains of the variables to be defined as finite sets, which is usual in a model for the test.

The abstraction predicates define a set of symbolic states as the cartesian product of the sets of the abstract domains of any variable of X A . We obtain for our example the set of abstraction predicates shown in the following table. This defines six symbolic states. Only five of them are reachable and appear in the abstraction computed by GeneSyst and shown in Fig. 5. In Proposition 1, we prove that with the assumption that the tester designs a TP compatible with M, this definition of the set of abstraction predicates SD makes that the TP is compatible with an abstraction A computed from them.

Variable Sub-domains

Proposition 1: Consider a TP compatible with M and an abstraction A computed from the set of abstraction predicates SD. Then the TP is compatible with A.

Proof: By assumption, the test purpose TP is compatible with M. Hence the three following conditions hold:

• O P ⊆ O M , • X P ⊆ X M ,
• for any x in X P and for any atomic proposition x ∈ {v} in AP M , there exists an atomic proposition x ∈ V in

AP P such that v ∈ V .
By definition of X A in this section, X P ⊆ X A and X A ⊆ X M . By definition of SD in this section, it is a partition of the domains of the variables of X A and SD = AP A . Moreover O A = O M . Let SD sp be the union of SD x sp for any x in X P . By definition of SD sp , AP P = SD sp . Then, by definition of SD, the predicates of SD sp are redefined in SD from some predicate of SD op in such a way that the predicates of SD define a domain partition of any variable of X P . Hence for any predicate x ∈ V A in AP A that concerns a variable x of X P , there exists a predicate x ∈ V P in AP P such that V A ⊆ V P . Therefore TP is compatible with A.

VII. ABSTRACTION AND TEST GENERATION

A. Generation of the Abstraction

We use GeneSyst to generate an abstraction from a behavioral model M and a set of symbolic states. This abstraction is an LTS that is an over-approximation of M: it simulates all the executions of M, but adds new ones. GeneSyst tries to prove automatically the feasibility or not of transitions between the symbolic states. It proceeds by weakest precondition computations and satisfiability evaluations over first order logical formulas [START_REF] Bert | Genesyst: a tool to reason about behavioral aspects of B event specifications[END_REF]. GeneSyst takes B specifications [START_REF]The B Book[END_REF] as input. The weakest precondition of a statement S that leads to the abstract state a ′ is defined by the B substitution calculus. It is denoted by [S]a ′ . A transition from an abstract state a to a ′ is feasible if a ∧ [S]a ′ is satisfiable. If a ⇒ ¬[S]a ′ is valid then the transition is not feasible. On the contrary, when the proof of ∃X • (a ∧ [S]a ′ ) succeeds, the transition a → a ′ is added to the LTS. It is also added when this proof is inconclusive, although it is possibly infeasible. This makes the abstraction more over-approximated.

Thus, some of the symbolic tests that we generate from the abstraction may not be possible to instantiate as executions of the behavioral model. This would result in a bad coverage of the abstraction by the instantiated tests. It is possible to use an interactive prover to try to get rid of the proof failures. We have chosen another alternative: using constraint solving techniques makes it possible to automatically check the feasibility of the unproved transitions when the state space is finite. The applicability of this technique depends on the size of the domains, as it proceeds by partial consistency checking and domain enumeration. We will assess the practical impact of the instantiation problem on some examples in Sec. VIII.

B. Generation and Instantiation of the Symbolic Abstract Tests

We compute the symbolic abstract tests as selected executions of the abstraction, by running an implementation [START_REF] Thimbleby | The directed chinese postman problem[END_REF] of the chinese postman algorithm on the synchronized product SP of the abstraction with the TP (see Fig. 2). This provides a set of paths such that every transition of SP is covered at least once. Every path is a symbolic abstract test that terminates in a final state of SP. It is a sequence of non parameterized action calls. We still have to instantiate the tests, i.e. to find parameter values that make these sequencings of actions possible according to the behavioral model M. We proceed by a symbolic animation of the tests on M. It is possible that a sequence can not be instantiated as it is: an action might not be enabled on a given instance of a symbolic state. Thus we will use a version of SP augmented with its reflexive transitions to complete the instantiation. Indeed, these transitions may lead to another instance of the same symbolic state, from which the action could be enabled. As a result, we insert bounded sub-sequences of (reflexive) action calls into the original sequence. We have implemented this instantiation procedure. Although naive and incomplete (invoking reflexive transitions is not always sufficient, sometimes cycles are necessary), our algorithm gave satisfactory instantiation results on our case studies, as shown in Sec. VIII.

VIII. EXPERIMENTAL RESULTS

We have applied our method to three various cases of reactive systems: a reverse phone book service (Qui-Donc [START_REF] Utting | Practical Model-Based Testing[END_REF]), an automatic conveying system (Robot [START_REF] Bouquet | Génération de tests à partir de critères dynamiques de sélection et par abstraction[END_REF]) and an electronic purse (DeMoney [START_REF] Marlet | Demoney: A demonstrative electronic pursecard specification[END_REF]). Tests have been generated for each of them from two TPs, on a 2.8GHz Pentium with 1GB of RAM.

The first two parts of Table I show the size of the behavioral models and the TPs. The symbol "♯" means number of, "Act." stands for Actions, and "Trans." stands for Transitions. For example, the TP of Fig. 4 (in bold font in Table I) is made of 6 states, 8 transitions, 2 explicit action calls and two non empty sets of atomic predicates. The behavioral model of the Qui-Donc is made of 4 actions, with a total of 20 EGAs. It is 122 lines long and it defines 13 states from three variables whose average domain size is 3.66.

A. Abstraction Generation and Synchronous Product

The last two parts of Table I are about the abstraction generation and the synchronous product (SP) computing. GeneSyst failed to prove from 66% up to 90% of the transitions. We have checked, with success on our examples, the satisfiability of the unproved POs by means of a constraint solver [START_REF] Bouquet | CLPS-B: A constraint solver to animate a B specification[END_REF] (see the Filter. columns in Table I). The filtered transitions are the ones really unsatisfiable. There are only few of them (from 3% up to 18%), with the exception of DeMoney. Filtering is almost immediate for Qui-Donc and the Robot, modelled with variables enumerated on small domains. But it takes one hour for DeMoney, whose model has some numerical variables.

B. Symbolic Test Generation and Complementarity

We have presented in [START_REF] Julliand | Generating tests from B specifications and dynamic selection criteria[END_REF] a technique to build a new behavioral model synchronized with a TP, from which LTG generates tests. The results in the first part of Table II have been obtained with this technique. We also have tried (see the second part of Table II) to first synchronize directly the LTS semantics of the behavioral models with the TPs, without using abstractions, and then to generate the tests with a chinese postman walk. Although it has been possible to do so with Qui-Donc and the Robot, it failed with DeMoney due to the size of the resulting state space. This shows the utility of using abstractions to apply this test generation method. The complementarity with the LTG tests has been studied in [START_REF] Julliand | Generating tests from B specifications and dynamic selection criteria[END_REF]. It also appears in our results. LTG covers every EGA and the chinese postman walk covers every transition. For example with the first TP of the Robot, 80 test steps have been generated by LTG to cover every EGA, and more than 10500 tests have been generated to cover every transition.

The tests in the last two parts of Table II have been obtained (in less than one second) by a chinese postman walk on the synchronized product SP between an abstraction and a TP. The tests of the third part have been obtained without filtering the unfeasible transitions by constraint solving, whereas in the fourth part they have been filtered. Although the transitions of the without filtering version of the abstraction are a superset of the ones of the with filtering version, the "without filtering" tests are not a superset of the "with filtering" ones. They cannot be compared as the chinese postman algorithm does not necessarily covers the same traces of the two abstractions.

C. Test Instantiation

Using abstractions require the generated tests to be instantiated from the concrete model. But our abstractions are over-approximations, and they contain unproved transitions potentially infeasible. The results of the "without Filtering" part in Table II are for abstractions where every unproved transition has been kept. From 35% up to 58% of the tests have been instantiated, except with the two TPs of DeMoney for which no test have been instantiated. In contrast, for the results of the "with filtering" part of Table II, we have removed the filtered transitions from the abstraction. From 35% up to 94% of tests have been instantiated, except with one TP of DeMoney. There are two reasons why with filtering, the ratio of instantiated tests grows. There are less transitions, thus less symbolic tests. Moreover, the former symbolic tests going through infeasible transitions are replaced by other tests, possibly instantiable. For example, with the second TP of DeMoney, the first transition of every symbolic test generated without filtering is infeasible, so that no test is instantiable. In contrast, with filtering, this transition is replaced by a feasible one and 94% of the tests become instantiable. Notice that even without unproved POs, the abstraction computed by GeneSyst is still an over-approximation and may produce uninstantiable tests. Our study shows that except in one case, this has a limited practical impact on our examples.

IX. CONCLUSION, RELATED AND FURTHER WORKS

We have presented in this paper an MBT process based on the use of an abstraction A of a model M. A is generated from a set of abstraction predicates that are defined based on the state variables involved and modified by a test purpose TP. A and TP are synchronized into a model SP made of all the sequences of A that match TP. By covering all the states and transitions of SP we get a set of symbolic abstract tests. Since A is an abstraction that models more executions than M, whose states and transitions are over-approximated, it is possible that at the end, the instantiated test suites do not cover all the states and all the transitions of SP. But Sec. VIII shows that the ratio of instantiated tests is satisfactory in practice, although we use a naive and incomplete algorithm.

Our method helps in finding executions of M that match TP. SP brings the following information to help the search for TP executions that exist in M: the predicates that define the symbolic states and the instantiation of the generic action calls. Our first experimental results indicate that the method should provide a valuable help in practice. We have shown in [START_REF] Julliand | Generating tests from B specifications and dynamic selection criteria[END_REF] the complementarity of our tests with the LTG ones.

Other works are about the generation of tests from abstraction. We make a predicate abstraction as in [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF]. T. Ball uses it to generate structural tests of a program. He computes a boolean abstraction from a set of predicates which is the set of all the control-flow conditions of the program. We use an abstraction to generate functional tests in an MBT approach. We compute abstractions from a set of predicates defined from a test purpose as presented in Sec. VI. These two abstraction methods are based on weakest precondition and strongest postcondition computations, but by considering a model instead of a program, our method benefits from invariant properties to obtain a finer abstraction. Moreover, as we are in an MBT context, we are able to compute an oracle. Both methods aim at maximizing the ratio of the number of instantiated tests to the number of symbolic tests. We compute an over-approximation and we experimentally show that this ratio is between 35% and 94% on our case studies (except in a particular case that is explained in Sec. VIII-C) using an incomplete algorithm. In [START_REF] Ball | A theory of predicate-complete test coverage and generation[END_REF], Ball presents a method to compute a lower bound of the set of reachable states. Then he only generates instantiable tests which cover this set. Our LTS should be extended in Tri-Modal Transition System [START_REF] Godefroid | On the expressiveness of 3-valued models[END_REF] to make this lower bound computation possible.

The method implemented in the tool Agatha [START_REF] Rapin | Behavioral unfolding of formal specifications based on communicating extended automata[END_REF] also computes an abstraction from a model, but by applying a symbolic execution technique. This abstraction approach on data of models is very different from predicate abstractions. In [START_REF] Rapin | Behavioral unfolding of formal specifications based on communicating extended automata[END_REF], Agatha does not make use of test purposes.

The methods in [START_REF] Calamé | Automatic model-based generation of parameterized test cases using data abstraction[END_REF] implemented in STG [START_REF] Jeannet | Symbolic test selection based on approximate analysis[END_REF] use an abstraction defined by the user and modelled by an IOSTS (Input Output Symbolic Transition System). These approaches use test purposes synchronized with abstractions, both defined as IOSTS. Then the synchronized product allows for generating tests after an optimization step, which consists of a pruning of unreachable states by abstract interpretation. Our approach is very similar in that we also use test purposes and abstractions, as well as synchronization and constraint solving techniques to instantiate the symbolic tests. The two following points explain the differences. First, our abstractions are computed from a set of predicates that are defined from the test purposes, whereas the abstractions used by STG are given by the user. Second, the optimization is performed by the abstraction computation. It consists of using the invariant properties (that do not exist in an IOSTS) of the models in the weakest precondition computation for the minimization of the symbolic state space and of the feasible transitions.

The approach in our paper differs from the one of [START_REF] Fraser | Coverage based testing with test purposes[END_REF], where the test purposes are generic and aim at achieving a static coverage of the instructions and the conditions. Our method intends to become integrated into LTG, that already achieves such a static coverage, to complete it with tests issued from dynamic criteria. Another difference with [START_REF] Fraser | Coverage based testing with test purposes[END_REF] is that our approach relies on abstractions.

As in [START_REF] Ammann | Using model checking to generate tests from specifications[END_REF] and [START_REF] Hong | A temporal logic based theory of test coverage and generation[END_REF], it is also possible to describe test purposes by means of LTL properties, that specify particular state sequencings. Our language allows for specifying action calls in addition to states descriptions.

This work has to be pursued to better assess the contribution of the method, from a practical point of view. It seems necessary to reduce the time for generating the abstraction, for example by using syntactic abstraction as defined in [START_REF] Namjoshi | Syntactic program transformations for automatic abstraction[END_REF]. Also, a finer combination of the proof and constraint solving techniques may significantly help to remove the transitions that really cannot be instantiated from SP. Our valuation algorithm also needs to be improved. This will provide a better generation of the instantiated tests.

Fig. 1 .

 1 Fig. 1. Model-Based Testing Approach

Fig. 2 .

 2 Fig. 2. Generating Tests from Test Purpose by Abstraction

Fig. 4 .

 4 Fig. 4. A Test Purpose for Qui-Donc

Fig. 5 .

 5 Fig. 5. An Abstraction of the Qui-Donc System

  For example, the strongest postcondition for the precondition State ∈ D M (State) of the only EGA of Call is the predicate State ′ ∈ {welcome}.

	So we have SD x sp ∪SD x op

  State variable has three subdomains: State ∈ {welcome}, State ∈ {put down}, State ∈ {enter num, find urgency, find num, busy} (shortly State / ∈ {welcome, put down}). They are obtained as follows. The variable State is not used in the state predicates (SD State The variable State is modified by every action appearing in TP (Call, HangUp). State ∈ {welcome} is the strongest postcondition of the action Call and State ∈ {put down} is the strongest postcondition of the action HangUp. State / ∈ {welcome, put down} is the complement of the domain of the variable State.

sp = {}).

TABLE I METRICS

 I ON BEHAVIORAL MODEL, ABSTRACTION GENERATION AND SIZE OF SYNCHRONOUS PRODUCT

	Model	LTG Test Generation ♯Tests Average Standard ♯Tests Test generation from M Average ♯Symbolic Average ♯Instant. Average ♯Instant. tests / Time Instantiation of the SP tests without Filtering length deviation length tests length tests length ♯Symbolic tests	Instantiation of the SP tests with Filtering ♯Symbolic Average ♯Filtered ♯Instant. Average ♯Instant. tests / Time tests length Trans. tests length ♯Symbolic tests
	Qui-Donc	20 9	3.65 2.66	1.02 0.81	23 26	9.3 8.3	10 15	5.3 8	4 5	3 5.6	4/10 (40%) ≤ 1 sec. 5/15 (33%) ≤ 1 sec.	10 11	4.9 8.2	2 2	6 6	3.8 7.8	6/10 (60%) ≤ 1 sec. 6/11 (55%) ≤ 1 sec.
	Robot	19 24	4.10 4.25	1.36 1.21	71 808	149.3 32.2	12 23	11.1 9.1	7 8	21 23.1	7/12 (58%) 8/23 (35%)	3 min. 5 min.	11 23	11.18 9.1	1 0	7 8	23.7 23.1	7/11 (64%) 8/23 (35%)	2 min. 5 min.
	DeMoney	26 13	1.57 1.07	0.53 0.14	-		32 42	10.88 10.2	0 0	--	0/32 (0%) 0/32 (0%)	2 h. 2 h.	19 18	10.78 10.1	49 56	0 17	-12.48	0/19 (0%) 17/18 (94%)	2 h. 1 h.

TABLE II TEST

 II GENERATION FROM STATIC AND DYNAMIC CRITERIA, TESTS INSTANTIATION STATISTICS

LTG and TD are from Smartesting: http://www.smartesting.com

Conformiq is from Qtronic : http://www.conformiq.com

Its LTS can be seen on: http://lifc.univ-fcomte.fr/∼testAndAbs/index.html


Christophe Guyeux

Senior Member IEEE Jacques M Bahi

Topological chaos and chaotic iterations Application to Hash functions

This paper introduces a new notion of chaotic algorithms. These algorithms are iterative and are based on so-called chaotic iterations. Contrary to all existing studies on chaotic iterations, we are not interested in stable states of such iterations but in their possible unpredictable behaviors. By establishing a link between chaotic iterations and the notion of Devaney's topological chaos, we give conditions ensuring that these kind of algorithms produce topological chaos. This leads to algorithms that are highly unpredictable. After presenting the theoretical foundations of our approach, we are interested in its practical aspects. We show how the theoretical algorithms give rise to computer programs that produce true topological chaos, then we propose applications in the area of information security.

I. INTRODUCTION

The use of chaos in various fields of information security such as data hiding, hash functions, or pseudo-random number generators is almost always based on the conception of algorithms that include known chaotic maps such as the logistic map. The goal is to obtain an algorithm which preserves the chaotic properties of the included chaotic functions. For example, in [START_REF] Wu | A chaos based robust spatial domain watermarking algorithm[END_REF] and [START_REF] Wu | A novel digital watermark algorithm based on chaotic maps[END_REF], a watermark W is encrypted in W e by using the bitwise exclusive or: W e = W ⊗ X, where X is a logistic map. Then, pixels of the carrier image designed to embed these bits are selected with the 2-D Arnold's cat map. A similar use of chaotic maps for watermarking can be found in e.g. [START_REF] Zhao | A novel wavelet image watermarking scheme combined with chaos sequence and neural network[END_REF], [START_REF] Song | Extracting information masked by chaos and contaminated with noise: Some considerations on the security of communication approaches using chaos[END_REF], [START_REF] Liu | An image fragile watermark scheme based on chaotic image pattern and pixel-pairs[END_REF], [START_REF] Cong | A wavelet packets watermarking algorithm based on chaos encryption[END_REF] and [START_REF] Dawei | A chaos-based robust wavelet-domain watermarking algorithm[END_REF]. In the domain of hash functions, the use of chaotic maps is seen in e.g. [START_REF] Fei | A secure digital signature algorithm based on elliptic curve and chaotic mappings[END_REF], [START_REF] Wang | One-way hash function construction based on the extended chaotic maps switch[END_REF], [START_REF] Xiao | Improving the security of a parallel keyed hash function based on chaotic maps[END_REF] and [START_REF] Peng | One way hash function construction based on two-dimensional hyperchaotic mappings[END_REF]. However, without rigorous proof it is not indisputable that an algorithm that includes chaotic functions preserves chaos properties: for example, using the logistic function with other "obvious" parameters does not guarantee that the algorithm is chaotic. Moreover, even if the algorithm obtained by the inclusion of chaotic maps is itself chaotic, the implementation of this algorithm on a machine can cause it to lose its chaotic nature. This is due to the finite nature of the machine numbers set. These issues are discussed in this document.

In this paper we don't simply integrate chaotic maps hoping that the security algorithm remains chaotic, we conceive algorithms for computer security that we mathematically prove chaotic. We raise the question of their implementation, proving in doing so that it is possible to design a chaotic algorithm and a chaotic computer program.

Christophe Guyeux and Jacques M. Bahi are with the Computer Science Laboratory LIFC, University of Franche-Comte, 16, route de Gray -25030 Besanc ¸on, France (phone: +33 381 666948; email: {christophe.guyeux, jacques.bahi}@univ-fcomte.fr).

The chaos theory we consider is Devaney's topological chaos. In addition to being recognized as one of the best mathematical definition of chaos, this theory offers a framework with qualitative and quantitative tools to evaluate the notion of unpredictability. As an application of our fundamental results, we are interested in the area of information security. We propose in this paper a new approach of security which is based on unpredictability as it is defined by Devaney's chaos.

The paper begins by introducing the theoretical foundation of the new approach. We recall the definition of Devaney's topological chaos as well as the definition of discrete chaotic iterations. Although these definitions are distinct from each other, we establish a link between them by giving conditions under which chaotic discrete iterations generate a Devaney's topological chaos. Because chaotic iterations are very suited for computer programming, this link allows us to generate Devaney's chaos topological in the computer science field. After having studied the theoretical aspects of our approach we focus on practical aspects. The important question is how to preserve the topological chaos properties in a set of a finite number of states. This question is answered by introducing a concept we call secure chaotic information machine. This is a Mealy machine generating chaos as defined by Devaney (Section IV). We also give some applications of our approach of chaos, in the domain of information security. Algorithms intended for information security and based on this new approach are explained in Section V, in the hash function domain

The rest of this paper is organized as follows. In Section II, the definitions of Devaney's chaos and discrete chaotic iterations are recalled. A link between these two notions is established and sufficient conditions to obtain Devaney's topological chaos from discrete chaotic iterations are given in Section III. In Section IV, the question on how to apply the theoretical result is raised and applications in the computer science field are given in Section V. The paper ends with a conclusion in which our contribution is summarized and the planned future work is discussed.

II. BASIC RECALLS

This section is devoted to basic definitions and terminologies in the field of topological chaos and in the one of chaotic iterations.

A. Devaney's chaotic dynamical systems

Consider a metric space (X, d) and a continuous function f : X -→ X.

Definition f is said to be topologically transitive if, for any pair of open sets U, V ⊂ X, there exists k > 0 such that

f k (U) ∩ V ∅. Definition An element (a point) x is a periodic element (point) for f of period n ∈ N * , if f n (x) = x. The set of periodic points of f is denoted Per( f ). Definition (X, f ) is said to be regular if the set of periodic points is dense in X, ∀x ∈ X, ∀ε > 0, ∃p ∈ Per( f ), d(x, p) ε.
Definition f has sensitive dependence on initial conditions if there exists δ > 0 such that, for any x ∈ X and any neighborhood V of x, there exists y ∈ V and n

0 such that | f n (x) -f n (y)| > δ. δ is called the constant of sensitivity of f .
Let us now recall the definition of a chaotic topological system, in the sense of Devaney [START_REF] Devaney | An Introduction to Chaotic Dynamical Systems, 2nd Edition[END_REF]:

Definition f : X -→ X is said to be chaotic on X if, 1) f has sensitive dependence on initial conditions, 2) f is topologically transitive, 3) (X, f ) is regular.
Therefore, quoting Robert Devaney: "A chaotic map possesses three ingredients: unpredictability, indecomposability and an element of regularity. A chaotic system is unpredictable because of the sensitive dependence on initial conditions. It cannot be broken down or decomposed into two subsystems, because of topological transitivity. And, in the midst of this random behavior, we nevertheless have an element of regularity, namely the periodic points which are dense." Fundamentally different behaviors are thus possible and occur in an unpredictable way.

B. Chaotic iterations

In the sequel S n denotes the n th term of a sequence S , V i denotes the i th component of a vector V and f k = f • ... • f denotes the k th composition of a function f . Finally, the following notation is used: 1; N = {1, 2, . . . , N}. Let us consider a system of a finite number N of elements (or cells), so that each cell has a boolean state. Then a sequence of length N of boolean states of the cells corresponds to a particular state of the system. A sequence which elements belong to 1; N is called a strategy. The set of all strategies is denoted by S.

Definition The set B denoting {0, 1}, let f : B N -→ B N be a function and S ∈ S be a strategy. Then, the so-called chaotic iterations are defined by x 0 ∈ B N and ∀n ∈ N * , ∀i ∈ 1; N ,

x n i =      x n-1 i if S n i f (x n-1 ) S n if S n = i. ( 1
)
In other words, at the n th iteration, only the S n -th cell is "iterated". Note that in a more general formulation, S n can be a subset of components and f (x n-1 ) S n can be replaced by f (x k ) S n (where k n -1), describing for example delays transmission (see e.g. [START_REF] Bahi | Stability of fully asynchronous discrete-time discrete state dynamic networks[END_REF]). For the general definition of such chaotic iterations, see e.g. [START_REF] Robert | Discrete Iterations: A Metric Study[END_REF].

III. CHAOTIC ITERATIONS AS DEVANEY'S CHAOS

A. The new topological space

In this section we will put our study in a topological context by defining a suitable metric space where chaotic iterations are continuous.

1) Defining the iteration function and the phase space: Let δ be the discrete boolean metric, δ(x, y) = 0 ⇔ x = y. Given a function f , define the function:

F f : 1; N × B N -→ B N (k, E) -→ E j .δ(k, j) + f (E) k .δ(k, j) j∈ 1;N
, where + and . are the boolean addition and product operations. Consider the phase space:

X = 1; N N × B N ,
and the map defined on X:

G f (S , E) = σ(S ), F f (i(S ), E) , (2)
where σ is the shift function defined by σ(S n ) n∈N ∈ S -→ (S n+1 ) n∈N ∈ S and i is the initial function i : (S n ) n∈N ∈ S -→ S 0 ∈ 1; N . Then the chaotic iterations defined in (II-B) can be described by the following iterations:

X 0 ∈ X X k+1 = G f (X k ).
With this formulation, a shift function appears as a component of chaotic iterations. The shift function is a famous example of a chaotic map [START_REF] Devaney | An Introduction to Chaotic Dynamical Systems, 2nd Edition[END_REF] but its presence is not sufficient enough to claim G f as chaotic. In the rest of this section we prove rigorously that under some hypotheses, chaotic iterations generate topological chaos. Furthermore, due to the suitability of chaotic iterations for computer programming we also prove that this is true in the computer science field.

2) Cardinality of X: By comparing S and R, we have the result. theorem 1 The phase space X has, at least, the cardinality of the continuum.

Proof: Let ϕ be the map which transforms a strategy into the binary representation of an element in [0, 1[, as follows. If the n th term of the strategy is 0, then the n th associated digit is 0, or else it is equal to 1. With this construction,

ϕ : 1; N N -→ [0, 1] is surjective. But ]0, 1[ is isomorphic to R (x ∈]0, 1[ → tan(π(x -1 2 )
) is an isomorphism), so the cardinality of 1; N N is greater or equal to the cardinality of R. As a consequence, the cardinality of the Cartesian product X = 1; N N × B N is greater or equal to the cardinality of R.

remark 1 This result is independent from the number of cells of the system.

3) A new distance: We define a new distance between two points

X = (S , E), Y = ( Š , Ě) ∈ X by d(X, Y) = d e (E, Ě) + d s (S , Š ), where                    d e (E, Ě) = N k=1 δ(E k , Ěk ), d s (S , Š ) = 9 N ∞ k=1 |S k -Š k | 10 k .
If the floor value ⌊d(X, Y)⌋ is equal to n, then the systems E, Ě differ in n cells. In addition, d(X, Y) -⌊d(X, Y)⌋ is a measure of the differences between strategies S and Š . More precisely, this floating part is less than 10 -k if and only if the first k terms of the two strategies are equal. Moreover, if the k th digit is nonzero, then the k th terms of the two strategies are different.

4) Continuity of the iteration function:

To prove that chaotic iterations are an example of topological chaos in the sense of Devaney [START_REF] Devaney | An Introduction to Chaotic Dynamical Systems, 2nd Edition[END_REF], G f must be continuous in the metric space (X, d).

theorem 2 G f is a continuous function.
Proof: We use the sequential continuity. Let (S n , E n ) n∈N be a sequence of the phase space X, which converges to (S , E). We will prove that G f (S n , E n ) n∈N converges to G f (S , E) . Let us recall that for all n, S n is a strategy, thus, we consider a sequence of strategies (i.e. a sequence of sequences). As d((S n , E n ); (S , E)) converges to 0, each distance d e (E n , E) and d s (S n , S ) converges to 0. But d e (E n , E) is an integer, so ∃n 0 ∈ N, d e (E n , E) = 0 for any n n 0 . In other words, there exists a threshold n 0 ∈ N after which no cell will change its state:

∃n 0 ∈ N, n n 0 =⇒ E n = E.
In addition, d s (S n , S ) -→ 0, so ∃n 1 ∈ N, d s (S n , S ) < 10 -1 for all indexes greater than or equal to n 1 . This means that for n n 1 , all the S n have the same first term, which is S 0 : ∀n n 1 , S n 0 = S 0 . Thus, after the max(n 0 , n 1 ) th term, states of E n and E are identical and strategies S n and S start with the same first term. Consequently, states of G f (S n , E n ) and G f (S , E) are equal, so, after the max(n 0 , n 1 ) th term, the distance d between these two points is strictly less than 1. We now prove that the distance between G f (S n , E n ) and

G f (S , E) is convergent to 0. Let ε > 0. • If ε 1, we see that distance between G f (S n , E n ) and
G f (S , E) is strictly less than 1 after the max(n 0 , n 1 ) th term (same state).

• If ε < 1, then ∃k ∈ N, 10 -k ε 10 -(k+1) . But d s (S n , S ) converges to 0, so

∃n 2 ∈ N, ∀n n 2 , d s (S n , S ) < 10 -(k+2) ,
thus after n 2 , the k + 2 first terms of S n and S are equal.

As a consequence, the k + 1 first entries of the strategies of G f (S n , E n ) and G f (S , E) are the same (G f is a shift of strategies) and due to the definition of d s , the floating part of the distance between (S n , E n ) and (S , E) is strictly less than 10 -(k+1) ε.

In conclusion,

∀ε > 0, ∃N 0 = max(n 0 , n 1 , n 2 ) ∈ N, ∀n N 0 , d G f (S n , E n ); G f (S , E) ε.
G f is consequently continuous.

In this section, we proved that chaotic iterations can be modeled as a dynamical system in a topological space. In the next section, we show that chaotic iterations are a case of topological chaos, according to Devaney.

B. Discrete chaotic iterations as topological chaos

To prove that we are in the framework of Devaney's topological chaos, we have to find a boolean function f such that G f satisfies the regularity, transitivity and sensitivity conditions. We will prove that the vectorial logical negation

f 0 (x 1 , . . . , x N ) = (x 1 , . . . , x N ) (3)
is a suitable function.

1) Regularity:

theorem 3 Periodic points of G f 0 are dense in X.
Proof: Let ( Š , Ě) ∈ X and ε > 0. We are looking for a periodic point ( S , E) satisfying d(( Š , Ě); ( S , E)) < ε. As ε can be strictly lesser than 1, we must choose E = Ě. Let us define k 0 (ε) = ⌊log 10 (ε)⌋ + 1 and consider the set

S Š ,k 0 (ε) = S ∈ S/S k = Š k , ∀k k 0 (ε) . Then, ∀S ∈ S Š ,k 0 (ε) , d((S , Ě); ( Š , Ě)) < ε. It remains to choose S ∈ S Š ,k 0 (ε) such that ( S , E) = ( S , Ě) is a periodic point for G f 0 . Let J = i ∈ {1, ..., N}/E i Ěi , where (S , E) = G k 0 f 0 ( Š , Ě
) , i 0 = card(J) and j 1 < j 2 < ... < j i 0 the elements of J. Then, S ∈ S Š ,k 0 (ε) defined by

• S k = Š k , if k k 0 (ε), • S k = j k-k 0 (ε) , if k ∈ {k 0 (ε) + 1, k 0 (ε) + 2, ..., k 0 (ε) + i 0 }, • and S k = S j , where j k 0 (ε) + i 0 is satisfying j ≡ k (mod k 0 (ε) + i 0 ), if k > k 0 (ε) + i 0 , is such that ( S , E) is a periodic point, of period k 0 (ε) + i 0 , which is ε-closed to ( Š , Ě). As a conclusion, (X, G f 0 ) is regular.
2) Transitivity:

theorem 4 (X, G f 0 ) is topologically transitive. Proof: Let us define E : X → B N , such that E(S , E) = E. Let B A = B(X A , r A ) and B B = B(X B , r B ) be two open balls of X, with X A = (S A , E A ) and X B = (S B , E B ). We are looking for X = ( S , E) in B A such that ∃n 0 ∈ N, G n 0 f 0 ( X) ∈ B B .
X must be in B A and r A can be strictly lesser than 1, so

E = E A . Let k 0 = ⌊log 10 (r A ) + 1⌋. Then ∀S ∈ S, if S k = S k A , ∀k k 0 , then (S , E) ∈ B A . Let us notice ( Š , Ě) = G k 0 f 0 (S A , E A ) and c 1 , ..., c k 1 the elements of the set {i ∈ 1, N / Ěi E(X B ) i }. So any point X of the set {(S , E A ) ∈ X/∀k k 0 , S k = S k A and ∀k ∈ 1, k 1 , S k 0 +k = c k } is satisfying X ∈ B A and E G k 0 +k 1 f 0 (X) = E B . Lastly, let us define k 2 = ⌊log 10 (r B )⌋ + 1. Then X = ( S , E) ∈ X defined by: 1) X = E A , 2) ∀k k 0 , S k = S k A , 3) ∀k ∈ 1, k 1 , S k 0 +k = c k , 4) ∀k ∈ N * , S k 0 +k 1 +k = S k B , is such that X ∈ B A and G k 0 +k 1 f 0 ( X) ∈ B B .
3) Sensitive dependence on initial conditions: theorem 5 (X, G f 0 ) has sensitive dependence on initial conditions.

Proof: Banks et al. proved in [START_REF] Banks | On devaney's definition of chaos[END_REF] that having sensitive dependence is a consequence of being regular and topologically transitive.

4) Devaney's Chaos: In conclusion, (X, G f 0 ) is topologically transitive, regular and has sensitive dependence on initial conditions. Then we have the following result: theorem 6 G f 0 is a chaotic map on (X, d) in the sense of Devaney.

remark [START_REF] Banks | On devaney's definition of chaos[END_REF] We have proven that the set C of the iterate functions f so that (X, G f ) is chaotic (according to the definition of Devaney), is a nonempty set. In future work, we will deepen the study of C, among other things, by computing its cardinality and characterizing this set.

IV. CHAOS IN A FINITE STATE MACHINE

A. The approach presented in this paper

In the section above, it has been proven that discrete chaotic iterations can be put in the field of discrete dynamical systems:

x 0 ∈ X x n+1 = G f (x n ), (4)
where (X, d) is a metric space and G f is a continuous function. Thus, it becomes possible to study the topological behavior of those chaotic iterations. Precisely, it has been proven that if the iterate function is based on the vectorial logical negation f 0 , then chaotic iterations generate chaos according to Devaney. Therefore chaotic iterations, as Devaney's topological chaos, satisfy: sensitive dependence on the initial conditions, unpredictability, indecomposability, and uniform repartition.

Two major problems typically occur when trying to develop a computer program with chaotic behavior. First, computers have a finite number of states, so the computations always enter into cycles. Second, the properties of chaotic algorithms are inherited from a real chaotic sequence (like a logistic map) and this behavior is lost when computing floating-point numbers (unlike real numbers, floating-point numbers have a finite decimal part). These two problems are solved in this paper due to the two following ideas:

1) Chaotic iterations are Mealy machines. At each iteration, data corresponding to the current strategy II-B are taken from the outside world, then computations are realized into the memory (the updates of the finite state of the system). The last state is returned after a desired number of iterations. Contrary to the existing points of view, based on a Moore machine, this machine can pass two times in a same state, without continuing the same evolution. Section IV-B explains in detail this original contribution, which allows the realization of true chaos in computers. 2) As mentioned above, the strategy S defined in II-B will not depend on real numbers, but on integers taken from the outside world. We work with the set X defined in Subsection III-A.1 which has the cardinality of the continuum. Section IV-C discusses the consequences of dealing with finite strategies in practice.

B. A chaotic Mealy machine

The algorithms considered chaotic usually follow the principle of a Moore machine. After having received its initial states, the machine works alone with no interaction with the outside world. Its outputs only depend on the different states of the machine. The main problem is that when a machine with a finite number of states reaches a same state twice, the two following evolutions are identical. Such an algorithm always enters into a cycle. This behavior is highly predictable and cannot be set as chaotic. Attempts to define a discrete notion of chaos have been proposed, but they are not completely satisfactory and are less recognized than the notion of Devaney's topological chaos. This problem does not occur in a Mealy machine. This finite state transducer generates an output O computed from its current state E and the current value of an input S (Fig. 1). By this accord, even if the machine reaches the same state twice, the corresponding following evolutions may be completely different depending on the values of the inputs. The method presented here is based on such a machine. Indeed, chaotic iterations are a Mealy machine: at each iteration, the computations take into account new inputs (strategies) which are obtained, for example, from the media on which our algorithm applies. Roughly speaking, as the set of all media is infinite, we obtain a finite state machine which can evolve in infinite ways, thus making it possible to obtain a true chaos in computers.

Definition A Mealy machine is said to be chaotic if this machine has a chaotic behavior, as expressed by Devaney.

The Mealy machine we used in this document will be the chaotic iterations with G f 0 as iterate function. Because these chaotic iterations satisfy the Devaney's definition of chaos, as stated in Section III-B.4, we can conclude that our Mealy machine is a chaotic machine.

C. The practical case of finite strategies

It is worthwhile to notice that even if the set of machine numbers is finite, we deal in practice with the infinite set of strategies that have finite but unbounded lengths. Indeed, as suggested before, it is not necessary to store all the terms of the strategy in the memory. Only its n th term (an integer less than or equal to N) has to be stored at the n th step, as it is illustrated in the following example. Let us suppose that a given text is input from the outside world into the computer character by character and that the current term of the strategy is computed from the ASCII code of the current stored character. Since the set of all possible texts of the outside world is infinite and the number of their characters is unbounded, we work with an infinite set of finite but unbounded strategies. Of course, the previous example is a simplistic one. A chaotic procedure should to be introduced to generate the terms of the strategy from the stream of characters. In the computer science framework, we also have to deal with a finite set of states of the form B N and as stated before an infinite set S of strategies. The sole difference with the theoretical study is that instead of being infinite the sequences of S are finite with unbounded length. The proofs of continuity and transitivity are independent of the finiteness of the length of strategies (sequences of S). Sensitivity can be proved too in this situation. So even in the case of finite machine numbers, we have the two fundamental properties of chaos: sensitivity and transitivity, which respectively implies unpredictability and indecomposability (see [START_REF] Devaney | An Introduction to Chaotic Dynamical Systems, 2nd Edition[END_REF], p.50). The regularity supposes that the sequences are of infinite lengths. To obtain the analogous of regularity in the context of finite sets, we define below the notion of periodic but finite sequences. Definition A strategy S ∈ S is said to be periodic but finite if S is a finite sequence of length n and if there exists a divisor p of n, p n, such that ∀i np, S i = S i+p . A point (E, S ) ∈ X is said to be periodic but finite, if its strategy S is periodic but finite.

For example, (1, 2, 1, 2, 1, 2, 1, 2) (p=2) and (2, 2, 2) (p=1), are periodic but finite. This definition can be interpreted as the analogous of periodicity definition on finite strategies. Following the proof of regularity (Section III-B.1), it can be proven that the set of periodic but finite points is dense on X, hence obtaining a desired element of regularity in finite sets, as quoted by Devaney ([5], p.50): "two points arbitrary close to each other could have completely different behaviors, the one could have a cyclic behavior as long as the system iterates while the trajectory of the second could 'visit' the whole phase space". It should be recalled that the regularity was introduced by Devaney in order to counteract the effects of sensitivity and transitivity: two points close to each other can have fundamentally different behaviors.

V. HASH FUNCTIONS BASED ON TOPOLOGICAL CHAOS

A. Introduction

The use of chaotic maps to generate hash algorithms has seen several developments in recent years. In [START_REF] Fei | A secure digital signature algorithm based on elliptic curve and chaotic mappings[END_REF] for example, a digital signature algorithm based on an elliptic curve and chaotic mapping is proposed to strengthen the security of an elliptic curve digital signature algorithm. Other examples of the generation of a hash function using chaotic maps can be found in e.g. [START_REF] Wang | One-way hash function construction based on the extended chaotic maps switch[END_REF], [START_REF] Xiao | Improving the security of a parallel keyed hash function based on chaotic maps[END_REF] and [START_REF] Peng | One way hash function construction based on two-dimensional hyperchaotic mappings[END_REF]. However, as for digital watermarking, the use of any chaotic map does not guarantee that the resulting hash function would behave chaotically too. To our knowledge, this point is not discussed in these referenced papers, however it should be considered as important. We define in this section a new way to construct hash functions based on chaotic iterations. As a consequence of the theory presented before, the generated hash functions satisfy the topological chaos property. Thus, various desired properties in this domain are guaranted by our approach. For example, the avalanche criterion is closely linked to the sensitivity property.

B. A chaotic machine for hash functions

In this section, we explain a new way to obtain a hash value of a digital medium described by a binary sequence. It is based on chaotic iterations and satisfies the topological chaos property. The hash value will be the last state of some chaotic iterations: the initial state X 0 , finite strategy S and iterate function must then be defined. The initial condition X 0 = (S , E) is composed by a N = 256 bits sequence E and a chaotic strategy S . In the following sequence, we describe in detail how to obtain this initial condition from the original medium.

1) How to obtain E: The first step of our algorithm is to transform the message in a normalized 256 bits sequence E.

To illustrate this step we state that our original text is: "The original text". Each character of this string is replaced by its ASCII code (on 7 bits). Then, we add a 1 to this string. We now have the definitive length of our digest. Note that a lot of texts have the same string. This is not a problem because the strategy we will build depends on the whole text. Let us now build the strategy S .

2) How to choose S : To obtain the strategy S , an intermediate sequence (u n ) is constructed from D as follows:

• D is split into blocks of 8 bits. Then u n is the decimal value of the n th block.

• A circular rotation of one bit to the left is applied to D (the first bit of D is put on the end of D). Then the new string is split into blocks of 8 bits another time.

The decimal values of those blocks are added to (u n ). • This operation is repeated again 6 times.

It is now possible to build the strategy S :

S 0 = u 0 , S n = (u n + 2 × S n-1 + n) (mod 256).
S will be highly dependent to the changes of the original text, because θ -→ 2θ (mod 1) is known to be chaotic as defined by Devaney [START_REF] Devaney | An Introduction to Chaotic Dynamical Systems, 2nd Edition[END_REF].

3) How to construct the digest: To construct the digest, chaotic iterations are done with initial state X 0 ,

f : 1, 256 -→ 1, 256 (E 1 , . . . , E 256 ) -→ (E 1 , . . . , E 256 ),
as iterate function and S for the chaotic strategy.

The result of those iterations is a 256 bits vector. Its components are taken 4 per 4 bits and translated into hexadecimal numbers, to obtain the hash value:

63A88CB6AF0B18E3BE828F9BDA4596A6 A13DFE38440AB9557DA1C0C6B1EDBDBD

To compare, if instead of using the text "The original text" we took "the original text", the hash function returns:

33E0DFB5BB1D88C924D2AF80B14FF5A7 B1A3DEF9D0E831194BD814C8A3B948B3

In this paper, the generation of hash value is done with the vectorial boolean negation f 0 defined in eq. ( 3). Nevertheless, the procedure remains general and can be applied with any function f such that G f is chaotic. In the following subsection, a complete example of the procedure is given.

C. Application example

Let us consider the two black and white images of size 64 × 64 in Fig. 2, in which the pixel in position (40,40) has been changed. In this case, our hash function returns: These examples give an illustration of the avalanche effect obtained by this algorithm. A more complete study of the properties possessed by our hash functions and resistance under collisions will be studied in future work.

VI. CONCLUSION

In this paper, a new approach to generate algorithms with chaotic behaviors is proposed. This approach is based on the well-known Devaney's topological chaos. The algorithms which are of iterative nature are based on the so-called chaotic iterations. This is achieved by establishing a link between the notions of topological chaos and chaotic iterations. This is the first time that such an approach is considered for chaotic iterations. Indeed, we are not interested in stable states of such iterations as it has always been the case in the literature, but in their unpredictable behavior. After a solid theoretical study, we consider the practical implementation of the proposed algorithms by evaluating the case of finite sets. We study the behavior of the induced computer programs proving that it is possible to design true chaotic computer programs. A simple application is proposed in the area of hash functions. The security in this case is defined by the unpredictability of the behavior of the proposed algorithm. The algorithm derived from our approach satisfies important properties of topological chaos such as sensitivity to initial conditions, uniform repartition (as a result of the transitivity), and unpredictability. The results expected in our study have been experimentally checked. The choices made in this first study are simple: the aim was not to find the best hash function, but to give simple illustrated examples to prove the feasibility in using the new kind of chaotic algorithms in computer science. In future work, we will investigate other choices of iteration functions and chaotic strategies. We will try to characterize transitive functions. Other properties induced by topological chaos, such as entropy, will be explored and their interest in the information security framework will be shown.

Fig. 1 .

 1 Fig. 1. Mealy machine for chaotic algorithms.

  binary value (1111000) of the length of this string (120) is added, with another 1:The whole string is copied, but in the opposite direction. This gives: obtain a multiple of 512, by duplicating this string enough and truncating at the next multiple of 512. This string in which the whole original text is contained, is denoted by D.Finally, we split our obtained string into blocks of 256 bits and apply the exclusive-or function, obtaining a 256 bits sequence. the context of Subsection V-B, N = 256 and E is the above obtained sequence of 256 bits.

  (a) Original image. (b) Modified image.

Fig. 2 .

 2 Fig. 2. Hash of some black and white images.

Fig. 3 .

 3 Fig. 3. Hash of some grayscale level images.