The current state of knowledge-based technology is such that most application systems are built from scratch. In order to move beyond the prohibitive cost of constantly reinventing, rerepresenting, and reimplementing the wheel, researchers are beginning to examine the feasibility of building application systems with heterogeneous and reusable agents. In this dissertation, we explore a comprehensive model of distributed-search systems comprising multiple agents where each agent is a complete and independent system that represents a specific area of expertise. Our approach acknowledges the inevitability of conflict among the agents, and exploits that conflict to drive agent interaction and guide local search. A primary objective of the research is to understand how to build distributed-search systems that can integrate multiple heterogeneous computational agents. These systems must be able to: (1) solve large-scale problems; (2) take advantage of knowledge embodied in existing reusable agents; (3) effectively coordinate the actions of agents to achieve efficient and coherent problem solving; and (4) effectively manage conflicts among agents, allowing them to find high-quality solutions despite inherent inconsistency. A second objective is to understand how to build expert reusable computational agents that (1) use the most appropriate representations, algorithms, and inference engines for their area of expertise; (2) coordinate with other agents to effectively work within a team; and (3) are developed outside the scope of particular application system. In this dissertation, we introduce the conceptual model we have developed for distributed search and conflict management among reusable heterogeneous agents. We present an implemented framework that provides flexible architectural support for agent integration, coordination, conflict management, and for multiagent solution evaluation. We also describe two implemented application systems built within the framework, and report results from our experimental investigation of the efficiency and effectiveness of agent configurations within those systems.

Beaucoup d'applications des méthodes formelles reposent sur la génération de formules en logique du premier ordre et la preuve de leur satisfiabilité par rapport à une théorie en arrière-plan, qui est souvent obtenu par mélange de plusieurs théories. Dans la littérature, cette forme de satisfiabilité est appelée Satisfiabilité Modulo Théories (SMT). Dans cette thèse, on s'intéresse à la conception de procédures de décision pour les problèmes SMT, en intégrant des techniques de saturation basées sur la réécriture pour des théories finiment axiomatisées et des techniques de combinaison pour des unions de théories. La première contribution de cette thèse est une reconstruction raisonnée, dans un cadre uniforme, des méthodes de combinaison proposées par Nelson-Oppen, Shostak et d'autres. Ceci est le point de départ pour de nouvelles investigations. Nous introduisons ensuite le concept de canoniseur étendu et dérivons un résultat de modularité pour une nouvelle classe de théories, ce qui contraste avec l'absence de modularité pour la classe de théories considérée par Shostak. La deuxième contribution concerne le problème de la combinaison de procédures basées sur la réécriture en utilisant la méthode de Nelson-Oppen. Nous utilisons la méta-saturation pour développer des techniques de preuve automatique permettant de tester les conditions pour la combinabilité de telles procédures. Lorsque la méta-saturation termine pour une théorie, le résultat obtenu permet de raisonner sur la combinabilité pour cette théorie d'une procédure de satisfiabilité basée sur la réécriture. La troisième contribution de cette thèse est liée à l'intégration des procédures de décision dans les solveurs SMT. Nous considérons le problème de rajouter aux procédures de décision la capacité de construire des justifications en cas d'insatisfiabilité, sans dégradation des performances, en nous focalisant sur la construction modulaire de telles justifications pour une théorie combinée. Pour ce faire, nous étendons la méthode de combinaison de Nelson-Oppen de manière à construire de façon modulaire des justisfications d'insatisfiabilité pour des unions de théories. Nous étudions également comment les justifications obtenues peuvent être reliées à une forme appropriée de minimalité.

Cette thèse constitue une contribution au génie logiciel appliqué à la programmation d'automates. Elle est née d'abord du simple besoin concret d'une bonne librairie de manipulation d'automate ouverte, efficace, extensible et simple d'utilisation. A priori, la programmation générique en C++ semblant la plus adaptée à ces besoins (son originalité par rapport à la programmation purement objets, vient de ce qu'elle impose des contraintes sur les temps de calcul des opérations), le but était d'étendre ces techniques de programmation et leurs domaines d'application aux automates puis aux machines à états en général tout en rendant la librairie plus abordable grâce à la programmation générative et des composants actifs. Ce travail couvre de plus un besoin d'étude sur la programmation par patron en C++ : faisabilité, pouvoir d'expression et efficacité. Cette thèse espère apporter une solution viable à la programmation générique d'automates avec des concepts novateurs, une implémentation sous forme de librairie C++ ouverte et une expérimentation de programmation générative généralisant les résultats obtenus à l'ensemble des machines dont la structure est basée sur celle d'un graphe.

.

.

.

.

.

La croissance en taille et en complexité des logiciels actuels, ainsi que les contraintes du marché, rendent de plus en plus nécessaires les techniques d'ingénierie concurrente. Ces techniques servent à réduire les temps de développement en permettant à plusieurs développeurs de travailler simultanément sur les mêmes objets. Malheureusement, la concurrence pose de nombreux problèmes mal gérés par les systèmes de support à la collaboration qui existent aujourd'hui. Le contrôle de la concurrence est donc un défi pour les concepteurs d'environnements de génie logiciel. Cette thèse s'intéresse au support informatique des procédés collaboratifs de génie logiciel et, en particulier, au contrôle de la concurrence.<br />Notre proposition sera divisée en deux parties. Dans la première partie nous définissons un langage pour la modélisation des procédés de génie logiciel concurrents et nous expliquons les mécanismes qui permettent l'application dans la réalité des procédés ainsi définis. La deuxième partie propose un système dit d'augmentation de l'information contextuelle, qui prend avantage de l'existence des modèles de procédés, pour fournir aux utilisateurs une information pertinente pour leur travail.<br />La proposition est implémentée au sein du logiciel CELINE. Ce logiciel a été mis en service dans un environnement industriel au sein de deux équipes de conception de la société STMicroelectronics.

L'analyse des systèmes communiquant par file a fait l'objet d'études scientifiques nombreuses mais qui n'ont pu offrir des solutions totalement satisfaisantes. Nous proposons d'aborder ce problème dans le cadre de l'interprétation abstraite, en définissant des treillis abstraits adaptés à ce type de systèmes. Nous considérons d'abord le cas où les messages échangés sont assimilables à un alphabet fini, puis nous nous attaquons au cas, plus difficile, des messages portant des valeurs entières ou réelles. Ce problème nous amène à définir et à étudier un nouveau type d'automate, les automates de treillis. Ces automates de treillis peuvent également être utilisés pour l'analyses des programmes utilisant une pile d'appels.