Les systèmes distribués sont au cœur des technologies de l'information. Il est devenu classique de s'appuyer sur multiples unités distribuées pour améliorer la performance d'une application, la tolérance aux pannes, ou pour traiter problèmes dépassant les capacités d'une seule unité de traitement. La conception d'algorithmes adaptés au contexte distribué est particulièrement difficile en raison de l'asynchronisme et du non-déterminisme qui caractérisent ces systèmes. La simulation offre la possibilité d'étudier les performances des applications distribuées sans la complexité et le coût des plates-formes d'exécution réelles. Par ailleurs, le model checking permet d'évaluer la correction de ces systèmes de manière entièrement automatique. Dans cette thèse, nous explorons l'idée d'intégrer au sein d'un même outil un model checker et un simulateur de systèmes distribués. Nous souhaitons ainsi pouvoir évaluer la performance et la correction des applications distribuées. Pour faire face au problème de l'explosion combinatoire des états, nous présentons un algorithme de réduction dynamique par ordre partiel (DPOR), qui effectue une exploration basée sur un ensemble réduit de primitives de réseau. Cette approche permet de vérifier les programmes écrits avec n'importe laquelle des interfaces de communication proposées par le simulateur. Nous avons pour cela développé une spécification formelle complète de la sémantique de ces primitives réseau qui permet de raisonner sur l'indépendance des actions de communication nécessaire à la DPOR. Nous montrons au travers de résultats expérimentaux que notre approche est capable de traiter des programmes C non triviaux et non modifiés, écrits pour le simulateur SimGrid. Par ailleurs, nous proposons une solution au problème du passage à l'échelle des simulations limitées pour le CPU, ce qui permet d'envisager la simulation d'applications pair-à-pair comportant plusieurs millions de nœuds. Contrairement aux approches classiques de parallélisation, nous proposons une parallélisation des étapes internes de la simulation, tout en gardant l'ensemble du processus séquentiel. Nous présentons une analyse de la complexité de l'algorithme de simulation parallèle, et nous la comparons à l'algorithme classique séquentiel pour obtenir un critère qui caractérise les situations où un gain de performances peut être attendu avec notre approche. Un résultat important est l'observation de la relation entre la précision numérique des modèles utilisés pour simuler les ressources matérielles, avec le degré potentiel de parallélisation atteignables avec cette approche. Nous présentons plusieurs cas d'étude bénéficiant de la simulation parallèle, et nous détaillons les résultats d'une simulation à une échelle sans précédent du protocole pair-à-pair Chord avec deux millions de nœuds, exécutée sur une seule machine avec un modèle précis du réseau.

Alors que les applications spatiales prennent une place de plus en plus cruciale dans nos vies, les coûts d'opération des satellites doivent être réduits. Ceci peut être obtenu par l'utilisation de systèmes de propulsion électriques, plus efficients que leurs homologues chimiques traditionnellement utilisés. Une des technologies de propulsion électrique la plus performante et la plus utilisée est le propulseur à effet Hall, toutefois ce système reste complexe et peu compris. En effet de nombreuses questions, concernant le transport anormal des électrons ou les interactions plasma/paroi, sont encore ouvertes.Les réponses à ces questions sont basées sur des mécanismes cinétiques et donc ne peuvent être résolues par des modèles fluides. De plus les caractéristiques géométriques et temporelles de ces mécanismes les rendent difficilement observables expérimentalement. Par conséquent nous avons, pour répondre à ces questions, développé un code cinétique bi-dimensionnel.Grâce à un modèle simplifié de propulseur à effet Hall, nous avons observé l'importance de l'instabilité de dérive électronique pour le transport anormal. Ensuite en utilisant un modèle réaliste de propulseur, nous avons pu étudier les effets des interactions plasma/paroi sur la décharge plasma. Nous avons également pu quantifier les effets intriqués des émissions électroniques secondaires et de l'instabilité de dérive sur le transport anormal. Par une étude paramétrique sur les émissions électroniques secondaires, nous avons pu identifier trois régimes de décharge plasma. Finalement l'impact des ergols alternatifs a pu être étudié en utilisant des processus collisionnels réalistes. / As space applications are increasingly crucial in our daily life, satellite operating costs need to be decreased. This can be achieved through the use of cost efficient electric propulsion systems. One of the most successful and competitive electric propulsion system is the Hall effect thruster, but this system is characterized by its complexity and remains poorly understood. Indeed some key questions, concerning electron anomalous transport or plasma/wall interactions, are still to be answered.Answers to both questions are based on kinetic mechanisms, and thus cannot be solved with fluid models. Furthermore the temporal and geometrical scales of these mechanisms make them difficult to be experimentally measured. Consequently we chose, in order to answer those questions, to develop a bi-dimensional fully kinetic simulation tool.Using a simplified simulation of the Hall effect thruster, we observed the importance of the azimuthal electron drift instability for anomalous cross-field electron transport. Then, using a realistic model of a Hall effect thruster, we were able to study the effects of plasma/wall interactions on the plasma discharge characteristics, as well as to quantify the coupled effects of secondary electron emission and electron drift instability on the anomalous transport. Through parametric study of secondary electron emission, three plasma discharge regimes were identified. Finally the impact of alternative propellants was studied.