Nathalie Job

Jean-Paul Pirard

Sandrine Berthon-Fabry

Marian Chatenet

Pt/CARBON XEROGEL CATALYSTS FOR PEM FUEL CELLS

Carbon xerogels have been used to replace carbon black as catalyst support at the cathode of proton exchange membrane (PEM) fuel cells in order to decrease the mass transport limitations in this electrode. Carbon xerogels are very clean nanostructured carbons with well-defined pore texture, which allows for better reactant/product diffusion. Pt/carbon xerogel catalysts with high metal dispersion (nanoparticles ca. 2 nm in size) and high metal content (~ 25 wt.%) can be engineered via rational synthesis methods such as the 'Strong Electrostatic Adsorption' technique. The results show that choosing correctly the average pore texture of the carbon xerogel allows for minimizing the diffusion overpotential of the H 2 /air cell. However, the catalyst characterization indicates that the presence of chlorine, coming from H 2 PtCl 6 , induces a dramatic decrease of the Pt utilization ratio in the final PEMFC catalytic layer. To remove chlorine, a reduction of the catalyst at 450°C, at least, is necessary.

INTRODUCTION

The catalytic layer configuration is a key-element in the design of PEM fuel cells [1]. Indeed, besides the characteristics of the chosen catalyst (composition, crystallographic structure, dispersion, connectivity with the membrane, etc.), the structure of the catalytic layer itself affects the mass transfer phenomena in the electrodes as well as their intrinsic reactivity [2]. To reach high performance, reactants and products should be able to circulate easily through the catalytic layers: (i) the catalyst must be accessible to the gas reactant, through the percolating porous structure of the catalytic layer; (ii) protons and electrons need to be collected by the ionomer and the catalyst support, respectively, and driven to the membrane (protons) and the current collector (electrons) [2]. Thus, the optimisation of mass transfer inside the electrodes is one of the foreseen ways to increase fuel cell performances [1].

Carbon blacks, commonly used for the preparation of the catalysts, are formed of primary carbon particles (~50 nm) assembled together as agglomerates (1 -100 µm) [3]. The pore structure of the catalytic layers strongly depends on the packing of these agglomerates; as a consequence, the choice of the carbon black used as well as the electrode processing influence the mass transport phenomena. Typically, at the air-fed cathode, where the transport of oxygen, protons and water are involved in the oxygen reduction reaction (ORR), high potential losses due to diffusion limitations offset the cell performance. To cope with this problem, PEM fuel cell designers generally use catalysts with very high platinum loadings (50 wt.% and more), which enables one to prepare thin catalytic layers with acceptable diffusion-induced potential losses. However, reducing the Pt loading of PEMFC electrodes is one of the requirements to reach commercially viable PEMFCs. This major drawback calls for the development of new carbon materials with controllable and tunable pore texture. In addition, and especially for electrochemical applications, high purity of the carbon supports is also essential [4]. The goal of the present work is to design new Pt/C catalysts using a support with adapted pore structure. Recently, it was envisaged to replace carbon blacks by carbon gels, i.e. synthetic porous carbons. In particular, carbon xerogels prepared by evaporative drying and pyrolysis of resorcinolformaldehyde aqueous gels [5,6] proved to be efficient as catalyst and electrocatalyst supports [7][8][9]: these materials are very clean nanostructured carbons with well defined pore size, which is easily tunable between a few nm and a few µm. This pore texture allows for better fluid diffusion in catalyzed processes [7]. The present paper aims at showing the advantages of carbon gels as electrocatalyst supports for PEM fuel cell electrodes.

EXPERIMENTAL

Catalyst preparation

Carbon supports were synthesized by the drying and pyrolysis of resorcinol-formaldehyde aqueous gels, following a procedure developed in a previous study [6]. The procedure consists of the polycondensation of resorcinol (R) with formaldehyde (F) in a solvent (water), followed by evaporative drying and pyrolysis. Globally, the pore texture of the final carbon is fixed by the pH of the solution, which is adjusted by adding a basification agent, usually sodium carbonate (C). In most works dealing with RF carbon gels, the pH adjustment is reported through the resorcinol/sodium carbonate molar ratio, R/C. In the present work, R/C was chosen equal to 750, 1000 and 2000 while all other synthesis variables (from gel preparation to pyrolysis conditions) were kept identical as in the above-mentioned study. In brief, resorcinol and sodium carbonate were solubilized in water, prior to formaldehyde addition. Gelation and ageing were performed at 85°C (72 h), followed by evaporative drying (60-150°C, 1 day) and pyrolysis (800°C, 2 h) under nitrogen flow.

Fig. 1 shows the evolution of the pore texture of carbon xerogels with R/C. Scanning electron microscopy (SEM) micrographs of carbon xerogels presenting extreme morphologies are shown on Fig. 1a and1b. Carbon xerogels are materials composed of interconnected spherical-like microporous nodules. So, they classically display a bimodal pore size distribution: micropores inside the carbon nodules, and larger pores identified as the voids located between the nodules [5,6]. The size of the nodules and that of the voids inbetween is controlled by the synthesis conditions of the pristine gel, and particularly by the pH of the precursors' solution [5,6]. Fig. 1c reports the mesopore size distribution of three carbon xerogels prepared and tested in this study: the average meso/macropore size is of ca. 30 nm (R/C = 750), 60 nm (R/C = 1000) and 200 nm (R/C = 1000). The meso/macropore volume increases with R/C (1.3, 2.1 and 2.2 cm³ g -1 , respectively), while the volume of micropores remains nearly constant (~0.26 cm³ g -1 ). This micropore volume corresponds to a specific surface area of about 650 m² g -1 .

Pt/carbon xerogel catalysts were obtained via the 'Strong Electrostatic adsorption' (SEA) method [START_REF] Regalbuto | Catalyst Preparation: Science and Engineering[END_REF]. This method consists of maximizing the electrostatic interactions between the metal precursor and the support by adjusting the pH of the slurry to the adequate value, the latter depending on the surface chemistry of the carbon and on the precursor chosen. Indeed, interaction between the support and the metal precursor depends on both the precursor nature (anion or cation, size, etc.) and on the carbon surface chemistry [START_REF] Regalbuto | Catalyst Preparation: Science and Engineering[END_REF]. At pH values lower than the Point of Zero Charge (PZC), i.e. the pH at which the surface is neutral in terms of charge, the surface is positively charged, and the adsorption of anions is favoured. At pH higher than the PZC, the surface is negatively charged, and the adsorption of cations is enhanced. However, the metal uptake is limited by steric and repulsive effects [START_REF] Regalbuto | Catalyst Preparation: Science and Engineering[END_REF]. As a consequence, depending on the support chemistry and metal precursor, one can define a pH window leading to a maximum uptake of metal. In a previous work [START_REF] Lambert | [END_REF], it was shown that the initial pH leading to the highest Pt uptake is equal to 2.5 (final pH at equilibrium ~ 3.0) for the impregnation of carbon xerogels with H 2 PtCl 6 aqueous solutions (1000 ppm Pt ); the corresponding maximum weight percentage per impregnation step ranges from 8 to 10 wt.% [START_REF] Lambert | [END_REF]. In that frame, the Pt/carbon xerogels were elaborated via the SEA method, as fully described in reference [9]. Briefly, the carbon support was contacted with the impregnation solution (H 2 PtCl 6 aqueous solution, 1000 ppm Pt ) at the optimal pH value of 2.5 until the equilibrium was reached. The impregnated catalyst was then filtered, dried and reduced under flowing hydrogen (200°C, 1 h). In order to increase the Pt weight percentage up to acceptable values for electrochemical applications, this impregnation-drying-reduction cycle was repeated up to three times using the same original catalyst batch. Note also that various final reduction temperatures (200, 350 and 450°C after the last impregnation cycle) were tested.

Catalyst characterization

Physico-chemical characterization

The pore texture of the carbon supports were characterized by classical methods, such as nitrogen adsorption-desorption and mercury porosimetry. These techniques give access to the specific surface area, the pore volume (micropores < 2 nm, mesopores between 2 and 50 nm and macropores > 50 nm) and pore size distribution. The methods for obtaining the pore texture characteristics of carbon xerogels are fully described elsewhere [5,6].

The catalysts were characterized using several complementary techniques. The Pt content was evaluated by ICP-AES after elimination of the carbon and solubilisation of the metal [12]. The size of the metal particles was investigated by transmission electron microscopy (TEM), with a Jeol 2010 (200 kV) device (LaB 6 filament). The samples were crushed and dispersed in ethanol and subsequently deposited onto a copper grid baring a lacey carbon membrane. Particle size distributions were obtained by image analyses performed on a set of at least 1000 particles, as described in [9]. The samples were analyzed by X-ray photoelectron spectroscopy (XPS), performed on an SSI-X-probe (SSX-100/206) spectrometer from Fisons [9].

Electrochemical characterization

All electrochemical measurements were carried out in sulphuric acid (1 M) at 25°C. The voltammetric experiments were performed using an Autolab-PGSTAT20 potentiostat with a three-electrode cell and a saturated calomel electrode (SCE) as a reference electrode (+0.245 V vs. normal hydrogen electrode, NHE).

The catalyst sample was deposited on a rotating disk electrode (EDT 101, Tacussel), used as working electrode. All details, from sample preparation to experimental conditions, are extensively described in reference [9].

The electrochemically active Pt surface area of the catalysts, S Pt-Strip , was determined by CO stripping, assuming that the electrooxidation of a CO ads monolayer requires 420 µC per cm 2 of Pt. Since CO stripping is performed in aqueous electrolyte, it implies 100% utilization of the Pt surface atoms and is influenced neither by contact problems between the metal and the electrolyte nor by mass-transport limitations. In addition, the electrooxidation of a CO ads monolayer is a structure-sensitive reaction and provides a wealth of information on the particle size distribution and the presence/absence of particle agglomeration [12,13].

The CO stripping voltammograms were recorded at 0.02 V s -1 between +0.045 and +1.245 V vs. NHE, after saturation of the electrolyte by CO (6 min bubbling) and removal of the non-adsorbed CO from the cell by purging with Ar (39 min).

The electrocatalytic activity for the ORR of the elaborated Pt/C nanoparticles was measured in O 2 -saturated liquid electrolyte. The quasi-steady-state voltammograms were recorded at 10 -3 V s -1 from +1.095 to +0.245

V vs. NHE. To account for the reactants diffusion-convection in the liquid layer, the experiment was repeated at four RDE rotation speeds (42, 94, 168 and 262 rad s -1 ) [START_REF] Bard | Electrochemical methods: fundamentals and applications[END_REF]. The results are reported in terms of (i) Tafel slope, b, and (ii) specific activity at 0.90 V vs. NHE, SA 90 . This potential corresponds to 0.34 V ORR overpotential in 1 M sulphuric acid, a value classically monitored in a PEMFC cathode at low current densities, i.e. under kinetic control.

Fuel cell test

The catalysts were tested as PEM fuel cell cathodic catalytic layers on a unit cell-test bench: 50 cm² Membrane-Electrode Assemblies (MEAs) were prepared by the decal method as described in reference [8].

The electrolyte was a Nafion ® membrane, and the anode a commercial anode made from Pt-doped carbon black (40 wt.%, TKK) deposited by Paxitech onto a carbon felt (0.6 mg Pt cm -2 mixed with Nafion ® ). The thickness of the cathode was kept constant by keeping constant the carbon mass in the catalytic layer. The Nafion ® /carbon mass ratio of the ink used to prepare the MEAs was fixed at 0.5. After a standardized startup procedure, polarization curves, i.e. the U cell vs. current curves, were measured by setting the cell voltage at each desired value for 15 min, which ensured the stabilization of the current. The current was normalized either to the electrode surface (j s ) or to the Pt loading of the cathode (j m ).

RESULTS AND DISCUSSION

Characteristics of the Pt/carbon xerogel catalysts

Fig. 2 shows an example of TEM micrograph and the corresponding Pt particle size distribution, obtained by image analysis, of a Pt/carbon xerogel catalyst. This catalyst was obtained by three consecutive impregnation-drying-reduction cycles performed on a support with a macropore size ranging from 50 to 85 nm, a specific surface area of 640 m² g -1 and a total pore volume of about 2.1 cm³ g -1 (including 0.26 cm³ g -1 of micropores, i.e. pores smaller than 2 nm). The results show that repeating the impregnation with H 2 PtCl 6 as Pt precursor yields to an increase of the catalyst metal content while keeping homogeneously dispersed Pt nanoparticles ca. 2 nm in size. The number of impregnation cycles does not modify the metal dispersion.

After three impregnation cycles, the Pt weight percentage of the catalyst was equal to 22.3 wt.%. Similar results were found using carbon xerogels with other pore textures (smaller or larger pores, various pore volumes). The metal dispersion observed by TEM is excellent. However, it is noteworthy that the final reduction temperature of the catalysts must be increased up to 450°C (5 h) to remove chlorine species coming from the metal precursor. Indeed, XPS measurements on catalysts reduced under various temperature conditions show that the Pt surface remains poisoned by chlorine when the reduction temperature is too low [9]. The relationship between the Cl/Pt ratio and the Pt surface detected by CO stripping, S CO-strip , is linear (Fig. 3a). This means that, due to Cl poisoning, the electroactive Pt surface is lowered compared to that calculated from TEM; this induces a dramatic decrease of the cell performance when the catalyst is reduced at low temperature (Fig. 3b). Note that increasing the reduction temperature up to 450°C does not induce any change in the Pt particle size: additional experiments have shown that the Pt nanoparticles begin to sinter at 650°C. Note also that consecutive CO stripping measurements can highlight the poisoning of the catalysts by Cl. Indeed, the detected Pt surface increases with the number of CO stripping procedures [9]; chlorine species are progressively removed by repetitive adsorption/desorption processes. In addition, the CO electrooxidation peak is shifted to more positive potentials when the reduction temperature decreases [9]. This may be ascribed to the competition between water and chloride species for the Pt adsorption sites. previous studies [START_REF] Maillard | [END_REF]16] have suggested that only a fixed number of active sites are able to form OH species and to initiate the CO electrooxidation kinetics on the Pt surface. Competitive adsorption by Cl - species decreases artificially the number of active sites and shifts both the onset and the main CO electrooxidation peak towards positive potentials.

U cell (V)
Oxygen Reduction Reaction (ORR) experiments performed in rotating disk electrode show that the presence of chlorine has little effect on the intrinsic reactivity of the Pt sites. Neither b nor SA 90 changes significantly with the reduction treatment (Table 1), indicating that the reaction mechanism and kinetics remain the same. The only difference between the three samples is the accessible Pt surface, which decreases due to Cl poisoning when the reduction temperature is too low. In that extent, it is interesting to note that the sites that are not accessible in CO stripping experiments are not accessible either in ORR experiments.

Architecture and performance of cathodes designed with Pt/carbon xerogel catalysts

A catalytic layer of a typical PEM fuel cell electrode is composed of Pt/carbon black catalyst particles, interparticle voids and ionomer, hot-pressed between a proton-exchange membrane and a diffusion layer (carbon felt) [4]. To be active, the Pt particles must be in contact with the carbon support and connected to the membrane via the ionomer (Nafion  ). In addition, reactants and products must circulate easily through the catalytic layers. In practice, a large fraction of the Pt can be inactive due to (i) a lack of contact between Pt and Nafion  , (ii) the presence of liquid water within the pores of the cathode and (iii) mass transport limitations. As carbon black particles are loosely bonded and packed together in aggregates, the pore structure of the catalytic layer not only depends on the nature of the carbon black, but also on the electrode processing. On the contrary, the meso/macropore texture of catalytic layers prepared from carbon gels is totally independent on the electrode processing and can be regulated by choosing correctly the composition of the pristine wet gel. In the electrode structure, the carbon black particle agglomerates are replaced by micromonoliths of carbon gel made of covalently bonded carbon nodules, which preserves the pores located in-between (Fig. 4).

Membrane-Electrode Assemblies (MEAs) were prepared with carbon xerogels of various pore textures as cathodic catalyst supports and tested in an air/H 2 monocell device at 70°C. The aim of these tests was to highlight the effect of the pore texture on the diffusion overpotential. Indeed, the total voltage losses of the cell with regard to the reversible H 2 /O 2 cell voltage can be decomposed into several components [START_REF] Gasteiger | Handbook of Fuel Cells -Fundamentals, Technology and Applications[END_REF]: (i) the cathode overpotential, η ORR , due to the sluggishness of the O 2 reduction kinetics; (ii) the ohmic losses, η Ohm , due to the resistance of the proton migration through the membrane and ionomer within the electrodes, the electronic contact resistances between the flow-fields plates and the diffusion media, and the contact between the carbon grains; (iii) the mass-transport losses, or 'diffusion overpotential', η diff , induced by slow O 2 diffusion through the diffusion layer and the catalytic layer. In such systems, kinetic and mass transport losses of the anode can be neglected [START_REF] Gasteiger | Handbook of Fuel Cells -Fundamentals, Technology and Applications[END_REF]. η ORR was obtained from measurements at low current densities, i.e. from data obtained in the near-absence of mass transport limitations and ohmic resistance; η Ohm was obtained by measurement of the ohmic resistance of the cell by impedance spectroscopy, performed in situ; η diff was calculated by difference. Fig. 5a shows the evolution of the diffusion overpotential with the pore texture of the carbon support: as the pore size increases, η diff decreases, which clearly shows the impact of the cathode architecture on the electrode performance.

The global performance of the MEAs prepared with Pt/carbon xerogel catalysts at the cathode side was compared to that of a MEA using a commercial catalytic layer at both electrodes. In all cases, the commercial catalyst used was made from Pt-doped carbon black (40 wt.%, TKK), and the catalytic layers were prepared by Paxitech via deposition onto a carbon felt (Pt loading: 0.60 mg Pt cm -2 ). In the case of Pt/carbon xerogel catalyst, the selected support was the carbon with 50-85 nm pores, and the Pt loading of the cathode was 0.15 mg Pt cm -2 . Fig. 5b shows the polarization curves for the two MEAs: the global performance of the MEA prepared with the Pt/carbon xerogel catalyst remains lower than that of the commercial electrode. However, since the cathodic catalytic layer prepared with the Pt/carbon xerogel catalyst contains much less Pt (0.15 mg Pt cm -2 ), the current should be normalized to the mass of Pt on the cathode (j m ) to compare the mass activity of the catalysts, and thus the utilization ratio of the precious metal. The results (not shown) indicate that both electrodes display quite similar performances in the so-called 'kinetic' region (j m < 1 kA g Pt -1 ), where the mass-transport limitations are negligible. As a consequence, the intrinsic mass activities of the Pt nanoparticles in these two electrodes are close, which points to no dramatic difference in the morphology of the Pt particles. On the contrary, in the mass-transport controlled region (j m > 1 kA g Pt -1 ), the Pt utilization is clearly higher in the case of the SEA catalyst supported on carbon xerogel. Such performance enhancement can be attributed to (i) the decrease of mass transport limitations and (ii) to the improvement of Pt-Nafion  contact, both inherent to the carbon texture.

CONCLUSION

Carbon xerogels are nanostructured carbon materials prepared by evaporative drying and pyrolysis of resorcinol-formaldehyde aqueous gels. These very clean carbon materials can advantageously replace carbon blacks as catalyst support for PEM fuel cell cathode, because their pore texture can be regulated so as to minimize mass transfer limitations within the catalytic layer. The pore size and void fraction of the

U cell (V)
catalyst support are determining in the mass transport phenomena, and both parameters can be tuned via the pristine gel composition and drying procedure.

Pt/carbon xerogel catalysts with high metal content can be synthesized via the 'Strong Electrostatic Adsorption' method. By repeating the impregnation-drying-reduction step with H 2 PtCl 6 as Pt precursor, it is possible to increase the catalyst metal content up to acceptable values (> 20 wt.%) while keeping a high metal dispersion (nanoparticles of homogeneous size, ca. 2 nm). However, the use of H 2 PtCl 6 , which is a very classical impregnation precursor, yields poisoning of the Pt catalysts by chlorine species which are quite difficult to remove completely. Even after reduction under H 2 at 450°C for 5 h, Cl is still detected via XPS peasurements and electrochemical methods. The presence of chlorine does not modify the intrinsic activity of the metal: the reaction mechanism and kinetics remain the same. However, the electroactive surface of the Pt particles decreases due to its blocking by chlorine species; this can dramatically reduce the Pt utilization ratio in the PEMFC catalytic layer. The reduction step is thus determining in the catalyst preparation.

Figure 1 .

 1 Figure 1. Morphology of carbon xerogels. SEM micrographs of carbon xerogels prepared at R/C = 500 (pH ~ 6.5) (a) and R/C = ∞ (pH ~ 4.0), i.e. without basification agent (b). Meso/macropore size distribution of carbon xerogels prepared at R/C = 750 ( ), 1000 ( ) and 2000 ( ), determined by mercury porosimetry.

Figure 2 .

 2 Figure 2. (a) TEM micrograph of a Pt/carbon xerogel catalyst and (b) particle size distribution obtained by image analysis. Sample prepared by SEA method, triple impregnation (22.3 wt.% Pt).

Figure 3 .

 3 Figure 3. (a) Relationship between the Cl/Pt ratio detected by XPS and the Pt active surface measured by CO stripping (first measurement) for Pt/carbon xerogel catalysts obtained via the SEA method (double impregnation, 15 wt.% Pt) and reduced at 200°C for 1 h (), 350°C for 3 h ( ) and 450°C for 5 h ( ). (b) Effect of the Cl poisoning on the performance of an H 2 /air cell: polarization curves at 70°C for MEAs with cathode processed with the same catalysts.

Figure 4 .Figure 5 .

 45 Figure 4. Structure of a PEM fuel cell electrode with carbon xerogel as catalyst support: the catalytic layer is composed of carbon gel micromonoliths made of a rigid 3D structure, insensitive to compression and with a defined pore texture. The Nafion  network and Pt particles are represented in light grey and black, respectively.

Table 1 .

 1 Physico-chemical and electrochemical characterization of Pt/carbon xerogel catalysts reduced under various conditions. The catalysts were prepared via the SEA method (double impregnation, 15.0 wt.% Pt). S CO-strip(1) and S CO-strip(7) represent the real surface area estimated by integrating the charge required to oxidize a CO monolayer after one/seven CO ads stripping, respectively.

		TEM	XPS	CO stripping	ORR
	Reduction conditions	d TEM	Cl/Pt	S CO-strip (1)	S CO-strip (7)	b	SA 90
		(nm)	(-)	(m² g Pt -1 ) (m² g Pt -1 )	(V dec -1 ) (µA cm² Pt -1 )
		± 0.2	± 10%	± 10%	± 10%	± 5%	± 5%
	200°C -1 h	1.8	0.33	37	69	-0.074	10
	350°C -3 h	1.8	0.23	61	87	-0.070	11
	450°C -5 h	1.8	0.07	129	142	-0.066	12

ACKNOWLEDGEMENTS

The authors wish to thank Dr Sophie Hermans, from the Institute of Condensed Matter of the Catholic University of Louvain (Belgium) for the XPS measurements.


M Ouattara-Brigaudet

S Berthon-Fabry
email: sandrine.berthon-fabry@mines-paristech.fr

C Beauger

M Chatenet

M Sennour

P Achard

Comparison of platinum deposit methods on carbon aerogels used in Proton Exchange Membrane Fuel Cells (PEMFC)

Keywords: carbon aerogel, platinum, Strong Electrostatic Adsorption, chemical reduction, UV

With the rarefaction and price increase of fossil fuels along with the consequences of greenhouse effect, many challenges have to be taken up. Consequently, a strong research effort is devoted to cleaner energy converters like fuel cells. In the car industry, Proton Exchange Membrane Fuel Cells (PEMFC) are chosen by a majority. But, remaining problems must be solved before a development at a large scale, among which: reducing the costs and increasing the power density and durability. Costs reduction mostly implies both diminishing the platinum quantity required for the oxygen reduction reaction at the cathode and increasing its activity. For these reasons, researches are devoted to the impact study of various methods of platinum deposit on the performances of new electrocatalysts and to the understanding of phenomena occurring in fuel cells.

Nowadays, state-of-the-art PEMFC electrodes supports are made of carbon blacks. However, these carbons (and as a consequence the catalytic layers) do not have a controlled texture. As a result, it is hard to understand the diffusive phenomena limiting electrochemical performances. By contrast, carbon aerogels present a controllable texture and are thus suitable PEMFC electrodes catalysts supports [1]: they conduct electrons and are permeable to reactant gases. In this study, we compare four platinum deposit methods in order to improve the catalytic activity and the platinum active surface area in Membrane Electrode Assembly (MEA) by reducing the particle size and improving the particles dispersion.

The reference method consists in a platinum impregnation by H 2 PtCl 6 followed by a chemical reduction in NaBH 4 and a thermal reduction in hydrogen. Such a method (referred as reference method) leads to large particles not-well dispersed (Fig. 1a). To limit the particle growth, we filtered the impregnated carbon solution and performed simply a chemical reduction in NaBH 4 (referred as controlled reduction method, Fig 1b). Then we tested the so-called "Strong Electrostatic Adsorption" method (referred as SEA method). The latter consists of maximizing electrostatic interactions between the platinum salts and the carbon support. The SEA method leads to small (2 nm) and well-dispersed platinum particles (Fig. 1c). Finally, we applied an UV reduction on platinum impregnated carbon (referred to as UV reduction method). This method leads to such small particles (Fig. 1d) and low Pt loading that we did not evaluate it in MEA.

The three remaining electrocatalysts were electrochemically characterized in rotating disk electrode and on a single fuel cell bench (Fig. 2). The characterizations showed that decreasing the particle size and improving their dispersion does not necessarily yield to good performance (SEA method in Fig. 2). This phenomenon was attributed to chloride pollution [3]: chloride ions adsorbed on platinum indeed block the active sites and modify the oxygen reduction reaction mechanism (2 electrons mechanism instead of a 4 electrons mechanism). Such chloride pollution is very sensitive with small platinum particles and less sensitive as the particle size increase (reference method and controlled reduction method in Fig. 2).

curves at 70°C obtained for the electrocatalysts used in MEA cathodes.

) controlled reduction method, (▲) SEA method.


Rémy Wyss

Frédéric Boniol

Julien Forget

Claire Pagetti

A synchronous language with partial delay specification for real-time systems programming

High-level formal programming languages require system designers to provide a very precise description of the system during early development phases, which may in some cases lead to arbitrary choices (i.e. the designer "overspecifies" the system). In this paper, we propose an extension of synchronous dataflow languages where the designer can specify that he does not care whether some communication is immediate or delayed. It is then up to the compiler to choose where to introduce delays, in a way that breaks causality cycles and satisfies latency requirements imposed on the system.

Introduction

Context. Implementing real-time critical systems is an increasingly complex process that calls for high-level formal programming languages. In this paper, we focus on synchronous languages [START_REF] Benveniste | The synchronous languages 12 years later[END_REF], such as Lustre [START_REF] Halbwachs | Programming and verifying real-time systems by means of the synchronous data-flow language lustre[END_REF] and its commercial version Scade [START_REF] Dormoy | Scade 6 a model based solution for safety critical software development[END_REF], which have successfully been adopted for the formal specification of control systems. These languages are based on the synchronous paradigm, where the behaviour of a program is seen as a sequence of reactions: (1) each reaction consists in reading the current inputs, computing the current outputs and updating the internal state of the system; (2) each reaction occurs in zero logical time (we do not care about when computations occur during a reaction). Relying on such a language imposes very early in the development process to specify a completely deterministic system, while in some specific cases the designer might want to leave some degree of liberty in the specification. This paper details how to avoid such overspecification.

Non deterministic communication specification. Let us consider the simplified mono-periodic flight control system depicted in the Figure 1. It consists of a set of avionics functions, which acquire information on the state of the aircraft and on the pilot orders, and which objective is to control the position, speed and attitude of the vehicle thanks to its control surfaces. The right part of the figure depicts the control of the ailerons while the left part depicts the control of the elevators. Each vertex depicts a function. Edges depict data-communications between functions and are of two different kinds. Plain arrows stand for immediate communications, which induce a precedence constraint from the producer to the consumer. Dashed arrows stand for less constrained communications that do not induce precedence constraints. We illustrate this distinction below.

The variable a_angle stands for the current angle of the aileron and is acquired by the function AAF (Aileron angle filter). This function consolidates the data and sends the variable o_a_angle (the observed angle) to the function AL (Aileron law). AL controls the aileron and maintains the required angle r_a_angle. According to the observed angle and the required angle, it sends an order a_order that enables to reach safely the required angle. Thus, the differential equations that command the aileron surface are implemented by the data-flow L 1 = a_angle → o_a_angle → a_order. Such a computation path, from a sensor acquisition to an actuator order is called a functional chain. In this case, L 1 corresponds to the discretisation of a command law and functions must be applied strictly sequentially for the computation to be correct. The elevator law behaves similarly.

The control laws of the ailerons and of the elevators communicate through the functions LtL and LgL, in order to verify that the orders sent to the different actuators (ailerons and elevators) are consistent. This consolidation is however less stringent than the command described in L 1 , therefore longer latencies in the communication can be supported. As a result, communications between such functions do not impose strict precedence constraints and a function is allowed to compute using data produced by another function during the previous reaction instead of the current reaction (delayed communication). Still, the comparison and consolidation must be done on sufficiently "fresh" data. Thus, the number of delayed communications that the functional chain L 2 = z_acc → o_z_acc → d2 → r_a_angle → a_order can tolerate is bounded by a maximum latency constraint.

The last part of the system, the guidance law (GL), computes a series of accelerations to apply in order to reach a position ordered by the pilot. This is described by the chain L 3 = p_order → r_lt_acc → r_a_angle → a_order. This function is temporally less constrained since the required position is reached only after several execution steps (several reactions). The function could even be implemented as a function executed less often than every logical instant. Thus, communications between GL and other functions are flexible. This illustrates two cases where the communication specification should remain non deterministic (unspecified): (1) when loosely coupled control laws communicate, (2) when there is a global latency imposed over a functional chain; local delays between each component of the chain are not explicitly required and may remain unspecified by the designer, provided that at run time the global end-to-end latency is satisfied.

Allowing such a liberty in the way functions communicate eases the design of large systems that are typically made up of several thousand components (for instance, a flight control system is made up of about 5.000 functional nodes). In such a system, specifying the temporal semantics of all the communications (more than 20.000 in a flight control system) is not humanly reasonable. A better solution would be to let designers specify only for critical communications and to leave the rest unspecified, meaning that he "does not care" whether the communications are immediate or delayed. The second advantage of this liberty is to ease the scheduling as it allows for more parallelism, in particular when the system is implemented on a distributed platform.

Contribution. With existing synchronous languages, the designer must explicitely choose between immediate and delayed communications, even for flexible communications. In this paper we detail how to transform this manual choice into an automated choice included in the compilation process. Notice that we still allow a system to contain explicitly immediate or delayed communications (for instance to memorize the current state of the system requires a delay). The new type of flexible communications comes as an additionnal mechanism, not as a replacement for either immediate or delayed communications.

We define a synchronous language with partial delay specification that provides a higher degree of flexibility during the design phase. We introduce a new operator called "don't care" to specify communications that are allowed to be either immediate or delayed. The semantics of the language is defined formally with a Kahn's semantics in section 2. A program with "don't care" operators is partially non deterministic as it accepts several different behaviours. The language also enables to impose latency constraints expressed as bounds on the number of delays involved in functional chains.

Though the initial specification is non deterministic, we want to generate completely deterministic code in the end, as we are interested in highly critical systems. We propose to translate a program with "don't care" operators into a standard synchronous program that respects the latency requirements imposed on the functional chains and that is causal (meaning that there is no cycle without delay). We have chosen a deterministic syntactic translation (section 3), which either simply drops a "don't care" operator or replaces it by a classic delay operator (the pre/fby of Lustre/Lucid Synchrone [START_REF] Halbwachs | Programming and verifying real-time systems by means of the synchronous data-flow language lustre[END_REF][START_REF] Pouzet | Lucid Synchrone, version 3. Tutorial and reference manual[END_REF]). We show that finding a valid translation (choosing where to keep delays) is equivalent to solving a set of pseudo-Boolean constraints and can thus be solved using existing techniques for this widely studied problem. Related work. Real-time embedded code is often implemented as a set of threads scheduled concurrently by a scheduling policy [START_REF] Cottet | Scheduling in real-time systems[END_REF]. These policies focus on ensuring the respect of temporal constraints and do not consider functional determinism as tasks are assumed to be completely independent. We might say that the system behaves as if all data-flows were tagged with a "don't care". There is however an important difference with our language: two different executions of the same system may have different functional behaviours due to timing variations (if a task executes for less than its worst-case execution time for instance). Precedence constraints can be imposed on tasks imposing direct communication and thus ensuring an order between tasks, however we lose the flexibility of the "don't care".

Architecture Description Languages such Aadl (Architecture and Analysis Design Language) [START_REF] Peter | The architecture analysis & design language (AADL): An introduction[END_REF], Marte (Modeling and Analysis of Real-time and Embedded systems) [START_REF] Omg | A UML profile for MARTE[END_REF] or Sysml (System Modeling Language) [START_REF]Systems modeling language[END_REF] enable to specify detailled communication patterns between functional components. In Aadl, data communications are either immediate or delayed. Immediate connections impose a precedence constraint from the producer to the consumer of the data, while delayed communications do not. End-to-end latency constraints can also be imposed on flows (a flow is a path through sub-components of a component). However, the patterns are always fully deterministic and no mechanism allows to handle "don't care" communications. The CCSL language [START_REF] Mallet | The clock constraint specification language for building timed causality models[END_REF] used in Marte is closer to our work. It enables to specify clock constraints, that is to say constraints on the relation between the activation rates of the different operations of the system. This can yield several different instanciated systems that satisfy the constraints.

In [START_REF] O'neil | Optimal scheduling of data-flow graphs using extended retiming[END_REF] and [START_REF] Leiserson | Optimizing synchronous systems[END_REF], the authors introduce a methodology to optimise the computation time of synchronous circuits. For a given deterministic specification, the method rewrites the specification into a functionally equivalent one by modifying the equations. To this intent, a synchronous program is represented as a graph where the vertices are functional units and the edges represents the communication between two functional units. The edges are tagged with an integer which represents the number of delay registers required for the communication. The idea of the methodology, called retiming, is to apply graph transformations which insert and remove delays.

In [START_REF] Maraninchi | Compositional semantics of nondeterministic synchronous languages[END_REF], the authors define a non deterministic language based on Input/Output Boolean Automata. The semantics of a non deterministic program is defined as the set of deterministic programs which behaviour is included in the non deterministic ones. This language has a higher expressive power than our data-flow language. The authors then define the product of non deterministic specifications. To convert a non deterministic specification into a deterministic one, the designer needs to define an "oracle" and synchronise the program with this oracle. How to define an oracle is out of the scope of the paper.

A synchronous language with partial delay specification

In this section, we extend synchronous data-flow languages with the ability to have partial delay specifications using a new "don't care" operator.

Syntax

We define the syntax of a very simple first-order synchronous data-flow language. The language is meant as a proof-of-concept and those concepts should later be included in a larger, more realistic language. The grammar is the following:

syst ::= n_list;
node N (io) returns (io) [ var io; req_list; ] let eqs tel n_list ::= imported node N(io) returns (io)

| imported node N(io) returns (io); n_list io ::= id | io, id eqs ::= eq | eqs eq eq ::= io = exp;

exp ::= id | cst | dop(id, . . . , id) | cst fby id | cst dc id A program (syst)
is made up of a list of imported nodes (n_list) and a unique main node which assembles the set of imported nodes. Imported nodes are black boxes (programmed with other existing languages) that have no side effects on the rest of the program. The program takes a set of inputs, produces a set of outputs and can use local variables. All of these are described by io. It is possible to specify a set of requirements (req_list). This will be explained in section 2.3. The assembly of imported nodes is described as a set of equations (eqs). An equation computes a list of local or output flows using a flow expression (expr ). A flow expression can be a flow variable (id ), a constant (cst), the application of an imported node (dop) on flows, the application of the fby operator (the delay operator of Lucid Synchrone [START_REF] Pouzet | Lucid Synchrone, version 3. Tutorial and reference manual[END_REF]) on a flow. This "followed by" operator introduces a delay of one reaction between its input and its output flow (parameter cst is the initialization value for the first reaction, as it has no previous value). Finally an expression can be the application of the new "partial delay" operator dc (called "don't care") on a flow. The equation x = cst dc x ′ can correspond to either x = x ′ or x = cst fby x ′ and thus introduces some non determinism. In the first case, the communication between x ′ and x is immediate and in the second it is delayed. Again, the operator dc can only be applied to identifiers and not to expressions in order to simplify our presentation. Notice that programs contain no hierarchy (no nodes decomposed into other non-imported nodes). Modular compilation/analysis is out of the scope of this paper. At the beginning of the code we declare 9 imported nodes, one for each functional block (we only show 3 declarations here for more conciseness). After that we define the node F CS which takes 4 inputs (a_angle, y_acc, e_angle and z_acc) and returns 2 outputs (a_order and e_order). We also declare a set of local variables which correspond to the variables exchanged between the nodes. The set of equations between let and tel defines how outputs and local variables are computed from inputs and how imported nodes communicate. To specify the "don't care" communications accordingly to the syntax, we add 6 auxiliary variables (dc1 to dc6).

Since the language does not include over-sampling or sub-sampling operators (such as when or current), all the flows are on the same clock (the base logical time). Therefore we do not provide any clock calculus. Mixing sampling operators and "don't care" will be studied in future work. All the flows are well initialised because the delay operator (fby) includes an initialisation value.

Kahn's semantics

We provide a Kahn's semantics [START_REF] Kahn | The semantics of simple language for parallel programming[END_REF] for our language, which details the sequence of values corresponding to flow expressions. We introduce the following grammar to represent such sequences:

E ::= {x 1 , . . . , x n } s ::= E.s
E is a set of values. E.s denotes the sequence whose head value is non deterministically chosen among the values in E and whose tail is s. We abusively write v.s instead of {v}.s to denote a flow whose first value is deterministic. Finally, we define:

< E 1 .s 1 | . . . |E n .s n >= ∪ 1≤i≤n E i . < s 1 | . . . |s n >
For any operator ⋄, ⋄ # (p 1 , ..., p n ) = s means that the operator ⋄ applied to parameters p 1 , ..., p n produces the sequence s. Let

n i=1 E i = E 1 × . .
. × E n denote the cartesian product of the sets E i . The semantics of flow expressions is given with:

cst # = cst.cst # imp # (E 1 .s 1 , . . . , E m .s m ) = ∪ t∈ m i=1 Ei {imp(t)}.imp # (s 1 , . . . , s m ) fby # (cst, s) = cst.s # dc # (cst, s) = < fby # (cst, s)|s # > 1.
The first rule describes the constant: it simply produces a flow that always has the same value.

2. The second rule is the call of an imported node. At each step of the sequence, we may take as input for the node any combination of the non deterministic values of its inputs (any tuple in the cartesian product of the possible head values of each input) and then we apply the imported node to each combination. In other words, we simply apply an imported node point-by-point on the sequence of values of its inputs. 3. The third rule is for the fby operator. It simply concatenates the initialisation value to the flow, thus delaying each value of the input flow by one reaction. 4. The last rule is for the dc operator. It introduces non-determinism by stating that the dc operator can either be replaced by a fby or by the identity.

Example 2. We illustrate the semantics in an example where the imported node plus simply computes the addition of the two inputs.

Latency requirements

Let x 0 -→ x ′ denote that the variable x ′ immediately depends on the variable x. Similarly, x 1 -→ x ′ denotes a delayed dependency and x

? -→ x ′ a "don't care" dependency. Let x → x ′ def ⇔ x 0 -→ x ′ ∨ x 1 -→ x ′ ∨ x ? -→ x ′ .
Let Var 0 (e) denote the variables that appear free in e and not as an argument of a fby or a dc, Var 1 (e) those that are an argument of a fby and Var ? (e) those argument of a dc. Given a program p and c ∈ {0, 1, ?}, we have x c -→ x ′ in p iff there is an equation io = e in p such that x ′ ∈ io and x ∈ Var c (e).

Definition 1 (Functional chain). A functional chain (x 1 , . . . , x n ) is a list of flow variables such that ∀1 ≤ i < n, x i → x i+1 . Example 3. Let us consider again the program ex of example 2. There are two chains from the input i to the output o:

L = (i, v 1 , v 2 , o) and L ′ = (i, v 1 , o).
The latency of a functional chain is the number of delays of the chain. Latency constraints impose a bound on this number and are in most cases maximum latency constraints, i.e. constraints of the form Lat(x 1 . . . x n ) < k, where k ∈ N ⋆ and (x 1 . . . x n ) is a functional chain. Our approach can however support constraints where < is replaced by any other comparison operator. In a program, latency constraints are specified using the keyword req.

Example 4. The flight control system specified in example 1 contains several chains. The requirements on those mentioned in the introduction are: req ( z_acc , o_z_acc , d2 , dc2 , r_a_angle , a_order ) < 1; --L2 req ( p_order , r_lt_acc , dc6 , r_a_angle , a_order ) < 4; --L3

Concretisation of an abstract program

We propose a compilation scheme in two steps: a) Translate the specification into a standard deterministic synchronous data-flow program; b) Apply a synchronous compiler. The second step is well studied [START_REF] Halbwachs | Generating efficient code from data-flow programs[END_REF] and is out of the scope of this paper. This section describes the first step, which consists in choosing one program among the different deterministic synchronous programs which semantics is included in the semantics of the original non deterministic program. The compiler performs a purely syntactic translation that replaces each "don't care" operator either by a direct communication or by a delayed communication.

Instance space

Non deterministic programs are called abstract programs, while deterministic ones are called concrete programs. Definition 2. A system (or a program) is said concrete if and only if it contains no dc operations, otherwise it is abstract.

Example 5. The abstract program ex given in example 2 corresponds to several concrete versions. If the "don't care" operator is syntactically translated into either the identity or the fby operator, there are 2 solutions (ex1 and ex2). A more complex solution (not supported in our approach) would be to interleave direct and delayed communications (for instance, ex3). Let sys denote an abstract system. Let dc(sys) = {dc 1 , . . . , dc n } denote the ordered set of dc operators in sys (we take the chronological apparition order of the operators in the set of equations). Let p = (dc i → fby)sys denote the program p resulting of the substitution of operator dc i by a fby operator in sys. Similarly, (dc i → id)sys denotes the substitution of dc i by the identity operator and (dc x → op, ..., dc y → op)sys denotes the program resulting of the set of substitutions dc x → op, ..., dc y → op (where op is either fby or the identity).

Definition 3 (Instance).

Let p be a concrete system and sys be an abstract program such that dc(sys) = {dc 1 , . . . , dc n }. p is an instance of sys iff there exists a set of substitutions dc 1 → op 1 , ..., dc n → op n such that:

p = (dc 1 → op 1 , ..., dc n → op n )sys
In the following, sys[b 1 , . . . , b n ] denotes the instance p = (sub 1 , . . . , sub n )sys such that:

sub i = dc i → id if b i = 0 sub i = dc i → fby if b i = 1
Example 6. The program ex has two instances as shown in example 5, with ex1=ex[0] and ex2=ex [START_REF] Benveniste | The synchronous languages 12 years later[END_REF].

Let us denote by I(sys) the set of instances of the system sys(dc 1 , . . . , dc n ). We define the relation ⊑ sys between instances of sys as follows: This is a very classical example of a Boolean lattice. We use a Hasse diagram to represent the lattice (I(sys), ⊑ sys ). In such a diagram, each element of I(sys) is a vertex and there is an upward edge from s to s ′ whenever s ⊑ s ′ and there is no s ′′ such that s ⊑ s ′′ ⊑ s ′ . Notice that (I(sys), ⊑ sys ) is a n-dimensional hypercube.

Example 7. The instance space of the simplified flight control system F CS(dc1, dc2, dc3, dc4, dc5, dc6) is described by the 6-dimensional hypercube:

Valid instance space

Only a subset of the instances of an abstract program are valid. We say that an instance p of sys is valid if and only if 1) p is causal and 2) p satisfies all the latency requirements of the system. Part 1) ensures that the instance is implementable (by checking that the instance does not contain an data-dependency cycle). However, not all implementable instances satisfy latency requirements, thus we also need to check 2).

Respecting latency requirements. Let us first define formally the latency of a functional chain. Definition 5. Let sys be a system and (x 1 , . . . , x n ) be a functional chain of sys. The latency of the chain in sys is defined inductively as:

Lat sys (x 1 , . . . , x n ) = 1 + Lat sys (x 1 , . . . , x n-1 ) if x n-1 1 -→ x n Lat sys (x 1 , . . . , x n-1 ) if x n-1 0 -→ x n or x n-1 ? -→ x n
with Lat sys () = 0, where () is the empty functional chain.

Example 8. For program ex and the chain

L = (i, v 1 , v 2 , o), Lat ex (L) = Lat ex1 (L) = 1 and Lat ex2 (L) = 2.
We say that dc i is involved in C if there exists two variables x, x ′ in C such that x ? -→ x ′ and dc i is the dc operator between x and x ′ . The following proposition details how the latency of a chain is computed for a given instance. Proposition 2. Let sys(dc 1 , . . . , dc n ) be an abstract system, let C be a functional chain of sys and let p = sys[b 1 , . . . , b n ] be an instance of sys. We have

1. Lat p (C) = l j=1 b ij + Lat sys (C)
, where the operators dc ij are those involved in C, l ≤ n and for all i j , 1

≤ i j ≤ n. 2. If p ′ is another instance such that p ⊑ p ′ : Lat p (C) < k =⇒ Lat p ′ (C) < k
This proposition allows us to partition the instance space into two sets: the instances satisfying the requirements and those which do not.

Example 9. The flight control system Figure 1 has to satisfy the requirement R = Lat(z_acc, o_z_acc, d2, dc2, r_a_angle, a_order) < 1. The partitioning is depicted below. A program is causal if it does not contain instantaneous data-dependency cycles. A non-causal program must be rejected because we cannot find a computation order that satisfies all data-dependencies. As a consequence, in a concrete program data-dependency cycles are allowed only if they contain a fby.

Definition 6. The functional chain C = (x 1 , . . . , x n , x 1 ) is a dc-cycle iff: ∃i, 1 ≤ i ≤ n, x i ? -→ x (i mod n)+1
Example 10. The following program contains a cycle where a dc is involved:

imported node n1 ( i1 , i2 ) returns ( o ); node causal ( i ) returns ( o ) var v1 ; l e t o = n1 (i , v1 ); v1 = 0 dc o ; t e l i o v 1 (o, v 1 , o) is a dc-cycle causal[0] is not causal, while causal[1] is.
Definition 7. Let sys(dc 1 , . . . , dc n ) be an abstract system. Proof. If p ⊑ p ′ , for all equations io = e, we have Var p ′ 1 (e) ⊆ Var p 1 (e). Thus, the dependency graph of p is a sub graph of the one of p ′ . If p ′ is causal, it means that the dependency graph of p ′ is acyclic and so is any subgraph.

As a consequence, the Hasse diagram of a system can be partitioned into two sets: a "south" partition which contains the causal instances of sys and a "north" partition which contains the non causal instances of sys.

Example 12. If we consider again the flight control system Figure 1, the graph of instances of this system can be partitioned as shown below. As a result, the set of valid instances of the abstract program is the intersection of the causal instances with the black instances in figure of If a cycle is a dc-cycle, it is possible to find an instance p where this cycle is broken by replacing one of the dc operations in the cycle by a fby. If a cycle is not a dc-cycle the program is not causal. The following property shows that causality can be treated as additional latency requirements that must be satisfied by valid instances: Proposition 5. Let sys be an abstract system, p be an instance of sys, C = (x 1 , . . . , x n , x 1 ) be a dc-cycle in sys:

C is a cycle in p ⇔ Lat p (C) = 0.

Generation of valid instances

Finding a valid instance p of sys(dc 1 , . . . , dc n ) consists in finding a valuation sys[b 1 , . . . , b n ] which satisfies the latency constraints explicitly specified in the node definition and the constraints generated by the causality analysis. If there exists several solutions, we arbitrarily choose one among them (there is no notion of "better" solution). In this section, we show that we can solve this problem by translating it into a pseudo-Boolean problem, which enables us to reuse existing solvers, such as SAT4J [START_REF] Berre | The sat4j library, release 2.2 system description[END_REF] for instance.

Let sys be a system with several latency requirements of the form L = Lat(C) ∼ k (where ∼∈ {<, >}). According to proposition 2, an instance p of sys satisfies L if and only if:

l j=1 b ij ∼ k -Lat sys (C)
where dc ij are the dc operators involved in the chain (x i1 , . . . , x i l ) and b ij ∈ {0, 1}. Thus, the set of latency constraints can be translated into a conjunction of linear pseudo-Boolean constraints of this form. The variables of the pseudo-Boolean problem are the b ij and k -Lat sys (C) can be considered as a constant as it does not depend on instance p.

The causality analysis can also be translated into pseudo-Boolean constraints. We enumerate the elementary cycles of the form C = (x i1 , . . . , x im , x i1 ) of the data-dependency graph of sys using a classic cycle detection algorithm such as that of Tarjan [START_REF] Endre | Enumeration of the elementary circuits of a directed graph[END_REF]. According to proposition 5, a cycle C will be avoided (broken) if and only if: The set of constraints is b1 + b2 + 1 < 3 b1 > 0

Implementation

To implement the valid instance search, we could proceed as follows:

1. Translate latency constraints into pseudo-Boolean (PB) constraints; 2. For each cycle, add a PB constraint to break the cycle; 3. Solve the whole set of PB constraints.

However, the enumeration of the cycles of a graph is a problem with exponential time-complexity (even though the complexity of Tarjan's algorithm is close to polynomial when the number of cycles is small). Thus, instead we use an iterative process, described in Algorithm 1: we ask the PB-solver for a solution, if the solution is non-causal we add a PB constraint to break a cycle and iterate. With this solution, we do not enumerate all cycles, because breaking one cycle often breaks several other cycles. Experiments suggest that we actually only perform a polynomial number of iterations (even in worst cases), but this remains a conjecture that needs to be proved in future works.

Algorithm 1 Implementation of the valid instance search

Translate latency constraints into pseudo-Boolean constraints. Check the causality for non-dc cycles only 1 . while The PB-solver finds a solution to the constraints do if The solution is not-causal then Add a PB constraint to break the first cycle we find else

We have found a valid instance, return the solution. end if end while

We have implemented an OCaml prototype, which translates a specification with partial delays into a valid synchronous program. The compilation process is shown in Figure 2. The compiler first takes an abstract program and generates the corresponding pseudo-Boolean problem. The problem is then solved using the solver SAT4J [START_REF] Berre | The sat4j library, release 2.2 system description[END_REF]. There may be several iterations between the solver and the compiler so that the compiler checks the causality of the solution returned by the solver. Finally, the compiler produces the valid instance corresponding to the final solution returned by the solver. We have experimented the compiler on several examples and in particular an avionic application similar to the one presented in [START_REF] Boniol | A framework for distributing real-time functions[END_REF]. It is made up of 3994 imported nodes and 16186 variables. We made the experiments by duplicating all the variables with a "don't care" variable. If we do not specify any latency requirements, the compiler produces the trivial solution where all dc are replaced by a fby. We then generate some latency requirements to have an overview of the performance of the compiler. The time needed to parse the file is about 1 second. The experiments were made on a Linux machine with 4 GB of memory. We make 10 different benchmarks on each point. These first results are very promising because they show that the method scales well on a representative case study. In this paper we have presented an extension of a synchronous data-flow language with a new operator (dc), which enables to specify communications that can either be immediate or delayed. We also introduced the possibility to specify latency requirements. We have detailled how a high level specification containing dc can be translated into a classic synchronous program without dc, taking latency and causality constraints into account.

There are several open questions and future works. First, experiments show that we should ease the specification of latency requirement. For instance we could introduce some kind of pattern matching, e.g. to compute all functional chains matching with (i,*,v,*,o).

Second, we need to study the problem complexity when considering only latency requirements of the form Lat(C) ≤ k. In that case, we have a conjection of slighly less general constraints of the form Σa j ≤ k and Σa j > 0.

The third perspective concerns the extension with sampling operators. If we define the exact latency of a functionnal chain (x 1 , . . . , x m ) as the maximum number of reactions before the value of x m actually depends on x 1 , then sampling operators have an impact on this latency. Indeed, applying sampling operators (such as the when/current operators of Lustre) on a delayed flow can increase the delay of the flow, thus increasing the latency of the chains it belongs to. The effect of general Boolean sampling operators on latencies is hard to analyse: latencies may fluctuate with the sampling condition and even be unpredictable if the condition is an input flow. Instead, we could focus on more restrictive sampling operators that can be analysed more efficiently, such as the strictly

Fig. 1 .

 1 Fig. 1. A simplified flight control system

Example 1 .

 1 Let us illustrate our syntax with the textual version of the flight control system of Figure1. imported node AL ( i1 , i2 ) returns ( o ); imported node EL ( i1 , i2 ) returns ( o ); imported node GL ( i1 , i2 , i3 ) returns ( o1 , o2 ); ... node FCS ( a_angle , y_acc , e_angle , z_acc , p_order ) returns ( a_order , e_order ) var o_e_angle , o_a_angle , r_a_angle , o_y_acc , r_e_angle , o_z_acc , lg_fb , r_lg_acc , d1 , d2 , r_lt_acc , lt_fb , dc1 , dc2 , dc3 , dc4 , dc5 , dc6 ; l e t o_a_angle = AAF ( a_angle ); o_y_acc = YAF ( y_acc ); o_z_acc = ZAF ( z_acc ); o_e_angle = EAF ( e_angle ); o_z_acc = ZAF ( z_acc ); o_e_angle = EAF ( e_angle ); ( lg_fb , d2 , r_e_angle ) = LgL ( dc1 , o_z_acc , dc4 ); ( r_a_angle , lt_fb , d1 ) = LtL ( dc2 , o_y_acc , dc6 ); ( r_lt_acc , r_lg_acc ) = GL ( dc3 , dc5 , p_order ); a_order = AL ( o_a_angle , r_a_angle ); e_order = EL ( r_e_angle , o_e_angle ); dc1 = 0 dc d1 ; dc2 = 0 dc d2 ; dc3 = 1 dc lt_fb ; dc4 = 0 dc r_lg_acc ; dc5 = 1 dc lg_fb ; dc6 = 0 dc r_lt_acc ; t e l

  node ex1 ( i ) returns ( o ) var v1 , v2 ; l e t v1 = i ; v2 = 1 fby v1 ; o = plus ( v1 , v2 ); t e l node ex2 ( i ) returns ( o ) var v1 , v2 ; l e t v1 = 0 fby i ; v2 = 1 fby v1 ; o = plus ( v1 , v2 ); t e l node ex3 ( i ) returns ( o ) var v1 , v2 , j ; l e t j = true fby ( not j ); v1 = i f j then i e l s e (0 fby i ); v2 = 1 fby v1 ; o = plus ( v1 , v2 ); t e l

Definition 4 .

 4 Let p = sys[n 1 , . . . , n m ] and p ′ = sys[n ′ 1 , . . . , n ′ m ] be two instances of sys:p ⊑ sys p ′ def ⇐⇒ ∀i ≤ m, n ′ i ≤ n iIn other words, dc communications are "more immediate" in p ′ than in p. Proposition 1. (I(sys), ⊑ sys ) is a finite lattice in which the top element is sys[0, . . . , 0] (all dc communications are immediate) and the bottom element is sys[1, . . . , 1] (all dc communications are delayed).

bExample 13 .

 13 ij + Lat sys (x i1 , . . . , x im , x i1 ) > 0 Let us consider the following program: node trad ( i ) returns ( o1 , o2 ) req (i , v1 , v2 , v3 , o2 ) < 3; var v1 , v2 , v3 ; l e t o1 = n1 (i , v1 ); v1 = 0 dc o1 ; --dc1 v2 = 0 dc v1 ; --dc2 v3 = 0 fby v2 ; o2 = n2 ( v2 ); t e l

Fig. 2 .

 2 Fig. 2. The compilation process

  1. sys is strongly causal if all its instances are causal. 2. sys is weakly causal if sys admits at least one causal instance. 3. sys is non-causal if it admits no causal instance. Example 11. The program ex of example 2 is strongly causal since there is no cycle in the data dependency graph. causal of example 10 is weakly causal. Proposition 3. Let sys(dc 1 , . . . , dc n ) be an abstract system, 1. If sys is strongly causal, then sys is also weakly causal. 2. sys is strongly causal if and only if sys[0, . . . , 0] is causal. 3. sys is weakly causal if and only if sys[1, . . . , 1] is causal.Proposition 4. Let sys(dc 1 , . . . , dc n ) be an abstract system. Let p and p ′ be two instances of sys such that p ⊑ p ′ . Then if p ′ is causal, so is p.

  example 9. There are 4 valid instances: 101111, 101011, 101010, 101101.

		not causal					000000
				100000	010000		000100	000010	000001
		. . .	100100	010100	001100	100010	010010	001010	000110	100001	. . .
	. . .	111000	110100	011100	110010	101010	011010	001110	101001	011001	010101	. . .
		. . .	011011	101011	110011	011101	101101	110101	111001	011110	. . .
		011111	101111	110111			111011	111101		111110
		causal					111111

Acknowledgment

The authors would like to thank Jean-Louis Colaço for his careful analysis and help for improving this work.

periodic clock sampling operators of Prelude [START_REF] Pagetti | Multi-task implementation of multi-periodic synchronous programs[END_REF]. On the contrary to Boolean sampling operators, latencies should be constant and computable fully statically.