Keywords: Axial flux machine, Additive manufacturing, Permanent magnet motor, Wind power generation

An ironless axial flux wind turbine motor is presented in this paper. The aim of this paper is to propose a motor that can be manufactured from simple components: magnets, copper and plastic. The motor must be feasible even in remote areas where machining facilities are limited. The winding and mechanical supports are sized from the magnets. The motor is therefore designed to be simple to reproduce and affordable in terms of manufacturing costs. Two rows of magnets are used to improve the performance of the motor. During design, choices on dimensions were made with fast calculations of output performance using models developed specifically for ironless motors. The performance measured on the prototype is in perfect agreement with the finite element simulations and the proposed models.

I. INTRODUCTION

ENEWABLE energies are very interesting sources of energy for isolated areas. It allows these distant areas to charge batteries and then to provide them electricity ready to use. WindAid [1] aims to allow remote areas of Peru to generate their own electrical energy. The targeted zones are very windy, so the creation of a complete wind turbine is planned with the possibility of manufacturing it on site. All components of the wind turbine and its electrical connection shall be manufactured, assembled and/or purchased locally. In this context, a motor is presented in this article to meet these needs.

Axial Flux Permanent Magnet Motors (AFPM) have already been used for power generation from wind turbines. The interest of these machines is that they generally have a higher power density than their radial flux equivalent [START_REF] Parviainen | Axial flux permanent magnet generator with concentrated winding for small wind power applications[END_REF]. AFPMs are also interesting because they can be used in direct connection to the wind turbine [START_REF] Ferreira | Prototype of an axial flux permanent magnet generator for wind energy systems applications[END_REF] which limits the losses by removing the gear box.

Different topologies of axial flux motors exist depending on the number of rotor and stator used. A structure with two rotors and one stator is preferred to maximize the magnetic field on the coils. In this structure, the iron in the stator is not mandatory [START_REF] Price | Design and testing of a permanent magnet axial flux wind power generator[END_REF]. Still on this structure, it is possible to use Halbach array magnets [START_REF] Subotic | Weight Optimization of Coreless Axial-Flux PM Machines[END_REF]. This allows the magnetic fields on the stator to be canalized even further. The flux lines of the magnets intrinsic to this structure make iron optional on the rotors. However, the cost and difficulties in assembling these magnets make this technology difficult to consider for a motor manufactured in a remote area. A structure with two stators and one rotor is chosen to limit the mechanical stresses on the rotor, to facilitate the cooling of the stators and to ensure continuity of operation even with a damaged stator [START_REF] Djebarri | Design and performance analysis of double stator axial flux PM generator for rim driven marine current turbines[END_REF]. In this structure, the rotor can be ironless while keeping very good performance [START_REF] Javadi | Design and analysis of 42-V coreless axial-flux permanent-magnet generators for automotive applications[END_REF].

The black spot of AFPM is the manufacturing of the iron lamination of the ferromagnetic sheets [START_REF] Gieras | Axial flux permanent magnet brushless machines[END_REF]. The present topologies allow the removal of iron but still have it on one of their parts. The YASA topology is an interesting alternative [START_REF] Woolmer | Analysis of the yokeless and segmented armature machine[END_REF] but remains difficult to manufacture locally in remote areas. Ironless motors are the simplest to manufacture because they do not require laminations or Soft Magnetic Composites (SMC) [START_REF] Bonnet | 3D magnetic field model of a permanent magnet ironless axial flux motor with additively manufactured nonactive parts[END_REF]. However, this motor has lower performances due to the non-canalization of the magnetic field. To have interesting performances, the air gap must be as small as possible. In the topology with two rotors and a central stator, depending on the number of winding layers, the air gap can be increased [START_REF] Yao | Novel design of a coreless axial-flux permanent-magnet generator with three-layer winding coil for small wind turbines[END_REF]. The structure with two stators and one rotor is therefore preferred. This also limits the mechanical attraction forces between two rotors.

On AFPM, several shapes of magnets can be used. This will have an impact on the performance and shape of the electromotive forces (EMFs) [START_REF] Radwan-Praglowska | Impact of permanent magnets shape and arrangement for selected parameters in coreless axial flux generator[END_REF]. Tile-shaped magnets are most often used to maximize the area of magnet covering the energized conductors [START_REF] Radwan-Praglowska | Impact of permanent magnets shape and arrangement for selected parameters in coreless axial flux generator[END_REF]. However, parallelepiped magnets [START_REF] Subotic | Weight Optimization of Coreless Axial-Flux PM Machines[END_REF] or cylindrical magnets [START_REF] Ferreira | Prototype of an axial flux permanent magnet generator for wind energy systems applications[END_REF][13] can be used for cost or assembly reasons.

Next references indicate from equations, how to choose the dimensions of an AFPM with iron [7][14] or without [START_REF] Subotic | Weight Optimization of Coreless Axial-Flux PM Machines[END_REF] [START_REF] Batzel | Design and test of an ironless axial flux permanent magnet machine using a halbach array[END_REF] for a wind turbine. The purpose of this article is to size an ironless axial flux motor from the dimensions of preselected magnets. Cylindrical magnets are chosen for their availability (easy to find on the shelves), cost and ease of assembly. To compensate for the lack of conductor coverage, a second ring of magnets is suggested. The coils and the stators are identical in shape and design. All the proposed coils are manufactured and assembled in exactly the same way. The main goal of this article is the reproducibility of the proposed motor topology. The motor performance is calculated from the dimensions imposed by the selected magnets and corresponding coils. Methods specifically developed for ironless motors [START_REF] Bonnet | Model of an ironless axial flux permanent magnet motor based on the field produced by a single magnet[END_REF] are used to calculate the output performance. There are then validated by 3D Finite Element Analysis (FEA) methods and experimental measurements. The design of the proposed motor is above all thought to be as simple as possible to manufacture and to limit manufacturing costs. To avoid iron machining, the motor has no iron in the stator and rotor. The magnets are cylindrical and can be found on shelves. The coils are all identical. Motors without iron have electromagnetic performances much lower than their equivalent with iron. Choices on coils and magnets are therefore made to try to compensate for the absence of iron. The magnets chosen on the shelves are the starting point of the sizing.

II. MOTOR DESCRIPTION

To give a correct idea of our approach, the final design of the prototype is shown in Fig. 1. The following explain all the choices done.

A. Magnets

To maximize the magnetic field with an axial flux motor, trapezoidal magnets are most commonly used for these motors. However, these forms of magnets are expensive. They are even more expensive if the magnets are custom made. Cylindrical magnets were therefore chosen to reduce costs. However, the shape of these magnets does not cover as much of the active part as the tile-shaped magnets. To have more active parts in the field of these magnets, a second magnet is added on the same pole (Fig. 2). The same active part is covered by two magnets of the same polarization.

B. Windings

The dimensions of the active parts are determined from the magnets. These coils must be larger than the two magnet diameters and the space between them.

To maximize the output torque, the radius of the motor is chosen to be large. What limits the maximum size of this radius is the material used for the mechanical supports. The mounts must be able to withstand the forces involved without mechanical deflection. In addition, when manufacturing these supports, care must be taken to ensure that the air gap is constant across the plane. With 3D printing of PA 2200HD [START_REF]Initial Design & Production Prodways[END_REF], these mechanical properties and accuracy are ensured for radii of less than 8cm.

To facilitate winding, the coils should not overlap. The Factional Slot Concentrated Windings (FSCW) type is preferred. This type of winding allows to limit the coil heads, and thus to limit the Joule losses [START_REF] De Donato | Integral-slot versus fractional-slot concentrated-winding axial-flux permanent-magnet machines: comparative design, FEA, and experimental tests[END_REF]. But it creates more eddy current losses in the magnets and the rotor iron. This is not a problem for a motor without iron, only the copper and magnet losses remain. This winding imposes a trapezoidal shape of the coils (Fig. 2).

The inner radius of the coils is defined by the coil heads on this radius. It must be possible to twist the wires without problems. This also depends on the diameter of the conductors and the thickness of the slots. The diameter of the conductor is chosen so that for a current 𝐼 of 1A, the current density 𝐽 corresponds to 5A/mm². The wire diameter is therefore 0.5mm. An FSCW can reach a filling factor 𝑘 of 0.5. To maximize the filling factor, the width of the coil is chosen as a multiple of the wire diameter, here this width 𝑙 is 4mm. The height of the coils should not be too high because the magnetic field is not channeled and therefore cannot reach conductors too far from the magnets. A height of 7mm is considered relevant for the performance but also for the manufacturing. A coil that is too thin is more complex to manufacture.

The number of conductors 𝑛 = 70 is deduced from:

𝐽𝑆 𝑘 = 𝑛 𝐼 (1)
The internal radius 𝑅 of the coils is then in turn imposed by these parameters. The number of coils in a stator must therefore take into account the angle 𝛼 of the coil which is related to the number of pole pairs 𝑝 (Fig. 2).

For more reproducibility, the two stators must be identical and produce the same EMFs. In order for the coils to see an identical flux generated by the magnets when the rotor rotates, there is no mechanical angular shift between the two stators. All the coils are wound in the same direction and in the same way, and the coils of the same phase of two different stators are connected in parallel.

C. Manufacturing

The motor performance is calculated by a dedicated model and by 3D FEA. If the calculated performance is lower than expected, it is necessary to choose larger magnets but also to adapt the size of the coils to these new magnets. Then the performance must be recalculated until the expected values are reached.

With the stator and rotor dimensions chosen previously, it is possible to have 12 cylindrical magnets on the rotor and 9 coils on a stator. The main dimensions of the active parts are summarized in Table I. The complete manufacturing of this prototype is available in video online [START_REF] Harribey | 3D printed alternator for micro-wind turbine[END_REF]. The mechanical supports of the stators, made of non-active materials, are identical. These supports are made here by additive manufacturing PA 2200 HD [START_REF]Initial Design & Production Prodways[END_REF]. This makes it possible to manufacture these motor parts quickly and accurately. It is possible to use other non-magnetic materials to reduce the price, such as wood. It must be ensured that the material chosen can mechanically withstand the speeds at which the rotor must rotate. The magnets are glued to this support at their dedicated locations. Ball bearings are then added to the non-active supports.

The non-active supports have a free shape. However, they must ensure that the active parts are held in place mechanically. The shapes printed for the prototype of this article can be adapted or modified.

III. CHARACTERIZATION AND FINAL SIZING

A. Open circuit magnetic field calculation

To calculate the performance of this motor before and during its design phase, a field calculation model is used [START_REF] Bonnet | Model of an ironless axial flux permanent magnet motor based on the field produced by a single magnet[END_REF]. This model allows to quickly know the open circuit magnetic field of the motor whatever the geometry of the magnets and conductors. From a single magnet, the total open circuit magnetic field created by several identical magnets is calculated.

By considering several magnets identical in shape and magnetization but located at different places in space, the field produced by these different magnetic field sources at a single target point 𝐶 is identical to the sum of the magnetic field produced by a single magnet at several target points. Each of these target points is the unique target point in the reference frame associated with each magnet (Fig. 3). I):

𝑂𝐶 ⃗ = 𝑂𝐶 ⃗ -𝑇 ⃗ (2)
To calculate the total open circuit magnetic field, two reference magnets must be used, one for each ring of the rotor. These reference magnets are positioned at the center of the cylindrical reference frame. To recompose the open circuit field from these magnets, it is necessary to reposition the necessary target points in the reference frame of these reference magnets (Fig. 3). For this purpose, two translation vectors are defined, one per reference magnet [START_REF] Ferreira | Prototype of an axial flux permanent magnet generator for wind energy systems applications[END_REF].

𝑇 ⃗ = 𝑅 (𝛼 ) 𝑅 0 0 (3)
With 𝑅 (𝛼 ) the rotation matrix around the z-axis by an angle 𝛼 , 𝑘 the number of the magnet ranging from 1 to 2𝑝 in this case and 𝑅 the radius of the center of the magnets (Table I and Fig. 2). The total flux magnetic density of the rotor can then be calculated from the field of the two reference magnets 𝐵 and 𝐵 .

𝐵 ⃗ = (-1) 𝐵 ⃗ + 𝐵 ⃗ (4)
With ( 4), the open circuit magnetic field of the rotor can be calculated at any point C in space. Only the knowledge of the field of the two reference magnets and the geometrical position of the magnets on the rotor are necessary.

B. Calculation of the static torque and FEM

For an ironless motor, it is sufficient to use the Lorentz force law to calculate the static torque. The torque is calculated in the rotor reference frame as in [START_REF] Bonnet | 3D magnetic field model of a permanent magnet ironless axial flux motor with additively manufactured nonactive parts[END_REF].

𝐶 = - 𝐽 ⃗ 𝑟 ⃗. 𝐵 ⃗ -𝐵 ⃗ 𝑟 ⃗. 𝐽 ⃗ • 𝑒 ⃗𝑑𝑉 (5)
The positions of the active parts at each instant of the rotation define new target points where the total flux magnetic density is calculated with (4). The active parts of conductors are only in the radial direction, so only the axial component of the field 𝐵 and the radial constant current density 𝐽 create a useful torque.

𝐶 = 𝐽 𝑟𝐵 𝑑𝑉 (6)

The conductors can be assimilated to a wire if the open circuit magnetic field is uniform in the coil volume. This can be the case for the motor topology with two rotors [START_REF] Bonnet | 3D magnetic field model of a permanent magnet ironless axial flux motor with additively manufactured nonactive parts[END_REF] [START_REF] Bonnet | Model of an ironless axial flux permanent magnet motor based on the field produced by a single magnet[END_REF]. For other ironless motor topologies, such as the prototype of this article, the open circuit magnetic field changes from nothing to everything in the volume of the coils. Thus, in order to have a relevant torque calculation whatever the topology of the motor adopted, the volume integral is preferred. The volume integral ( 6) is developed according to 𝑟. The volume element can be expressed: 𝑑𝑉 = 𝑑𝑆 𝑑𝑟. Where 𝑆 is cross-section of the coil of normal 𝑒 ⃗:

𝐶 = 𝐽 𝑟𝐵 (𝑟, 𝜃, 𝑧) 𝑑𝑆 𝑑𝑟 (7)
The surface integral of ( 7) is associated with a conductor section at a given radius. The open circuit magnetic field is evaluated at four Gauss points distributed over a coil section 𝑆 (Fig. 4.a). The surface integral is calculated numerically by the Gauss-Legendre method. The calculation of this surface integral for several radii allows to know the function to integrate according to the radius (Fig. 4. b). This line integral is calculated by the trapezoid method. For a given position of an active part, for 100 different sections and 4 points per section, 4x100 different target points are needed. As this motor has smooth poles, the static torque of a phase is the image of the EMF of this same phase (8) with a constant current 𝐼.

𝑒 = 𝐶 Ω 𝐼 ( 8
)
Calculating the EMF with this method allowed to quickly study the performances of the prototype during its design, in particular on the height of the coils. Indeed, the magnetic field in vacuum decreases rapidly in intensity with distance. Thus, having a coil too high is not relevant because the conductors farthest from the magnets are only slightly bathed in the magnetic field.

C. 3D finite elements calculation

To validate the dimensions and performances announced by the model, a 3D numerical simulation is performed on ANSYS Maxwell. The stator and one rotor are represented in full. As the two rotors are identical and connected in parallel, only one is needed to calculate the FEMs and the static torques (Fig. 5). The magnets are placed in a bearing strip. The magnets are moved during the transient simulation on a pair of mechanical poles. Since the motor is ironless, the air box is large enough to consider the magnetic field to be zero at the outer surfaces. The calculation of the torque by ANSYS on this type of motor is inaccurate if a large number of mesh elements is not used. It is possible to quickly calculate the load torque by a no-load simulation without using too many mesh elements. By calculating the no-load fluxes of the coils and by derivation, we obtain the EMFs and then the torque according to [START_REF] Gieras | Axial flux permanent magnet brushless machines[END_REF].

D. Winding type

With the number of magnets and coils defined in part II, it is possible to describe several types of windings. The winding is defined for one stator and is reproduced identically on the second stator. The slots and teeth on this ironless motor are defined as in Fig. 6. There are two coils in the same slot, so it is a double layer winding. The number of poles pair 𝑝 can be 1, 2, 3 or 6; which corresponds to NNNN-SSSS, NNN-SSS, NN-SS and N-S magnets respectively. To define these windings, [START_REF] Bianchi | Use of the star of slots in designing fractional-slot single-layer synchronous motors[END_REF] is used for this motor with 𝑄 the number of slots, 𝑄 the number of slots per phase, 𝑞 the number of slots per pole and per phase and 𝑚 the number of phases (Table II).

The winding for 𝑝 = 1 is not retained because it is a distributed type winding (𝑞 > 1) which implies an overlap of the coil heads. To choose the winding among the three other possibilities, the EMFs are calculated theoretically. The winding that generates the least amount of harmonics on these EMFs is the selected winding. According to Fig. 7, the solution with 𝑝 = 6 is therefore the selected winding.

E. Interest of the two magnet rings

With the length of the active part of the conductors, it is interesting to observe the contribution of this second magnet ring. Fig. 8 shows the calculated static torque generated by each magnet ring for a current of 1A in the coils. The small ring contributes to the creation of 20% of the total torque. With a current of 1A, the torque is 151.5mN.m for a mass of active parts of 830.8g. The torque per unit of mass is then 0.182N.m/kg. If only the outer ring is kept with the inner radius 𝑅 of the coils adapted to this only ring, the torque for 1A is 119mN.m. For a mass of active parts of 676.3g. The torque per unit of mass is therefore 0.176N.m/kg, which is slightly lower than that with two rings. With the calculation model it is possible to compare the theoretical EMFs of this prototype with what it would have given with trapezoid magnets. In order for the magnets to operate with the same winding, the dimensions of the trapezoidal magnets used are defined from the dimensions of the cylindrical magnets (Fig. 9) and ( 9), ( 10) and [START_REF] Yao | Novel design of a coreless axial-flux permanent-magnet generator with three-layer winding coil for small wind turbines[END_REF]. Both types of magnets have the same height of 12 mm.

𝑅

= 𝑅 + 𝑅 (9) = 𝑅 -𝑅 (10) The open circuit magnetic field is also recomposed with the method used in [START_REF] Bonnet | Model of an ironless axial flux permanent magnet motor based on the field produced by a single magnet[END_REF]. This time, the reference magnet is merged with one of the rotor magnets. The relative position of the magnets to this reference magnet is found with the rotation matrix. The position of the new target points for the trapezoid magnets are found with:

𝛼 = 2 sin 𝑅 𝑅 (11)
𝑂𝐶 ⃗ = 𝑅 (𝛼 ) 𝑂𝐶 ⃗ (12)
The total magnetic flux density of the rotor can then be calculated from the field of the reference magnet 𝐵 :

𝐵 ⃗ = (-1) 𝑅 (𝛼 ) 𝐵 ⃗ ( 13
)
The EMFs as a function of the magnet shapes are given in Fig. 10. The maximum amplitude goes from 35.89V with trapezoidal magnets to 31.74V with cylindrical magnets. This means a 12.6% decrease in motor output performance. But switching from trapezoidal to cylindrical magnets reduces the magnet mass by 26.8%. So the torque density remains interesting even with cylindrical magnets. Moreover, the cost of cylindrical magnets is much lower than the trapezoidal magnets used here. The EMF of cylindrical magnets is closer to a sine than that of trapezoidal magnets. The shape of these curves was obtained without optimization.

IV. EXPERIMENTAL MEASUREMENTS

This ironless axial flux motor, used in generator operation in the WindAid project, has two special features (Fig. 1):

-two magnet rings with 𝑝 = 6, -an identical FSCW on both stators, with 𝑄 = 9. To match the output voltage to the voltage of the battery to be supplied, the delta coupling is chosen (Fig. 11).

A. Measurement of EMFs

The EMFs are measured in open circuit. Fig. 12 shows the EMF waveform with one stator and the rotor rotated by hand. To validate the model, the motor shaft is mounted on a drilling machine that rotates it at constant speed. The measured EMFs are compared to the voltages calculated by ANSYS and the model in Fig. 13.

B. Measurement of static torque

A single phase of a single stator is supplied with a direct current 𝐼 . For this purpose, the coupling of the motor is undone and the static torque is measured for each phase separately (Fig. 14 a).

The motor is then rotated at very low speed to avoid any transient phenomenon (such as eddy current or hysteresis losses in the magnets). The force developed by the interaction between the open circuit magnetic field and the coils is measured by a force sensor. With the knowledge of the lever arm, i.e. the distance of the sensor from the center of the motor, the torque can be deduced from the measured force (Fig. 14 b). The speed of rotation is slow enough to consider that each position of the rotor is at a static position. The measured force is directly the Laplace force developed between the magnets and the coils [START_REF] Bonnet | 3D magnetic field model of a permanent magnet ironless axial flux motor with additively manufactured nonactive parts[END_REF]. The amplitude of the static torque for a DC current of 2A is 303.1mN.m by the model, 309.7mN.m by 3D FEA and 330 mN.m measured on the prototype (Fig. 15). The models remain in agreement with the measurements on prototype even if the differences are slightly larger than with the EMF.

C. Tests with rectifier and load resistance

For the load tests, the motor is maintained at a constant speed by a drill (Fig. 16). The torque of the motor is measured by the help of a force sensor. The motor is connected to a voltage rectifier and a load resistance (Fig. 17). A power meter is connected to the output of the rectifier to measure the electrical power output. The mechanical input power is calculated from the motor speed and the torque developed. The efficiency of the motor and rectifier assembly can therefore be calculated.

With a speed of 2207.8rpm and a torque of 1.306N.m, the mechanical power is 302W. The measured electrical power given to the load resistance is 216W. The efficiency of the generator with the rectifier is therefore 71.5%. This torque corresponds, according to the model, to a 2A rms in a coil. Considering only the Joule losses and an efficiency of 90% for the rectifier, the theoretical efficiency is 76.5%. Compared to trapezoidal magnets, the cylindrical magnets used have a slightly lower performance but a much lower mass and cost. The proposed prototype can be manufactured on site in remote areas. It allows to have more than 200W electric with an interesting efficiency. Several motors of this type can be associated on the same wind turbine to reinforce the electric power produced. The voltages produced are almost perfect sine, which can be interesting for the rectifier. It should be noted that this ironless motor has a low inductance, due to the absence of iron. To make high power motor, stronger magnets must be chosen. The materials of mechanical supports will then have to withstand the pressure involved. The increase in power is limited by the technology of materials used.

Fig. 1 .

 1 Fig. 1. Prototype of the wind turbine axial flux motor

Fig. 2 .

 2 Fig. 2. Magnets and a winding on one pole

Fig. 3 .

 3 Fig. 3. Recomposition of the magnetic field produced by three magnets from the field produced by a single magnet Let be a target point C where the open circuit magnetic field of the rotor must be calculated. The vectors (2) are used to represent the position of the point 𝐶 in the reference frame associated with each rotor magnet. The index 𝑗 indicates whether the magnet belongs to the inner or outer ring (TableI):

Fig. 4 .

 4 Fig. 4. a) Gauss points to calculate the surface integral b) Distribution of coil sections of a conductor above a permanent magnet to calculate the line integral

Fig. 5 .

 5 Fig. 5. Motor simulated on ANSYS Maxwell with some induction magnetic field lines displayed

Fig. 6 .

 6 Fig. 6. Definition used for "slots" and "teeth" of the ironless stator

Fig. 7 .

 7 Fig. 7. Phase to phase EMF for three different values of 𝑝

Fig. 8 .

 8 Fig. 8. The calculated static torque for one phase supplied with 1A

Fig. 9 .

 9 Fig. 9. Trapezoid magnet (blue) sized from cylindrical magnets (black)

Fig. 10 .

 10 Fig. 10. Theoretical one phase EMF at 2000 rpm

Fig. 11 .

 11 Fig. 11. Coupling of the coils of the wind turbine motor

Fig. 12 .

 12 Fig. 12. Line to line EMF measured for one stator at 330 rpm

Fig. 14

 14 Fig. 14. a) Coupling and power supply used for static torque tests b) The prototype on the static torque test bench

Fig. 15 .

 15 Fig. 15. Comparison of static torques calculated theoretically, by ANSYS and measured

Fig. 16 .

 16 Fig. 16. Motor connected to a rectifier and a load resistance

Fig. 17 .

 17 Fig. 17. Line to line voltage before rectification, current after rectification


Erwan Jahier
email: erwan.jahier@imag.fr

Nicolas Halbwachs
email: nicolas.halbwachs@imag.fr

Pascal Raymond
email: pascal.raymond@imag.fr

Synchronous modeling and validation of priority inheritance schedulers ⋆

Keywords: Embedded systems, Simulation, Scheduling, Formal Verification, Architecture Description Languages, Synchronous Languages

Architecture Description Languages (ADLs) allow embedded systems to be described as assemblies of hardware and software components. It is attractive to use such a global modelling as a basis for early system analysis. However, in such descriptions, the applicative software is often abstracted away, and is supposed to be developed in some host programming language. This forbids to take the applicative software into account in such early validation. To overcome this limitation, a solution consists in translating the ADL description into an executable model, which can be simulated and validated together with the software. In a previous paper [1], we proposed such a translation of Aadl (Architecture Analysis & Design Language) specifications into an executable synchronous model. The present paper is a continuation of this work, and deals with expressing the behavior of complex scheduling policies managing shared resources. We provide a synchronous specification for two shared resource scheduling protocols: the well-known basic priority inheritance protocol (BIP), and the priority ceiling protocol (PCP). This results in an automated translation of Aadl models into a purely Boolean synchronous (Lustre) scheduler, that can be directly model-checked, possibly with the actual software.

Introduction

The European project ASSERT is devoted to safe model-driven design of embedded systems, with aerospace systems as a main application domain. Such systems are deployed on specific architectures that need to be described and simulated in order to allow early validation of the integrated system.

The approach taken in the ASSERT project is to describe the execution architecture separately from the software components. The target architecture is described in the Aadl architecture description language [START_REF] Feiler | Embedded system architecture analysis using SAE AADL[END_REF][START_REF]SAE: Architecture Analysis & Design Language (AADL)[END_REF]. Aadl provides a collection of classical systems components, which can be instantiated and assembled to describe the actual execution platform. In a typical Aadl description, a system is made of several computers, communicating through buses; a computer is made of memory and processors, and a processor runs a scheduler and several tasks; at last, tasks are running applicative software. Those software components can be developed using several programming languages, including ADA, C, or even Scade and Lustre via a C wrapping.

Aadl components are decorated with information like rates and Worst Case Execution Time (WCET) for periodic tasks, scheduling policy, etc. Those informations are intended to be used in the validation of the platform, mainly by checking properties like the absence of deadlocks, or the respect of deadlines. The functional part is expressed by the software components, and thus generally completely ignored, although it may influence some non-functional aspects. For instance, a software component may produce some event that wakes up a task; the scheduling environment and the execution times are then modified.

Our main objective is to perform simulation and validation that take into account both the system architecture and the functional aspects. We consider the case where software components are implemented in the synchronous programming language Lustre/Scade1 . Our proposal in [START_REF] Halbwachs | Virtual execution of AADL models via a translation into synchronous programs[END_REF] is to build automatically a simulator of the architecture, expressed in a synchronous language like the software components. This approach presents several advantages: first, synchronous languages are well-known to be able to express non-synchronous behaviors, while the converse is more difficult; now, getting all aspects in the same model allows both functional and system aspects to be considered jointly. For instance, in Aadl, sporadic tasks can be activated by the output of some other components. Therefore, in such cases, more realistic simulation and finer-grained formal verification can be performed.

The translation proposed in [START_REF] Halbwachs | Virtual execution of AADL models via a translation into synchronous programs[END_REF] takes into account various asynchronous aspects of Aadl such as task execution time, periodic or sporadic activations, multitasking (using Rate Monotonic Scheduling [START_REF] Liu | Scheduling algorithms for multiprogramming in a hard real-time environment[END_REF]), and clock drifts. The result is an executable integrated synchronous model, combining architecture behavior with actual software components, which can be validated with tools available for synchronous programs.

In this paper, we propose to extend this work by taking into account shared resources using different protocols (no lock, blocking, basic inheritance, priority ceiling). We also show how various properties related to determinism, schedulability, or the absence of deadlock can be automatically checked on given architecture models.

The article is organized as follows. We first recall in Section 2 the principles of simulation of Aadl in the synchronous paradigm. Then we describe in Section 3 how to deal with shared resources and various shared access protocols in a synchronous program. Finally, we show in Section 4 how one can use the resulting executable model to check various kinds of properties (determinism, schedulability, absence of deadlock), and to perform monitored simulations.

From Aadl to synchronous programs

This section recalls the main features of the Architecture Analysis & Design Language (Aadl), as well as the synchronous paradigm. Then it briefly recalls how the behavior of an (asynchronous) Aadl model can be modeled by a nondeterministic synchronous program. This subject is presented in detail in [START_REF] Halbwachs | Virtual execution of AADL models via a translation into synchronous programs[END_REF].

The Aadl description language

An Aadl model is made of an arborescent assembly of software and hardware components [START_REF] Feiler | Embedded system architecture analysis using SAE AADL[END_REF][START_REF]SAE: Architecture Analysis & Design Language (AADL)[END_REF]. A component is defined by an interface (input and output ports), a set of sub-components, a set of connections linking up the subcomponents ports, and a set of typed attributes (called properties). The main kinds of Aadl components are the following.

Systems are top-level components; they describe the mapping between software and hardware components. Device components model hardware responsible for interfacing the system with its environment. They are typically used to represent sensors or actuators. From a functional point of view, they correspond to the inputs and the outputs of the system. Processor components are abstractions of hardware and software responsible for scheduling and executing threads.

Memory components (hardware) are used to specify the amount and the kind of memory that is available to other components.

Data components (software) are used to represent data types in the source text. Other components might have a shared access to data components. The access policy is controlled by the Concurrency Control Protocol property (lock, priority ceiling protocol, cf. Section 3). Bus components (hardware) are used to exchange data between components on different processors.

Process components are abstractions of software responsible for defining a memory space that can be accessed by the thread sub-components it contains. Thread components are abstractions of software responsible for executing applicative programs. When several threads run under the same processor, the sharing of the processor is managed by a runtime scheduler. The dispatch protocol property is used to specify that scheduling policy. For instance, the value periodic means that the thread must be activated according to the specified period; the value aperiodic means that the thread is activated via one of the other components' output ports (called event ports). Sub-program components are the leaves of this arborescent description. Their implementations need to be provided in some host language. In our approach, if one wants to be able to formally analyze aperiodic threads whose activation depends on the functional output of some program component, one needs to provide for it a synchronous program (or at least a wrapper), e.g., written in Scade or Lustre. The property compute exec time specifies a range for the worst case execution time (WCET) of the program. In the sequel, we use the term task to denote a thread running a program.

The synchronous paradigm

We present now the essentials of the synchronous paradigm, focusing on the aspects that will be used later on.

A synchronous program (also called a node) is a dynamic system evolving on a discrete time scale. It has an internal memory made of state variables, inputs and outputs, and its behavior is a (virtually infinite) sequence of atomic reactions. Each reaction consists in reading current inputs, computing outputs, and updating the internal memory (state). In other terms, synchronous programs are a straightforward generalization of synchronous circuits (i.e., sequential circuits or Mealy machines), where data can be of arbitrary types rather than just Boolean values.

A synchronous program is characterized by a vector of inputs i, a vector of outputs o, a vector of state variables s. Its semantics is defined by its initial state s 0 (the initial value of s), and the functions f o and f s , respectively returning the output and the next state from the current inputs and the current state. For each instant t:

o t = f o (i t , s t ) ; s t+1 = f s (i t , s t )
A program without state is called a combinational node; usual functions like arithmetic or logical operators are then naturally lifted to synchronous programs.

For any data-type τ with a well-defined default value d, a "delay" (or register) program can be defined as follows:

s 0 = d ; f o (i, s) = s ; f s (i, s) = i
In the sequel we mainly use Boolean (resp. integer) registers, with false as default value (resp. 0), and represented by the symbol •.

The main characteristic of synchronous programs is the way they are composed: when connecting several sub-programs, a reaction of the whole program consists of a simultaneous reaction of all the components. In other words, the synchronous paradigm provides an idealized representation of parallelism.

An important consequence is that a big synchronous program can be described as a parallel composition of smaller sub-programs. In this approach, a program is described as a data-flow network of synchronous programs connected by wires. Fig. 1 shows the data-flow network of a synchronous counter, made of a delay node and three combinational nodes (two "if-then-else" and an adder). For the sake of conciseness, we use sets of equations rather than drawings for representing such networks. For instance, the set of equations equivalent to the counter is the following:

c = if r then 0 else s ; s = •c + if x then 1 else 0
Note that such a set of equations has a straightforward solution as long as it does not contain combinational loops. In other words, any feed-back loop in the network should pass through a delay operator. In the following, we will take care to define only such well-founded data-flow networks.

At last, all synchronous formalisms are providing a notion of under-sampling, also called activation condition, or clock-enable in the domain of synchronous circuits. The activation condition is an higher-order operator that takes a synchronous node P , a Boolean input b, and produces a new node. The behavior of that node is defined as follows: whenever b is true, it behaves exactly like P , and whenever b is false, both the internal state and the outputs are "frozen" (i.e. they keep their previous value).

Modeling asynchrony in the synchronous framework

The ability of the synchronous framework to model asynchrony is well-known [START_REF] Milner | On relating synchrony and asynchrony[END_REF], and has been often used [START_REF] Baufreton | SACRES: A step ahead in the development of critical avionics applications[END_REF][START_REF] Baufreton | Visual notations based on synchronous languages for dynamic validation of gals systems[END_REF][START_REF] Gamatié | Synchronous modeling of avionics applications using the signal language[END_REF][START_REF] Gamatié | The signal approach to the design of system architectures[END_REF][START_REF] Guernic | Polychrony for system design[END_REF]. In [START_REF] Halbwachs | Virtual execution of AADL models via a translation into synchronous programs[END_REF], we used a similar technique for translating a subset of Aadl into synchronous data flow equations.

This goal is mainly achieved by using "oracles" (i.e., additional inputs) for modeling non-determinism, and activation conditions for modeling the asynchronous aspects: time-consuming tasks, multi-tasking, clock jitter.

However, in this previous work, multi-tasking was only considered in the case of simple fixed priorities rate monotonic scheduling. In this article, we consider more sophisticated policies that take into account shared resources with protected access, and all the problems they raise: priority inversion, and deadlock.

Handling shared resources

In Aadl, Data component accesses can be shared between several components. In contrast to other kinds of components (thread, process, sub-program) which are translated into nodes, data components are translated into local variables of the surrounding component node. Depending on the kind of access that is associated with them (read only, write only, or read write), the necessary wires are added to the interface of the node: a data component that has a write (resp., read) access to a resource has an additional output (resp., an additional input), and the data update is performed at its dispatch time using an activation condition.

In order to guarantee the data integrity, it is necessary to prevent the resource from being accessed by several components at the same time. For that purpose, several concurrency control protocols were defined [START_REF] Sha | Priority inheritance protocols: An approach to real-time synchronization[END_REF], that modify the classical Rate Monotonic scheduling. In Aadl, this is specified through the "Concurrency Control Protocol" property, attached to a data component. In this section, we explain how to implement four kinds of concurrency control protocol:

-NoneSpecified: components access the shared resource with no constraint at all (no lock mechanism). -Lock: Before accessing a shared resource, a component should ask for it, and gets it only if no other component has locked it before; otherwise, it is suspended until the resource is unlocked. When a component obtains a resource, we say that the component enters a critical section.

Hence, a low priority thread tl can block a high priority one th if th wants to access a resource that is locked by tl. The problem with this protocol is that tl can block th, even when tl is not in critical section. This is referred to as the priority inversion problem [START_REF] Sha | Priority inheritance protocols: An approach to real-time synchronization[END_REF]. -BIP: The Basic Inheritance Protocol, also known as Priority Inheritance Protocol, refines the previous one to prevent priority inversions. -PCP: The Priority Ceiling Protocol is a refinement of BIP defined in order to prevent deadlock.

In the following, we describe those protocols more precisely, and explain how to implement them in terms of synchronous data-flow equations. Defining a scheduling protocol consists of defining a node, called hereafter a scheduler, that decides at each instant which thread the CPU is attributed to.

The No Lock protocol

The simplest way of handling shared resources is to ignore them, and to always give the CPU to the highest priority thread. This (absence of) protocol is straightforward and generally useless for systems involving shared resources. But this simplest scheduler is refined in later sections for the other protocols. It is basically the scheduler used in [START_REF] Halbwachs | Virtual execution of AADL models via a translation into synchronous programs[END_REF].

Concretely, we need to generate a synchronous program that takes as inputs Boolean variables indicating which threads ask for the CPU (Dispatched 1 , ..., Dispatched n ), and that returns Boolean variables indicating which thread is elected (cpu 1 , ..., cpu n ). Of course, at most one among the cpu i should be true at each instant. The program that computes the Dispatched i variables is derived from the period and the WCET of threads, which is specified in the Aadl code.

The convention here is that t i has priority over t j if i < j. A possible way of implementing that node is as follows:

∀k ∈ [1, n] : cpu k = Dispatched k ∧ 0<i<k cpu i (1)
Henceforth, the convention is that the program input variables begin with an uppercase letter (e.g., Dispatched k ); and cpu i stands for the negation of cpu i .

The Blocking protocol

In order to take into account shared resources, we need additional inputs: the Boolean variable named Asks cs ti r ℓ indicates that the thread t i wants to access the resource r ℓ (their values come from the output of the predefined Aadl subprograms Get resource and Set resource [START_REF]SAE: Architecture Analysis & Design Language (AADL)[END_REF]).

In order to ease the definition of cpu k , we introduce the following auxiliary variables:

the Boolean variable has cs t k r ℓ indicates that the thread t k is in Critical Section on resource r ℓ ; -the Boolean variable t i blocks t k r ℓ indicates that the thread t k asks for a resource r ℓ , which is locked by another thread t i .

Computing which thread is in critical section. A thread t k is in critical section for a resource r ℓ if it asks for the resource, and if either it was in critical section before (• has cs t k r ℓ );2 -or it enters in critical section at the current instant. It enters a critical section when and only when it obtains the CPU. Hence, the following definition of has cs t k r ℓ :

∀k ∈ [1, n], ∀ℓ ∈ [1, m] : has cs t k r ℓ = Asks cs t k r ℓ ∧ (cpu k ∨ • has cs t k r ℓ ) (2)
Note that when we define such a relation, the quantification "∀k ∈ [1, n], ∀ℓ ∈ [1, m]" suggests that we generate n × m equations for defining the scheduler. But in fact, it is generally much less, since in the Aadl model, all threads may not have access connections to all resources. This remark actually holds for all the variables relating threads and resources in the following.

Computing the blocks relation. We say that a thread t i blocks a thread t k via a resource r ℓ if both threads ask for the resource, and if the thread t i was owning r ℓ at the previous instant.

∀k, i ∈ [1, n], i = k,∀ℓ ∈ [1, m] : t i blocks t k r ℓ = Asks cs t k r ℓ ∧ Asks cs ti r ℓ ∧ •has cs ti r ℓ (3)
Computing the elected thread. Once we have defined those two auxiliary relations, cpu k can easily be defined similarly as in Section 3.1: the highest priority thread obtains the CPU, except if it is blocked by some other thread:

∀k ∈ [1, n] : cpu k = Dispatched k ∧ 0<i<k cpu i ∧ i =k,ℓ∈[1,m] t i blocks t k r ℓ (4)
Note that those three sets of equations defines a valid synchronous program, since they do not contain any combinational cycle (cf Section 2.2).

The Basic Inheritance Protocol

The Basic Inheritance Protocol was introduced [START_REF] Sha | Priority inheritance protocols: An approach to real-time synchronization[END_REF] to avoid the priority inversion problem. Indeed, with the previous protocol, when a high-priority thread t 1 wants to access a resource shared by a lower priority thread t 3 , which have put a lock on it, then t 3 keeps the CPU. Moreover, t 3 can be interrupted by t 2 of lower priority than t 1 , even though t 2 does not try to access any shared resource.

The idea of the Basic Inheritance Protocol (BIP) is to modify the priority of t 3 in such a way that it inherits the priority of t 1 , when t 3 has the lock on a resource r ℓ requested by t 1 . Indeed, this prevents t 2 to interrupt t 3 , and hence prevents the priority inversion.

The intuition of our BIP (synchronous data-flow) encoding is the following: first consider the dispatched thread with the highest priority. If it is not blocked, it must obtain the CPU. Otherwise, consider its blocking thread, and check if it is itself blocked, and so on until we find a thread that is not blocked. When we find the thread that is not blocked3 , we give it the CPU. Hence, the first thing to do is to compute the transitive closure of the t blocks t r relation.

Computing the t i blocks * t k relation. Let an inhibition path from a thread t i to a thread t k be a set of s + 1 threads {t i = t i0 , ..., t is = t k } such that there exist s resources r 1 , ..., r s , that may be respectively accessed by t i0 and t i1 , t i1 and t i2 , ..., t is-1 and t ks . Such a path is said to be cycle-free if all the threads in the path are distinct. Let P ath(i, k) be the set of cycle-free paths from t i to t k (this set can be computed from the Aadl source code). A thread t i blocks * another thread t k if t i is not itself blocked, and if there exists an inhibition path in P ath(i, k) that is true.

∀i, k ∈ [1, n], i = k :
(5)

t i blocks * t k = t i is blocked ∧ p={i0,...,is}∈P ath(i,k) t i0 blocks ti 1 r1 ∧ ... ∧ t is-1 blocks ts rs where: ∀k ∈ [1, n] : t k is blocked = ℓ∈[1,m],j∈[1,n],j =k t j blocks t k r ℓ
The protocol. The BIP states that a thread in critical section on a resource inherits the priority of any other higher priority thread that asks for the same resource. The difficulty is to translate this "dynamic" condition 4 into a Boolean condition. To do that we use an accumulator, (named ii, which stands for inhibiting index), that carries the value of the inhibitor of the thread that has the highest priority, if the dispatched thread with the highest priority is blocked (ii is set to 0 or -1 otherwise). For readability, we use a switch-like notation, where

c 1 → x 1 , c 2 → x 2 , ..., c n → x n stands for if c 1 then x 1 else if c 2 then x 2 ... if c n then x n . ii 0 = 0 ∀k ∈ [1, n] : (cpu k , ii k ) = dispatched k → (F alse, ii k-1 ) (6) (cpu 1 ∨ ... ∨ cpu k-1 ) → (F alse, -1) (7) ii k-1 = k → (T rue, -1) (8) ii k-1 > 0 → (F alse, ii k-1 ) (9)
{ t j blocks * t k → (F alse, j) } j∈[1,n],j =k (10)
T rue → (t k is blocked, 0) (11)
For each k > 0, cpu k and ii k depend on cpu k-1 and ii k-1 , which means that cpu 1 and ii 1 are computed first, and then cpu 2 and ii 2 , and so on, until cpu n and ii n . At the beginning, the inhibiting index is equal to 0 (ii 0 = 0). Then, the pairs (cpu 1 ,ii 1 ), ..., (cpu n ,ii n ) are computed in turn. As long as cpu k-1 is set to F alse (i.e., when conditions of lines 8 and 11 do not hold):

-If t k is blocked by a lower priority thread t j (line 10), the inhibiting index takes the priority of the inhibitor j. Then, the inhibiting index keeps this value (lines 6 and 9), until the index of the inhibitor is reached (line 8).

In that case, the corresponding cpu variable is set to T rue, the remaining values of cpu are set to F alse (line 7), and ii k is unused for bigger k (-1). -Otherwise (line 11), if t k is not blocked at all, it gets the CPU, and all the remaining values of cpu are set to false (line 7). If it is blocked, the system deadlocks.

The Priority Ceiling Protocol

The problem with the BIP is that it does not prevent deadlocks. Indeed, consider the following scenario, where 2 threads t 1 and t 2 share 2 resources r 1 and r 2 :

1 One solution is to (statically) forbid such intertwined use of locks. Another solution is to use the so-called Priority Ceiling Protocol (PCP). The PCP is a refinement of the BIP.

The priority ceiling of a resource r ℓ is the maximal priority of all the threads that may use r ℓ ; we note it P C(ℓ). The priority ceiling of a thread t k is the maximum of the priority ceilings of the resources locked by other threads; we note it P C k . Contrary to P C(ℓ), P C k is a dynamic value. The PCP consists in adding the following constraint to the BIP: t k can lock a resource r only if its priority is higher than its priority ceiling (k < P C k ).

The Priority Ceiling of resources locked by threads other than k. P C k formal definition is just a direct translation of the definition given above.

∀k ∈ [1, n]

: P C k = (12) M in {n + 1} ∪ P C(ℓ) / Asks cs ti r ℓ ∧ •has cs ti r ℓ ℓ ∈ [1, m] i ∈ [1, n], i = k
The tk ask relation. We first define yet another auxiliary relation that states whether a thread wants to enter a critical section at the current instant (i.e., a thread asks for a resource that it hasn't locked yet).

∀k ∈ [1, n] :

asks cs t k = ℓ∈[1,m] (Asks cs t k r ℓ ∧ •has cs t k r ℓ )
The protocol. The PCP encoding is the same as the BIP one, except that we modify the definition of the blocks relation (previously defined in equation 3). Indeed, there is now a second reason for a thread t k to be blocked by another thread t i : if t k wants to enter a critical section (asks cs t k ) when its priority ceiling P C k is not higher than its own priority (P C k ≤ k). Note that the priority ceiling of t k (i.e., the value of P C k ) is a consequence of the lock that t i has on the resource ℓ (P C(ℓ

) = P C k ). ∀k, i ∈ [1, n], i = k, ∀ℓ ∈ [1, m] : t i blocks t k r ℓ = (13)
Asks cs ti r ℓ ∧ •has cs ti r ℓ ∧ (Asks cs t k r ℓ ∨ (asks cs t k ∧ P C(ℓ) = P C k ≤ k))
Here again, those set of equations defines a valid synchronous program as they do not contain any combinational loop.

Validation

We have encoded all the equations given in the previous Section into an Ocaml (meta-)program that, given a set of tasks, a set of resources, and a set of task/resource pairs, generates a Lustre program5 . The resulting Lustre program is a task scheduler, computing one Boolean variable (cpu i ) per thread (t i ), from Boolean inputs indicating which threads ask for the CPU (Dispatched ti ), and which threads ask for which resource (Asks cs ti r l ). In the following, we illustrate the use of a state-explorer (i.e., a modelchecker) to prove various properties of this generated program. This was very useful to debug the equations given in this paper, and also to debug the Ocaml encoding of those equations. We'll also argue why we believe it might also be useful for Aadl end-users.

Absence of deadlock

In order to prove the absence of deadlock, we used Lesar [START_REF] Halbwachs | Programming and verifying real-time systems by means of the synchronous data-flow programming language Lustre[END_REF], a Lustre model-checker. This tool implements state-of-the-art state-reachability algorithms, based on Binary Decision Diagrams. We used both a enumerative algorithm which complexity is related to the number of states, and a symbolic algorithm, which complexity is related to the diameter of the state space.

We proved with Lesar that, whenever at least one thread asks for the CPU, at least one of the cpu i is true. Actually, we even prove that exactly one cpu i is true in that case, which simply proves that our scheduler is correct in the sense that it does not give the processor to more than one thread:

( i∈[1,n] Dispatched i ) ⇒ i∈[1,n] cpu i
We performed this on the examples of Fig. 2. For instance, the first example (ex. 1) of Fig. 2 consists of a system with two threads t1 and t2, that can access two resources r1 and r2. This example is precisely the one given in [START_REF] Sha | Priority inheritance protocols: An approach to real-time synchronization[END_REF] to illustrate the fact that the BIP does not prevent deadlock, and which motivates the definition of PCP.

Lesar was indeed able to generate a counter-example that exhibits a deadlock; the scenario it provides is almost the same as the one given [START_REF] Sha | Priority inheritance protocols: An approach to real-time synchronization[END_REF] (and also in Section 3.4). Lesar proved the absence of deadlock for the PCP on the three examples. The results of those experiments are outlined in Fig. 3. When the property is false, we indicate the length of the counter-example. When the property is true, we indicate the diameter of the graph, and its number of states. All runs lasted less that a second. An interesting point in those experiments is that it is not always worth using the PCP (that is deadlock-free by construction) since the BIP and the lock protocol can provably be deadlock-free in some configurations (e.g., in ex. 2). Note that in order to avoid false alarms, we need to tell the state-explorer that the inputs of the scheduler are not completely random. For instance, it was necessary to assert that a thread cannot change its requests for resources when it does not own the CPU.

Priority inversion

The priority inversion corresponds to situations when a thread is blocked by a lower priority thread. This occurs very naturally when two threads share the same resource, locked by the lower priority thread. Priority inversion is more problematic when it happens as in the example of Section 3.3 (which was the example given in [START_REF] Sha | Priority inheritance protocols: An approach to real-time synchronization[END_REF] to motivate the introduction of the BIP). Indeed, threads are generally supposed to remain in critical section for a short time. Now, if a thread that does not lock any resource preempts a lower priority thread in critical section, the corresponding resource might be locked for a long time.

Therefore, we check the following property: if a thread t k gets the CPU, when a higher priority thread asks to enter in critical section, then t k should have at least a lock on one of the resource. In other words, we want to be sure that a thread that does not lock any resource cannot block any higher priority thread:

∀i ∈ [2, n], ∀j ∈ [1, i -1] : (cpu i ∧ asks cs tj ) ⇒ ℓ∈[1,m] has cs ti r ℓ
We actually ask the model-checker to prove a slightly higher refined property, which is that for any system that does not deadlock, there is no priority inversion. Indeed, as soon as two tasks deadlock, any other thread can get the CPU even if it is not supposed to, according to the priorities defined by the protocol. This is the kind of subtlety that can be discovered using a model-checker.

As summarized in Fig. 4, Lesar found counter-examples that falsify the property for the last two examples of Fig. 2 using the lock protocol. And it proved the property with the BIP and the PCP. The second example is the one given [START_REF] Sha | Priority inheritance protocols: An approach to real-time synchronization[END_REF] (and in Section 3.3) for motivating the introduction of the BIP.

Schedulability

The thread scheduler we generate in Section 3 is just a part of the Aadl2lustre translator [START_REF] Halbwachs | Virtual execution of AADL models via a translation into synchronous programs[END_REF]. The program that computes the values of the Dispatched i variables is derived from the AADL code (from the threads period and WCET).

In order to check the schedulability of an Aadl system, we look at the sequences of values taken by the Dispatched i and cpu i variables. The set of valid sequences is defined by the automaton of Fig. 5. In this automaton, d stands for "dispatch", and is defined as the Dispatched rising edge; a stands for "activate", and is defined as the cpu rising edge; and r stands for "release", and is defined as the Dispatched falling edge. All omitted transitions in this automaton target the "scheduling-error" state. A system is well-scheduled if this error state is never reached. Indeed, nothing prevents the generated scheduler to issue a "dispatch" event between an "activate" and a "release" event. This is what occurs when the system is not schedulable, i.e., when some deadline is missed. Once encoded into a Lustre formula, this automaton can be used to prove (by state-exploration) that the system is schedulable.

Note that this schedulability property somehow does not only concern the part of the Aadl2lustre translator described in this article. But we mention it here because we believe this analysis is particularly interesting in presence of shared resources.

Related work

The Cheddar tool [START_REF] Hugues | Rapid prototyping of distributed real-time embedded systems using the AADL and Ocarina[END_REF][START_REF] Singhoff | Cheddar: a flexible real time scheduling framework[END_REF] can perform Schedulability analysis over Aadl specification, but it ignores the functional aspects of Aadl components, and it is more oriented towards quantitative analysis: resource usage, number of preemptions, number of context switches, etc. Cheddar allows users to define dedicated (user defined) schedulers and perform simulations [START_REF] Singhoff | Scheduling and memory requirements analysis with AADL[END_REF].

Using a synchronous framework to model software architectures is not a new idea [START_REF] Gamatié | Synchronous modeling of avionics applications using the signal language[END_REF][START_REF] Gamatié | The signal approach to the design of system architectures[END_REF][START_REF] Baufreton | Visual notations based on synchronous languages for dynamic validation of gals systems[END_REF][START_REF] Guernic | Polychrony for system design[END_REF]. Gamatié et al. [START_REF] Gamatié | Synchronous modeling of avionics applications using the signal language[END_REF][START_REF] Gamatié | The signal approach to the design of system architectures[END_REF] defined a framework that provides a library of components, written in Signal [START_REF] Guernic | Signal, a data flow oriented language for signal processing[END_REF] and C++, suitable for modeling systems following the ARINC (Aeronautical Radio Incorporated) 653 standard. They demonstrate how to use the Signal language as an ADL -whereas we translate Aadl architecture models into Lustre. They mention that modelchecking could be possible since the system is described in Signal, but the task scheduler is implemented in C++, which would make its model-checking difficult -they do not pretend to be able to check the scheduler tough. Anyway, they do not mention any particular protocol with respect to shared resource handling.

Formal verification of priority inheritance protocols has also been conducted using the Pvs theorem prover [START_REF] Dutertre | Formal analysis of the priority ceiling protocol[END_REF]. The kind of outcome that one obtains using a theorem prover is of course different of what can be achieved with a modelchecker. With Pvs, Dutertre proves very general property about the PCP correctness. On the contrary, we model-check the protocol together with the system architecture description, plus the functional components. We are therefore able to prove much more fine-grained properties, not only about the whole system behavior, but also about the scheduling protocol itself. Moreover, some protocol properties can be false in the general case; for example, we proved that the second system of Fig. 2 does not deadlock with the BIP.

Penix et al. used a model-checker to verify a rate monotonic scheduler of a real time operating system [START_REF] Penix | Verification of time partitioning in the deos scheduler kernel[END_REF]. But as their scheduler model is very detailed, here again the rest of the architecture is kept abstract. Elaborated protocols for dealing with shared resources are not addressed either.

Defining an automated translation from Aadl models to a purely Boolean synchronous scheduler, that can be directly model-checked, has many advantages.

-Firstly, the model-checker was very useful to debug our scheduler generator.

-Secondly, we claim it can also be useful for the Aadl end-users; for example, the PCP is a refinement of the BIP that has been introduced to avoid deadlocks. However, for some particular topologies of threads and resources, it may happen that deadlocks cannot occur even with the BIP scheduler, and that a model-checker is able to prove it on our model. -Finally, in presence of shared resources, the analytic schedulability criteria may be too conservative, and reject schedulable systems. Moreover, as soon as the system contains sporadic events (when the thread activation depends on the output of some other thread), the analytic method can be meaningless.

Consider for example two components activated by a third one, which both outputs cannot be true at the same instant. Of course with our technique, one cannot deal with generic properties (i.e., for any number of tasks and resources), but since the generation of models for verification is automatic, the verification can be replayed for each instance.

When the verification problem is too large, an exhaustive verification can be untractable. However, our encoding can still be useful to perform intensive automatic simulations using testing tools like Lurette [START_REF] Jahier | Case studies with Lurette V2[END_REF]. The absence of deadlocks, the schedulability, and the non-inversion properties are used as test oracles (i.e., runtime monitors). The assertions on the scheduler inputs (e.g., no rising edges for the asking of a resource by threads that do not have the CPU) are used to constrain the random input generator [START_REF] Raymond | Describing and executing random reactive systems[END_REF].

Another case where such tests and simulations are the only tractable methods is when the Aadl model contains sporadic threads activated by software components that are not implemented in Lustre (or in any other language with formal semantics). A way around this problem would be to have a Lustre abstraction of all the possible behavior of such components; but such an abstraction is not always easy to define.

Fig. 1 .

 1 Fig. 1. The data-flow network of a synchronous counter.

Fig. 2 .

 2 Fig. 2. Examples of tasks accessing shared resources.

Fig. 4 .

 4 Fig. 4. Priority-inversion property exp.

Fig. 5 .

 5 Fig.5. The automaton recognizing well-scheduled systems. There is one such automaton per thread to schedule.

  . t 2 asks for the CPU (Dispatched 1 ) and gets it. 2. t 2 locks r 1 . 3. t 1 asks for the CPU. It has a higher priority than t 2 , hence t 1 gets the CPU. 4. t 1 locks r 2 . 5. t 1 tries to lock r 1 . But t 2 has locked it. Therefore t 2 gets the CPU. 6. t 2 tries to lock r 2 . But t 1 has locked it. Nobody can get the CPU. The system is blocked (or deadlocks).

Scade is the industrial version of Lustre[START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF], and is maintained and distributed by the Esterel-Technology company.

All Boolean delays (•) are implicitly initialized to false.

if such a thread does not exist, the model-checker will tell us (cf Section

4.1).[START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF] The priority of each thread depends on the history. But by chance, it only depends on a very short history, that is, the previous instant.

We put a copy of this Ocaml program as well as a copy of the resulting Lustre programs at the url http://www-verimag.imag.fr/∼jahier/aadl-schedul/

Acknowledgments

We thank Karine Altisen for fruitful (nearby office) discussions about scheduling.

⋆ This work was partially supported by the European Commission under the Integrated Project ASSERT, IST 004033, which ended in 2008