Ce travail de thèse a pour objectif de fournir un outil de modélisation rapide de l'interaction d'une source électromagnétique 3D avec une pièce de géométrie ou de propriétés physiques complexes dans le domaine des basses fréquences (régime quasi-statique). La principale application est la simulation d'un procédé de Contrôle Non Destructif (CND) d'une pièce conductrice présentant une surface ou des propriétés physiques perturbées. La plateforme logicielle CIVA, comportant un module dédié à la simulation des procédés de CND par courants de Foucault intègre à l’heure actuelle des modèles semi-analytiques limités aux géométries canoniques : pièces planes, cylindriques. Afin de lever ce verrou, le formalisme des équations de Maxwell covariantes, déjà très utilisé dans le domaine optique pour la caractérisation des réseaux de diffraction (méthode des coordonnées curvilignes) est étendu au régime quasi-statique. L’utilisation d’un nouveau système de coordonnées curvilignes non-orthogonal associé à la géométrie de la pièce conduit à écrire très facilement et de manière analytique les conditions de passage aux interfaces de formes complexes. La résolution numérique des équations de Maxwell sous leur forme covariante est abordée par une approche modale qui repose sur le calcul préalable de solutions propres d’un système d’équations différentielles en absence de source. La représentation des composantes du champ électromagnétique à partir de deux fonctions de potentiels du second ordre (SOVP) ou potentiels de Hertz dans des systèmes de coordonnées canoniques est d’abord étendue au système de coordonnées curvilignes. On obtient alors les expansions modales des composantes covariantes et contra-variantes du champ électromagnétique. Les coefficients de ces expansions modales sont déterminés ensuite en introduisant le champ d’excitation et en imposant les conditions de passage adéquates entre les différents milieux. Cette approche est ensuite couplée d'une part à un algorithme récursif (les paramètres S) afin de prendre en compte la présence d'interfaces internes complexes dans la pièce, et d'autre part à une méthode numérique d'ordre élevé (Méthode pseudo-Spectrale) afin de prendre en compte de façon rigoureuse des variations des propriétés physiques (perméabilité magnétique et/ou conductivité électrique...) du matériau avec la profondeur. La validation de la méthode numérique proposée s’appuie sur des comparaisons avec des données simulées à l'aide d'un logiciel commercial de calcul par éléments finis et des données expérimentales obtenues au laboratoire. En outre, les codes développés ont été intégrés à une version de développement de la plateforme CIVA afin de répondre aux besoins des partenaires dans le cadre du projet européen SIMPOSIUM. / This PhD work concerns the development of fast numerical tools, dedicated to the computation of the electromagnetic interaction between a low frequency 3D current source and a complex conductor, presenting rough interfaces and/or conductivity (and/or permeability) variations. The main application is the simulation of the Eddy Current non-destructive testing process applied to complex specimens. Indeed, the existing semi-analytical models currently available in the CIVA simulation platform are limited to canonical geometries. The method we propose here is based on the covariant Maxwell equations, which allow us to consider the physical equations and relationships in a non-orthogonal coordinate system depending on the geometry of the specimen. Historically, this method (cf. C-method) has been developed in the framework of optical applications, particularly for the characterization of diffraction gratings. Here, we transpose this formalism into the quasi-static regime and we thus develop an innovative formulation of the Second Order Vector Potential formalism, widely used for the computation of the quasi-static fields in canonical geometries. Then, we determine numerically a set of modal solutions of the source-free Maxwell equations in the coordinate system introduced, and this allows us to represent the unknown fields as modal expansions in source-free domains. Then, the coefficients of these expansions are computed by introducing the source fields and enforcing the boundary conditions that the total fields must verify at the interfaces between media. In order to tackle the case of a layered conductor presenting rough interfaces, the generalized SOVP formalism is coupled with a recursive algorithm called the S-matrices. On the other hand, the application case of a complex shape specimen with depth-varying physical properties is treated by coupling the modal method we developed with a high-order numerical method: pseudo-spectral method. The validation of these codes is carried out numerically by comparison with a commercial finite element software in some particular configurations. Besides, the homogeneous case is also validated by comparison with experimental data.

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL. / The work in this thesis is at the intersection of two major research domains~: Model-Driven Engineering (MDE) and formal methods, and has various fields of application. This thesis deals with the formal verification of parallel applications modelled by the MDE approach. In this approach, models play a central role and enable to develop an application through successive transformations (automated or not) between intermediate models of differing levels of abstraction, until executable code is produced. When models have a formal semantics, the application can be verified, either automatically or semi-automatically. These principles are used in TOPCASED, an ECLIPSE-based development environment for critical embedded applications, which enables formal verification by interconnecting existing tools. This thesis implements the TOPCASED approach by relying on the CADP toolbox for verifying systems, and on its most recent input formalism : LOTOS NT. This thesis tackles the formal verification of MDE applications through two real problems : 1) For GALS (Globally Asynchronous, Locally Synchronous), a generic verification method, based on a transformation to LOTOS NT, is proposed and illustrated by an industrial case-study provided by AIRBUS : a communication protocol between the airplane and the ground described in the synchronous langage SAM designed at AIRBUS. 2) For Web services specified with the BPEL (Business Process Execution Language) norm, a verification method is proposed. It is based on a BPEL to LOTOS NT transformation which takes into account XML Schema, Xpath, and WSDL, the languages on which the BPEL norm is built.

Résumé indisponible / Résumé indisponible

Ce travail de recherche vise à caractériser les propriétés hydrodynamiques des sols des Cévennes, une zone de moyenne montagne du sud de la France connue pour être sujette à des crues à cinétique rapide, appelées « crues éclair ». Il s'agit donc de déterminer les paramètres relatifs à la conductivité hydraulique et à la rétention en eau du modèle de Mualem-van Genuchten, leur variabilité spatiale à l'échelle du versant ou du petit bassin, et les facteurs qui expliquent cette variabilité spatiale. Il s'agit également d'évaluer la perméabilité du sous-sol constitué d'une roche plus ou moins altérée, et d'en déduire des informations sur les processus de saturation des sols pouvant être à l'origine de ruissellement.Les propriétés hydrodynamiques des sols et du sous-sol ont été estimées par modélisation inverse de la teneur en eau sols, à partir d'une station pilote sur le site de Sumène et d'un réseau de 50 stations de mesure répartis sur 4 versants granitiques (site de Valescure) et 2 versants schisteux (site de Tourgueille). La station pilote comprend 3 sondes de mesure installées à 20, 40, 60 cm de profondeur, et les stations installées sur les versants comprennent chacune 2 sondes de mesure installées à des profondeurs variables allant de 15 à 45 cm. Les teneurs en eau du sol ainsi que les précipitations ont été mesurées en continu au pas de temps 15 min sur les différents sites. La procédure de modélisation inverse est basée sur l'algorithme génétique multi-objectif NSGA-II. Cette procédure a été appliquée pour chaque station, en considérant que le sol d'épaisseur variable constitué de la superposition de 2 horizons, surmontant un troisième horizon figurant la roche altérée sous-jacente. Au total, quinze paramètres doivent être calibrés pour chaque station, et sont estimés à partir de périodes sélectionnées correspondant aux épisodes de pluie les plus importants. Les processus d'évapotranspiration ont été considérés comme négligeables au cours de ces épisodes. L'analyse des propriétés de rétention et de conductivité obtenues a mis en évidence la très forte conductivité hydraulique des sols étudiés, de l'ordre de 1000 à 2000 mm/h, et leur faible rétention en eau. Les teneurs en eau à saturation estimées s'échelonnent de 0.30 à 0.60 cm3.cm-3, traduisant une grande hétérogénéité locale. On retrouve cette forte variabilité pour l'estimation des profondeurs de sol qui varient de 31 à 120 cm. Pour l'horizon représentant le sous-sol, les perméabilités sont très contrastées, avec des valeurs de conductivités hydrauliques variant de quelques unités à plus d'une centaine de mm/h. Les stations présentant les sols les moins profondes et des sous-sols moins perméables génèrent des zones saturées qui se développent à la base du profil de sol, comme ça a été observé et simulé lors des épisodes pluvieux les plus intenses. Si les propriétés des sols apparaissent très variables d'une station à une autre et d'un versant à un autre, les résultats n'ont pas montré d'organisation particulière de cette variabilité spatiale. La position de la station sur le versant n'apparaît pas être déterminante pour les porosités, les profondeurs, les perméabilités et les rétentions en eau des sols ; les distributions de ces propriétés, calculées à l'échelle des différents versants, ne semblent pas reliées aux grands traits du paysage : géologie, orientation, végétation. / This research work aims to characterize soil hydrodynamic properties of the Cévennes area, a low mountain region known to be prone to flash floods. We thus chose to estimate hydraulic conductivity and water retention properties of the Mualem –van Genuchten model and their spatial variability at the hillslope scale and between multiple hillslope profiles. The objectives are also to evaluate the weathered bedrock permeability, and consequently to enhance our understanding of the soil saturation processes.The soil and bedrock hydrodynamic properties were estimated by inverse modelling of soil moisture from a pilot station and a network of 50 stations distributed on 4 granitic hillslope and 2 schist hillslope. The pilot station was instrumented with 3 soil moisture sensors located at 20, 40 and 60 cm deep whereas the hillslope stations were instrumented with 2 soil moisture sensors located variably from 15 to 45 cm deep. Both soil moisture and precipitation were recorded with a 15 min time step for every station. The inverse modelling procedure is based on the multi-objective genetic algorithm NSGA-II. This procedure was used for every station considering a variably deep soil composed by 2 layers surmounting a 100 cm deep third layer representing the weathered bedrock. Fifteen parameters were calibrated for every station, and were estimated from small selected rainfall periods of 1 to 15 days corresponding to the major rainfall events during the monitoring period. Evapotranspiration has been considered as negligible during those events. The analysis of those retention and conductivity properties shows a very important hydraulic conductivity for the studied soils, ranging from 1000 to 2000 mm/h, and their low retention capacity. The soil saturated water content varies from 0.30 to 0.60 cm3.cm-3, which is a consequence of the important soil heterogeneity at the hillslope scale. We also find that heterogeneity on the estimation of soil depth which varies from 31 to 120 cm. For the weathered bedrock layer, we also found contrasted permeability varying from a few units to a hundred of mm/h. Stations with the shallowest soils and the less permeable bedrock presenting a saturation process at the soil/bedrock contact, as monitored and simulated during the most intense rainfalls. If the estimated soil hydrodynamic properties exhibit important variations at the hillslope scale from a station to another, results showed no specific spatial organization of this variability. The station's position on the hillslope is not decisive to estimate saturated soil moisture, soil depth, soil permeability or water retention capacity. The distribution of those properties, calculated for the 6 studied hillslope is not either correlated to the landscape general characteristic: geology, orientation, land cover.

Un modèle structurel est fourni afin d'appréhender les phénomènes de capacité dans un modèle d'affectation de flux de voyageurs sur un réseau de transport collectifs. Cela a été fondé sur une représentation du réseau de transports collectifs en deux couches : sur la couche inférieure, le modèle traite séparément chaque sous système du réseau (ligne, station et rabattement) en fonction des effets de capacité spécifiques ; sur la couche supérieure, le choix d'itinéraire d'un voyageur individuel est adressée par une représentation du réseau en leg (ou segment de ligne) en utilisant le coût et les caractéristiques opérationnelles des sous-systèmes respectifs. On établit une cadre novateur pour modéliser les effets de capacité et on développe le modèle CapTA (pour Capacitated Transit Assignment). Il s'agit d'un modèle d'affectation de flux systémique et modulaire. Il adresse les phénomènes de capacité ci dessous : La qualité du service en véhicule est liée au confort de voyageurs à bord. L'occupation d'états de confort hétérogènes (places assises, strapontins et debout à de densités de voyageurs variables) influence la pénibilité perçu du voyage ; La capacité du véhicule à la montée impacte le temps d'attente de voyageurs et leur distribution aux missions disponibles ; La capacité de l'infrastructure de la ligne établit une relation entre le temps de stationnement des véhicules (and par extension les flux de voyageurs en montée et en descente) et la performance des missions et leur fréquence de service. Ces phénomènes sont traités par ligne d'exploitation sur la base d'un ensemble des modèles locaux qui rendent de flux et de coût spécifiques. Par conséquent, ils modifient les conditions locales d'un trajet en transports collectifs pour chaque voyageur individuel. Cependant, ils doivent être adressés dans le cadre d'un réseau de transports collectifs afin de recueillir leur effet sur les choix d'itinéraire sur le réseau ; essentiellement sur les arbitrages économiques qui impactent le choix entre itinéraires alternatifs. Leur traitement sur la couche réseau garantir la cohérence du choix d'itinéraire. Le modèle de station traite de contraintes de capacité spécifiques et évalue les conditions locales de marche, qui est sensible aux interactions des voyageurs à l'intérieur de la station : le goulot instantané à l'entrée d'un élément de circulation retard l'évacuation de la plateforme ; la densité de voyageurs et l'hétérogénéité des leur flux ralenti les voyageurs qui circulent dans une station ; la présence de l'information en temps réel influence le processus de décision des voyageurs. Ces effets n'ont pas seulement un impact sur le choix d'itinéraire à l'intérieure de la station, mais notamment ils modifient les choix de service sur le niveau du réseau. La Région Ile-de-France fournit un champ d'application idéal pour un modèle d'affectation de flux de voyageurs en transport collectifs sous contraintes de congestion. Plus précisément, il est utilisé dans le cadre du modèle CapTA pour illustrer les capacités de simulation et la finesse de l'approche de modélisation adoptée. Le réseau de transports collectifs contient 1 500 missions de cars et autocars, tout comme 260 missions ferroviaires et inclut 14 lignes de métro et 4 lignes de tramway. L'affectation de trafic à l'heure de pointe du matin est caractérisée d'une charge importante en voyageurs sur les sections centrales de lignes ferroviaires qui traversent la ville. Un temps de stationnement élevé, en raison de flux de montée et descente, et la réduction de la fréquence de service impactent la capacité des missions et des lignes. Le temps généralisé d'un trajet est impacté notamment de sa composante de confort à bord. De résultats détaillés sont présentés sur le RER A, la ligne la plus chargée du réseau ferroviaire régional / A structural model is provided to capture capacity phenomena in passenger traffic assignment to a transit network. That has been founded on a bi-layer representation of the transit network : on the lower layer the model addresses each network sub-system (line, station and access-egress) separately, on the basis of specific capacity effects ; on the upper layer a leg-based representation is used with respect to the sub-systems' costs and operating characteristics to address the trip maker's path choices. We establish a novel framework for modelling capacity effects and develop the CapTA network model (for Capacitated Transit Assignment). It is systemic and modular and addresses in particular the following capacity phenomena, the in-vehicle quality of service is linked to the comfort of the passengers on-board. The occupation of heterogeneous comfort states (seats, folding seats and standing at different passenger densities) influences the perceived arduousness of the travel ; the vehicle capacity at boarding influences the waiting time of the passengers and their distribution to the transit services ; the track infrastructure capacity relates the dwelling time of the vehicles (and by extent the alighting and boarding flows) with the performance of the transit services and their service frequency. These phenomena are dealt with by line of operations on the basis of a set of local models yielding specific flows and costs. Accordingly, they modify the local conditions of a transit trip for each individual passenger. However, these should be addressed within the transit network in order to capture their effect on the network path choices; essentially the economic trade-offs that influence the choice between different network itineraries. Their treatment in a network level assures the coherence of the path choice. Equivalently, a station sub-model addresses specific capacity constraints and yields the local walking conditions, sensible to the interaction of the passengers in the interior of a station : the instant bottleneck created at the entry of the circulation elements delays the evacuation of the station platforms; the passenger density and presence of heterogeneous passenger flows slows down the passengers who circulate in the station; and the presence of real-time information influences the decision making process of the transit users exposed to. These effects do not only impact locally the in-station path choice, but most notably they modify the choices of transit routes and itineraries on a network level. The Paris Metropolitan Region provides an ideal application field of the capacity constrained transit assignment model. It is mainly used as a showcase of the simulation capabilities and of the finesse of the modelling approach. The transit network involves 1 500 bus routes together with 260 trains routes that include 14 metro lines and 4 light rail lines. Traffic assignment at the morning peak hour is characterized by heavy passenger loads along the central parts of the railway lines. Increased train dwelling, due to boarding and alighting flows, and reduction in the service frequency impact the route and the line capacity. The generalized time of a transit trip is impacted mainly though its in-vehicle comfort component. Detailed results have been provided for the RER A, the busiest commuter rail line in the transit network

Ce travail de thèse, réalisé dans le cadre d’une collaboration avec la société Hispano-Suiza (groupe SAFRAN) porte sur la modélisation et l’analyse des vibrations et surcharges dynamiques sur les engrènements d’un réducteur aéronautique multi-étage constitué de plusieurs cascades d’engrènements situés dans des plans décalés. Une modélisation originale est proposée qui repose sur le couplage entre la résolution des équations du mouvement et la prise en compte des conditions de contact instantanées sur l’ensemble de tous les engrènements. Le modèle gère les phases relatives entre engrènements ainsi que l’influence des modifications de corrections de forme des dentures. En s’appuyant sur de nombreux exemples d’application, il est montré que des corrections de profil linéaires et symétriques adaptées permettent d’abaisser très sensiblement le niveau de surcharges dynamiques sur une plage de vitesse de rotation importante. Il est également confirmé que les efforts dynamiques sur les engrènements sont fortement corrélés aux amplitudes des variations temporelles des erreurs de transmission locales pour un fonctionnement quasi-statique sous charge. Considérant différentes architectures de transmissions, des optimisations conduites grâce à un algorithme génétique montrent que les paramètres optimaux de corrections de profil sont à choisir au voisinage d’une ‘courbe maîtresse modifiée’, initialement définie pour un seul engrènement et dont les propriétés semblent pouvoir être extrapolées à des systèmes avec plusieurs engrènements simultanés. Les résultats de simulations prouvent que l’ensemble des corrections sélectionnées sur les courbes maîtresses modifiées améliorent sensiblement le comportement dynamique des systèmes d’engrenages multi-étages. En revanche, pour des systèmes soumis à des niveaux de charge différents, des corrections optimales courtes semblent plus adaptées en termes de dynamique de l’engrènement tandis que des corrections optimales longues semblent plus efficaces en ce qui concerne le niveau de contraintes en pied de dents. / This research work, conducted in cooperation with Hispano-Suiza (SAFRAN group), is focused on the modelling and analysis of vibrations and dynamic loads in aeronautical multi-mesh gears comprising several spatial gear arrangements (idler gears, several pinions on one shaft). An original model is presented which relies on the simultaneous solution of the equations of motion and the instant contact conditions for all the tooth contacts and all the meshes. The phasing between the various meshes along with tooth shape modifications are integrated in the simulations. Based on a number of simulation results, it is shown that linear symmetric profile modifications can substantially reduce dynamic tooth loads over of broad range of speeds. It is also confirmed that dynamic mesh forces are strongly correlated with the time-variations amplitudes of local quasi-static transmission errors under load. Considering several gear arrangements, tooth profile optimisations have been performed using a genetic algorithm which indicate that optimum reliefs always lie in the vicinity of the so-called ‘modified Master Curve’ initially defined for a single pinion-gear pair. This finding suggests that the concept of Master Curve can probably be extended to more complex gear systems. The simulation results prove that all the optimal profile modifications on the Master Curve improve the dynamic tooth loading conditions in multi-mesh gears. However, for systems submitted to several load levels, short optimal reliefs seem preferable whereas long optimal reliefs are more effective in terms of root stresses.

Ce manuscrit de thèse présente l’étude des processus d’émission de deux types de noyaux actifs de galaxie détectés aux rayons gamma : des blazars vues au TeV et des Narrow Line Seyfert 1s (NLS1s) détectés au GeV. La distribution spectrale d’énergie des blazars peut être décrite en général par des modèles 'one-zone synchrotron self-Compton'. Ce modèle a été appliqué au blazar 1ES2322-409 qui fut premièrement détecté au TeV par l’expérience HESS. Des composantes externes comme le tore, le disque d’accrétion, la couronne X ou la 'Broad Line Region' sont nécessaires pour expliquer la radiation observée dans des NLS1 qui émettent des rayons gamma. Un modèle numérique qui considère ces champs des photons externes a été développé. Ce modèle explique l’émission observée et la transition entre des états bas et des états d’émission augmentée pour trois NLS1s vues au régime gamma : 1H0323+342, B20954+25A et PMN J0948+0022. / This thesis manuscript presents the study of the emission processes of two types of gamma-emitting active galactic nuclei: TeV-detected blazars and GeV-detected Narrow Line Seyfert 1s (NLS1s).The Spectral Energy Distribution (SED) of TeV blazars can in general be well described by simple one-zone synchrotron self-Compton models. Such model has been applied to the blazar 1ES2322-409 that was first detected at TeV by the HESS collaboration.Additional external photon fields such as the obscuring torus, the accretion disc, the X-ray corona or the broad line region are necessary to describe the observed radiation and broad-band SED of gamma-emitting NLS1s. A numerical model that takes into account emission from these external fields has been developed. The model explains the observed emission and the transition from quiescent to gamma-ray flaring states of three gamma-emitting NLS1s: 1H0323+342, B20954+25A and PMN J0948+0022.

La mobilité est une composante importante de la liberté des personnes. L’évolution des moyens technologiques y contribue au premier chef. Outre la question du transport, celle du maintien du lien entre les individus est en ce sens particulièrement prégnante. Elle a mis à rude épreuve la notion de réseaux de télécommunications puisqu’il s’agit de répondre, pour des individus éparpillés ou concentrés, mais mobiles, au besoin de rester reliés. De l’ère des réseaux analogiques à celle des réseaux numériques, de l’ère des réseaux filaires à celle des réseaux sans fil et mobiles, la technologie n’a cessé d’évoluer. Ces dernières décennies ont vu apparaître des réseaux numériques sans fil, où non seulement il y a mobilité des utilisateurs mais aussi mobilité de l’infrastructure du réseau à laquelle ils contribuent. Ces réseaux se constituent de façon spontanée. Ils se maintiennent de manière autonome. On les désigne par le terme réseaux ad hoc mobiles (en anglais Mobile Ad hoc Networks ou MANET) qui s’oppose naturellement à celui de réseaux à infrastructure. La sécurité est une préoccupation générale des êtres humains. Ils en ressentent aussi le besoin en matière de réseaux. Ce besoin est particulièrement criant lorsque sont échangées des données critiques, financières ou stratégiques. La confidentialité des échanges, l’authentification des sources, l’assurance d’intégrité, la prévention de la récusation sont autant d’objectifs qu’il faut alors atteindre. Diverses solutions de sécurité ont été conçues dans cette optique pour les réseaux filaires puis ont ensuite été adaptées aux réseaux sans-fil et mobiles. Les architectures AAA (Authentication, Authorization, Accounting) en font partie. Elles sont en général utilisées dans un contexte commercial. Tant par leur facilité de déploiement que par la baisse des coûts de mise en œuvre qu’ils engendrent, les réseaux ad hoc mobiles, après avoir bien servi dans le domaine militaire, semblent avoir un avenir dans les applications commerciales. C’est pourquoi, nous nous proposons dans cette thèse de concevoir une architecture AAA adaptée aux spécificités de ces réseaux. Nous étudions d’abord les réseaux ad hoc mobiles et leurs caractéristiques. Ensuite, nous présentons les solutions de sécurité qui existent dans les réseaux à infrastructure. Nous examinons, en particulier, les solutions qui permettent le contrôle d’accès et dont sont engendrées les architectures AAA. Les solutions AAA proposées pour les MANETs sont par la suite analysées et classifiées afin de déterminer les manques et les vulnérabilités. Cette étude approfondie nous amène à proposer une architecture AAA répondant aux attentes identifiées. C’est une architecture distribuée qui répond, en particulier, au besoin d’autonomie des opérations dans les MANETs et où les protocoles exécutés peuvent impliquer simultanément plus de deux parties. Un ensemble de protocoles et de mécanismes d’authentification et d’autorisation s’intégrant avec la suite des protocoles IPv6 a été proposé. Leur sécurité a été discutée. Celle, en particulier du protocole d’authentification a fait l’objet de validation formelle. Contrairement aux protocoles utilisés dans la phase d’autorisation des services AAA proposés, le mode de communication multi-parties et multi-sauts du protocole d’authentification nous a poussé à mener une analyse approfondie de ses performances. Pour cela, nous avons eu recours, dans un premier temps, à la modélisation au moyen de calculs mathématiques explicites ensuite à la simulation. Les résultats obtenus montrent que ce protocole passe à l’échelle d’un MANET comprenant au moins cent nœuds. Dans certaines conditions d’implémentation que nous avons définies, ses performances, tant celle liée à sa probabilité de terminaison avec une issue favorable que celle portant sur son temps d’exécution, atteignent des valeurs optimales. / Mobility is an important component of people’s liberty. The evolution of technological means contributes to its enhancement. In addition to the transport issue, the question of keeping people connected is, in that context, particularly significant. Technological change strained the notion of telecommunications networks in the sense that scattered or clustered but mobile individuals had to remain in touch with others electronically. From the age of analogue networks to the digital networks era, from wired networks to wireless and mobile networks, technology has never stopped evolving. The last decades have witnessed the emergence of digital and wireless networks where not only the users, but also the network infrastructure to which they contribute, are mobile. These networks are spontaneously formed and autonomously maintained. They are termed Mobile Ad hoc Networks (MANETs), in contradistinction to infrastructure networks. Security is a general concern of human beings. They feel the need for it when using a network, too. This need is particularly glaring when it comes to exchanging critical, financial or strategic data. Confidentiality of communications, source authentication, integrity assurance, prevention of repudiation, are all objectives to be achieved. Various security solutions have been devised in this context as wired networks were then adapted to wireless and mobile networks. AAA (Authentication, Authorization and Accounting) frameworks are among these solutions. They are generally used for commercial purposes, which raises financial issues — and we all know how much important they are. Due to their ease of deployment and inexpensive implementation, MANETs, first used in the military field, seem to have a future in commercial applications. That is why the present thesis proposes to design an AAA service that is adapted to the characteristics of such networks. In this perspective, the thesis examines, to begin with, mobile ad hoc networks in order to understand their characteristics and potentials. It then probes the security solutions that exist in infrastructure networks, with special emphasis on those dealing with access control and AAA services. The AAA solutions for MANETs proposed up to now are subsequently analyzed and classified in order to determine their strengths and weaknesses. This in-depth study led to the design, in the second part of the thesis, of an AAA service that meets the expectations identified. It is a distributed service intended to answer the needs of autonomous operations in MANETs when a nearby operator is absent. It features several detailed authentication and authorization mechanisms and protocols with an authentication protocol simultaneously involving one or more parties. These protocols are designed such that they can be easily integrated to the IPv6 protocols suite. Moreover, their security is discussed — in particular, that of the authentication protocol thanks to a formal validation tool. Unlike the communication mode of the authorization protocols, that of the authentication protocol is one-to-many, which led us to study more deeply its performances thanks to modeling using explicit mathematical computations and to simulations techniques. The obtained results showed that the protocol scales for a MANET including a hundred nodes. Under certain conditions that we explained, its performances, in terms of the probability of authentication success and the length of the executing time, reach optimal values.

De nos jours, divers systèmes ou organisations peuvent collaborer et échanger des informations ou des services. Ainsi grâce à cette collaboration, ces derniers vont pouvoir travailler ensemble et mener des échanges afin d'atteindre un but commun. Ceci ne peut pas être réalisé sans des problèmes de sécurité. Pour collaborer chaque participant doit définir une politique d'interopérabilité. Cette politique sera en charge de : (i) définir les informations et les ressources partageables et (ii) définir les privilèges d'accès des utilisateurs qui participent à un projet commun qui nécessite une collaboration. Pour garantir un certain niveau de sécurité, il est indispensable de vérifier si le comportement des systèmes des différents participants respecte bien leurs politiques de sécurité. Pour atteindre cet objectif, nous proposons une méthode pour tester les politiques d'interopérabilité en se basant sur deux approches différentes de test : l'approche active et l'approche passive. Le principe de test actif consiste à générer automatiquement une suite de scenarios de test qui peuvent être appliqués sur un système sous test pour étudier sa conformité par rapport à ses besoins en matière de sécurité. Quant au test passif, il consiste à observer passivement le système sous test sans interrompre le flux normal de ses opérations. Dans notre étude nous avons remarqué que les techniques de test actif et passif sont complémentaires pour tester les politiques d'interopérabilité contextuelles. Une politique est dite contextuelle si l'activation de chacune de ses règles est conditionnée par des contraintes qui peuvent être liées à l'environnement de la collaboration ou à chaque participant. Afin de pouvoir générer automatiquement les scenarios de test, il est indispensable de modéliser les politiques d'interopérabilité et le comportement fonctionnel des participants. Dans cette thèse, nous proposons une méthode pour intégrer les politiques d'interopérabilité dans les modèles fonctionnels des participants afin d'obtenir un modèle sécurisé des participants. Le comportement fonctionnel des participants est modélisé par un modèle formel basé sur des automates à états finis. Tandis que les besoins de sécurité sont spécifiés en utilisant le modèle formel OrBAC et son extension O2O. De plus, nous proposons une méthode fondée sur la technique de model checking pour vérifier si le comportement des modèles utilisés dans notre processus de test respecte bien les politiques de sécurité. La génération de cas de test est ensuite effectuée en utilisant un outil développé dans notre laboratoire. Cet outil permet d'obtenir des cas de test abstraits décrits dans des notations standards (TTCN) facilitant ainsi leur portabilité. Dans l'approche de test passif, nous spécifions la politique d'interopérabilité que le système doit respecter en utilisant un langage temporel de premier ordre. Nous analysons ensuite les traces d'exécutions des participants afin d'élaborer un verdict sur leur conformité par rapport à la politique d'interopérabilité. Finalement, nous avons appliqué nos méthodes sur un cas d'usage d’un réseau hospitalier. Cette application permet de démontrer l’efficacité et la fiabilité des approches proposées / Nowadays, there is an increasing need for interaction in business community. In such context, organizations collaborate with each other in order to achieve a common goal. In such environment, each organization has to design and implement an interoperability security policy. This policy has two objectives: (i) it specifies the information or the resources to be shared during the collaboration and (ii) it define the privileges of the organizations’ users. To guarantee a certain level of security, it is mandatory to check whether the organizations’ information systems behave as required by the interoperability security policy. In this thesis we propose a method to test the behavior of a system with respect to its interoperability security policies. Our methodology is based on two approaches: active testing approach and passive testing approach. We found that these two approaches are complementary when checking contextual interoperability security policies. Let us mention that a security policy is said to be contextual if the activation of each security rule is constrained with conditions. The active testing consists in generating a set of test cases from a formal model. Thus, we first propose a method to integrate the interoperability security policies in a formal model. This model specifies the functional behavior of an organization. The functional model is represented using the Extended Finite Automata formalism, whereas the interoperability security policies are specified using OrBAC model and its extension O2O. In addition, we propose a model checking based method to check whether the behavior of a model respects some interoperability security policies. To generate the test cases, we used a dedicated tool developed in our department. The tool allows generating abstract test cases expressed in the TTCN notation to facilitate its portability. In passive testing approach, we specify the interoperability policy, that the system under test has to respect, with Linear Temporal logics. We analyze then the collected traces of the system execution in order to deduce a verdict on their conformity with respect to the interoperability policy. Finally, we show the applicability of our methods though a hospital network case study. This application allows to demonstrate the effectiveness and reliability of the proposed approaches

Le vieillissement du patrimoine routier est observé dans la plupart des pays du monde, générant des besoins croissants en matière de travaux d'entretien et de réparation des chaussées. Dans un contexte de contraintes économiques et environnementales de plus en plus exigeant, ces travaux nécessitent souvent encore le développement de solutions techniques appropriées, résistantes et durables dans le temps. Se pose alors le problème de l'évaluation prévisionnelle de ces techniques, qui doit se faire sans attendre les longs délais nécessaires aux enseignements provenant avec le temps des retours d'expérience sur chaussées réelles. Dans le cadre de la présente thèse Approche expérimentale et numérique de la fissuration réflective des chaussées, on s'intéresse aux sollicitations mécaniques gouvernant les mécanismes de remontée de la fissuration à travers les couches de surface bitumineuses. Il peut s'agir de la fissuration régnant dans les couches d'assise de chaussées dégradées ayant fait l'objet de travaux de renforcement et également de celle régnant dans les couches d'assise en matériaux traités aux liants hydrauliques de chaussées semi-rigides neuves. L'objet est de caractériser ces sollicitations afin de définir les protocoles de chargement aussi réalistes que possible pour piloter le banc de fissuration MEFISTO en cours de développement du Laboratoire Régional d'Autun. Cet équipement permettra d'étudier en laboratoire le comportement de matériaux bitumineux. Pour la détermination de ces protocoles, la démarche générale guidant le déroulement de notre travail s'articule selon deux principales phases. Dans une première phase, le phénomène de remontée de la fissuration est étudié sur des planches de chaussées expérimentales soumises à un trafic accéléré à l'aide des simulateurs de trafic lourd FABAC du LCPC. Ces essais mettent en évidence un délaminage systématique et très rapide avec le trafic de l'interface entre le rechargement bitumineux et son support fissuré. La remontée de la fissuration dans l'enrobé résulte alors de l'endommagement par fatigue sous l'effet des contraintes de traction par flexion induites par ce délaminage. L'interprétation des résultats expérimentaux conduit à proposer un modèle numérique aux éléments finis 3D, permettant de reproduire les états initiaux de sollicitations dans la couche de rechergement bitumineuse. Le modèle met en ½uvre le logiciel CESAR-LCPC . Dans une deuxième phase ce modèle numérique est utilisé pour déterminer les conditions de pilotage de la machine de fissuration MEFISTO. La démarche proposée est illustrée par un exemple de chaussée tiré du Catalogue de dimensionnement SETRA/LCPC. Elle repose sur la minimisation des écarts entre les efforts supportés par le matériau dans la chaussée réelle et le matériau testé à proximité de la fissure. Cette démarche nous conduit à proposer une position optimale des vérins verticaux, ainsi que des trajets de chargements complètement définis. Ces résultats pourront être utilisés pour la réalisation prochaine des tout premiers essais. Il reste encore à tester et à valider la pertinence de la démarche, qui sera à juger en fonction de la représentativité de l'essai MEFISTO par rapport au comportement de chaussées réelles, sans doute après quelques adaptations. Ceci sera possible lorsque le banc en cours de modification sera à nouveau opérationnel.