Lucien Loiseau

Nicolas Montavont

Xavier Lagrange

Forwarding by Retransmission in IEEE 802.11

Keywords: IEEE 802.11, cooperation, wireless communication, relays

This paper presents a cooperation-based retransmission mechanism for IEEE 802.11 networks called Forwarding By Retransmission (FBR). This mechanism aims at reducing the mean number of retransmissions in an infrastructure network, or it can be used to forward frames in a small ad hoc network. FBR enables any node that received a frame to participate in the retransmission process, as long as it has a higher probability to reach the destination than the sender. We detail our implementation in NS-2 and analyze the FBR operations in a simple scenario. We show that using only one relay allows reducing the number of retransmissions by 60%.

I. INTRODUCTION

The wireless transmission medium is subject to loss due to physical property of the environment separating a source from its destination, path loss, shadowing, or fading effects. The radio medium is unpredictable, and varies over time. Given a source and a destination, some frames may be correctly received while other not. The wireless medium is shared among all stations, and collisions and interferences may also impact performances. In this challenging environment, different standards define how wireless stations can communicate together, such as IEEE 802.11, Bluetooth or LTE to cite only a few. Several modes of communication are proposed, which can be grouped into two main sets. In the infrastructure mode, all exchanges are made with a central entity called an access point (AP). This AP either plays the role of a bridge between the wireless network and the wired network, or it can relay frames from a wireless station to another one. In the ad hoc mode, stations communicate directly with each other. To reach a destination out of its range, a station may use its neighbors as relays, that will forward the frame hop by hop toward the destination. In this case, a routing protocol is usually needed to set up the routes.

A routing protocol for ad hoc network is usually operating in two steps. First, nodes discover their neighbors and establish routes to their destination. We can distinguish two approaches; in proactive protocols, the discovery is made independently from any data traffic. Another approach called reactive protocol consists in determining a specific route only if a source needs to send traffic to a destination. Once the routes are known, the second step is the forwarding process. Data packets are forwarded in unicast, hop by hop up to the destination. These methods do not consider the nature of the wireless transmission medium as described above. It makes the assumption that once a route is discovered, it remains valid and fixed for data transfer. If one hop is not operational anymore (because of a node mobility or another neighbor appears to be more suitable for the fowarding), the routing protocol may adapt the path. However, this adaptation requires a long time to be set up. These approaches rely on the principle of choosing a given hop based on previous performance information. In our proposal, potential relays are selected frame by frame, among all stations that received the frame.

We propose a novel approach for frame relaying in both infrastructure and ad hoc network. In our proposal, a source sends its frames directly to the destination, whether the destination is in its radio range or not. Neighbors that overheard these frames and do not receive the acknowledgement (ACK) from the destination may participate to the retransmission process. For each individual transmission, any receiver can participate in the retransmission process if it allows making progress toward the destination. We call this opportunistic relaying because a source can not know in advance which nodes will receive its transmission and potentially act as a relay. We apply our mechanism in the IEEE 802.11 standard, with as few as possible modification to the standard. We need to change a node behavior with regards to the overheard frames: a receiver will process every frame, even those for which if it is not the destination.We also slightly modify the acknowledgement system, by adding two types of acknowledgement: one is the passive acknowledgement where the retransmission of a frame by a neighbor is considered as an acknowledgement. The other one is the delayed acknowledgement, when a node receives an unexpected but legitimate ACK for a queued frame.

The remainder of this paper is organized as follows. Section II introduces our approach and explains how it can apply to both infrastructure and ad hoc networks. Section III formally presents the protocol and section IV describes its implementation in NS-2 and preliminary results. Section V concludes the paper.

II. RELATED WORK AND APPLICABILITY

The wireless transmission medium is broadcast by nature, so any node in the radio range of a source may receive its frames, even if they are not the intended destination. While traditional routing protocols predefine a next hop for routing a frame through multiple hops, we propose to take advantage of opportunistic frame reception by any node. We assume that the set of receiving nodes is different from one transmission to another, so instead of selecting a (fixed) next hop, we aim at selecting a forwarder among those which received a frame. The selection process is decentralized and computed individually on each receiver. Each potential forwarder will compete to retransmit a frame. Once a station wins the contention and retransmits a frame, all potential forwarders (including the source itself) must consider this retransmission as an acknowledgement. The selected forwarder is then responsible for the correct reception of the frame to the next hop or the destination. This mechanism relies on a discriminant that allows a receiver to know whether it is potentially a better retransmitter than the sender. This discriminant can be any link metric that can estimate the link quality between a node and a given destination. For example, it can be the RSSI or the ETX. In the following, we develop how our mechanism can operate in infrastructure or ad hoc networks.

A. Relaying in infrastructure topologies

In the infrastructure mode, a node sends all its frames to an AP. So a cell is defined as the set of nodes that are able to communicate (send and receive) frames with a given AP. In order to optimize the cell size, different modulations can be selected to adapt to the link quality between the AP and a given node. For example, a node with a low signal strength may choose a robust modulation scheme that allows repairing the channel errors. On the contrary, a node that is close to the AP may use a less robust modulation scheme that allows higher data rate. In 802.11g, data rates can vary from 6Mbps to 54Mbps. Nodes usually select the highest possible data rate depending on their link quality.

Low data rate stations can access the channel as often as high data rate stations, but once they access the medium, they require more time to transmit their frames [START_REF] Heusse | Performance anomaly of 802.11 b[END_REF]. For example, transmitting a 1500 byte frame at 6Mbps requires 2ms while it only takes 0.22ms at 54Mbps. So even if stations with bad radio conditions are able to connect to an AP, they degrade the performance of all stations in the cell. In recent studies that we conducted in city centers [START_REF] Castignani | Urban 802.11 Community Networks for Mobile Users: Current Deployments and Prospectives[END_REF], we showed that the signal strength between a mobile station and its AP in community network is quite low, equal or less than -75dBm in 80% of the cases. To avoid low data rate stations to decrease the entire cell performance, stations could cooperate together: high data rate stations could relay frames from stations with low signal strength.

In this context, an AP is periodically sending beacons at 6Mbps. These frames can be used by stations to evaluate their link quality with the AP. By adding this information in their frames, a receiving station is able to determine whether it is in a a better or worst condition to retransmit a frame. Assuming that there is a large density of stations, a station will send its frame at the maximum data rate, whatever its link quality. If the frame is not received by the AP, a receiving station can retransmit the frame to the AP. As shown by [START_REF] Bahl | Opportunistic use of client repeaters to improve performance of wlans[END_REF], a station that retransmits other station frames may increase its own performance (compared to a situation where the source would send its frames at a low data rate without any help from other stations).

B. Relaying in ad hoc networks

In ad hoc networks, a routing protocol is needed to establish the paths between a source and a destination. Usually the network topology is first discovered and then the paths are computed. For example, the RPL protocol [START_REF]Rpl: Ipv6 routing protocol for low-power and lossy networks[END_REF] builds a tree where each station determines which other station is its parent toward the root. The network topology is discovered via the DIO messages periodically sent by all stations. This message contains the rank information, i.e., the "distance" between the sending node and the root of the tree. From the DIO sent by all its neighbors, a station can select its parent. The frequency at which the DIO is sent decreases when the topology is stable.

In AODV [START_REF] Perkins | Rfc 3561 ad hoc ondemand distance vector (aodv) routing[END_REF], a route request flooded in the network allows discovering a path toward a destination and feed intermediate node routing tables. For each destination, the routing table indicates which neighbor is the next hop toward the destination.

Selecting a parent or the next hop by default is sub-optimal if we take into account that each individual transmission is unique, and each transmission may reach a different set of receivers. By selecting a default parent, a station has to select the neighbor with which it has a reliable link, i.e., the neighbor that will require the minimum number of retransmissions. However, some transmissions may be received by other neighbors than the default parent, including nodes that are closer to the destination. With our mechanism, we enhance such routing protocols by selecting the neighbor that has the better rank with regards to the destination, even if this neighbor may require multi-hops for certain transmissions. Thus, we could split the topology into steps, and use opportunistic relaying inside those steps.

For relative small ad hoc networks, where all stations are able to listen each other beacons, our mechanism applies as well. The link quality with a given destination can be determined by the beacons, and data frames can be sent directly to the destination. If a frame is not acknowledged by the destination, because it has not been received, any intermediate node can participate in the retransmission process.

III. FORWARDING BY RETRANSMISSION

We propose a lightweight mechanism called Forwarding By Retransmission (FBR) that enhances wireless communication either in an infrastructure network, or an ad hoc network. We provide a retransmission mechanism where a receiving station can participate in retransmitting a frame on behalf of a source if it has a higher probability of successfully transmitting the frame to the destination.

We assume that a destination is sending a beacon frame, which limits the coverage where FBR can be used. Each station can thus compute a link metric with the destination, and include this information in all frames it will send. We used the fourth address field of 802.11 frame to add this information. A source station follows the IEEE 802.11 standard to send a frame. Once it accesses the channel, it sends the frame and waits for the ACK from the destination. If the destination receives the frame, it sends an ACK that is received by all stations, and the transmission is over. Note that the IEEE 802.11 standard recommends to send management frames at the lowest data rate possible. This ensures that the ACK frames are unlikely to be lost. If the destination does not send the ACK, all receivers of the frame compare their link quality with the one indicated in the frame. If their link quality is better than the one in the frame, they will be considered as Potential Forwarder, i.e., they enter in competition to retransmit the frame. At this point of time, the source and all stations that received the frame and have a better link quality than the source are competing to access the channel. The station that had the lowest backoff time, will access the medium and send the frame. This station has now the responsibility of further retransmission if needed. If other potential forwarders and the source receive this retransmission, they will cancel their own retransmission of the same frame. And the same process reproduces with this new transmission, i.e., either the destination receives it and sends back an ACK, or a new retransmission process takes place.

Figure 1 shows all possible scenarios when we consider a source sending a frame to a destination, with an intermediate node (called a relay) in between. We classified the scenarios in three states: state A represents the case where only the source is competing for the medium. This is the case for the initial transmission, or when the relay did not receive the transmission. State B represents the cases when both the source and the relay compete to access the medium. State C represents the cases when only the relay competes to access the medium. The white boxes (A3, A8, A9, B1.3, B1.9, B2.2, B2.7, B2.8, C2, C7, C8) represent a final state, where the transmission is done (the destination received and acknowledged the frame, and the source and the relay do not try to Fig. 1. Scenarios for data transmission send the frame anymore). Transitions from any state are either to the same state, or forward (e.g., from A to B), except for states B1.5, B1.7 and B2.4 which return to state A. In both B1.5 and B1.7 the source won the contention, and retransmitted the frame. In both cases, the destination received the frame, and the relay received the ACK from the destination while the source did not received it. Thus the relay discards the frame from its retransmission queue but the source will try again sending its frame. This is a non usual situation since ACKs are usually received by the sender of a frame, and in any case not caused by our algorithm. The consequence is that the destination will receive a duplicated frame. In B2.4, the relay won the access to the channel and the destination sent an ACK that is only received by the relay, not the source. Note that the source did not receive the retransmission as well. In this case, the source will still try to retransmit its frame. As we will show in the next section, this In states B1.3, B1.7, B2.2 and B2.3 we observe delayed ACK, which is the reception of an ACK following a successful retransmission by another station. The received ACK still acknowledges the corresponding frame in queue and the receiving stations should discard the queued frame. In states B2.6, B2.9 and B2.10, we consider passive acknowledgement, which is the overhearing of a retransmission by another station of a frame for which a station is waiting to send. For example, in state B2.6, the relay retransmits the frame, and the initial source considers that transmission as an acknowledgement of its previous transmission even though it did not receive the ACK. In this case, the transmission is delegated to the relay. In the next section, we detail the FBR implementation in NS-2 and show preliminary results.

IV. IMPLEMENTATION IN NS-2

A. NS-2 Implementation

NS-2 is an open source and well known network simulator written in TCL and C++. We based our implementation on the 802.11Ext module which is one implementation of the IEEE 802.11g from the university of karlsruhe [START_REF] Chen | Overhaul of ieee 802.11 modeling and simulation in ns-2[END_REF]. The 802.11Ext module comes with two submodules called mac-80211Ext and phy-80211Ext. We modified mac-80211Ext in order to implement our solution and we improved the physical layer by adding a more realistic packet error rate (PER) model based on Bit Error Rate (BER) sampling found in the literature.

1) Modifying the mac-80211Ext module: This module is composed of several submodules, each of them coordinating the internal parts of the MAC mechanisms. While we left unchanged the Channel State Manager submodule, we modified the Reception Coordination (RxC), the Transmission Coordination (TxC) and the Backoff manager submodules. Figure 2 shows the FBR implementation in RxC, the submodule responsible for handling frames received by a station. In the RXC IDLE state, a station may receive a frame that can be a data, ACK, RTS or CTS. If the received frame is a data and the receiving station is not the destination, we implemented additional functions. First, we check if the received frame is a frame that the receiving station is currently trying to send. If this is the case and the received frame was sent by a better station, it will be considered as a passive acknowledgement; it shows that the frame has already made progress toward the destination. Thus, the station will remove this frame from its queue. Otherwise, if the frame is not a passive acknowledgement, it might need a retransmission. The receiving station checks if it is a potential forwarder i.e. if it has more chances to reach the destination than the sending station. If so, it prepares the frame for relaying (setting its own signal quality into the fourth address field) and waits for the ACK (state TXC WaitACKRelay).

Figure 3 shows the FBR implementation in TxC, the submodule responsible for managing the frame to be transmitted by the station. We only show the FBR part of the module that starts with the state WaitACK-Relay. This state means that the station overheard a unicast data frame sent by a station with a lower signal quality than the current station. If the station receives an ACK before the timer expires, no retransmission is needed and the overheard frame is dropped. If the timer however expires, a retransmission is needed and the station starts a backoff procedure to retransmit the frame (state RELAY PENDING). Then two outcomes are possible. Either the station receives a passive acknowledgement (as explained above) in which case the backoff is cancelled and the frame is dropped. Or the backoff timeouts and the station retransmits the frame, waiting again for an ACK (state WaitACKRelay). This loops until it is acknowledged (passively or with an ACK) or until it reaches the maximum number of retransmissions.

In order to implement a fair queuing between the frames originating from a station and the frames being relayed by this station, we modified the backoff management submodule in order to manage two independent backoffs. Each backoff manages its own contention window size and randomly picks a number of slots (as long as the two backoffs are different to avoid collision). 2) Implementing a realistic Packet Error Rate model: The 80211Ext does not take into account the frame size in the computation of the PER. It provides a threshold algorithm based on the receiving power of a frame to state whether the frame is received or not. Since our algorithm strongly depends on the reception of the ACK, such a limitation would have strongly biased our results as an ACK would have had the same chance of being lost than a 1500 byte frame. IEEE 802.11g uses OFDM to provide various data rates (from 6 to 54 Mbps). Each data rate has its own characteristics such as the valence (number of bits that one carrier can code), the modulation (BPSK, QPSK, 16QAM or 64-QAM), the coding rate (redundant information to make it more resistant to perturbation) or the hamming distance d. The BER is different from one data rate to another as it depends on these characteristics. We used a sampling array found in the literature [START_REF] Miller | Validation of 802.11 a/uwb coexistence simulation[END_REF] in order to estimate the BER values. Given the BER, we were able to compute the PER using the following formula: where d is the hamming distance corresponding to the data rate used to transmit the frame and L is the frame size.

P ER 1 = L.BER

B. Validation and Results

We performed simulations to validate the implementation and to show that FBR improves legacy IEEE 802.11. The scenario consists of one IEEE 802.11 AP, one station acting as a source of traffic and a FBR station in between. The source is located so that its PER with the AP is 33%. This means that over 100 frames sent, 33 will not be received by the access point and will need a retransmission. The FBR node being placed between the source station and the AP, it has a PER lower than 0.01% with both of them. We performed two runs, one with the FBR mechanism disabled and another one with the FBR algorithm enabled. In both cases, the source sends a CBR (Constant Bit Rate) traffic to the AP at the maximum rate possible, saturating the channel.

Figures 4 and5 represent the transition probability of the source station when it tries to send a frame. When the source sends a frame for the first time, it goes from the state IDLE to the state WAIT RX ACK through a TX transition. This means that the source sent a frame to the access point and is now waiting for an ACK from the AP. In the Legacy IEEE 802.11, presented in figure 4, two transitions are possible: one is labelled RX ACK and goes back to IDLE. This first transition means that the station has received the ACK sent by the AP and thus acknowledges the frame. It goes back to the IDLE state because the retransmission process for this frame is done. The other transition is labelled TX RETRY and goes to the state WAIT RX ACK RETRY 1. This means that a timeout fired and the station has retransmitted its frame and is now waiting for an ACK. If the transmission failed again, it retransmits the frame and goes to the state WAIT RX ACK RETRY 2, and it goes on until the frame is acknowledged or it reaches the maximum number of retransmissions as shown by the RETRY LIMIT transition.

In the FBR mode shown in figure 5, a third transition is possible from the state WAIT RX ACK. This transition is labelled RX DELAYED ACK and goes back to IDLE. This transition means that the FBR station placed between the source and the AP has overheard the transmission of the source and has decided to retransmit the frame after it has detected that no ACK had been sent. This retransmission made by the FBR node on behalf of the source is immediately followed by an ACK from the AP. Whether it is the overhearing of the retransmission or the reception of its following ACK by the AP, both are considered by the source as a delayed acknowledgement because the frame is being acknowledged (passively or by the ACK) after the standard timeout for which the value is SIFS (10µs in IEEE 802.11g).

We observe that the mean number of transmissions (ETX) decreased from 1.30 without FBR, to 1.26 when FBR is enabled. In both cases, the source succeeds in transmitting a frame in the first attempt in 67% of the times (as expected since its PER is 33%). If we focus on the frames that actually needed a retransmission, we can see that without FBR, the retransmission overhead is 30% which means that for 100 frames that needed to be retransmitted, 130 transmissions have been necessary. The retransmission overhead is only 12% with FBR enabled which means that we reduced the number of retransmissions by 60%. If the relay would have won every contention, we woud have needed only one retransmission for each unacknowledged frame, reaching 100% of reduction, because the relay almost never fails its transmission. Even though the relay does not win every contention, the contention window of the relay is always lower than the source's. The source increases its contention window at each retransmission giving the relay better chance to win the contention. Moreover, as the number of retransmissions is reduced, it creates more opportunities for the source to send new data. Indeed, less retransmission means that the contention window size will be lower on average, reducing the backoff time as well. As a consequence, the source is able to send more frames, reaching 7.03Mbps with FBR against 6.7Mbps without FBR. We described a new mechanism called FBR designed for IEEE 802.11 networks for frame relaying. FBR allows, under certain conditions, surrounding nodes to retransmit a frame on behalf of the source. We detailed the FBR implementation into the Network Simulator NS-2 which is two fold. Firstly we modified the Mac-80211Ext module so that FBR can be enabled and secondly, we enhance the physical layer in order to take into consideration the size of the frame in the computation of the Packet Error Rate. Finally we provided a simulation analysis using transition diagram that shows how FBR works and how it outperforms the legacy IEEE 802.11 mechanism.

Fig. 2 .

 2 Fig. 2. Modifications to the RxC submodule

Fig. 3 .

 3 Fig. 3. Modification of the TxC submodule

  d , P ER 2 = 1 -(1 -BER) L , P ER = min(P ER 1 , P ER 2 ).

Fig. 4 .

 4 Fig. 4. Transition probability for legacy 802.11

Fig. 5 .

 5 Fig. 5. Transition probability for FBR


Julien Tanguy

Jean-Luc Béchennec

Mikaël Briday

Sébastien Dubé
email: sebastien.dube@see4sys.comjean-luc.bechennec

Olivier H Roux
email: olivier-h.roux@irccyn.ec-nantes.fr

Device driver synthesis for embedded systems *

Currently the development of embedded software managing hardware devices that fulfills industrial constraints (safety, real time constraints) is a very complex task. To allow an increased reusability between projects, generic device drivers have been developed in order to be used in a wide range of applications. Usually the level of genericity of such drivers require a lot of configuration code, which is often generated. However, a generic driver requires a lot of configuration and need more computing power and more memory needs than a specific driver. This paper presents a more efficient methodology to solve this issue based on a formal modeling of the device and the application. Starting from this modeling, we use well-known game theory techniques to solve the driver model synthesis problem. The resulting model is then translated into the actual driver embedded code with respect to an implementation model.

By isolating the model of the device, we allow more reusability and interoperability between devices for a given application, while generating an applicationspecific driver.

Introduction

The development of device drivers in embedded systems is a critical and error-prone task. Because a device driver is the interface between the hardware device and the application or the operating system, the designers must have a knowledge of all those three components in order to develop efficient and safe drivers. The security aspect is emphasized by the execution context of most drivers: Being executed with supervisor privileges, any error in a driver may have a serious impact on the integrity of the entire system.

Another difficulty for designing device drivers is the device datasheet. Although it is designed to help a driver designer by explaining briefly how the device works, it does not document all possible behaviors. For example, a datasheet might specify that a device must be shut down in order to change some configuration registers, but it does not explain the outgoing of a configuration register change while the device is running.

To improve driver correctness and quality, a number of verification techniques [START_REF] Ball | Thorough static analysis of device drivers[END_REF][START_REF] Post | Integrated static analysis for linux device driver verification[END_REF] has been developed. An alternative to verification is to improve the development process by synthesizing the driver from a formal specification. The verification method ensures that the driver behaves correctly and can check protocol violations between the application and the driver, while the synthesis approach ensures a correct-by-construction driver. However, for configurability and inter-operability reasons, such generated drivers, still conform to the traditional model of a driver consisting of multiple API endpoints, with minimal state.

Our research targets real-time embedded systems with hard timing constraints, mainly but not exclusively for automotive systems. These systems have usually high requirements in terms of functional safety, but on the other hand they have few resources in terms of computing power and memory storage.

An example of such constraints is the reaction time of an airbag controller, which has to be around a few microseconds.

Given these constraints, the automotive industry have developed AUTOSAR, a configurable architecture [START_REF] Kirschke-Biller | Autosar -A worldwide standard current developments, roll-out and outlook[END_REF]. It defines a basic software architecture, consisting of several generic modules which implements all possible features.

These modules are usually defined as i) a core of basic functionalities which can do everything, ii) some configuration code which selects or refines the previously defined behaviors and wrapper code to encapsulate the module functionalities in APIs -see figure 1. The configuration code is usually generated at compile-time and compiled along the core code, but the specification allows a postcompilation configuration which is passed to the core code by pointers. This high level of configurability at every level increases greatly the complexity of such systems; they usually require multiple modules and abstraction levels. It can also result in a lot of dead code and if the configuration is not perfectly tuned to the application demands unnecessary behaviors make it into the code and may be executed. This comes at the cost of decreased performance and greater memory footprint, in terms of stack size, ROM and RAM usage. The consistency of the configuration must also be checked in order to be sure that the driver cannot behave in an unspecified way.

Even with consistency checks, there is no certain method to ensure that all behaviors which make their way to the final binary will be used by the application.

However, the automotive standards are quickly evolving and safety constaints are becoming more and more strict.

Driven by the industrial need for more formalism and verification, we have developed a synthesis approach based on a formal modeling of the system. By using a formal model approach, we can use well-developed modelchecking techniques to ensure safety constraints functionnaly on the model and on the generated code.

This methodology has the particularity of being a more application specific approach than existing conventional drivers, which reduces the number of abstraction layers between the application and the driver, and generates the sufficient and necessary behavior, producing a small code.

Related works Some work has already been done in driver synthesis.

The Devil language [START_REF] Mérillon | Devil: An idl for hardware programming[END_REF] is a Domain Specific Language (DSL) targeted at the description of basic communication protocols with a device. Devil comes with tools to check for consistency of such models. However, being a low- The Termite tool [9] uses a generic approach to driver synthesis, by specifying a driver in three different specifications:

• a device-class specification, which defines the messages used internally for a class of device drivers; • a device specification, which defines the access protocol with the device; • an OS specification, defining the communication protocols between the driver and the Operating System.

These three separate specifications allows reusability and exchangeability of devices and operating systems; their specifications depending only on device-class one. However, Termite-generated drivers work only in the context of a special framework, which simplifies the internal structure of the driver. For example, all events going in and out of the driver (API calls, hardware interrupts, etc.) are serialized and dealt with several handlers sequentially. This serialization behaves nicely in the context of UNIX drivers for desktop use, because these systems have enough computing power to handle all events in a reasonable time, but in the context of embedded systems, which have a very limited computing power and memory, the additional memory and computing cost cannot be afforded.

Our contribution

We propose a new approach to device driver synthesis using an untimed reachability game on a formal model of the device, controlled by the application. Such information is often unavailable until runtime, but in the case of critical embedded systems it is known at compile-time. By introducing more information from the application, it is possible to reduce the complexity of the exposed API, thus reducing the number of errors that can be made. For instance, instead of having to initialize an analog to digital converter, setting up the conversions settings and starting the conversion -which is a typical usage of a conventional API -it is better to have a reduced semantic API for sampling a speed value, or sending a temperature message through the network. In this context, the driver would perform such initializations and configuration automatically, depending on the current objective.

This allows to generate more application-specific drivers, and limits the need for abstraction layers, since the driver API is exposed directly to the application.

Outline of the paper This paper is organized as follows: first we present the underlying modeling which supports the methodology presented in section 3. The methodology is explained on a simple example in section 4. At last some concluding remarks and considerations about future work are presented in section 5.

Definitions

This methodology relies on a model derived from Labeled Transitions Systems (LTS), in which transitions can have guards. In order to define this model formally, let us define some common terms beforehand.

Let N be the set of natural numbers. For a finite set E, we denote by 2 E the set of all its subsets. Let γ P be a propositional logic over the predicates p ∈ P , e.g. of the form ϕ := p|¬ϕ|ϕ ∧ ϕ, where p ∈ P For A ⊆ P , we define the semantics of such propositional logic:

• A p iff p ∈ A; • A ¬ϕ iff A ϕ • A ϕ ∧ ψ iff A ϕ and A ψ
For g, g ∈ γ P we say that g and g overlap if ∃A ⊆ P, such that A g and A g

Definition 1 (Guarded labeled transition system) A guarded labeled transition system (GLTS) is the tuple

(Q, Q 0 , A, P, E, l) , where • Q is a set of states; • Q 0 is a set of initial states; • A is a set of actions; • P is a set of atomic properties; • E ⊆ Q × γ P × A × Q is the set of edges between the states; • l ⊆ Q × 2 P is a labeling function.
Deriving the definition for standard Labeled Transition Systems, we say that a GLTS (Q, Q 0 , A, P, E, l) is deterministic if:

• |Q 0 | = 1.
We denote it as q 0 .

• if (q, a, g , q ) and (q, a, g , q ) ∈ E, then g , g do not overlap if q = q .

In the sequel we will only consider deterministic GLTS. We also define an asynchronous product operation on networks of GLTS. For the following definition, we con-

sider n GLTS S i = Q i , q i 0 , A i , P i , E i , l i , i ∈ 0, n , where ∀i, j ∈ 0, n , i = j =⇒ A i ∩ A j = ∅. We denote A • i = A i ∪ {•}, where • / ∈ A i .
Definition 2 (Asynchronous product of GLTS) The asynchronous product S = S 0 × • • • × S n of the n GLTS is the GLTS (Q, q 0 , A, P, E, l) where:

• Q = Q 0 × • • • × Q n , • q 0 = (q 0 0 , . . . , q n 0 ), • A = A 0 ∪ • • • ∪ A n • P = P 0 ∪ • • • ∪ P n • ((q 0 , . . . , q n ), a, g, (q 0 , . . . , q n )) ∈ E such that ∀i ∈ 0, n , g = g i and (q i , a, g, q i ) ∈ E if A ∈ A i q i = q i otherwise. • for q = (q 0 , . . . , q n ) ∈ Q, l(q) = l 0 (q 0 )∪• • •∪l n (q n ) Definition 3 (Semantics of a GLTS)
The behavioral semantics of a GTLS (Q, q 0 , A, P, E, l) is the LTS (Q, q 0 , A, →), where ∀(q, a, g, q ) ∈ E, (q, a, q ) ∈→ ⇐⇒ l(q) g.

Methodology

The synthesized driver is derived from two separate models: one of the device, which models the internal behavior of the device, and one of the application settings, which models how the device will be used by the application.

In order to synthesize such drivers, we propose the following workflow:

1. Model the hardware device, with some synchronization primitives. This modeling does not require any knowledge about the application, thus can be done once for a particular device. 2. Model the application configurations, or modes of operations the application needs the device to be in. 3. Define driver objectives; 4. Generate the configured device model and compute strategies; 5. Translate abstract actions into actual code.

The application settings model is the representation of how the device is used by the application. In this model, several functional modes are defined, each mode representing a set of values of the configuration registers.

Modeling the components

Modeling the device The first step -the device model -models only the device behavior at register level: writing to control and configuration registers, reading from data and status registers, and sending interrupt to the driver.

It is the only reusable model between different applications, and can be part of some sort of model database. It is based only on the device datasheet. As part of the synthesis methodology, a device modeling methodology is proposed.

First, the set of all register fields is partitioned into three sets, depending on the effects a register read/write has on the device:

• the Control Fields. Writing in a control field has an immediate effect on the device's behavior. • the Configuration Fields. Writing to a configuration field has no immediate effect on the device, but alters future behavior of the device. For example, an input channel selection field, or a device mode fields are considered part of the configuration space. • the Data Fields, on which reading or writing to has no effect.

For each of the control actions, one or more abstract actions is added to the alphabet A of the model. For example, from a Power Down boolean register field, two actions can be defined: PowerUp and PowerDown. These are called the controllable actions A C . The uncontrollable actions A U of the device are also modeled, such as some internal action or hardware interrupts.

For the configurations, a set of atomic properties P is defined such that each atomic property corresponds to a valuation of a register field. The properties are used as guards in the device model, but are attached to states of the application settings model.

Sometimes, the datasheet imposes constraints on the changing of certain register fields in certain states, or it simply does not make sense to allow the modification of some registers while the device is busy. These restrictions are modeled by adding new properties to the states in which changing a register field is allowed, and some application settings model generation rules.

With all these guidelines, it is possible to produce a device model which corresponds to the behavior described in the device datasheet. The use of additional properties is allowed, to mark particular states of the device.

In a nutshell, the device model exposes to the application designer:

• a set of configuration properties P cf g . These properties can be further grouped into sets of semantically related properties. For instance, a 1-bit interrupt mask can be split into two properties interrupt and polling. • a set of synchronization rules, in the form of (P sync , g), where P sync ⊂ P and g ∈ γ P : if one of the properties in P sync is used, then the corresponding GLTS must add g as a guard for every of its transitions. For instance, one might define a rule (interruptSync, {interrupt, polling}). • a set of additional informative properties P inf o about the state of the device, such as PowerDown, Idle, Busy, Waiting, etc.

Modeling the application settings Once the model of the device is defined, the application designer has to define how it will be used by the application. The application settings are modeled by a global mode which is split into several independent sub-modes. These submodes can represent runtime behavior -e.g. Low-Power, Sleep -or statically defined properties -e.g. Channel groups in Analog-Digital Conversion, Types of frames in CAN/LIN/SPI communication, etc. Formally, the global mode M divided into several submodes M = (m 1 , . . . , m n ). Each of these sub-modes have a set of possible values: m i ∈ m 1 i , . . . , m pi i . Each value m j i of a sub-mode is mapped to a set of atomic properties among those exposed by the device model, representing the required configuration of the device in that sub-mode.

Even though it is possible to split valuations of a register field into several properties (for example, a 1-bit interrupt mask can be split into two properties interrupt and polling), there is an implicit restriction that only one of these properties can tag a sub-mode. Adding both properties to a sub-mode would render the sub-mode inaccessible, because of the way deterministic GLTS are defined.

These sub-modes are independent in the sense that they have no influence on each other, but they are linked by the synchronization constraints of the device.

Once defined, each sub-mode m i is transformed into a GLTS (Q mi , q mi 0 , A mi , P mi , E mi , l mi ) by the following method:

1. each valuation m j i of the sub-mode is mapped to a state Q mi of the GLTS; 2. all properties tagging any sub-mode tags the corresponding state; 3. a default reset state q mi 0 with no properties attached to it is added; 4. the alphabet of actions A mi is derived from the state names, e.g. toLowP ower , toReset, etc. 5. the transitions from and to every state are generated with respect to the synchronization rules by adding a conjunction of all the required guards to every transition, i.e. for all synchronization rules (P sync k , g k ) and all transitions (q 1 , a, g, q 2 ) ∈ E mi , l mi (q 1 ) ∪ P sync k =⇒ ∃g such as g = g ∧ g k .

The initial reset state assumes that the state of the device is not known when the driver (re)starts. The fact that it does not hold any property ensures that one of the first actions taken by the driver is to configure the device into a defined mode before doing any work.

The global mode GLTS M is obtained by computing the asynchronous product of all sub-modes.

Driver generation

Once the model of the device and its configuration are defined, well developed control and game theory techniques [START_REF] Church | Logic, arithmetic and automata[END_REF][START_REF] Ramadge | The control of discrete event systems[END_REF][START_REF] Pnueli | Controller synthesis for timed automata[END_REF] are used in order to generate the driver model. Although the problem defined by the GLTS model could be reduced to a shortest path problem in a graph, this methodology uses a more generic, model-agnostic approach which can be easily extended to timed models by simply changing the underlying modeling and game rules. But first let us define the outline of a driver.

Anatomy of the driver

In this model, a driver consists of an arena G a a set of objectives O. An objective represents a set of atomic properties which the configured device is to satisfy, for instance the power down or idle state, a busy state while converting a certain analog input, or the end of the sending of a given frame over the network.

For each objective, the driver has a strategy, i.e. a sequence of actions to take in order to get from the current state to an objective state. For this model it is sufficient to consider only memoryless strategies, i.e. strategies in which the actions to take are dictated only by the current state, and not the sequence of states which led to the current one. These strategies are computed with respect to the model of the configured system which represents the possible behaviors of the device and any mode change in the application settings.

At any point in time, the driver has only one active objective, and is taking actions to fulfill this objective. When it is reached, the driver does not take any action until the objective is changed.

More formally, given a model D of the device, we want to generate a controller C -the driver -such that the system D|C composed of the device controlled by the driver satisfies a given property ϕ, expressed by the LTL property for all paths:

ϕ = A, with A ⊆ P.
Problem 4 (Control problem) Given D and ϕ, is there any driver (or controller) C such that D|C ϕ?

Generating the game arena and the game The model of all possible behaviors of the configured device -including changing sub modes -is called the arena G a . It is obtained from the semantics of the asynchronous product Π async of the device model D and the driver modes M. The product Π async is computed as described in definition 2.

Taking the semantics of this product, we obtain the following LTS:

(Q a , q a 0 , A a , → a ) .
The game arena is derived from this LTS by partitionning the alphabet A a of actions in A C a and A U a . The alphabet of controllable actions groups the controllable actions of the device and all the sub-mode change actions:

A C a = A C D ∪ A M .
The alpbabet of uncontrollable actions is the uncontrollable actions of the device only:

A U a = A U D .
Assuming the initial device model is correctly defined, taking the semantics of the product ensures that any nonspecified behavior is not accessible.

The problem reduces to an untimed two-player safety game between the driver, performing controllable actions of the device and all sub modes switches, and the device performing its uncontrollable actions. There are several algorithms to compute a strategy which resolves this game.

One of the most used is the algorithm defined in [START_REF] Pnueli | Controller synthesis for timed automata[END_REF], with the controllable predecessor method.

Intuitively, this method computes iteratively the set of states for which a strategy exists -these are called winning states -starting from the set of goal states. At each iteration, the algorithm adds to the set of winning states all its controllable predecessors.

A controllable predecessor of a set S of states is a state for which there exists at least a controllable action a c ∈ A C to S and all uncontrollable actions a u ∈ A U also lead to S.

More formally, the controllable predecessor set π(S) of S ⊆ Q is defined as follows:

∀q ∈ Q \ S, q ∈ π(S) if and only if ∃q ∈ S, a ∈ A C s.t. (q, a, q ) ∈→ ∀q ∈ Q, ∀b ∈ A U s.t. (q, b, q ) ∈→, q ∈ S. (1)
When computing the controllable predecessors, the algorithm deduces a strategy to execute in order to reach the goal states.

This algorithm ends when it has reached a fixpoint, i.e. when it cannot add any new state to the winning states. The remaining states which could not be added are the loosing states. In these state there is no action to take in order to go to a winning state, whatever the device does.

More formally, the algorithm is as follows:

Win 0 ← Goal i ← 1 repeat Win i = Win i-1 ∪ π(Win i-1 ) i ← i + 1 until Win i = Win i+1 ;
Algorithm 1 (Computing the winning states) Future work will lift part of the constraints, allowing the driver to wait for an uncontrollable action because it will happen eventually, whereas the current hypothesis allows the device to withhold the interrupt and lock the driver indefinitely.

From the computation it is possible to derive a memoryless strategy for each objective: each state is either a goal state -the driver has nothing to do -, a losing state -the driver cannot do anything and may fail into some error recovery mode -or the driver has a controllable action to take in order to reach one of the goal states.

Example

In this section, we will apply the methodology to a simple example. Let us consider a simple and generic Analog to Digital Converter. This device is part of almost all micro-controllers, and its role is to sample analog signals and convert them into digital values. Usually, a single ADC has several input channels. It can sample and convert its inputs either sequentially or in parallel.

The example ADC has the following features:

• two different clock modes, one half speed and one full-speed; • a power-down mode, only in which the clock configuration can be changed; • multiple input channels, converted sequentially in a conversion chain; • the conversion of each of the channels can be enabled or disabled, while the device is idle or shutdown; • two conversion modes: oneshot, in which only one conversion chain is performed, and continuous, in which conversion chains are performed indefinitely until the user stops the conversion (the last chain still ends the normal way) • the device triggers an End Of Conversion (eoc) interrupt at the end of each channel conversion, and an End of Chain (ech) interrupt at the end of a chain.

Modeling the device For this high-level model, the granularity is set at chain conversion level, so all the single channel conversions are abstracted.

From the specification, the following alphabet of actions is derived: abort, ech, sleep, start, stop and wakeup.

From the register description, the following properties are defined:

• Clock configuration: clkFull and clkHalf, for the two values of the speed, and clkCfg for the synchronization constraints. • Conversion configuration: Os, and Cont, for the oneshot/continuous setting, and convCfg for the synchronization constraints. • Informative properties: Idle, poweroff and busy.

The device model is straightforward, as presented in figure 3.

Modeling the configuration Once the driver model is defined, we can define the application configuration, or the driver modes. For this example, the application usage is as follows: • The driver shall perform conversions fast, so only the clkFull setting will be used. • The driver will convert two groups of signals: one is to be monitored continuously, with the Cont setting, while the other corresponds to on demand conversions, using the Os setting.

These modes are then translated into GLTS, following the method defined in 3. For the example, the general driver modes is divided into two sub-modes: the conversion submode and the clock sub-mode. Here only the conversion sub-mode is detailed. First three states are defined: reset, G1 and G2. G1 is tagged with clkfull and Os, while G2 is tagged with clkfull and Cont. Since these states involve the conversion properties, all the transitions must have convSync in their guard.

The resulting automaton is presented figure 4. Note that all these transitions will be controllable for the driver, since they represent changes of its internal mode.

Defining driver objectives For this example, the application needs to perform two types of conversions: one for the group G1 and one for the group G2. We will also consider a low-power mode of the driver, where the device is switched off. These two conversion groups and the lowpower are then translated into three driver objectives:

1. Go to a state labeled by poweroff 2. Go to a state labeled by G1 and busy 3. Go to a state labeled by G2 and busy Generating the arena and computing strategies Once all the components of the configured system are defined in terms of GLTS, the arena of the game is generated. First, all the models are composed into an asynchronous product.

The semantics of the product is shown figure 5. In any of the states the driver can take the controllable actions, represented with solid lines, and the uncontrollable actions are represented in dashed lines.

This product model is then processed with the driver objectives in order to generate adequate strategies. The computed strategies for all the objectives are presented in table 1.

These strategies are similar, except for one loosing state for the first two objectives. This is due to the untimed nature and the worst-case hypothesis of the game. In this context, a strategy wins if the driver can force a behavior whatever the device does. But here the untimed strategy does not work because the zeno behavior where the device does the ech action infinitely often prevents the driver to act. This behavior is obviously unrealistic: in reality, the ech interrupt has a minimum period, so the driver has time to cancel an ongoing conversion, or the related interrupt can be masked.

Future improvements of this work will consider timed models of the device, which are more complex to analyze and to compute strategies for.

Conclusion

We have developed a generic methodology and supporting models for device driver synthesis. It is designed specifically for embedded real-time systems, with low complexity and small memory footprint, and can be adapted to more complex models.

It relies on a particularity of such systems, which are to be completely defined at compile-time. It is possible to reduce the amount of generated code by performing optimisations at the model level -cutting unreachable states when applying the possible strategies -thus producing only necessary and sufficient code. 1. Computed strategies on the arena Future development Future developments of this methodology will include more complex elements into the model. We will include the management of shared data variables and buffers, allowing the definition of safety objectives such as "This buffer shall not overflow".

In order to manipulate finer models, we need to add time to these models, like in [START_REF] Alur | A theory of timed automata[END_REF]. Along with the notion of time, it is possible to express the notion of urgency, adding a whole range of available behaviors to the driver.

At last we will build a complete prototype being able to generate a device driver code from a model. Performance will be evaluated on an actual platform and compared to device drivers developed in a traditional way.

Figure 1 .

 1 Figure 1. Current development methodology

Figure 3 .

 3 Figure 3. Model of the device. Controllable actions are represented with solid lines, and the uncontrollable actions are represented in dashed lines.

Figure 4 .

 4 Figure 4. Conversion sub-mode GLTS. This GLTS is generated with 3 modes: One Shot mode (1), Continuous mode (2) and the default reset mode.

Figure 5 .

 5 Figure 5. Generated model of the arena

This work was partially funded by the ANR national research program ImpRo (ANR-2010-BLAN-0317).