Le problème de l'exploitation commune de ressources limitées et coûteuses se pose très souvent dans le milieu industriel, et plus particulièrement dans le domaine spatial pour lequel les projets sont très souvent financés par plusieurs entités, pays ou organismes. L'exploitation de ces ressources doit bien entendu répondre à des critères d'efficacité, afin d'empêcher sa sous-exploitation, mais aussi à des critères d'équité, chaque agent espérant un retour sur investissement en rapport avec sa contribution financière. Nous nous sommes intéressés, au cours de ce travail de thèse, au problème de partage équitable de biens indivisibles (autrement dit d'objets) entre des agents, dont nous abordons trois aspects principaux : modélisation du problème, complexité et algorithmique. La modélisation du problème de partage que nous proposons s'inspire tout d'abord de la théorie du bien-être social et des nombreux travaux sur l'agrégation de préférences dans les problèmes de décision collective et de partage que l'on peut trouver dans le domaine du choix social et de la microéconomie. Elle s'appuie de plus sur un langage de représentation compacte inspiré des travaux sur l'expression logique de préférences. Nous nous intéressons dans un deuxième temps à la complexité du problème de partage tel qu'il a été défini, dont nous étudions deux aspects particuliers : complexité du problème de maximisation de l'utilité collective, et complexité du problème d'existence d'un partage efficace et sans envie. Enfin, dans la dernière partie du travail de thèse, nous nous penchons sur le problème de calcul d'un partage égalitariste au sens du leximin, problème pour lequel nous proposons et analysons plusieurs algorithmes fondés sur la programmation par contraintes. Ce travail de thèse s'appuie sur un problème réel d'allocation de prises de vue pour une constellation de satellites d'observation de la Terre.

Le thème de la thèse est la modélisation du trafic de données transitant sur des systèmes de communications par satellite. Les services concernés sont multiples (voix, navigation sur la toile, courrier électronique, audio/vidéo) et s’effectuent au travers d’un lien satellitaire. Après un chapitre introductif précisant le cadre de l’étude, le second chapitre introduit un modèle hiérarchique pour la description du trafic: le modèle en pyramide. Ce modèle est basé sur différents niveaux d’abstraction dénommés application, souscripteur, noeud et transport. On y introduit également des opérateurs qui manipulent les paquets au sein de chaque niveau. Le chapitre 3 est dédié à l’étude des modèles de trafic. On y aborde certains modèles théoriques ainsi que les modèles choisis pour la description des applications. Diverses méthodes pour la détermination des modèles sont envisagées. Dans le chapitre 4, un scénario de référence pour les communications aéronautiques est présenté. Le modèle hiérarchique en pyramide est utilisé et les opérateurs peuvent être décrits de façon précise. Ensuite les caractéristiques des principaux modules d’un simulateur le reproduisant sont décrites synthétiquement. Les chapitres 5, 6 et 7 présentent les résultats obtenus aux niveaux souscripteur, noeud et transport. Au niveau souscripteur, les propriétés des applications sont vérifiées et des modèlesagrégés sont dérivés. L'utilisation d'un modèle agrégé au niveau noeud étant d'un intérêt supérieur, les résultats sont ensuite étendus à ce niveau. Les équivalences entre modèles agrégés et précis sont démontrées sous différents points de vue (volume de donnée, distribution des files d’attente, …). Finalement, le dernier chapitre résume les résultats obtenus.

Avec le développement de nombreux systèmes de navigation, la nécessité de partager efficacement la bande spectrale allouée aux nombreux signaux de ces futurs systèmes est apparue. Dans ce souci, la sous-modulation BOC a été retenue pour un grand nombre de signaux GNSS. Cette sous-modulation présente non seulement de très bonnes propriétés en terme de séparation spectrale, mais apporte aussi une meilleure précision et une robustesse accrue vis à vis des multitrajets. Néanmoins, l'utilisation de cette sous-modulation BOC rend l'acquisition des signaux plus complexe. Ce travail de thèse concerne l'optimisation d'une chaîne de réception de signaux BOC, et des signaux composites dérivés du BOC. Nous avons analysé les problèmes que pose l'utilisation de cette modulation lors de l'acquisition du signal, celle-ci étant rendue ambiguë. Plusieurs algorithmes résolvant ce problème d'ambiguïté ont été évalué. Les résultats ont été validés grâce à un simulateur de récepteur. Ensuite, l'étude s'est focalisée sur l'acquisition des signaux BOC en présence de multitrajets. Après une analyse approfondie de l’impact des multitrajets sur le traitement des signaux BOC, une étude visant à obtenir une forme optimisée du discriminateur de boucle de code a été menée. Utilisant au mieux les caractéristiques des signaux BOC, ce discriminateur a été recherché sous la contrainte de lutter le plus efficacement possible contre les multitrajets sans pour autant dégrader la robustesse face au bruit. Une autre méthode originale de réduction de l'erreur due aux multitrajets basée sur un concept différent a été proposée et analysée. Cette méthode très simple affiche de très bonnes performances.

Cette thèse se propose d'étudier les fonctions CAC pour les systèmes satellitaires à capacité variable. Dans ces systèmes, la fonction CAC doit pouvoir anticiper la variation de la capacité afin de n'accepter une connexion que si la capacité reste disponible suffisamment longtemps pour la maintenir avec le niveau dé qualité requis. On parle alors de CAC adaptatif. Ce travail s'est, alors, construit autour de l'analyse de la variation de la capacité due aux phénomènes atmosphériques, de leur prédiction et des procédures FMT. L'étude des modèles d'évolution spatiotemporelle des atténuations et leur prédiction a mis en évidence leur inadéquation pour une fonction CAC. En effet, d'une part, ils agissent sur de courtes échelles de temps (quelques secondes) et d'autre part, ils sont trop complexes pour leur utilisation dans le contexte d'un système réel. Une méthodologie simplifiée a donc été proposée: séparer le cas de la survenue de la pluie sur la Gateway/NCC de celui de la pluie sur les terminaux utilisateurs. Quant à la politique d'admission, elle peut s'appuyer sur deux types de fonctions CAC. Le premier, dit CAC pessimiste, suppose que la variation de la capacité est rapide par rapport à la durée des connexions. Ainsi sa décision d'admission est prise en évaluant la capacité comme étant celle correspondante au pire cas de propagation survenant dans le système. Le second, dit CAC optimiste, supposé que la capacité du système reste constante pour une durée plus grande que les durées des connexions. Sa décision d'admission est alors prise en se fondant sur l'état courant de la capacité tout en tenant compte des conditions de transmission instantanées des terminaux.

Les travaux présentés dans ce manuscrit proposent une approche formelle pour la validation d'applications interactives Java-Swing vis-à-vis d'une spécification décrite par un modèle de tâches CTT. L'objectif de cette approche est de valider une partie de l'utilisabilité du système en s'appuyant sur l'extraction d'un modèle formel décrivant le comportement dynamique de l'application (modèle de dialogue). Cette extraction est obtenue par analyse statique du code source Java-Swing de l'application. La validation du système consiste alors à démontrer formellement que les structures d'interaction encodées dans le programme s'inscrivent bien dans les scénarii d'usage représentés en compréhension par le modèle de tâches CTT. Cette étape de validation exploite d'une part le modèle formel extrait par analyse statique et d'autre part une formalisation du modèle de tâches. La démarche d'extraction et de validation est abordée suivant deux techniques formelles distinctes : la méthode B événementielle basée sur la démonstration de théorèmes (theorem-proving), et la méthode NuSMV basée sur la vérification exhaustive de modèles (model-checking). Une étude de cas permet d'illustrer tout au long du mémoire la démarche de validation proposée suivant ces deux techniques formelles.

La documentation a rencontré des changements radicaux au cours de cette dernière décennie. Un pas important a été franchi avec l’avènement de la documentation en format électronique. La documentation opérationnelle aéronautique est elle aussi de plus en plus disponible en format électronique, et offre de nouvelles opportunités d’utilité et des défis d’utilisabilité. Nous nous attachons à étudier comment cette documentation peut être développée pour répondre à cette évolution. Grâce à une modélisation cognitive de la tâche de recherche d’information, nous catégorisons puis discutons les activités documentaires des pilotes telles que : support de performance, aide à la préparation ou entraînement. Dans ces différentes activités, l’interactivité entre le pilote et la documentation présuppose une notion de pertinence de l’information choisie. Nous utilisons la notion de contexte comme référentiel de pertinence. Notre modélisation du contexte est composée de trois catégories de descripteurs sémantiques, qui sont : les tâches, les conditions et les ressources. L’articulation de ces trois catégories de contexte définit l’ensemble des situations décrites dans la documentation aéronautique. La thèse met en application les propositions de notre modélisation en utilisant une approche centrée utilisateur. D’abord, un questionnaire sur l’utilisation de la documentation illustre les besoins des pilotes. Ensuite, deux cycles de conceptions/évaluations d’un prototype de documentation contextuelle permettent de spécifier une méthode de contextualisation de la documentation, ainsi que de proposer des interactions susceptibles de supporter les catégories d’activités documentaires des pilotes.

La performance de la requête d’intersection, nécessaire à la simulation intensive de la propagation d’ondes, et indispensable aux rendus interactifs à base de lancer de rayons, est située au coeur du travail de cette thèse. En partant des meilleures structures de recherches et algorithmes de calculs d’intersections rayon/surface présents dans l’état de l’art, ce travail s’est concentré sur l’efficacité des groupes de rayons, sources de performance supplémentaire. Cependant, à l’inverse des rayons simples, la cohérence nécessaire aux groupes de rayons pose la problématique de leur organisation spatiale pour approcher la performance optimale. Après avoir montré comment construire et traiter efficacement les groupes de rayons avec deux structures de recherche particulières, le cas des rayons à origine commune a été étudié, et optimisé, pour l’évaluation des sources ponctuelles et de l’occlusion ambiante. Pour répondre à la problématique des rendus générant aussi bien des rayons cohérents que des rayons incohérents, une solution de couplage des structures de recherche est proposée en s’appuyant sur une stratégie globale d’affectation des rayons. Une autre solution, plus générale et destinée à exploiter la cohérence dans les cas les plus difficiles, est proposée pour regrouper automatiquement les rayons selon un critère a priori de cohérence. En se plaçant dans le contexte des modèles ayant une très forte complexité géométrique, la mise en place d’une pile de rayons, ainsi que sa distribution sur une grappe de calculateurs sont proposées afin d’améliorer la localité d’accès aux données, et de fournir une solution de visualisation interactive. Pour permettre la réorganisation automatique des rayons, et donc faciliter l’exploitation des groupes de rayons, cette thèse conclut qu’il est impératif de définir une nouvelle interface de programmation, en remplacement de la simple requête d’intersection.

Ce manuscrit réunit les résultats d’études consacrées à la modélisation spatio-temporelle des affaiblissements de propagation dans la troposphère. La modélisation de ces affaiblissements est utile pour l’optimisation et le dimensionnement des dispositifs adaptatifs de gestion de la ressource des satellites de télécommunication opérant en bande Ka ou Q/V. Ce manuscrit est organisé autour de cinq articles de revues. Les deux premières contributions sont dédiées à la modélisation des distributions statistiques de contenus troposphériques en vapeur d’eau et en eau liquide à partir respectivement de mesures radiométriques et de bases de données climatiques. La troisième étude touche à l’évaluation des performances d’un système utilisant la diversité de site à partir de données de radar météorologique ; une étude de l’advection des champs précipitations et de son paramétrage par des sorties de modèles de prévision météorologique est également entreprise. Le quatrième article vise à établir une expression analytique de la distribution de la fraction d’une zone, d’une taille comparable à celle d’un faisceau satellite, affectée par la pluie ; ce modèle est établi en assimilant les champs de précipitations à des champs aléatoires. Le formalisme des champs aléatoires est repris dans le cinquième article qui propose une modélisation spatio-temporelle des champs de précipitations et des atténuations sous-jacentes à hautes résolutions et à l’échelle d’une couverture satellite continentale.

Pour les organismes nationaux et/ou internationaux, disposer d’un moyen de communication flexible et rapidement déployable sur une zone de service étendue représente un enjeu majeur. Pour assurer la sécurité des personnes dans des zones parfois difficiles d’accès, il est également important de posséder une infrastructure de communication qui fonctionne même en présence de brouilleurs. Un système satellite disposant d’une antenne réseau à rayonnement direct (DRA) associée à un formateur de faisceaux numérique (DBFN) et à un algorithme d’allocation de la ressource temps-fréquence-position permet d’atteindre ces objectifs, en réalisant un accès multiple à répartition spatiale (SDMA). Le SDMA est le couplage d’une allocation flexible de la ressource et de la formation de faisceaux adaptative. Compte tenu des contraintes spatiales, l’utilisation de traitements à faible complexité et faible support d’entraînement est nécessaire pour la mise en place d’une stratégie SDMA afin de permettre une utilisation efficace de la ressource en fréquence. Les conditions d'utilisation de tels algorithmes de formation de faisceaux requis dans le SDMA sont déterminées en fonction du contexte opérationnel rencontré. La quantification des bénéfices apportés par le SDMA montre qu’en temps de paix l’efficacité spectrale, et donc le débit des liens sont augmentés, et qu’en présence de brouilleurs, le maintien d’une partie des communications est réalisé.

Ce travail porte sur la programmation de systèmes de Contrôle-Commande. Ces systèmes sont constitués d'une boucle de contrôle qui acquiert l'état actuel du système par des capteurs, exécute des algorithmes de contrôle à partir de ces données et calcule les commandes à appliquer sur les actionneurs du système dans le but de réguler son état et d'accomplir une mission donnée. Ces systèmes sont critiques, leur implantation doit donc être déterministe, sur le plan fonctionnel (produire les bonnes sorties en réponse aux entrées) mais aussi sur le plan temporel (produire les données aux bonnes dates). Nous définissons un langage de description d'architecture logicielle temps réel et son compilateur pour programmer de tels systèmes. Il permet d'assembler les composants fonctionnels d'un système multirythme avec une sémantique formelle synchrone. Un programme consiste en un ensemble d'opérations importées, reliées par des dépendances de données. Des contraintes de périodicité ou d'échéance peuvent être spécifiées sur les opérations et un ensemble réduit d'opérateurs de transition de rythme permet de décrire de manière précise et non ambiguë des schémas de communication entre opérations de périodes différentes. Des analyses statiques assurent que la sémantique d'un programme est bien définie. Un programme correct est ensuite compilé en un ensemble de tâches temps réel concurrentes implantées sous forme de threads C communicants. Le code généré préserve la sémantique du programme original et s'exécute à l'aide d'un Système d'Exploitation Temps Réel standard disposant de la politique d'ordonnancement EDF.