La recherche du ou des services de calcul scientifique disponibles sur une grille qui répondent aux besoins d'un utilisateur, aussi appelée courtage de services, est une activité complexe. En effet, les services disponibles sont souvent conçus pour répondre de manière efficace à de nombreux besoins différents. Ceux-ci comportent donc en général de nombreux paramètres et la simple signature du service ne suffit pas pour que l'utilisateur puisse le trouver. La solution proposée dans ces travaux consiste à utiliser une description formelle du domaine d'application comportant l'ensemble des données et des opérateurs du domaine ainsi que les propriétés des opérateurs. Dans le cadre de cette thèse, cette description est effectuée sous la forme d'une spécification algébrique. Un service ou une requête sont alors des termes de l'algèbre associée. En ce qui concerne les signatures, nous combinons le sous-typage des sortes et la surcharge des opérateurs selon le système de type proposé par G. Castagna pour le λ&-calcul. Le courtage consiste alors à effectuer un filtrage modulo la théorie équationnelle associée à la spécification, entre le terme représentant le service souhaité et les termes représentant les services disponibles. Nous proposons et avons implanté deux algorithmes différents inspirés d'un parcours de l'arbre de recherche des solutions contraint par une quantité d'énergie (nombre d'équations et/ou de compositions applicables). Le premier algorithme est directement dérivé des travaux de Gallier et Snyder sur l'unification équationnelle. Nous avons montré sa correction et argumenté sa complétude (ou exhaustivité). Le second algorithme découle d'une définition constructive de l'ensemble des services qui peuvent répondre à la requête d'un utilisateur. L'algorithme consiste alors en un parcours particulier de l'arbre construit pour engendrer le service requis. Nous avons également montré sa correction, et sa complétude pour certaines formes d'équations. Nous illustrons notre approche dans les domaines applicatifs suivants : algèbre linéaire et optimisation, et nous nous intéressons au traitement de la combinaison de domaines applicatifs.

Cette thèse de recherche vient en complément des études suivies à l'école ESCP-EAP, à Paris, dans le cadre d'un mastère spécialisé en stratégie et management des systèmes d'information. Celui-ci fait suite à une formation d'ingénieur expert en systèmes et réseaux informatiques à l'Ecole Supérieure de Génie Informatique, à Paris. Ce document est divisé en trois parties à travers lesquelles il est présenté une analyse de l'intégration des logiciels libres au sein des ministères français et de leurs administrations. La première partie donne un aperçu du concept ainsi que du monde du libre et des logiciels qui le forment. Le but de cette partie est d'acquérir une meilleure compréhension du domaine " Open source ". On y trouve ainsi la présentation d'un rapide historique, d'une définition du terme et des caractéristiques des logiciels libres, des principaux enjeux qui résultent de cette technologie et de son cadre juridique, tous aspects qui constituent l'environnement dans lequel s'inscrit l'orientation des ministères vers le " libre ". La deuxième partie réunit le résultat d'une phase d'enquêtes menées auprès de différents ministères français, de leurs administrations et des responsables des directions des systèmes d'information respectifs. Il y est exposé les principales migrations vers les logiciels libres au sein de ces ministères avant de caractériser plus précisément le choix de cette reconversion, ses intérêts et ses éventuelles difficultés. La dernière partie de ce document s'attache à examiner les suites de changement. Inévitablement, des réactions antagonistes se manifestent mais qui, n'empêchent pas une réelle réflexion sur l'avenir des logiciels libres au sein des ministères. En tout état de cause, ceux-ci apparaissent comme un tremplin pour les logiciels libres dans les différents secteurs.

Nombre d'applications ont pour comportement principal l'attente d'un événement venant d'un environnement extérieur, la préparation d'un résultat et l'exécution d'actions sur cet environnement. Les interfaces graphiques et les systèmes avioniques en sont des exemples. Le paradigme SCC, pour Sense--Compute--Control, est particulièrement adapté à la description de ces applications. Le développement d'applications suivant ce paradigme est cependant rendu difficile par le manque de cadre conceptuel et d'outils de support. Cette thèse propose un cadre conceptuel dédié au paradigme SCC et se concrétise par un langage de description d'architectures nommé DiaSpec. Ce langage fournit un cadre de travail pour guider le développement d'une application SCC en assignant des rôles aux membres du projet et en proposant une séparation des préoccupations. En plus de fournir un cadre de conception, cette thèse fournit un support de programmation. En effet, à partir de descriptions écrites en DiaSpec, un framework de programmation dédié est généré dans un langage cible. Ce framework de programmation guide l'implémentation d'une application SCC en exposant les mêmes abstractions que le langage DiaSpec. Ce framework de programmation est conçu de façon à assurer que l'implémentation d'une application est conforme à l'architecture décrite en DiaSpec, en s'appuyant sur le système de types du langage cible. Les contributions de cette thèse sont évaluées suivant des critères d'expressivité, d'utilisabilité et de productivité.

Pour devenir ou rester compétitif, un opérateur télécom doit constamment enrichir ou adapter son offre de services. Cette recherche permanente d'innovation implique de rendre agiles les processus de création de service. Par agilité nous entendons non seulement la capacité à mettre rapidement sur le marché de nouvelles idées de service mais également de s'assurer de leur évolution dans un environnement technologique changeant. Dans ce mémoire de thèse nous défendons l'idée qu'une utilisation pragmatique et combinée des principes du SOA avec les technologies d'ingénierie des modèles peut être un facteur clef pour l'optimisation du processus de création de services et pour répondre aux exigences de l'agilité. L'approche que nous recommandons dans le cas des services de télécommunications que nous avons étudié (les services composites intégrés et les services vocaux) c'est d'abord d'utiliser des langages dédiés (DSL) graphiques et/ou textuels pour la spécification de haut niveau des services, ensuite d'exploiter ces spécifications dans des environnements de création et d'exécution (frameworks) orientés modèles supportant nativement le DSL, afin de permettre le test et la simulation au plus tôt des fonctionnalités du service via des itérations rapides. Enfin une automatisation importante du déploiement vers les plates-formes de production (serveurs d'application) et les terminaux mobiles (code client) via le développement de transformateurs dédiés. Le travail présenté dans cette thèse est validé par plusieurs expérimentations et démonstrations portant sur des services vocaux et des services de télécommunication intégrés composites (exploitant des ressources télécom et des facilités issues de l'industrie informatique).

Selon le Larousse, un programme informatique est un "ensemble d'instructions et de données représentant un algorithme et susceptible d'être exécuté par un ordinateur." Une forte adéquation entre instructions et données est donc nécessaire afin d'éviter tout dysfonctionnement d'un programme. Nous nous sommes ainsi intéressés ces dernières années aux analyses statiques, réalisées avant l'exécution du programme, permettant de garantir que la manipulation des données se passera correctement. Nous illustrerons nos recherches sur ce thème en considérant trois grandes familles de données: les arbres non ordonnés, les arbres ordonnés (dont XML), et les programmes eux-mêmes en tant que données. Dans chacun de ces domaines, nous avons conçu des analyses statiques, sous forme de système de types ou de bisimulations, adaptés à plusieurs problématiques telles que la manipulation de messages dans un système à composants, les langages bidirectionnels, la manipulation de XML ou les calculs de processus d'ordre supérieur avec passivation.

Le thème principal de cette recherche est d'étudier et développer des techniques pour la modélisation des systèmes où la sécurité est critique. Cette thèse est focalisé sur l'étape de la spécification du domaine où de tels systèmes vont fonctionner, et de sa validation. La contribution de cette thèse est double. D'abord, nous modélisons le domaine des transports terrestres, un bon candidat pour cette étude en raison de sa nature critique vis-à-vis de la sécurité, dans le cadre formel de B événementiel et proposent quelques directives pour cette activité. Ensuite, nous présentons une approche, basée sur les techniques de l'animation et des transformations, pour la validation par étapes des spécifications formelles.

La notion de données semi-structureées est liée au monde du web. On appelle donnée semi-structurée une donnée dont le schéma n'est pas défini a priori. Par exemple, il peut s'agir d'une page HTML, d'un site Web tout entier ou encore d'un document XML. Cette thèse étudie les requêtes sur les données modélisées par des graphes. Plus précisément, on s'intéresse à différents langages de requêtes associés. Dans le cas des graphes orientés, on utilise des techniques de réécriture et d'automates pour étudier - à des fins d'optimisation de requêtes - les contraintes d'inclusions. Elles portent sur les chemins qui permettent de naviguer dans la donnée. Par ailleurs, on génère un index d'une donnée qui préserve toutes les contraintes d'inclusions. Ensuite, on étend cette étude pour obtenir le concept de requête graphe. Appliqué au cas des documents "XML coloré", elles permettent d'étudier formellement l'expressivité et la complexité de langages de requêtes inspirés de XPath et de XQuery. Enfin, les résultats théoriques sont validés par des expérimentations.

La participation des entreprises aux logiciels libres touche des domaines différents aux sciences économiques et sciences sociales. Elle est parmi d'autres une expérience naturelle pour la production des biens publics, pour l'innovation collective, pour les technologies disruptives, pour l'externalisation des technologies ou pour les organisations décentralisées. Cette thèse se concentre sur la production des biens publics, l'innovation collective et l'externalisation des technologies. Dans notre analyse, nous utilisons une base de données de 10 000 logiciels libres trouvables sur SourceForge et lions l'information des développeurs aux profils académiques, salariés et bénévoles.

Un très grand nombre de problèmes combinatoires appartient à la famille des problèmes de satisfaction de contraintes (Constraint Satisfaction Problem ou CSP) : configuration, ordonnancement, affectation de ressources... Ces problèmes partagent une description commune qui autorise en général une modélisation claire et intuitive. Dans cette thèse, nous avons proposé et étudié une nouvelle méthode de résolution hybride pour les CSPs. Nous avons nommé cette méthode Tabu-NG pour Tabu Search based on NoGood. Le nom est un peu réducteur car il s'agit d'une hybridation d'algorithme de filtrage, de propagation de contraintes, de Recherche Tabou et de gestion de nogoods. La méthode a été appliquée sur deux types de problèmes. Le premier est l'affectation des fréquences (FAP) dans les réseaux de radiocommunications militaires, en particulier les problèmes proposés de 1993 (instances du projet européen CALMA) jusqu'à 2010 (instances d'un projet DGA). Le deuxième est le problème académique de k-coloration de graphes sur les instances DIMACS. La méthode a amélioré quelques meilleurs scores connus actuellement. Dans les deux problèmes nous avons traité des contraintes unaires et binaires, ainsi que des contraintes n-aires et de l'optimisation de fonction sous contraintes pour le FAP. Les principes de Tabu-NG sont généraux et elle peut s'appliquer sur d'autres CSP. Elle peut par ailleurs accueillir des heuristiques spécifiques aux problèmes, nous l'avons pratiqué sur les problèmes cités, et en ce sens nous pensons pouvoir qualifier la méthode de métaheuristique sans abuser de cette définition.

Les méthodes formelles pour la conception des software et hardware génèrent souvent des formules qui doivent être validées, de manière interactive ou automatique. Parmi les outils automatiques, les solveurs SMT (Satisfiabilité Modulo Théories) sont particulièrement adaptés à la résolution de ces obligations de preuve, puisque leur langage d'entrée est la logique équationnelle avec des symboles provenant de divers fragments décidables utiles tels que les symboles non interprétés, l'arithmétique linéaire et des structures de données habituelles comme les tableaux ou les listes. Dans cette thèse, nous présentons une approche pour combiner des procédures de décision et des solveurs propositionnels dans un solveur SMT. Cette approche est fondée non seulement sur l'échange d'égalités déductibles entre les procédures de décision, mais aussi sur la génération d'égalités de modèle par des procédures de décision. Cela étend très bien la procédure classique de combinaison due à Nelson-Oppen dans une simple plate-forme pour combiner sans heurts des théories convexes et non convexes. Deuxièmement, nous présentons un algorithme original pour le fragment de l'arithmétique, appelé la logique de différence, et les détails sur la façon de mettre en oeuvre une procédure de décision basée sur cet algorithme. La logique de différence est modélisée en utilisant la théorie des graphes. Les déductions et les vérification de la cohérence effectués par l'algorithme se font par des recherches de cycles négatifs et des calculs de plus courts chemins de manière incrémentale. La dernière partie de la thèse présente une variation incrémentale originale de la méthode du simplexe que nous utilisons pour construire une procédure de décision pour l'arithmétique linéaire. Comme pour la logique de différence, nous présentons les détails de la procédure de décision qui la rend approprié pour notre plate-forme de combinaison utilisée par des solveurs SMT. Les méthodes et les techniques décrites dans cette thèse ont été mises en oeuvre et sont disponibles dans notre solveur SMT open-source, veriT.