Il est propose dans cette thèse une méthode de composition modulaire de systèmes à partir d'éléments pouvant exister en plusieurs versions, ainsi qu'une base de données. Conservant les relations de compositions de versions. La réalisation de systèmes complexes s'accompagne de la vérification automatique de contraintes de composition. Une réalisation prototype de la base a été effectuée dans le cadre du projet ADELE

Ce travail porte sur le test structurel des programmes réactifs synchrones érits en Lustre et sur la définition de critères de couverture pour assurer ce test structurel. Lustre est un langage réactif synchrone flot de données, largement utilisé pour la spécification et la programmation des applications critiques dans des domaines comme l'aéronautique, l'énergie ou les transports. L'application à Lustre des critères de couverture usuels basés sur le flot de contrôle (couverture des instructions, couverture des branches,...) n'est pas significative. <br /><br />Nous avons, en conséquence, défini une hiérarchie de critères adaptés au paradigme flot de données synchrone. Les critères permettent de mesurer la couverture des chemins dans un réseau d'opérateurs. Un réseau d'opérateurs est une modélisation graphique des flots de données dans un programme Lustre. Les critères sont basés sur le calcul symbolique des conditions d'activation de ces chemins. <br /><br />Un outil nommé Lustructu, a été réalisé pour mesurer la couverture atteinte par un jeu de tests selon ces critères. Lustructu analyse le programme sous test et calcule les chemins et leurs conditions d'activation. L'évaluation de la couverture par Lustructu est non-intrusive (pas d'instrumentation du code). L'applicabilité et la pertinence des critères ont été évaluées sur une étude de cas significative issue du secteur de l'aéronautique.

L'évolution constante des processeurs vers des architectures proposant des capacités superscalaires, de parallélisme au niveau des instructions, de prédiction, de spéculation et la multiplication des niveaux de hiérarchie mémoire donnent de plus en plus d'importance au travail du compilateur.<br />Dans cette thèse, nous nous intéressons aux transformations du programme source destinées à l'optimisation dans la chaîne de compilation, et plus particulièrement à une transformation appelée décalage d'instructions.<br />Cette transformation sert de base au pipeline logiciel, elle a une influence sur le parallélisme au niveau des instructions et l'utilisation des registres.<br />Elle intervient également comme composante des techniques de parallélisation de boucles par ordonnancement affine.<br />Nous avons voulu mieux comprendre les perspectives offertes par le décalage d'instructions, savoir quels objectifs il permettait d'atteindre mais aussi savoir quels problèmes de décalage restaient difficiles.<br />Pour cela nous avons étudié le décalage d'instructions dans plusieurs contextes plus ou moins proches, et apporté des contributions à chacun d'entre eux.<br /><br />Dans le cadre du pipeline logiciel, nous proposons un algorithme polynomial pour déterminer le décalage le plus à même de produire un maximum de parallélisme au niveau des instructions, et une étude expérimentale de l'efficacité absolue de la technique à l'aide de l'outil logiciel que nous avons réalisé dans ce but : PASTAGA (pour Plate-forme d'Analyse Statistique et de Tests d'Algorithmes sur Graphes Aléatoires).<br />Dans le cadre de l'utilisation des registres (stage scheduling), de la parallélisation de boucle et de la localité, nous apportons des réponses aux problèmes de décalage d'instructions associés~: complexité, solutions exactes, approximations.

L'évolution des besoins des logiciels entraîne la croissance de la complexité des environnements répartis. La recherche effectuée dans le domaine de la conception de ces environnements vise à réduire cette complexité. Un des principaux problèmes de la conception des infrastructures réparties concerne la composition des propriétés non fonctionnelles (également appelées services techniques). Les services interagissent entre eux. Nous avons identifié deux types d'interaction : les interactions de type structurel et les interactions de type comportemental.<br />Il existe actuellement de nombreuses approches (académiques et industrielles) qui permettent de concevoir ces infrastructures.<br />Dans un premier temps, nous exposons les concepts de la composition et nous étudions les mécanismes de composition mis en oeuvre dans ces approches de conception.<br />A partir de cette étude, nous proposons une nouvelle approche de composition appelée composition comportementale qui permet de supprimer un certain nombre de limites identifiées dans les autres approches. L'approche de composition comportementale utilise le modèle de composants Fractal et introduit un modèle d'automates qui permet de décrire les comportements des composants.<br />Les interactions de type structurel s'expriment à partir du modèle de composants et se matérialisent par des liaisons entre les interfaces des composants. Les interactions de type comportemental s'expriment à partir du modèle d'automate et se matérialisent par des contraintes d'ordonnancement. Les mécanismes de composition de notre approche mettent en oeuvre ces différents types d'interaction.<br />Nous avons réalisé un canevas logiciel qui implante le modèle de composant et le modèle de comportement. Le canevas a été conçu afin que les approches de conception puisse l'utiliser. L'implantation du canevas génère un environnement d'exécution basé sur le langage synchrone réactif Esterel.<br />Pour conclure, nous positionnons notre approche avec les autres approches de conception à partir de critères d'évaluation que nous avons définis. Quelques perspectives concernant l'approche sont données.

Cette thèse adresse une recherche d'automatisation pour la conception d'architecture matérielle de systèmes monopuces.<br />L'accroissement incessant de la complexité des systèmes, l'amincissement des fenêtres commerciales et la réduction du temps accordé à la conception qui en résulte apportent une divergence non résolue entre les besoins en productivité et celle effective des équipes de concepteurs. Une réponse est proposée par l'abstraction de ces systèmes jusqu'à un niveau où les caractéristiques de l'architecture matérielle ne sont que des directives d'implémentation annotées à un modèle purement fonctionnel de l'application. Ce modèle est alors pris en charge par un flot d'étapes de raffinement automatisées, le conduisant jusqu'à un niveau de détail permettant l'utilisation d'outils de synthèse matérielle commerciaux qui, à leur tour, le transposent en silicium.<br />La contribution de cette thèse à cette méthodologie concerne la définition d'une représentation de ces architectures matérielles à chaque niveau utilisé au cours de la conception, ainsi qu'une approche d'automatisation du flot de raffinement par l'assemblage systématique de composants de bibliothèques. La pertinence de ces travaux a été évaluée par leurs applications à la conception de plusieurs systèmes dont un modem VDSL et un terminal GSM WCDMA présentés dans ce mémoire.

Cette thèse présente une approche pour la construction d'évaluateurs de requêtes adaptés aux besoins des applications et/ou à l'environnement d'exécution. L'approche proposée distingue trois types d'adaptation : statique (à la construction de l'évaluateur), personnalisée (avant l'exécution de requête ayant des contraintes spécifiques) et dynamique (pendant l'exécution de la requête). Nous avons présenté une analyse systématique des différentes dimensions d'un évaluateur. La principale contribution de cette thèse est un canevas d'évaluation de requêtes nommé QBF (Query Broker Framework). QBF présente les fonctionnalités d'un évaluateur de requêtes de manière abstraite et séparée dans le but de favoriser leur réutilisation et leur adaptation. En s'appuyant sur QBF, nous avons proposé les mécanismes pour assurer les trois types d'adaptation, à savoir l'instanciation de QBF, l'évaluation personnalisée et l'évaluation interactive de requêtes. Une implémentation de QBF ainsi que de quelques instances (i.e. évaluateurs) ont été réalisées. Elles nous ont permis de montrer la faisabilité de notre approche et le bénéfice de la séparation et de l'abstraction des fonctionnalités proposées dans QBF. Nous avons également mené une évaluation expérimentale des mécanismes implémentés (i.e. opérateurs, surveillances) afin de mesurer le surcoût de l'adaptation dans QBF et d'aider les programmeurs à choisir des éléments (ou composants) appropriés pour construire leurs évaluateurs.

Lorsque de nombreux agents interagissent, des conflits peuvent survenir. Pour les résoudre, différentes méthodes peuvent être utilisées, comme la coordination, les systèmes de vote et la négociation. Celle qui nous intéresse dans cette thèse est la négociation à base de contrats portant sur des ressources. L'objectif de notre travail est de concevoir un modèle général de négociation que nous avons appelé GeNCA : Generic Negotiation of Contracts API. Afin de concevoir un tel modèle, nous commençons par étudier les formes de négociation les plus courantes. L'analyse de ces négociations nous permet de dégager leurs points communs et nous fournit une base pour concevoir notre modèle. Grâce à la collecte de ces points communs et à l'étude du déroulement de ces négociations, nous montrons qu'il est possible de concevoir un protocole général de négociation, paramétrable, qui offre la possibilité de formuler des contre-propositions et qui permet de décrire le déroulement d'une négociation particulière.

Cette thèse porte sur la construction d'un environnement pour développer des librairies de calcul formel certifié. Nous présentons d'abord les espèces, structures servant à décrire des spécifications par héritage multiple, raffinement et paramétrisation. Les collections, construites par encapsulation d'espèces constituent la librairie utilisateur. Nous définissons également les analyses statiques garantissant la correction d'une définition d'espèce. Ensuite, nous étudions la compilation des espèces et collections vers le langage d'exécution OCAML, en utilisant les objets et modules OCAML. Puis nous détaillons la traduction dans le langage de preuves COQ, la liaison retardée étant traduite par des lambda-abstractions. Nous montrons ensuite comment utiliser cette technique pour optimiser les exécutables OCAML. Enfin, nous prouvons que les analyses faites par le compilateur ainsi que les techniques de traduction sont conforme à la formalisation des espèces faites auparavant en COQ.

Dans les deux dernières décennies, le logiciel libre a pris un essor considérable. Des distributions qui au début comptaient une centaine de paquets, en ont maintenant des dizaines de milliers, tous de provenance très différente. Ceci engendre des problèmes pour la gestion de qualité. Les outils et procédures ne sont plus adaptés à la taille et la complexité des distributions d'aujourd'hui. Dans cette thèse, nous commençons par présenter une modélisation mathématique des points communs entre les différents types de distribution (Debian et RPM); notamment le concept des paquets et des relations qui existent entre eux: les dépendances et les conflits. Cette modélisation est en partie formalisé avec l'assistant de preuves Coq. Cette modélisation sera ensuite utilisée pour proposer des relations 'sémantiques', qui sont plus adaptés que les relations existantes pour repérer et corriger des erreurs dans les distributions. Nous présentons aussi des algorithmes pour calculer ces relations d'une façon efficace, et nous utiliserons Coq pour prouver formellement les théorèmes les plus importantes utilisées par ces algorithmes. Finalement, nous avons validé les algorithmes sur des distributions existantes. Nous présenterons une analyse de la structure des distributions qui est le résultat de cette validation, ainsi qu'une discussion de la phénomène du "petit monde" en rapport avec les distributions.

C'est au travers d'un panel d'applications de conception en génie électrique, issu de mes travaux de recherche et d'encadrements doctoraux, qu'est illustrée une problématique inhérente à la " conception système ", celle des couplages. Ceux-ci interviennent au niveau de la définition des modèles du système (multi-physiques, multi-formalismes, multi-niveaux...) mais aussi au niveau des analyses possibles sur ce système (simulation dynamique, analyse de sensibilité, optimisation sous contraintes, robustesse, ...). Cette nature complexe est associée à la nature dynamique de la conception système, dans le sens où les couplages naissent en cours de processus. Ces deux caractères font que la réalisation d'outils de CAO adaptés est un véritable challenge que je cherche à relever en répondant à un ensemble d'enjeux décrits dans ce rapport. Pour ce faire, nous disposons, dans mon équipe de recherche, du framework logiciel CADES. Il constitue à la fois notre plateforme expérimentale et le réceptacle de méthodologies que nous valorisons pédagogiquement et industriellement. Mes contributions à ce framework, sont principalement méthodologiques mais également applicatives dans le domaine des MEMS magnétiques et du bâtiment intelligent. Elles sont majoritairement axées vers l'optimisation sous contraintes, en particulier par des formalismes de modélisation dédiés et des méthodes de génération automatique de calcul de Jacobien. En outre, c'est par l'approche à composants logiciels, mise en oeuvre dans CADES, que sont plus spécifiquement pris en compte les couplages dynamiques en question. Les perspectives ouvertes par ces travaux vont de la conception robuste et fiable de systèmes, à la commande optimale en temps réel, en s'appuyant sur des méthodologies de modélisation, de capitalisation et de réutilisation collaborative des connaissances, en exploitant au mieux Internet et les technologies logicielles.