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.

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 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.

L'optimisation multi-disciplinaire propose des solutions aux problèmes de conception de systèmes complexes. Le terme « optimisation multi-disciplinaire » laisse sous-entendre à tort qu'il ne s'agit que d'un problème d'optimisation. Nous lui préférons ici le terme de « conception collaborative ». En effet, l'optimisation ne représente qu'un aspect, qui ne peut être séparée du reste du problème de conception. Le but n'est pas de créer un processus automatique, mais de faciliter les échanges entre les équipes des différentes disciplines. De nombreuses méthodes, appelées communément formulations MDO (de Multi-Disciplinary Optimization), apparaissent dans la littérature (MDF, IDF, AAO, BLISS, CO). Elles proposent des stratégies permettant, d'une part, d'assurer la cohérence de la description du système complexe et, d'autre part, d'effectuer la recherche de la configuration optimale. Dans un premier temps, nous dressons un état de l'art des formulations MDO. Nous mettons en avant leurs points communs et leurs différences, afin de proposer une implémentation de la manière la plus générale qui soit. Nous proposons, avec la méthode DIVE (Discipline Interaction Variable Elimination), un cadre d'utilisation de méta-modèles au sein des formulations MDO. Le méta-modèle peut se limiter à une approximation linéaire ou quadratique. Il peut s'appuyer sur des méthodes classiques d'apprentissage, telles que les réseaux neuronaux, le Krigeage ou la SVM. Chaque méta-modèle est accompagné d'une région de confiance qui en détermine la validité. Cette approche par approximations locales et successives permet d'aborder les problèmes de grande dimension. Nous présentons des résultats obtenus avec deux cas-tests d'avions d'affaires supersoniques obtenus sous deux environnements différents (Scilab et ModelCenter).

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.

Le système de commande de vol (CDV) est un des systèmes les plus critiques à bord d'un avion. Les fonctions logicielles de ce système sont donc soumises à un effort de vérification important. Chez Airbus, le développement des fonctions critiques suit une approche basée sur des modèles formels, à partir desquels la majeure partie du code embarqué est générée. Certaines vérifications peuvent ainsi s'effectuer dès le niveau de la modélisation formelle, et sont aujourd'hui réalisées par test des modèles dans un environnement de simulation. L'objet de cette thèse est d'étudier comment une technique formelle, le model-checking, s'insère dans ces vérifications amonts. La contribution comporte trois parties. La première partie tire le bilan des études passées d'Airbus sur l'application du Model Checking au système de CDV. Nous analysons notamment les caractéristiques des fonctions de CDV, et leur impact sur l'applicabilité de la technologie. Le deuxième partie complète la précédente par une nouvelle étude, expérimentant le Model Checking sur la fonction Ground Spoiler de l'A380. Les expérimentations ont permis de consolider notre analyse du positionnement du Model Checking dans le processus Airbus. Un des problèmes pratiques identifiés concerne l'exploitation des contre-exemples retournés par le model-checker, en phase de mise au point d'un modèle. La troisième partie propose une solution à ce problème, basée sur l'analyse structurelle des parties d'un modèle activées par le contre-exemple. Il s'agit, d'une part d'extraire l'information pertinente pour expliquer la violation de la propriété cible et, d'autre part de guider le model-checker vers l'exploration de comportements différents, activant d'autres parties du modèle. Un algorithme d'analyse structurelle est défini, et implémenté dans un prototype afin d'en démontrer le concept.

Cette thèse s'intéresse aux systèmes multiagents dans lesquels les agents échangent des informations de façon à atteindre un but commun. Lors de l'échange d'informations entre agents, il est souhaitable que les agents aient un comportement coopératif, c'est-à-dire qu'ils ne se transmettent que les informations qui leur sont utiles. Nous définissons donc en logique modale quelles sont les informations utiles pour un agent étant donné un besoin en information de celui-ci. A partir de ces travaux, nous travaillons sur la notion d'agent coopératif et en proposons plusieurs définitions. Les échanges des agents sont en général réglementés par une politique d'échange d'informations. Pour qu'une telle politique soit efficace, il faut qu'elle soit cohérente et complète. Nous formalisons ces deux notions en logique déontique pour des réglementations générales. Nous proposons ensuite une méthode pour raisonner avec des réglementations incomplètes et appliquons nos résultats aux politiques d'échange d'informations. Finalement, nous analysons dans quelle mesure il est possible d'être à la fois coopératif et obéissant à une politique d'échange d'informations.

Les services de localisation de personnes et de matériels sont de plus en plus demandés. En environnement extérieur, les outils GPS offrent une réponse à cette demande croissante, avec une précision de l'ordre du mètre en espace dégagé. En intérieur, il n'existe pas d'outil aussi performant. Les solutions commerciales sont coûteuses en équipement. Les propositions de recherche, quant à elles, font appel soit à du matériel coûteux soit à une infrastructure lourde. Enfin, le succès actuel des téléphones mobiles “intelligents” auprès du grand public d'une part, et l'émergence des réseaux de capteurs dans le monde académique nous amènent à étudier des solutions viables y compris pour des mobiles ne disposant que de la réception de signaux radio. L'objectif de cette thèse est de proposer une mécanisme de localisation en intérieur à la fois peu coûteux, sans recours à des équipements dédiés du type UWB ni à des infrastructures supplémentaires, tout en offrant une précision de l'ordre du mètre. Pour cela, nous faisons l'hypothèse que l'utilisateur désirant se localiser est environné de pairs sachant estimer leur position, éventuellement de façon grossière, et que l'utilisateur peut patienter quelques instants pendant que l'algorithme de localisation s'exécute. L'utilisateur collecte alors de façon opportuniste les informations de localisation de tous ces pairs. Dans cette thèse nous étudions les performances en termes de précision d'une méthode de localisation utilisant des inégalités matricielles linéaires (LMI), en faisant varier un grand nombre de paramètres. Nous comparons systématiquement ces performances à celles de l'une des solutions les plus simples, celle du centre de gravité de tous les pairs à portée. Nous améliorons ensuite l'approche LMI en la couplant à une moyenne pondérée dans le temps, qui permet d'obtenir une bien meilleure précision proche du mètre. Enfin, nous terminons par des considérations d'implémentation. Les travaux de cette thèse ont été menés dans le cadre du projet ANR Fusion d'Information de Localisation (FIL).

Depuis l'avènement de la théorie de l'information, la question de la fiabilisation des transmissions est allée de pair avec l'évolution des technologies et des applications. La fiabilisation des transmissions couvre l'ensemble des techniques permettant de lutter contre les erreurs et les pertes d'un canal de transmission. Parmi les mécanismes existants, la fiabilisation pro-active consiste à mettre en place une redondance au niveau d'un émetteur, celle-ci permettant de compenser à priori les pertes subies par le canal. La fiabilisation pro-active trouve son sens lorsque l'émetteur ne peut avoir d'information sur l'état actuel du canal de transmission, ou lorsque elle est inutile du fait de contraintes temporelles, mais aussi lorsqu'un émetteur doit s'adapter aux contraintes de plusieurs récepteurs. Initialement, les mécanismes de fiabilisation pro-actifs utilisant cette redondance sont connus sous le nom de codes correcteurs. La problématique associée à ces codes est alors une problématique d'optimisation : il s'agit de créer des codes flexibles permettant une génération rapide de la redondance par l'émetteur et une récupération des données initiales par le récepteur à faible coût, tout en conservant la meilleure capacité de correction possible. Par extension, la question de la fiabilisation concerne également l'étude de l'impact de mécanismes de suppression de redondance sur la fiabilité d'un système. Dans des réseaux plus spécifiques, où la question de l’utilisation de la bande passante est cruciale, des mécanismes de compression protocolaire peuvent être mis en place afin de diminuer la proportion de trafic engendrée par les en-têtes protocolaires.

Pour certifier un système aéronautique, des études de Sûreté de Fonctionnement (SdF) visent à démontrer qu’il répond à des exigences de sécurité de haut niveau. La complexité des systèmes étudiés ayant évolué, les exigences à démontrer devenant toujours plus nombreuses, les analyses actuelles (e.g. arbre de défaillance) peuvent aujourd’hui présenter des limites d’utilisation. Pour aller à l’encontre de ces limites, l’Ingénierie Dirigée par les Modèles s’est développée et s’intéresse aux études de SdF. L’objectif est alors de 1) modéliser dans un langage adapté (le langage AltaRica a ici été utilisé) les comportements fonctionnels et dysfonctionnels d’un système et de ses composants en présence de défaillances, 2) s’assurer que le modèle est une abstraction valide du système réel et 3) vérifier la tenue des exigences du système par le modèle. Les travaux effectués dans cette thèse se sont intéressés aux deux premiers points. Une méthodologie a été proposée pour spécifier l’abstraction du comportement de composants de systèmes multi physiques. Des bibliothèques AltaRica ont été réalisées pour modéliser des sous-systèmes d’un turbomoteur d’hélicoptère. Les résultats obtenus via le modèle ont été comparés avec ceux des analyses existantes de SdF. Pour les projets futurs où celles-ci ne seraient plus disponibles, un processus de validation a été proposé pour caractériser le degré de revue atteint lors de la simulation d'un jeu de tests sur le modèle. Inspiré du « génie logiciel », ce processus s’étend sur trois niveaux de validation (unitaire ; intégration des composants ; modèle complet) et propose des critères de couvertures applicables et mesurables sur un modèle AltaRica.