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.

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.