Francesco Bongiovanni

Ludovic Henrio

A Mechanized Model for CAN Protocols

Keywords: Structured P2P, CAN, broadcast algorithm, theorem proving

Formal reasoning on Peer-to-Peer (P2P) systems is an intimidating task. This paper focuses on broadcast algorithms for Content Addressable Network (CAN). Since these algorithms run on top of complex P2P systems, finding the right level of abstraction in order to prove their functional correctness is difficult. This paper presents a mechanized model for both CAN and broadcast protocols over those networks. We demonstrate that our approach is practical by identifying sufficient conditions for a protocol to be correct and efficient. We also prove the existence of a protocol verifying those properties.

Introduction

Structured Overlay Networks (SONs) are a class of P2P systems that emerged in the last decade to provide an abstraction of a lookup service over a large number of distributed nodes. These technologies are widespread and can be found at the heart of companies such as Amazon, Facebook and Twitter [START_REF] Decandia | Dynamo: amazon's highly available key-value store[END_REF][START_REF] Lakshman | Cassandra: a decentralized structured storage system[END_REF].

Distributed applications operate now at a very large scale, and interactions between computers are no longer limited to one-to-one communications. Broadcast communication primitives simplify the application development by avoiding to explicitly write code for dissemination. In the context of a P2P system, communication primitives can be designed to take advantage of the logical topology to communicate efficiently. More important, such generic primitives can be proved to be correct, which increases the confidence the programmer and the user have in the system. In this article we are particularly interested in a broadcast algorithm running on top of the Content Addressable Network (CAN) [START_REF] Ratnasamy | A Scalable Content-Addressable Network[END_REF] in which the broadcasted message is received exactly once by each node; we say that such a broadcast algorithm is efficient. Previous works such as M-CAN [START_REF] Ratnasamy | Application-level multicast using content-addressable networks[END_REF] and Meghdoot [START_REF] Gupta | Meghdoot: contentbased publish/subscribe over P2P networks[END_REF] also attempt to leverage CAN in order to build an efficient dissemination infrastructure that can be used by distributed applications.

However, there is no free lunch. Building high-assurance distributed applications which are correct remains a very difficult challenge but various methods have emerged over the years to tackle it [START_REF] Bakhshi | Verification of peer-to-peer algorithms: A case study[END_REF][START_REF] Borgström | Verifying a structured peerto-peer overlay network: The static case[END_REF][START_REF] Guo | Practical software model checking via dynamic interface reduction[END_REF][START_REF] Lu | Towards Verification of the Pastry Protocol Using TLA +[END_REF][START_REF] Zave | Using lightweight modeling to understand chord[END_REF]. Theorem proving seems to be among the best method to prove generic properties on distributed systems of arbitrary size; in particular verification techniques based on model-checking are, in general, limited to systems of a predefined size and suffer from combinatorial explosion. This article promotes the use of theorem proving in the safe design of distributed systems, more particularly concerning the CAN overlay network.

We present here a mechanized model of CAN that will help the design of communication primitives and the formal proof of their properties. We use this model to define the characteristics and the properties of broadcast primitives. Our first contribution is thus a set of abstractions, properties, and theorems regarding the topological and the communication aspects of CAN. We formalize the CAN network, the messages over such a network, and a notion of connectivity: a zone is connected if any two nodes of this zone can communicate, possibly indirectly. Some of these proven abstractions can be reused with resembling topologies such as the Delaunay triangulation protocol (DT protocol) [START_REF] Liebeherr | Application-layer multicasting with delaunay triangulation overlays. Selected Areas in Communications[END_REF] and the Voronoi-based Overlay Network (VON) [START_REF] Hu | VON: a scalable peer-to-peer network for virtual environments[END_REF], widely used in online games. Our second contribution is to use our framework to characterize broadcast protocols and prove the existence of an efficient broadcast protocol by presenting a naive yet efficient correct-by-construction protocol and which directly leverage the topology of the structure; we do not build and maintain an extra layer on top of CAN (such as a broadcast tree) but rather make use of locally available information. Knowledge of the entire network is necessary for proving intermediary lemmas, but we show that such a knowledge is not used by the protocol itself.

We are interested in the proofs of functional correctness of broadcast algorithms for CAN, and of the fact that there is a protocol for which each node receives a message exactly once. We present selected Isabelle/HOL definitions and theorems to give an overview on how to reason about such algorithms and prove their properties. Our model is general and flexible enough to study CAN networks, as it provides the formalization of basic building blocks composing it. However, we are not interested in formalizing the full CAN protocol but rather on the minimal set of abstractions needed to reason about communication protocols for CANs. Overall, not only this paper proves that it is possible to design an efficient broadcast protocol for CAN but also that we can formally prove its correctness and efficiency. Compared to a realistic P2P network, we do not consider node churn in this study. Also we assume that reliability of point-to-point communication is an orthogonal concern that should be studied independently.

In §2, we present the CAN overlay network, the existing broadcast primitives for CAN, and the objectives of this paper. In §3 we present a mechanized model of CAN along with the proven abstractions making up the model. Broadcast algorithms are presented in §4. Finally we compare our study to other related work in §5.

Background and motivation

A CAN [START_REF] Ratnasamy | A Scalable Content-Addressable Network[END_REF] is a structured P2P network based on a d -dimensional Cartesian coordinate space, labelled D. This space is dynamically partitioned among all nodes in the system such that each node is responsible for storing data, in the form of (key, value) pairs, in a sub-zone of D. Each node is responsible for a zone, and the set of zones is disjoint and covers the whole space. To store (k, v)-pairs, the key k is deterministically mapped onto a point in D, using consistent hash functions, and the value v is stored by the node responsible for the zone containing this point. The search for the value corresponding to a key k is achieved by applying the same hash function on k in order to find the node responsible for storing the value. The routing process starts at the query originator and traverses iteratively its neighbors (a node only knows its adjacent neighbors), until the zone responsible for the key to store/retrieve is reached.

To limit the load on the network, we want to minimize the number of messages necessary to perform a broadcast. We first define precisely the hypotheses on the network topology to know exactly on which kind of networks our algorithms are valid. There are several ways to construct a broadcast algorithm depending on the structure of the CAN:

-The appendix of the seminal paper [START_REF] Ratnasamy | A Scalable Content-Addressable Network[END_REF] suggests to build a construction tree, where a node is child of another if it joined this other node. This construction tree can be used to perform an efficient broadcast but the root of the tree would be overloaded. The main drawback of this approach is that keeping the tree structure when nodes leave leads to strong constraints (only a leaf node can take the place of a leaving node) and may require huge data transfers. -In M-CAN [START_REF] Ratnasamy | Application-level multicast using content-addressable networks[END_REF] and Meghdoot [START_REF] Gupta | Meghdoot: contentbased publish/subscribe over P2P networks[END_REF], a CAN is defined as a structure where each node is responsible for an hyperrectangle: when a node leaves the network, its neighbour(s) can, for example, extend their own zone with the zone left by the leaving node. The only structure that can be exploited by a broadcast protocol is the graph of neighbors. Maintaining a spanning tree on such a structure with nodes joining and/or leaving the network is far from trivial. -A CAN can be defined as a structure where each node is responsible for an area with no particular shape. This structure fits with the protocol described in [START_REF] Ratnasamy | A Scalable Content-Addressable Network[END_REF] (Sec. 2.3): when a node leaves the network, its neighbour becomes responsible for its area. This is the most general case (it encompasses the two previous ones), and the one used here. Even in this unconstrained setting, we prove that an efficient broadcast algorithm exists.

Thus, we represent the network as a graph and provide an efficient algorithm on such a graph; computing a minimum spanning tree on this potentially evolving graph without global knowledge of the graph seems impossible. However, in a CAN, geometrical information can be exploited to avoid any two nodes from sending the same information to the same node. In this paper, our objective is to rely on a notion: "is a set of points connected?" which can be computed locally and to prove that, from this notion, we can design an efficient broadcast algorithm. The algorithm we propose here does not tolerate changes in the network during the broadcast, but it does support changes in the network between two broadcasts. Considering the case where a peer joins or leaves the CAN, i.e. node churn, is left for future work.

Figure 1 shows an efficient broadcast as ensured by M-CAN [START_REF] Ratnasamy | Application-level multicast using content-addressable networks[END_REF], the protocol sends messages first vertically (to a single neighbor above or below) and then horizontally, avoiding duplicates by sending only to the node that touches the lower corner. Unfortunately, this algorithm does not eliminate all duplicates if the dimension is greater than two. In a publish/subscribe context, Meghdoot [START_REF] Gupta | Meghdoot: contentbased publish/subscribe over P2P networks[END_REF], built atop CAN, also proposes a mechanism to avoid duplicates but requires the broadcast to originate from one corner of the zone to be covered. We underline here that no broadcast algorithm atop CAN has been actually formally specified.

Using an interactive theorem prover such as Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: a proof assistant for higher-order logic[END_REF] and its higherorder logic provides us the expressiveness needed to formalize distributed algorithms and reason about them. A higher order logic naturally supports the formalization of the data structures of the algorithms; it also provides the reasoning tools to prove properties on those algorithms and structures. The expressiveness of Isabelle's logic allows us to reason about an abstraction of the system we design, meaning that we can abstract away some details of the CAN overlay and focus on the aspects ensuring the properties of the broadcast algorithm.

Our motivation is to put forward abstractions for proving correctness properties of distributed algorithms on top of CAN, and to promote the development of distributed algorithms proven correct. CAN is a difficult setting for proofs, because the structure entails a geometrical structure, which is more difficult to handle in Isabelle than inductive structures. We abstract away most of the geometrical notions, and rely on the notion of connection between nodes, expressed as a neighbor relation. We focus on two properties of broadcast protocols:

-Efficiency: a node receives only one message during a broadcast.

-Coverage: all the nodes receive the message (correctness property). We write our specification in such a way that an external reader familiar with basic logic and mathematics can understand it. Indeed, our purpose is to make our results accessible and convincing for the community of distributed systems, including people not familiar with formal methods.

Efficiency vs. Robustness. One can easily argue that duplicating messages can actually increase the robustness of the broadcast in case of communication failures. However, the redundancy provided by a non-efficient broadcast algorithm is not satisfactory. Indeed with an inefficient algorithm, as shown in Figure 1, some nodes receive the message once, while other can receive it more than twice. Relying on an efficient algorithm is a better starting point in order to design robust algorithms in a smarter way. For example, to increase robustness, one could perform two efficient broadcasts in parallel from two different places in the network and reversing the dimensions of the CAN (considering the first one as the last one); this would ensure that each node receives each message exactly twice, most of the time coming from two different directions.

Reasoning about a CAN-like structure

This section presents the formalization of CAN written in Isabelle/HOL3 . We present below the most important definitions and lemmas, expressed in mathematical style; some notions will be defined informally but most of the details are omitted; instead we prefer to give some insights regarding the principles of the formalization. For manipulating structures we use the following notations: ! accesses an element of a list; # adds an element at the beginning of the list; @ appends two lists; fst and snd access the elements of a pair.

A first crucial question when formalizing a complex structure like a CAN is which level of abstraction should be used, and which notions of Isabelle/HOL should represent basic notions of CAN networks. We chose to represent a CAN by a set of nodes, a zone for each node, and a neighboring relationship, stating whether any two nodes are neighbors. More precisely, a CAN is a set of integers identifying the different nodes. A function CZ matches each node to a Zone; a zone is simply a set of points, where each point is represented by a tuple of integers: CZ N is the zone under the responsibility of the node N. Also we require that the set of nodes is finite and the set of their zones partitions the whole space into disjoint zones covering the whole space. Each node is responsible for a zone that never changes and is called the zone of a node; note that our broadcast algorithm will also rely on some zones, i.e. sets of points.

Definition 1 (CAN). The set of valid CANs is defined as follows: CAN ≡ {(Nodes, CZ, Neighbours).Nodes ∈ P(N)∧CZ ∈ N→Zone∧Neighbours ∈ P(N×N)

∧ symbN odes is finite ∧ Neighbours is finite ∧ ∀x, y. (x, y) ∈ Neighbours ⇒ (y, x) ∈ Neighbours ∧ ∀x. (x, x) / ∈ Neighbours ∧ ∀tup. ∃N ∈ Nodes. tup ∈ CZ(N ) ∧ ∀N, N ∈ Nodes. CZ(N ) = ∅ ∧ N = N ⇒ ¬(CZ(N ) intersects CZ(N )) }
We also define three auxiliary functions Nodes, Zones, and Neighbour returning each part of a CAN. We adopt a formalization more general and flexible than the strict CAN protocol, more precisely:

-As discussed in Section 2, each node is responsible for a zone of any shape, whereas in most CANs, each node should always be responsible for a single hyperrectangle. We believe that this formalization is better adapted to model a dynamic CAN with nodes joining/leaving the network. -We do not relate zones with the concept of neighbor. This alleviates us from geometric reasoning: we mainly rely on two relationships: "is a node neighbor of another?" and "do two zones intersect?" This allows us to reason at a topological level rather than a geometrical level.

We thus define a predicate Z intersects Z' that checks whether a zone Z intersects a zone Z' : it is true if Z and Z' have at least one point (tuple) in common. In the following, we say that "a node intersects a zone Z" if the zone of the node intersects Z. Then we define NodesInZone C Z, the set of nodes whose zones intersect the zone Z :

NodesInZone C Z = {N ∈ Nodes(C). Zones(C, N ) intersects Z}
We define the size of a zone ZoneSize C Z as the number of nodes it contains. Then we define the connectivity of a CAN zone. This notion is close to the geometrical notion of path connectivity but dedicated to the CAN networks. The idea is that a zone is connected if a message can go between any two nodes in the zone passing only through nodes intersecting the zone. In the context of a broadcast algorithm, we will know that in such a zone the broadcast is possible; this notion will also give us a criteria that we have to follow when dividing the area to be covered into smaller zones. We state that a zone is connected if between any two nodes intersecting the zone, there is a path of nodes intersecting the zone where two consecutive nodes of the path are neighbors.

Definition 2 (Connected). Connected C Z ⇔ ∀N, N ∈ NodesInZone C Z.
∃NL a list of distinct nodes starting by N and finishing by N .

∀i < length(NL)-1. NL!i ∈ NodesInZone C Z ∧ Neighbour(C, NL!i, NL!(i+1))
Lemmas. To reason about CAN structures, we define several generic lemmas related to topology. These lemmas ease the reasoning on connectivity, intersection and nodes. Some typical lemmas prove generic properties on connectivity or intersection on the union or the intersection of zones. These small lemmas will reveal particularly useful for proving the properties of broadcast protocols. Lemma 1, for instance, states that the union of two connected zones is connected if two nodes of the two zones are neighbors.

Lemma 1 (Connected-union).

Connected C Z Connected C Z N ∈ NodesInZone C Z N ∈ NodesInZone C Z Neighbour(C, N, N ) Connected C Z ∪ Z
We also prove a symmetric lemma, allowing us to find neighboring nodes in two zones, provided those two zones and their union are connected (and the union contains at least two nodes).

Reasoning by induction on a zone. We also provide induction principles that allow one to prove a property related to a zone by induction on the size of the zone. A trivial induction lemma expresses directly induction on the number of nodes in the zone on which the property is verified. More interestingly, one can prove a property by adding one by one the nodes belonging to the zone of interest; this allows some form of structural induction on a CAN zone.

Theorem 1 (induct-node-zone2).

P (∅) ∀Z. P (Z) ⇒ ∀N∈Nodes(C).N / ∈NodesInZone C Z ⇒ ∀Z . NodesInZone C Z = {N} ⇒ P (Z ∪Z ) P (Z)
This theorem states that, if (1) we prove that a property P is true for an empty zone, and (2) we prove that if P is true for a zone then it is true for a zone intersecting one more node; then the property is true for all zones. The proof of this induction principle mainly relies on the fact that the set of all nodes of the CAN C must cover the entire space. Messages and message paths. Once the network is defined, we define messages and paths followed by messages. As we will use messages to perform a broadcast towards a zone, a message is made of four parts: an identifier for the message m (which could represent also its payload), a source node x, a destination node y, and the zone Z to which it must be transmitted. We also define an abbreviation <m|x,y,Z > for defining a Message. Message-source, Message-dest, and Messagezone are functions accessing the last three fields.

We believe it is important to provide tools to reason about the path followed by a message. Indeed, communication inside CAN heavily relies on the notion of paths. For this, we define a path as a set of consecutive messages, and provide tools to reason inductively on those path.

Definition 3 (valid-path). valid-path is a predicate that checks whether the message path ML is valid, i.e. each message is sent from the destination of the previous message.

valid-path msgs ML

⇔ ML = [] ∧ distinct(ML) ∧ ∀i < length(ML). ML!i ∈ msgs) ∀i < length(ML)-1. Message-dest(ML!i) = Message-source(ML!(i+1))
For a path to be valid, we additionally require that no two messages are the same; indeed, we will only consider paths of messages among a finite set msgs and we would like to consider only paths of finite length, this allows us to reason about the longest path in a zone. We provide various lemmas for building (valid) paths and reasoning about them.

Broadcast Algorithms over a CAN

Defining a broadcast in a natural way using Isabelle/HOL is not trivial; here we decide to put an emphasis on the way messages are processed. Our formalization is centered around the specification of messages which are the consequences of a given message and on the specification of the set of messages used to broadcast the original message. Then we define the way messages are broadcasted by an inductive definition, where messages are "processed" one message after the other sequentially. In our formalization, Broadcasts are triple made of a CAN, a message set, and an initiator node constrained by several well-formedness rules. The constraints expressed in the definition state that: (1) There is a single message between any 2 nodes. (2) The initiator is a node of the CAN. [START_REF] Charron-Bost | Formal verification of a consensus algorithm in the heard-of model[END_REF] messages are exchanged between neighbor nodes of the CAN, and thus the broadcast pattern respects the CAN protocol. ( 4) All messages must be sent by a node that has been reached by a list of messages MsgL originating from the initiator. The existence of such a valid path ensures that a broadcast only relies on messages transmitted from nodes to nodes, and no message is spontaneously created (except for the initiator of course). Note that it is not sufficient to require that each message source is the destination of another message, because that would allow loops of messages not passing by the initiator. We denote <C,M,n> a Broadcast, and define functions BC-CAN, BC-msgs, and BC-init to access its fields. We can then define a predicate checking whether a broadcast covers the whole CAN, i.e., whether each node of the CAN is either the initiator or the destination of a message:

Definition 5 (Coverage).
Coverage (C, msgs, init) ⇔ ∀N ∈ Nodes(C).N = init ∨ ∃m, s, Z. < m|s, N, Z >∈msgs

We decided to rely on the notion of zone to be covered to define a broadcast algorithm because this seems quite adapted to the structure of the CAN. This zone to be covered can have two purposes depending on the algorithm. First it allows the specification of broadcast protocols where only the nodes in a given zone have to receive the message. Also, since we are interested in an efficient algorithm that minimizes the number of messages necessary to broadcast the information, it seems reasonable to split efficiently the zone to be covered in order to avoid sending a message to the same node twice. A broadcast algorithm can be entirely characterized by a function that, given a node N receiving a message and the zone Z to be covered by the message, returns a list of pairs (Zone, Node), that we call ZNL (Zone-Node list). Each pair (Z i , N i ) of the ZNL consists of Z i , a sub-zone of Z, and N i a neighbour of N belonging to Z i : the message is forwarded to N i that is now responsible for covering Z i . The zone Z i must be connected (as defined above) otherwise it would be impossible to cover it while staying inside Z i . Figure 4 illustrates the notion of ZNL for the first step of the broadcast: the message to be broadcasted is sent from the initiator to its neigbhors belonging to three different zones to be covered, which in turn, will be responsible for broadcasting the message to the zone they received.

Definition 6 defines an optimal ZNL, which underpins an efficient broadcast. To guarantee efficiency, we require that the zones of the list form a partition of the original zone, and that each node belong to the zone it receives. A broadcast will be efficient if every message generates an optimal ZNL. Definition 6 (Set-of-Optimal-ZNL).

Set-of-Optimal-ZNL C N Z ≡ ZNL. i<length(ZNL) fst(ZNL!i) = Z ∧ ∀i < length(ZNL). Neighbour(C, N, snd(ZNL!i)) ∧ Connected C fst(ZNL!i) ∧ snd(ZNL!i) ∈ NodesInZone C fst(ZNL!i) ∧ ∀j < length(ZNL). j = i ⇒ snd(ZNL!i) = snd(ZNL!j)∧ NoNodeInBothZones fst(ZNL!i) fst(ZNL!j)
Definition 7 specifies the set of messages of a broadcast algorithm based on ZNLmap, which is a function that, given a node and zone, returns an optimal ZNL. The set of messages of the broadcast is defined by induction rules expressing how messages are processed. The inductive definition is of the form ZNL-BC-msgs C Mid init znlmap msgs ML where C is the CAN network, Mid is the message identifier, init is the initiator node, and znlmap is the ZNLmap used by this instance of the algorithm. The inductive definition works as follows: it takes one by one messages in ML, called the list of messages to be treated, processes them and put them in the set of treated messages, msgs. Processing a message consists in using the function znlmap to compute the consequences of this message: for each couple (Z i , N i ) returned by (znlmap(Z, d)), a new message with destination N i and zone Z i minus the zone of N i which we just covered is created and put in the new ML list. The original message that has been processed is then put in msgs. The rules of Definition 7 are applied iteratively treating one message after the other. At the end, ML, the list of messages to be treated is empty, and msgs, the set of treated messages contains the list of messages of the broadcast.

Relying on a znlmap function is important here because it ensures that the broadcast algorithm is built without the knowledge of the messages already sent by the protocol. This ensures that only the knowledge of the current node and the zone to be covered is used to decide which message to send. We will see in the definition of the efficient broadcast how the znlmap function can be modified to take into account local information (i.e., neighbors and their zones). Some design choices have been made in the way messages are actually processed in our formalization. Messages are treated sequentially, but this of course does not correspond to the parallelism that occur in a real system. However this classical simplification has no consequence on the properties of interest here. More important is the fact that the messages to be treated (ML) are represented as a list, this total ordering is artificial and one could improve the representation by defining an equivalence relation allowing reordering of messages. However, the list is a good structure to reason inductively on the messages and to allow rules to be applied iteratively. Concerning treated messages (msgs), as we do not perform any further computation on them, a list was not necessary and we considered them to be a set; a multiset is not necessary because it is easy to prevent the same message to be sent twice between the same nodes.

We prove that the set of messages generated by an optimal ZNL constitutes a valid broadcast that covers the entire network:

Theorem 2 (ZNL-BC). ZNL-BC-msgs C Mid init znlmap Finalmsg [] init ∈ Nodes(C) ∀(Z, N ) ∈History(C, init, Finalmsg, []).znlmap(Z, N ) ∈ (Set-of-Valid-ZNL C N Z) (C, Finalmsg, init) ∈ Broadcast Theorem 3 (coverage-ZNL). ZNL-BC-msgs C Mid init znlmap Finalmsg [] N, init ∈ Nodes(C) ∀(Z, N ) ∈History(C, init, Finalmsg, []).znlmap(Z, N ) ∈ (Set-of-Valid-ZNL C N Z) ∃s, Z. < Mid|s, N, Z >∈ Finalmsg
In these two theorems, we consider the last step of induction, when the list of messages to be treated is empty ([]). Also, we require that for each zone and node of History, znlmap verifies set-of-Optimal-ZNL. History(. . .) is the set of pairs (zone, destination node) that influenced the previous treatment of messages, and will influence the processing of the next message if there is one. In other words, it is the set of pairs (zone,destination node) for the set of treated messages (msgs), and the next message to be treated (head of ML), plus the couple (initiator node, entire space). We also proved additional lemmas ensuring correctness and easing further proofs, e.g. that the message content is unchanged during the process.

The theorems presented above are not sufficient to prove that the final step of the induction (where no more message is to be treated) is reachable. That is why we proved that ensuring ∀Z N. znlmap(Z, N ) ∈ Set-of-Optimal-ZNL C N Z is sufficient to ensure progress from each step. However, this is still not sufficient to ensure reachability of the final step while we do not ensure that the broadcast process is finite. Also, the approach presented above requires to compute, from the beginning, the function znlmap, which is unrealistic. Below, we prove the existence of an efficient broadcast, built step by step, which ensures reachability of the final step.

An efficient broadcast algorithm A simple but efficient algorithm can be designed by constructing ZNLs as follows: suppose a node N receives a message with a given zone Z to cover, where Z ∪ CAN -Zones(C, N ) is connected. We split this zone into several zones Z i , where each zone is connected, no zone touches another (i = j ⇒ Z i ∪ Z j is not connected), and each zone contains a node N i neighbour of N . We first prove that such a decomposition necessarily exists (Lemma 2). The decomposition is optimal if the same node does not belong to two zones, which is true because, for any two zones, Z i ∪ Z j is not connected. We can thus prove that under the conditions mentioned above (Z ∪ CAN -Zones(C, N ) is connected), an optimal decomposition exists (Lemma 3).

Lemma 2 (Zone-decomposition).

∃zl.

i<length(zl) zl !i = Z ∧ ∀i <length(zl). Connected C zl !i ∧ ∀i, j <length(zl).i = j ⇒ ¬Connected C zl !i∪zl !j Lemma 3 (OptimalZNL-existence). N ∈ Nodes(C) Connected C (Z ∪Zones(C, N )) N / ∈ NodesInZone C Z ∃ZNL. ZNL ∈ Set-of-Optimal-ZNL C N Z
Then, we forward the message to each of the neighbour N i , delegating to it the zone Z i minus the zone of N i ; note that this new zone verifies the hypothesis above, and thus the decomposition mechanism can be applied recursively until each node receives the message. The drawback of the decomposition lemma is that it seems to require the knowledge of C. More precisely we need to know C to decide whether a zone Z is connected or not. In a real CAN, geometrical connectedness is sufficient to ensure network connectedness, and thus connectedness can be computed without knowing the exact network topology. Consequently, in a real CAN, the decomposition can be computed locally at the node that needs to forward the information.

Remember that, to reason about the whole algorithm, we parametrized ZNL-BC by the znlmap, supposed to be known originally, not computed at each step. To prove that our algorithm works, we need to compute the optimal znlmap at each step with local information. This issue can be resolved in two steps. First, we show that the messages of the broadcast are only sensitive to the values of znlmap for the history History(. . . ). Second, we show that, provided the history is optimal, we can treat one more message and provide an extended znlmap that is still optimal for the new history. Additionally, we prove side conditions on the set of messages treated and to be treated so that, e.g., we can prove that the algorithm terminates.

Theorem 4 (Progress-ZNL).

ZNL-BC-msgs

C Mid init znlmap msgs MList init ∈ Nodes(C) MList = [] ∀(Z, N ) ∈History(C, init, msgs, MList).znlmap(Z, N ) ∈ (Set-of-Valid-ZNL C N Z) ∃Mlist , znlmap . msgs∪set(Mlist) ⊆ msgs∪{MList!0}∪set(MList')∧ Message-zone(MList!0) = ∅ ∨ i<length(MList ) NodesInZone C Message-zone(MList !i) ⊂ i<length(MList) NodesInZone C Message-zone(MList!i) ∧ ∀(Z, N ) ∈History(C, init, msgs ∪ {MList !0}, MList ).znlmap(Z, N ) ∈ (Set-of-Valid-ZNL C N Z)
The consequences of those last steps are twofold. First, they allow us to build the znlmap at each step by finding, each time we treat a message, the new zone-node-list corresponding to the new message. Also, the specification above ensures that our algorithm terminates: it can always progress (because of the optimality of the ZNL) and we exhibited a well-founded order along which the set of messages to be treated decreases: at each step, the size of the zone to be covered by all the messages to be treated decreases strictly (i.e. the number of nodes intersecting it), or it stays the same and the number of messages to be treated decreases strictly.

Finally, we prove the two following theorems stating that the same node is not reached twice. More precisely, at each step, if a node received a message (it is the destination of a message treated or to be treated) then it is not the destination of another message, and it is not in a zone to be covered. Several intermediate lemmas guarantee the fact that zones to be covered are well-separated and finally, we prove that, at the last step of the broadcast protocol, no two nodes receive the message. Overall, we have proved that there is a broadcast protocol that do not send twice the message to the same node. All the steps shown above ensure that the znlmap function can be built iteratively from local information, and that no knowledge of the message history is necessary to build it. Concerning locality, we rely on the local decidability of the predicate "Connected C Z ", which can be evaluated without the knowledge of the whole network in the case of a real CAN thanks to geometrical considerations. Relying only on local knowledge is crucial for a P2P algorithm but we cannot prove it formally here. To solve this issue the solution would be to prove that the Lemma 3 is true in a n-dimensional space without knowledge of the whole network; such a proof would require the geometrical formalization of a CAN which is out of the scope of this study.

Concluding Remarks. It is important for us to have a formalism for expressing the CAN broadcast that is easy to understand. Although the specification we showed here is inductive and thus not in a classical form for a broadcast algorithm, we think it is clear enough to be convincing, and that it is easy to implement the program corresponding to our definitions. This way of expressing a broadcast algorithm is not as natural as one would expect because a form of event-based formulation of the algorithm "when a message M is received, send messages M1, M2, and M3" would be more adapted. However, such an eventlike formulation is not well supported in Isabelle/HOL, even if we could try to provide new abbreviations for expressing message transmission more easily. In fact, the definition of ZNL-BC distinguishes the messages for which the consequence have already been computed from the others, which is crucial in our proofs, changing this definition to a more implicit set-oriented one would make the proofs even more complex or unfeasible.

In our proofs, we rely on a single axiom that states that the entire space is connected, which is a necessary prerequisite that we are not able to prove since we do not relate neighborhood with any geometrical notion.

The current specification and proofs consist of almost 5000 lines of Isabelle, for more than 150 lemmas and theorems. The length of the proofs is however not uniform: simple properties on the network or the connectivity could take a couple of lines, whether advanced properties on connectivity, and most of the properties of the broadcast algorithm require dealing with a lot of cases, or rely on complex inductions, they necessitate several hundreds of lines.

Related Work

A fair amount of work has been done on the verification of distributed systems. This section presents representative works that use theorem provers for reasoning on distributed algorithms, or discuss the formalization of DHT protocols.

Chou [START_REF] Ching Tsun | Mechanical verification of distributed algorithms in higher-order logic[END_REF] proposes a reasoning infrastructure using HOL to formalize and verify distributed algorithms and validates his approach on a propagation of information with feedback algorithm. In the same line of direction, the work done by Qiao Haiyan [START_REF] Haiyan | Testing and proving distributed algorithms in constructive type theory[END_REF] reports experiences in verifying distributed algorithms in constructive type theory using the Agda/Alfa proof assistant and provides a methodology mixing testing and verification of distributed algorithms. Ridge, in his work [START_REF] Ridge | Verifying distributed systems: the operational approach[END_REF], takes an operational approach to distributed systems verification. His goal is to demonstrate, through a combination of symbolic evaluation and invariant checking, that the verification of distributed system is feasible down to the executable code level. His work relies on previous notable efforts, such as a rigorous approach to describe network protocols [START_REF] Ridge | A rigorous approach to networking: TCP, from implementation to protocol to service[END_REF], a formal model of the OCaml programming language, and an operational verification of OCaml code. Charron-Bost and Merz [START_REF] Charron-Bost | Formal verification of a consensus algorithm in the heard-of model[END_REF] formally verified a modified version of the Paxos consensus algorithm using Isabelle/HOL. They modeled the consensus algorithm using the Heard-Of model (HO), a round-based computational model for fault-tolerant distributed systems. Their abstractions and proven properties as well as the formalization of the HO model can be used to study a large class of distributed algorithms; however the formalization does not embed any topological aspects of the underlying topology. Contrary to "classical" distributed algorithms such as consensus, distributed algorithms running on top of structured P2P systems, can not abstract away the underlying infrastructure, particularly if the algorithm relies on it. A formalization of an efficient broadcast algorithm on top of CAN has to rely on the needed abstractions and proofs regarding the topological aspects of CAN in order to prove the efficiency of the algorithm. The closest works on distributed algorithms for P2P systems are Meghdoot [START_REF] Gupta | Meghdoot: contentbased publish/subscribe over P2P networks[END_REF] and M-CAN [START_REF] Ratnasamy | Application-level multicast using content-addressable networks[END_REF] which are broadcast/multicast algorithms atop CAN which claim partial efficiency in terms of number of exchanged messages; they were briefly described in Section 2. Unfortunately no formalization nor any proofs were presented in these works. On the contrary, our objective is to use formal methods to prove with high confidence the correctness and efficiency of dissemination protocols.

Borgström et al. [START_REF] Borgström | Verifying a structured peerto-peer overlay network: The static case[END_REF] were interested in the verification of DHT protocols. They formalized and verified a variant of Chord in static settings (i.e. no churn) using CCS, a process algebra. In a subsequent work, Bakshi et al. [START_REF] Bakhshi | Verification of peer-to-peer algorithms: A case study[END_REF] used π-calculus to prove the correctness properties of Chord in the pure-join model of the protocol. Zave, in her work [START_REF] Zave | Using lightweight modeling to understand chord[END_REF] proved the Chord protocol in its two models: the pure-join and full, using the Alloy analyzer. By providing a rigorous correctness proof of the pure-join model and that the full model of the protocol she proved that the original Chord protocol is indeed not correct.

Pastry was also the subject of a recent verification effort [START_REF] Lu | Towards Verification of the Pastry Protocol Using TLA +[END_REF], which focus was to ensure the correctness of Pastry's algorithms. The join and lookup protocols were specified using TLA + and the properties verified using the TLC model checker and the TLAPS proof assistant. Compared to the model-checking in general, theorem proving requires the help of the programmer to prove properties that are valid on an arbitrary number of processes. We focused in this paper on the pure use of Isabelle/HOL because most of our reasoning were about topology and induction, but we do not exclude the use of a proof assistant in conjunction with SMT solvers [START_REF] Merz | Automatic verification of tla+ proof obligations with smt solvers[END_REF] in the future to ease reasoning, or reason more deeply about liveness properties for example.

Conclusion

To the best of our knowledge, we are the first ones to formalize an abstraction of the CAN overlay network using a theorem prover, and provide a framework to reason about those networks. This formalization efforts should increase the understanding of distributed algorithms for structured P2P networks, and the confidence one has in their correctness. We define formally all the constructs necessary to specify and prove properties of a broadcast algorithm on top of CAN. This paper presented the most important notions and support lemmas we designed in order to provide a convenient level of abstraction for reasoning on communication algorithms while abstracting away the geometrical concerns. The structured network represented is more general than a CAN: in a CAN, zones are necessarily hyperrectangles, whereas ours could be any tuple set. We prefer relying on a less restrictive definition of the structure to see which properties of our algorithm are verified in those conditions and also to lay down the groundwork for future challenges such as node churn. Later, requirements on the structure can be added to prove further properties, e.g. an algorithm may only be efficient if the zones are hyperrectangles. Difficult parts of the formalization concern reasoning by induction on a set that is finite but not inductively defined. To ease this kind of reasoning when dealing with zones, we developed an induction principle based on the number of nodes inside a zone (theorem induct-node-zone-2, Section 3). The reasoning relies on the topology of the network, defined by a neighbor relation, and related lemmas deal with the notion of connected zone, i.e. a node where any two nodes can (indirectly) communicate. We used this framework to describe a class of broadcast algorithms that relies on the notion of "zone to be covered". We proved that there exists an algorithm that covers the whole network without sending twice a message to the same node. This development also shows the capabilities of our framework.

In the future, we plan to formalize an algorithm that sends more messages in parallel than the one we exhibited here. Also, a next logical step would be to see how we can take churns, i.e. nodes joining/leaving the network, into consideration in our formalization since P2P systems exhibit dynamic behaviors and we can not overlook this feature.

Fig. 1 .

 1 Fig. 1. M-CAN: Efficient flooding in 2 dimensional CAN

Definition 4 (Fig. 2 .Fig. 3 .

 423 Fig. 2. Zone node list (ZNL) definition

Definition 7 (

 7 ZNL-BC-msgs). ZNL-BC-msgs C Mid init znlmap ∅ [< Mid|init, init, Entire-Space\Zones(C, init) >] ZNL-BC-msgs C Mid init znlmap msgs < Mid |s, d, Z > #ML ML = map (λZN. < Mid |d, snd(ZN), fst(ZN)\Zones(C, snd(ZN)) >) (znlmap(Z, d)) ZNL-BC-msgs C Mid init znlmap (msgs ∪{< Mid |s, d, Z >}) ML@ML'

Theorem 5 (

 5 Efficiency-final-step).ZNL-BC-msgs C Mid init znlmap Finalmsg [] init ∈ Nodes(C) M, M ∈ Finalmsg M = M ∀(Z, N ) ∈History(C, init, Finalmsg, []).znlmap(Z, N ) ∈ (Set-of-Valid-ZNL C N Z) Message-dest(M ) = Message-dest(M ) Theorem 6 (Efficiency-existence). init ∈ Nodes(C) ∃Finalmsg, znlmap. ZNL-BC-msgs C Mid init znlmap Finalmsg [] ∧ ∀M, M ∈ Finalmsg. (M = M ⇒ Message-dest(M ) = Message-dest(M )

see: www-sop.inria.fr/oasis/personnel/Ludovic.Henrio/misc.


François Cluzel
email: francois.cluzel@ecp.fr

Bernard Yannou
email: bernard.yannou@ecp.fr

Markus Dihlmann
email: dihlmann@mathematik.uni-stuttgart.de

Using Evolutionary Design to Interactively Sketch Car Silhouettes and Stimulate Designer's Creativity

Keywords: interactive genetic algorithm, evolutionary design, shape design, subjective evaluation, user tests, car profile

An Interactive Genetic Algorithm is proposed to progressively sketch the desired side-view of a car profile. It adopts a Fourier decomposition of a 2D profile as the genotype, and proposes a cross-over mechanism. In addition, a formula function of two genes' discrepancies is fitted to the perceived dissimilarity between two car profiles. This similarity index is intensively used, throughout a series of user tests, to highlight the added value of the IGA compared to a systematic car shape exploration, to prove its ability to create superior satisfactory designs and to stimulate designer's creativity. These tests have involved six designers with a design goal defined by a semantic attribute. The results reveal that if "friendly" is diversely interpreted in terms of car shapes, "sportive" denotes a very conventional representation which may be a limitation for shape renewal.

Introduction

The art of sketching, and the sketches themselves, are considered to be an important part of conceptual design as well as the way for designers to condense their knowledge and exploration [START_REF] Römer | External Support of Problem Analysis in Design Problem Solving[END_REF][START_REF] Tovey | Sketching, concept development and automotive design[END_REF][START_REF] Yang | Observations on concept generation and sketching in engineering design[END_REF]. In their work, Yang et al. [START_REF] Yang | An Analysis of Sketching Skill and Its Role in Early Stage Engineering Design[END_REF][START_REF] Yang | Concept generation and sketching: Correlations with design outcome[END_REF] address the correlation between the quantity of generated sketches and their impact on design outcomes. Moreover, they explore the relationship between the moment of sketching in the design process, especially early in the design, and the impact on the outcomes. Based on the correlation coefficient exploration, statistically it is found that the quantity of concept generation is significantly correlated with project outcome quality. This is also the case for the timing of sketches: Yang [START_REF] Yang | Observations on concept generation and sketching in engineering design[END_REF] found that early sketching and prototyping gave the best project outcome qualities. Moreover, some studies focus on the importance of the prototyping stage. Yang [START_REF] Yang | An examination of prototyping and design outcome[END_REF] explores the influence of the prototype complexity, prototype quantity and the time spent on this activity and their relationship with the design outcome. The results of the study show that the lesser number of parts in a device, then the greater the project outcome quality.

Evolutionary Computation (EC) has become a major approach for the exploration and evaluation of design solutions, and especially 2D sketched solutions. An EC method basically uses the genetic algorithms (GA) [START_REF] Bentley | Introduction to creative evolutionary systems[END_REF][START_REF] Renner | Genetic algorithms in computer aided design[END_REF], which were originally used to find solutions for complex optimization problems. For example, Poirson et al use GAs to optimize the design of brass musical instruments by considering mathematical and perceptual objectives [START_REF] Poirson | User-centered design by genetic algorithms: Application to brass musical instrument optimization[END_REF]. Taking the evolution in nature as a paradigm, the GAs work on the basis of a population of individuals, where each individual represents a possible solution for the initial problem. The structure and qualities of each individual are encoded in their genomes. Through the recombination of these genomes individuals can reproduce themselves and produce new individuals (solutions), and through a sort of natural selection, individuals who are not adapted to the environment (whose properties do not satisfy the expectations) are not selected for procreation. In this way, individuals display better and better qualities over the generations. Interactive Genetic Algorithms (IGA, see [START_REF] Nicaise | Indirect encoding of structures for evolutionary design[END_REF][START_REF] Kelly | Interactive Genetic Algorithms for use as Creativity Enhancement Tools[END_REF]) represent a special class of GAs where a human (here, the style designer) is a key player embedded within the task of selecting individuals from a generation. IGAs are then particularly adapted to situations where it is impossible to explicitly express a preference function (the fitness function) on individuals or even when it is hard to qualify expected properties. This is typically the case with style designers.

A major difficulty when using GAs in automatic design systems is the encoding of the genome (see [START_REF] Nicaise | Indirect encoding of structures for evolutionary design[END_REF]), which means the way of coding the individual's phenotype (physical structure) into the genotype (genome). Most systems use a direct encoding where the geometrical dimensions and structures of the design object are directly represented in the genome (see for example [START_REF] Kelly | Interactive Genetic Algorithms for use as Creativity Enhancement Tools[END_REF]). For example, when designing a bottle [START_REF] Ang | Combining Evolutionary Algorithms and Shape Grammars to Generate Branded Product Design[END_REF][START_REF] Kelly | Evidence for using interactive genetic algorithms in shape preference assessment[END_REF] or when finding a design for cylindrical shapes [START_REF] Yanagisawa | Interactive Reduct Evolutional Computation for Aesthetic Design[END_REF], the phenotype is represented in the genome by a sequence of geometrical parameters such as the radii, lengths and part locations. Consequently, encoding is context dependent. Other works use tree structures [START_REF] Liu | Supporting evolution in a multi-agent cooperative design environment[END_REF] or shape grammars [START_REF] Osborn | Creating cross-over vehicles: Defining and combining vehicle classes using shape grammars[END_REF] to encode the genome. Kim and Cho [START_REF] Kim | Application of interactive genetic algorithm to fashion design[END_REF] have used a set of predefined parts of clothes to find new fashion designs by recombining these parts. In addition, all of these systems are conceived for a given design domain. Implementing these methods in new design fields is a difficult and time consuming process. However, a good design method should be applicable, as much as possible, to a large spectrum of situations.

In this paper, we first propose an encoding method for a 2D-closed-curve which is supposed to meet a desired style. This method can be applied to all possible objects represented by their 2Dsilhouettes. For instance, a car silhouette or profile is an essential style feature for a car. Indeed, Cheutet [START_REF] Cheutet | 2D semantic sketcher for a car aesthetic design[END_REF] has shown that the character of a car profile is primarily expressed through a series of about ten lines (see Figure 1). Five of them: hood line, windshield line, roof line, wheelbase line and wheel arch, may be merged into a silhouette closed line. It has been proved that these lines, and especially the silhouette, have a strong determining influence on the perception of the car while embedding perceptual attributes such as: sportiveness, aggressiveness or peacefulness, etc.

Figure 1. Cheutet models a car using key lines [18]

In addition, it has been proved that the aesthetic aspects of a car amounts for 70% of customers purchase intents [START_REF] Cheutet | 2D semantic sketcher for a car aesthetic design[END_REF]. Other approaches consider car shape design in a tool for assisting the designer. Petiot and Dagher [START_REF] Petiot | Preference-oriented form design: application to cars' headlights[END_REF] propose a tool to evaluate car front-end designs through semantic attributes (see Figure 2). Osborn et al. [START_REF] Osborn | Creating cross-over vehicles: Defining and combining vehicle classes using shape grammars[END_REF] use shape grammars to assist the user in the design of new car profiles (see Figure 3). Kelly et al. [START_REF] Kelly | Interactive Genetic Algorithms for use as Creativity Enhancement Tools[END_REF] describe a car silhouette with 12 points (8 fixed points and 4 varying points) and use an IGA to find new designs (see Figure 4). Consequently, it turns out that the design of car shapes or silhouettes has been studied with different techniques, one of them -Kelly et al. [START_REF] Kelly | Interactive Genetic Algorithms for use as Creativity Enhancement Tools[END_REF] -is even with an IGA. In this paper we propose an IGA based on the encoding of the car silhouette genes after a Fourier decomposition. In section 2, we provide some arguments to compare this GA modeling technique with parameterized curves and shape grammar approaches. Next, the Interactive GA (IGA) is presented and the crossing-over operation between genes detailed. The interactivity consists in allowing a style designer to qualitatively assess individuals at each generation. As such, new innovative designs are expected to emerge through a balanced collaboration between an automatic design space exploration process and the interaction of a designer. In section 3, we propose a method to identify an index of a perceived similarity between two car profiles. In section 4, we use this index through a series of user tests to prove that innovation and surprise may emerge from this process in an effective way. Section 5 concludes on the properties of the IGA approach for innovative sketching.

Model description

Quality of an encoding model

In this work, we have decided to approximate the visual perception of a car through a 2D "side-view" closed curve. Mathematically, we define ℳ, the set of closed curves in . We define the quotient set ℳ∖ℛ where ℛ is the following equivalence relation: "Two curves of ℳ are equivalent with respect to ℛ, if and only if, they are similar through rotations, homotheties and translations".

Numerically, an equivalence class can be described in different ways (resampled curve, Fourier spectrum, wavelet coefficients…). The book of Mallat [START_REF] Mallat | A Wavelet Tour of Signal Processing[END_REF] discusses these different modeling techniques thoroughly. These are different surrogate representations for a same object; each of which have their advantages and disadvantages.

Considering their ability to be appropriate to encode closed curves for an evolutionary design purpose, three properties must be characterized:

• Ability to avoid the emergence of "degenerated individuals" (aberrations are likely to be invisible for frequential representation) (improving "consistency"), • The ability to define a convenient cross-over mechanism, • The ability to define a convenient mutation mechanism.

Finding a way to efficiently represent car silhouettes is an essential point in our study. This issue is closely related to the notion of ontology. Indeed, we need a formal representation of our knowledge in order to decide how to manipulate our objects while remaining in the restricted field of car design. Thus, we must ensure that, for example, crossing two vehicles will create a new object that will still be an "acceptable vehicle", i.e. an apparently possible vehicle. The main principles to design an efficient ontology have already been investigated by researchers such as Tom Gruber [START_REF] Gruber | Toward principles for the design of ontologies used for knowledge sharing[END_REF]. Gruber gives some important dimensions that one must take into consideration when designing a new ontology:

• Clarity: In our case, this implies that our representation must be objective and is not context dependent. • Consistency: A very consistent ontology should not be able to create "monsters" from valid rules. However in our case, too much consistency will constrain creativity.

• Extensibility: One should keep in mind that extensions are likely to be added in the future.

• Weak coding distortion: When we are representing a real object, such as a car, there is always some "distortion" due to the fact that our ontology cannot represent all sides of the object. An essential drawback of 2D descriptive methods (cf. infra) is their strong distortion. • Ontological complexity: Our representation must be parsimonious.

It must be kept in mind that the main goal of ontologies is, above all, to conceptualize a "fixed" field of knowledge. A trade-off between the ontology "quality" and the potential creativity is essential in our work. A car can thus be described as a special realization of some taxonomic scheme. This method leads to generative models such as shape grammars [START_REF] Osborn | Creating cross-over vehicles: Defining and combining vehicle classes using shape grammars[END_REF]. Likewise, an approach based on Fourier harmonics is not as rigid as the "classical" approach by contour parameterization for multiple reasons:

• This encoding is supposed to embrace a much vaster space of possible 2D-closed-curves -or 2D-silhouettes -than by a parameterization approach whose risk is not to be able to propose "out of the box" solutions; • All kind of shapes may be represented, even with small details that can be of the highest importance for provoking feelings and emotions; • Encoding may be performed through a constant length of the genotype, which greatly simplifies crucial GA stages such as the cross-over operation between parent individuals; • Finally, the genes in our solution have proved to be narrowly associated with apparent characteristics that must converge after several generations to the ideal 2D shapes. For these reasons we decided to use a simplistic ontology based on Fourier harmonics, which is described in the next part and which is known as the "purely descriptive model".

Fourier harmonics to encode car silhouettes

McGarva [START_REF] Mcgarva | Harmonic representation of closed curves[END_REF] has proposed a method for coding the phenotype of 2D-closed-curves using their development into a Fourier series. Personally, we have already used this theory in [START_REF] Vasiliu | Dimensional synthesis of planar mechanisms using neural networks: application to path generator linkages[END_REF] for encoding a 2D-closed-curve into the five first Fourier harmonics of this decomposition. The McGarva's theory of Fourier decomposition of a closed curve [START_REF] Mcgarva | Harmonic representation of closed curves[END_REF] considers that the position of each point belonging to this curve can be expressed by a complex function in the complex plane, as written in formula (1):

(1)

As the curve is closed, z(t) is a periodic function. The period is normalized with: z(t+1) = z(t). z(t) can be developed into a Fourier series in formula [START_REF] Tovey | Sketching, concept development and automotive design[END_REF].

∑ exp 2 ∞ ∞ (2)
where the complex Fourier coefficients can be calculated by formula [START_REF] Yang | Observations on concept generation and sketching in engineering design[END_REF].

exp 2 (3)
Coefficient a 0 is called the fundamental, a 1 and a -1 represent the first harmonic, a 2 and a -2 the second harmonic, etc.

As we will see later, the function z(t) is not known as an explicit function from the beginning. Instead, we assume that the curve has been initially defined by a set of successive points z k (k=0,..,N) which belong to the curve. So, in order to calculate the a m coefficients (3) a numeric approximation is required. This approximation is obtained by dividing the curve into N segments connecting each point with its successor. We call t k the length of the curve between the first point z 0 and the point z k . Under these conditions the integral can be calculated by the trapezium formula (4):

∑ ! " "# exp 2 "# " exp 2 " ( 4
)
where z is a periodic function, (z N+1 = z 0 ).

The value of t k is the ratio of the length of the curve to point k and the total length of the curve (see formula 5).

" $ $ , % ∑ & ' '# ' '# ! ' and % " ∑ & ' '# ' '# " ' (5)
where the total length L is the sum of the lengths of all segments, L k is the length from the origin to the current point, x N+1 = x 0 and y N+1 = y 0 .

The construction of the genome of an object is made by developing its silhouette into a Fourier series and defining the fundamental (the coefficient a 0 ) as gene number zero. The first harmonic (a 1 , a -1 ) will be called the first gene, the second harmonic the second gene, etc.

On the basis of the genome, the original shape of the individual can be reconstructed. Each point P k , with coordinates (x k , y k ) on the curve z* which approximates the silhouette of the car, can be calculated by formula [START_REF] Yang | An examination of prototyping and design outcome[END_REF].

( " " " ∑ exp ) ) 2 " (6)
where t k (0≤t k ≤1) is the position on the curve and p fixes the number of harmonics used for the decoding. The more harmonics used for the decoding the more precise the approximation of the original curve (as seen in Figure 5). p is called the decoding "precision".

An IGA-based model

The IGA model is divided into two phases, Phase 1, while Phase 2 concerns the evolution of the population through multiple generations.

Figure . Decoding a genome of a Smart car with different precisions

allows an initial population that further evolve generations, depending on user choices, to be created. This process is explained in the next section.

The IGA model is divided into two phases, as shown in Figure 6. An initial population is created during Phase 1, while Phase 2 concerns the evolution of the population through multiple generations. an initial population that further evolves along several . This process is explained in the next section.

. An initial population is created during Phase 1, while Phase 2 concerns the evolution of the population through multiple generations.

A genetic algorithm requires an initial population. In our case, this population consists of 30 car body silhouettes which already exist. These cars have been chosen to represent a large range of possible forms (different car brands, types or ages). To easily sketch this population, a Java interface has been programmed to draw curves on a plane and code them into a genome. From a picture of the car, the user has the possibility to draw a contour-chart around it by clicking on the screen. We obtain a closed curve representing the silhouette of the car (see Figure 7). In our experience a number M of 60 to 80 points are required to obtain satisfactory results, that means to visually capture the finest details of a car silhouette. However, as this "hand made" silhouette is a non smooth curve we would obtain a high numerical approximation error when applying the trapezium formula (4) to calculate the integral (3). This would lead to a very inaccurate representation of the silhouette and would result in high oscillations when trying to reconstruct the curve with (6) (see Table 2). That is why we increase the number of points by smooth interpolations, using bicubic splines linking three successive points (see Figure 8). Thereby we finally obtain a number of points N describing the silhouette by a smooth curve where N>M.

. The tangent of the spline at point i is parallel to the line passing through points i-1 and i+1

A good encoding quality is reached if the phenotype obtained after the encoding-decoding process is visually similar to the initial profile. In our model, it corresponds to finding a satisfactory balance between the number N of points on the curve used for coding and the number p of the harmonics used when decoding the genome into a curve. Indeed, the higher the number of harmonics used for decoding the more precise the approximation to the original curve. On the other hand, the number N of points on the curve used for coding the genome has an influence on the precision of the Fourier coefficients. A simple full factorial design of experiments (see Table 2) has been performed to identify the best compromise between N and p. The evaluation of the fidelity level of the complete encoding-decoding process has been qualitatively -visually -performed by us on a 5-level scale {Iinaccurate, O -oscillations, SO -strong oscillations, G -Good result, GG -very good result}. In definitive, we found that a satisfactory choice was achieved with a genome size of 71 and a number N of approximately 1500 points for the interpolation since both initial and resulting silhouettes were visually identical.

G G G G G G G 30 SO O G G G G G G G 40 SO SO O O GG GG GG GG GG 50 SO SO O O GG GG GG GG GG 55 SO SO SO O O GG GG GG GG 60 SO SO SO SO O O GG GG GG 70 SO SO SO SO O O O GGG GG 80 SO SO SO SO O O O GG GG 90 SO SO SO SO SO O O O GG 100 SO SO SO SO SO O O O GG 120 SO SO SO SO SO O O O GG 140 SO SO SO SO SO O O O GG 170 O GG 200 O GG Table 2.

The design of experiments carried out to find an ideal (p, N). Initial and reconstructed silhouettes are visually compared to result in subjective assessments: I -inaccurate, Ooscillations, SO -strong oscillations, G -Good result, GG -very good result

A last normalization operation is required for the genomes so that the phenotypes -silhouettes -are independent of a particular location, size or rotation and are only compared in terms of their shape, as discussed at the beginning of this paper.

Once the initial population has been created, the second phase of the IGA consists in the evolution of generations to create innovation.

As Kelly writes, "By using IGAs, we hope to allow designers to enhance their creativity through design space exploration" [START_REF] Kelly | Interactive Genetic Algorithms for use as Creativity Enhancement Tools[END_REF]. The individuals can reproduce among themselves and in this way, produce new solutions.

Our IGA is built upon four operators that influence the evolution of generations:

• Selection: decides which individuals will reproduce and create children.

• Crossover: builds a child's genome from two parent genomes.

• Mutation: changes a genome in a random way after the crossover.

• Killing: decides which individuals from the parents' population will survive in the new generation. The selection and killing operators depend on the fitness values assigned by the user to each individual, i.e. to each car silhouette representing a design solution. The fitness value * is a number between 0 and 6 according to the grade given by the user via an interface showing six individuals at the same time. The user browses through individuals from a generation and gives them a fitness value corresponding to his objective, where 0 is the worst and 6 is the best (see Figure 9). We decided to adopt some conventional choices in term of selection and killing operators and to propose an original crossover operator. First, apart from the initial population of 30 individuals, we have fixed the number of individuals at 100 for each generation. We have chosen a turnover rate of 0.7, meaning that, for a coming generation, 30 individuals are kept from the previous one and 70 children are generated. In this way, potentially good design solutions are not lost. The probability for an individual to be selected as a parent is proportional to its fitness value (between 0 and 6). After two individuals are chosen from the parents' population, their genomes are combined into a child's genome by applying the crossover and mutation operators. Afterwards, the two individuals are put back into the parents' population. Indeed, the selection operator can select an individual more than once.

The crossover operator consists in a weighted average between the gene values of the two parents to build the genome of the child. A crossover weight W is chosen randomly between 0 and 100. A new gene g* is formed by calculating the weighted average of the genes g m,1 and g m,2 of the parents using formula [START_REF] Bentley | Introduction to creative evolutionary systems[END_REF].

+ ( ,-., # , -.,0 (7)
In function of the weight W, we obtain different new design solutions which continuously interpolate a silhouette between the two parents' silhouettes (see Figure 11). In this way, a child greatly resembles its parents and produces almost no useless car solutions; for instance, the tires keep their rounded shapes. The disadvantage is the relatively small space explored for possible solutions: we stay in the convex of the initial individuals. Consequently, the population of design solutions tends to converge rapidly. To enlarge the space of possible solutions we must apply a mutation operator (not detailed here). Finally, the killing operator is applied to the original population and at first, kills all individuals who have a fitness of 0. These individuals are considered to be totally useless or totally unsatisfactory and shall no longer contribute to the evolution of the population. All other individuals have a chance of survival. The individuals to be killed are chosen by an inverse roulette wheel method. This means that the probability 12 ' for an individual to be killed can be expressed by formula [START_REF] Renner | Genetic algorithms in computer aided design[END_REF].

where f i is the fitness of the individual i and N * is the number of individuals in the population who have not been evaluated with a fitness of 0.

Similarity index : a validation tool

Is our system really capable of producing both innovation and novelty? With the help of our system, is it possible for a user to design a new car body silhouette which was not part of the initial population?

To answer these questions, it may be useful to have a tool that automatically measures the perceived difference between two car silhouettes and to prove whether the two car silhouettes are similar or not. We have then proposed to create a similarity index. Built upon user assessments, it measures the distance between two car profiles. The similarity index is an essential point in this study to perform tests and prove the relevance of the present evolutionary design framework to inspire designers. Two important criteria for the design of the index can be quoted:

• It must be mathematically founded.

• The calibration process must be stable and user-friendly.

The objectiveness issue is not a basic criterion: each designer can have his/her own conception of distance but it must, in all cases remain consistent from one assessment to another, when assessed by the same user (this is what we mean by the stability of the calibration process).

Hereafter, we propose a description of the process to obtain this similarity index. Two different models have been tested.

Mathematical definition

We first define D(k,l), the distance between two genomes G k and G l . Since modifications on the first ten genes only are significant (modifications on other genes do not change anything on the visual perception of the car profile), we hypothesize that the distance between two genomes D(k,l) may be expressed as a weighted sum of the elementary distances between the first ten genes by formula (9).

8 2, 9 ∑ : ; + ", + <, ; (9)
The factors : are weighting factors that must give more importance to some genes in accordance with their participation in the apparent modification of the silhouettes. Here g k,m is gene number m from genome k and g l,m is gene number m from genome l. One gene consists of two harmonics, called a m and a -m , which are complex numbers. They can be written as:

a m = u m + i.v m .
Then, we define an elementary distance between two genes of the same order with formula [START_REF] Nicaise | Indirect encoding of structures for evolutionary design[END_REF]

where u max,k and u min,k (respectively v max,k and v min,k ) are the maximal and the minimal values of u k and v k on the whole initial population.

Finally, the similarity index is defined between two genomes k and l as expressed in formula [START_REF] Kelly | Interactive Genetic Algorithms for use as Creativity Enhancement Tools[END_REF].

F GH 2, 9 #I ",< % #∑ K ;-,. -?,. ; 0 L .7 % (11)
So, with this definition, the similarity index is included between 0 and 100%, where 100% means that the two individuals are identical.

We now have to define the factor series : . Two solutions have been tried: an exponential form and a series of independent weights. These solutions are based on different assumptions and have been tested using a comparative experiment.

Exponential form

In this section we assume that : can be written as an exponential expression which gives more importance to the first genes than to higher order genes, since a modification to the first genes impacts the car silhouette more than a modification to the last ones. So, :

is expressed by formula [START_REF] Ang | Combining Evolutionary Algorithms and Shape Grammars to Generate Branded Product Design[END_REF].

: M N (12)
where a and b are two constant terms. So D(k,l) is now given by formula (13).

8 2, 9 ∑ M N ; + ", + <, ; O ∑ M N ; + ", + <, ;

But now we need to find the significant values of a and b.

We propose the following process to measure b:

• To choose a genome, which is copied 3 times: G0, G1, G2.

• To choose a gene i in G1 (more significant with a low weight): g1 i .

• To choose a gene j (i ≠ j) in G2 (more significant with a low weight): g2 j .

• To modify the gene g1 i of G1 in an arbitrary way.

• To modify the gene g2 j of G2 in such a way that there is an iso-similarity (defined below) between G0 and G1 on the one hand, and G0 and G2 on the other hand. The iso-similarity is defined as follows: Two pairs of car silhouettes are iso-similar if the perceived level of similarity is the same for the two pairs. For example, here this means that the level of similarity is the same between G0 and G1, and between G0 and G2. Practically, it means that the user has to modify gene g2 j until the level of perceived similarity becomes the same between G0 and G1 as between G0 and G2. In this way, G2 and G1 are not identical, but their level of dissimilarity compared to G0 is the same.

Then, this experiment results in equality as given in formula [START_REF] Yanagisawa | Interactive Reduct Evolutional Computation for Aesthetic Design[END_REF].

: O; +0 ' +1 ' ; : R O; +0 S +2 S ;

And b is finally given by formula [START_REF] Liu | Supporting evolution in a multi-agent cooperative design environment[END_REF].

T S ' O ln

;-5 -5 ; 0 ;-W -W ; 0

By performing these tests n times with different car profiles, different users, and different i and j values, we get n different b values. The final value of b adopted is the average. The next step consists in measuring a. We propose the following process: for each of the previous comparisons (between G0, G1 and G2), the user defines the level of similarity % ("the similarity between G0 and G1 on the one hand and G0 and G2 on the other hand is 70%" for example). To simplify the designer's evaluation task, the designer is asked to provide a similarity judgment on a 7level scale which is converted into the percentage value as shown in Table 3.

The relation linking % and a is given by formula [START_REF] Osborn | Creating cross-over vehicles: Defining and combining vehicle classes using shape grammars[END_REF].

% #XO∑ Y Z. ;-. -. ; 0 [L .7 ( 16
)
where b is the average value of the previous tests and a is finally obtained by formula [START_REF] Kim | Application of interactive genetic algorithm to fashion design[END_REF].

∑ Y Z. ;-. -. ; 0 [L .7 O \ ]% 1^ (17)
We also obtain 2n different values of a. The average value is acceptable if the standard deviation is low. The calculation of the similarity index is now completed.

Level of similarity Value of similarity index

0 5% 1 30% 2 50% 3 65% 4 80%
5 90%

6 100%

Table 3. Scale of similarity for user assessments

Practically, we use a Java interface (see Figure 12) that follows the processes described above through a series of random trials on individuals from the initial populations and with i and j values.

Weighted form

In the previous section, we assumed that : should give more importance to the first genes than the last ones and can be written as an exponential expression. Let us ignore this assumption and try to associate each :

to a given weight p m . Actually if this assumption easily seems true for the 3 or 4 first genes, it may be wrong for the next ones as it visually become harder to rank the influence of a modification on the (for instance) 5 th or 6 th harmonics.

So D(k,l) is expressed by formula [START_REF] Cheutet | 2D semantic sketcher for a car aesthetic design[END_REF].

8 2, 9 ∑ 1 ; + ", + <, ; (18)
To obtain the weights values, we follow the same process as with the exponential form. We finally obtain expressions linking weights 1 ' and 1 S as in formula [START_REF] Petiot | Preference-oriented form design: application to cars' headlights[END_REF].

'

;-W -W ; 0 ;-5 -5 ; 0 . 1 S [START_REF] Petiot | Preference-oriented form design: application to cars' headlights[END_REF] By performing this test n times (n>10) with different values for i and j (to cover all of the first ten genes), we have a system of n equations, that can easily be resolved with the logarithmic least square method.

The tests are performed with a modified version of the Java interface as described in the previous section.

Choice of the index form

To find the best version of the similarity index, we performed the tests as described in Figure 13. 30. Cars were extracted from the initial population and were used to construct the two similarity indexes (calculation of a and b in the first case, calculation of the weights 1 ' in the second case). 20 supplementary individuals from the initial population were then used to choose the most accurate index by calculating a similarity matrix. These matrices were compared to a third matrix containing the evaluation of the same 20 car silhouettes directly made by the users. These three matrices led to the calculation of the RMSE (Root Mean Square Error) associated with the two index versions.

Figure 13. Choice of the similarity index type

We found an average RMSE of 7.04 for the exponential form index, and 31.82 with the independent weight form. Furthermore, in the first case we obtained a MAE (Mean Absolute Error) of 4.51, which shows a good precision for the model compared to the evaluation scale (0 to 100%). As such, the exponential form has been chosen for the similarity index. It has then been used to validate our model thanks to several user tests presented in the next section.

Choice of the similarity index

Exponential form

Discrete weights form

Index construction

Index validation

Model validation

Several tests have been performed to validate the model. We propose a short synthesis of some of these tests before detailing the ones that particularly prove t stimulates creativity.

Synthesis of the validation tests

These first tests are presented in more detail in conclusions and findings concerning user satisfaction and section details three tests that mainly

User satisfaction

The first way to validate the model consists in observing the evolution of user satisfaction along the generations. A test inspired by [START_REF] Kim | Application of interactive genetic algorithm to fashion design[END_REF] generations. These users are students in the design engineering 4 users were asked to find their best friendly semantic attribute (find their best hedonistic assessments (i.e. including their own preference). The mutation probability and the selection rate were respectively set to 0.05 and 0.7.

The average fitness values evolution on the 10 generations (see satisfied by the model. Indeed, attribute sportive, and from 3.0 to 5.0 for the two cases.

Convergence

To assess the ability of the model to converge, two tests based on the data obtained with the previous 8 users and the similarity index have been proposed. They aim the first ten generations of the average similarity between in and between the users (for the second one). In addition, we study the similarities that exist between the best individuals from the last generation On average, a similarity of 6.5% ha average value increases rather quickly with the generations, reaching for the similarity between 60 and 90% at the 10 visually perceive strong differences between individuals IGA is able to converge towards a single individual family.

Several tests have been performed to validate the model. We propose a short synthesis of some of before detailing the ones that particularly prove that this evolutionary design schema

Synthesis of the validation tests

These first tests are presented in more detail in [START_REF] Cluzel | Evolutive design of car silhouettes using an interactive genetic algorithm[END_REF] and [START_REF] Cluzel | Efficiency Assessment of an evolutive design system of car contours[END_REF]. In this section, we only draw the main conclusions and findings concerning user satisfaction and the convergence of the model. The next mainly focus on creativity.

The first way to validate the model consists in observing the evolution of user satisfaction along the [START_REF] Kim | Application of interactive genetic algorithm to fashion design[END_REF] has been performed by asking 8 users to evaluate 10 successive These users are students in the design engineering field in the last year of master class 4 users were asked to find their best sportive car profile, while the 4 other users worked with the semantic attribute (find their best friendly car silhouette). We asked the users to perform ssments (i.e. including their own preference). The mutation probability and the selection rate were respectively set to 0.05 and 0.7.

The average fitness values evolution on the 10 generations (see Figure 14) proves that the users are the average user fitness increases from 2.3 to 3.9 for the semantic attribute sportive, and from 3.0 to 5.0 for the friendly attribute, i.e. an increase

Fitness evolution for the convergence test

To assess the ability of the model to converge, two tests based on the data obtained with the previous 8 users and the similarity index have been proposed. They aim to study the evolution along the first ten generations of the average similarity between individuals for each user (for the first test) and between the users (for the second one). In addition, we study the similarities that exist between the last generation for each designer.

6.5% has been calculated for the initial population. For all users average value increases rather quickly with the generations, reaching for the similarity between 60 and 90% at the 10 th generation. This qualitatively means that it is hard to ually perceive strong differences between individuals from the last generation. It shows that the IGA is able to converge towards a single individual family.

Several tests have been performed to validate the model. We propose a short synthesis of some of hat this evolutionary design schema e only draw the main convergence of the model. The next The first way to validate the model consists in observing the evolution of user satisfaction along the has been performed by asking 8 users to evaluate 10 successive in the last year of master class. car profile, while the 4 other users worked with the car silhouette). We asked the users to perform ssments (i.e. including their own preference). The mutation probability and the ) proves that the users are from 2.3 to 3.9 for the semantic e of about 70% in the To assess the ability of the model to converge, two tests based on the data obtained with the study the evolution along dividuals for each user (for the first test) and between the users (for the second one). In addition, we study the similarities that exist between lculated for the initial population. For all users, this average value increases rather quickly with the generations, reaching for the entire user range a generation. This qualitatively means that it is hard to the last generation. It shows that the Moreover, the study of similarity between the best individuals from the last generation for all users shows important results:

• For the "sportive" semantic attribute, the similarity between the best individuals of the last generation gives a similarity of about 51%: all users converge towards the same individual family (see Figure 15). However, it is not possible to identify if the behavior is due to the choice of users or the model that does not converge towards another family of profiles. It is also useful to note that this common family is very close to a Porsche 911 profile, which shows that this profile is probably perceived by the users as the ideal sportive car silhouette.

• For the "friendly" semantic attribute, the similarity between the best individuals from the last generation is only 9.21%: there are only a few connections between the individual families reached by the different users (see Figure 16). It answers a previous question: the model preserves the freedom of thinking for each designer, who is able to converge towards his/her own mental target. The results of these first tests show that the IGA has a really promising behavior. However, some crucial questions remain and further tests are required to complete a full validation. The main questions are as follows:

• Is the model really able to create novelty, or are the final car profiles that emerge always correlated to some individuals from the initial population?

• How can we be sure that the IGA obtains better results compared to a more classical (manual) method? In other words, what is the real added value of the IGA?

In the next sections, new tests are proposed that mainly focus on novelty emergence and creativity enhancing, which are essential aspects for innovation.

Novelty emergence

A major element to enhance creativity is the model's ability to create novelty, i.e create any individual, randomly chosen or imagined by the user. In other words, the purpose of this test is to show that it is possible to reach a defined individual which is not part of the initial population.

To answer this question, we can execute a simple test. A subject draws a car body silhouette on a sheet of paper which comes spontaneously to his or her mind and which is not part of the initial population. This car body silhouette is taken as a "target individual". Using our proposed IGA, the user must now try to obtain the "target silhouette" he has drawn on a sheet of paper by the end of the IGA process. Of course, the objective of this test is to prove that there is no limit to our system to converge towards the imagined shape. Then, keeping this reference drawing in front of him or her, the user evaluates the car contour individuals, providing higher grades to contours which are similar to the target contour and lower grades to those that are dissimilar. By considering both the number of generations required to resemble the target individual and the similarity value, we can estimate the quality of our design system.

Alternatively, the target car silhouette may be an individual from the initial population which is removed from this initial population.

We have preferred to make abstraction of the designer subjectivity by automating the ability of the system to converge towards an ideal car silhouette, in order to measure the sole quality of the method. The role of the designer is played by a similarity fitness calculation algorithm, which automatically evaluates individuals from a generation in terms of their similarity to the target individual, thanks to the similarity index previously defined.

This test has been repeated several times, with different target individuals extracted from the initial individual population for an average final similarity index of 90%. Let us provide a practical example with the target individual given in Figure 17.a. The genetic algorithm parameters were as follows: population of 100 individuals, turnover rate of 0.7 and mutation probability of 0.3. The mutation can change a gene within a range of ±(50%-200%). After 10 generations, our system reached the car body silhouette in Figure 17.b which has a similarity index of 92%, and which can be visually considered as a much more satisfactory result. The average fitness of the population converges over the generations to a high value (see Figure 18), whereas the value of the best similarity index in the population (the fitness of the fittest individual) rises rapidly from a relatively low 44% to 92%. 4 for User 2 working with the "sportive" semantic attribute. It shows that his/her best car profiles are highly inspired by the 13 th individual from the population, namely the Porsche 911 silhouette. However, no correlation is observed with the "friendly" semantic attribute, and it can be concluded that the correlation between the Porsche 911 and the results of the users with the "sportive" semantic attribute are the consequence of a choice (voluntary or not), and not a constraint of the model. Finally, the results of these two tests show that the final individual is genetically very similar to the target individual. The IGA is then able to create totally new individuals that are not part of the initial population. For us, this is a necessary condition to improve creativity. However, further tests are required to show that our model brings added value compared to a classical "manual" method.

Creativity enhancing

To show that the results obtained with the IGA are better than without the IGA, we have performed two different tests from a same base inspired by Kim and Cho's works [START_REF] Kim | Application of interactive genetic algorithm to fashion design[END_REF].

The same set of data as used for some of the previous tests was used (8 users during 10 generations, with 2 semantic attributes). However, we also asked the user to evaluate 400 randomly generated individuals with the same fitness scale (between 0 and 6). These individuals were printed on a large sheet of paper and numbered. An Excel routine was given to the users to identify, in several evaluation steps, their three preferred profiles according to their assigned semantic attribute ("friendly" or "sportive"). To clarify the explanations in the rest of the document, these best individuals are called paper individuals.

The users were then asked to compare the three best paper individuals with the three best individuals from the 10 th generation of the IGA, thanks to a pairwise comparison matrix. The comparisons were performed according to the scale presented in Some details have to be explained to understand the meaning of Table 6. Pairwise comparisons are made in accordance with the following scheme: the best individuals from the IGA are compared to the best paper individuals. For example, User 4 has an average evaluation of +1.00. According to Table 5, this means that User 4 found the best individuals from the IGA slightly superior to the best paper individuals. Thus, positive numbers prove that the results obtained with our model are better than without.

The results show good behavior for the sportive semantic attribute: the average score is +1.50, so the best IGA individuals are between "slightly superior" and "superior" to the best paper individuals.

For the friendly attribute, the results show good behavior as well, even if the difference is slightly less perceptible. All users prefer individuals from the IGA except user 5, who prefers the individuals without the model. Globally, the results for this attribute are not really homogenous, and can be explained by a more subjective comprehension (and as such, characteristic to each user) of the word friendly rather than the word sportive (this observation is highlighted in other tests presented hereafter). Now, let us compare if these two sets of 3 best solutions can have close solutions or not. The maxima of similarity are shown in Table 7. For 5 users out of 8, the maximum similarity is above 70%. For 2 users, the maximum is between 20 and 30%. For the last user, the similarity is only 2.67% . This means that, most of the time, the final solutions obtained are quite similar, whatever the design method (IGA system or brute force enumeration). Indeed with the IGA, without any judgment of value, 5 users have found at least one individual that is very close to one of the paper individuals.

Sportive

But, 400 individuals were proposed on paper and it takes about 45 minutes for one user to evaluate them. Comparatively, less than the 200 individuals used with the IGA process (10 generations of 20 individuals, minus those who survive from one generation to the next), and the evaluation only lasts about 20 minutes. So, it appears that our system brings at least comparable results more quickly and with fewer individuals; this is clearly a proof of its utility.

Concluding remarks

Shah et al. [START_REF] Shah | Metrics for measuring ideation effectiveness[END_REF] propose four separate measures to assess the effectiveness of a generation process towards innovation:

• Novelty, which is a measure of how unusual or unexpected a concept is, as compared to other concepts,

• Variety measures the size of the solution space,

• Quality explores the feasibility of a concept and how close it comes to meet the design specifications,

• Quantity concerns the total number of concepts generated.

Transposed to this study, these measures allow the creativity enhancing of the proposed IGA model to be highlighted.

We have shown that the model is able to create individuals that are not closely linked with individuals from the initial population. The model reaches a high level of novelty potential.

Concerning variety, the size of the solution space is theoretically unlimited since continuous genes are used.

Here, the quality measure can be related to the user satisfaction of the end-result of the design activity. Here, the superiority of designs generated by the IGA has been proved compared to a brute systematic exploration of shapes.

Finally, the quantity can be totally customized by the user: he/she chooses the size of the population, as well as the sensibility of the algorithm (killing and mutation factors). The choice of precise semantic attributes is a guide to generate different car profile concepts.

In addition, our model is extensible as defined by Gruber [START_REF] Gruber | Toward principles for the design of ontologies used for knowledge sharing[END_REF], since a designer may introduce, at any moment of the evolutionary algorithm, a customized profile he or she has just sketched, or that he/she locally modifies from an existing individual of the current generation. This facility has not been detailed here but completes the numerous advantages to further study Interactive Genetic Algorithms to explore spaces of 2D innovative curves.

Figure 2 .Figure 3 .Figure 4 .

 234 Figure 2. Perceptual evaluation of car front-end designs by Petiot and Dagher [19]

Figure 5 .

 5 Figure 5. Decoding a genome of a Smart car with different precisions The encoding of individuals allows generations, depending on user choices

Figure 6 . 7 .

 67 Figure 6. Diagrammatic plan of the IGA process

Figure 7 .

 7 Figure 7. After bordering we obtain a closed curve representing the car silhouette of an existing car

Figure 9 .

 9 Figure 9. The User Interface for the designer evaluation showing 6 individuals of a larger population. The designer can browse through the individuals by clicking on the arrow buttons

Figure 10 .Figure 11 .

 1011 Figure 10. Two parent individuals

Figure 12 .

 12 Figure 12. Java interface to calculate parameters a and b

Figure 15 .

 15 Figure 15. Examples of best "sportive" car silhouettes (one from each user)

Figure 16 .Figure 17 .

 1617 Figure 16. Examples of best "friendly" car silhouettes (one from each user)

Figure 18 .Figure 19 .

 1819 Figure 18. The average fitness of all individuals in the population over the generations

Table 4 .

 4 Similarity values between the best individuals and the initial population for the "sportive" semantic attribute (in %)

Table 1

 1 gives some example of such ontologies.

		Completeness	Robustness	Consistency Extensibility	Adaptivity	to
						genetic
						algorithms
	Shape grammars	++	++	++	-	--
	Parameterized	--	--	--	++	++
	contour
	Fourier harmonics	--	++	--	++	++
	Wavelets	--	++	-	++	++

Table 1 . Comparison of different encoding methods

 1

	Many ontologies are based on taxonomic relationships: entities, such as cars, are classified in
	different families organized in a global hierarchical structure.

  .

	; + ",	+ <, ;	=> ,. > ?,. @ 0 => .AB,. > .5C,. @ 0	0 => ,D. > ?,D. @ => .AB,D. > .5C,D. @ 0
			=E ,. E ?,. @ 0 =E .AB,. E .5C,. @ 0	0 =E ,D. E ?,D. @ =E .AB,D. E .5C,D. @ 0

Table 5 .

 5 As such, users filled the matrix with the mathematical symbols (>, >>, =…) that were then replaced by numbers to analyze the data.

	-3	<<< highly inferior
	-2	<<	inferior
	-1	<	slightly inferior
	0	=	equal
	1	>	slightly superior
	2	>>	superior
	3	>>> highly superior

Table 5 . Hedonistic (preference) scale of pairwise comparisons of car profiles

 5 Considering this data, the first test evaluates the user satisfaction of results obtained with the IGA. The second test analyses the data with the similarity index.

Table 6

 6 shows the test results for each user and for each semantic attribute.

	Sportive User 1	+1,78
	User 2	+1,67
	User 3	+1,56
	User 4	+1,00
	Average	+1,50
	Friendly User 5	-0,33
	User 6	+0,67
	User 7	+0,78
	User 8	+1,22
	Average	+0,58
	Total Average	+1,04

Table 6 . Results of the pairwise comparisons between best IGA solutions and best paper (random) solutions highlighting the superiority of IGA

 6

Table 7 . Maxima of similarity values between best individuals of the IGA and of paper individuals (in %)

 7

		User 1	84,49
		User 2	21,26
		User 3	80,92
		User 4	97,93
		Average	71,15
		User 5	2,67
		User 6	98,09
	Friendly	User 7	71,32
		User 8	26,94
		Average	49,75
	Total Average		60,45

Corrresponding author

Acknowledgments

We gratefully thank François Bleibel, Nicolas Cordier, Gilles Foinet and Thomas Ricatte for their contributions to this work.