Aujourd'hui, il existe un nombre important et croissant de sources de données, qui peuvent être des documents et des données structurées ou semi-structurées. En général, aussi bien les documents que les bases de données sont autonomes et gérés par des systèmes différents. D'autre part, beaucoup de ces sources sont reliées tout en étant sémantiquement hétérogènes : elles modélisent la même réalité externe tout en utilisant des concepts et des structures distincts. <br />Or, les organisations et les entreprises qui sont confrontées à de telles sources de données ont besoin d'en avoir une vision homogène et cohérente. La conséquence est qu'il est nécessaire de les intégrer et de disposer d'un système qui gère ces données.<br /><br />L'objectif d'un système d'intégration des données est de proposer une interface homogène pour interroger plusieurs sources, qui peuvent être hétérogènes et autonomes. Derrière une telle interface il y a plusieurs défis, parmi lesquels nous soulignons l'hétérogénéité structurelle et sémantique des sources de données, la fragmentation des données, le traitement et l'optimisation des requêtes. <br /><br />Il existe de nombreux travaux qui présentent des approches distinctes pour l'intégration des données, et chaque approche propose des solutions spécifiques à chacun des problèmes évoqués. On considère en général que ces approches appartiennent à deux grandes catégories : l'approche matérialisée et l'approche virtuelle. Cependant, on peut aussi considérer une troisième approche, dite hybride, qui propose qu'une partie des données du système intégré soit matérialisée et qu'une autre partie des données soit virtuelle.<br /><br />Dans cette thèse, nous proposons une architecture hybride pour un système d'intégration de sources de données hétérogènes, qui vise à étendre l'optimisation des requêtes à toutes les requêtes du système d'intégration. Elle permet aussi de fournir un mécanisme flexible pour traiter la mise à jour des données afin de tolérer les différentes caractéristiques des sources et de leurs données.<br /><br />Cette approche est basée sur un système d'indexation d'objets multicritères au niveau de la médiation. Dans notre approche, nous utilisons le système Osiris et son mécanisme d'indexation. Osiris est un système de gestion de bases de données et de bases de connaissance orienté objet, où une famille d'objets est définie par une hiérarchie de vues " object-preserving ". Le système d'indexation d'Osiris est un système multi-attributs, et notre approche propose la matérialisation du sous-ensemble des données directement reliées aux attributs d'indexation. <br /><br />Le système d'intégration des données proposé, IXIA, matérialise la structure d'indexation des objets sous-jacents au niveau du médiateur. Les Oids des objets, leur correspondance avec les objets des sources et les données nécessaires pour la mise à jour de l'indexation des données sont aussi matérialisées. <br /><br />Cette approche offre une plus grande flexibilité de rafraîchissement des données qu'une approche entièrement matérialisée, et une meilleure optimisation des requêtes que les méthodes entièrement virtuelles.

Le problème de l'optimisation des systèmes utilisant l'arithmétique virgule fixe est un problème d'optimisation combinatoire de complexité NP-difficile. Savoir analyser et optimiser des applications complexes et de taille réelle est le thème central de cette thèse. Une technique de type diviser-pour-régner, où un système donné est décomposé en plusieurs petits sous-systèmes organisés selon une hiérarchie est au cœur de cette approche. Cette décomposition ouvre la voie à l'évaluation rapide de la précision et au problème d'optimisation hiérarchique de la largeur des données et des opérations du système. En raison de la réduction du nombre de variables, la convergence du problème d'optimisation hiérarchique vers une solution est beaucoup plus rapide que dans le cas classique. Le modèle "Single Noise Source" (SNS) est proposé pour étudier les statistiques des erreurs de quantification. Au lieu de simplement se concentrer sur la moyenne et la variance du bruit des erreurs dues à la quantification, il fournit également des formules analytiques pour dériver les paramètres statistiques des processus aléatoires produisant les erreurs de quantification équivalentes à une simulation en virgule fixe. En présence des opérations " non-lisses " (un- smooth) telles que la décision dans les modulations QAM, les fonctions Min() ou Max(), etc., il est pour l'instant inévitable d'utiliser la simulation en virgule fixe. Une technique pour l'évaluation analytique des statistiques des erreurs de quantification en présence d'opérateurs non-lisses dans les graphes ne contenant pas de rebouclage est également proposée. Afin de tenir compte également des systèmes ayant des rebouclages, une technique hybride qui utilise le modèle SNS pour accélérer les simulations en virgule fixe est de plus proposée. Un cadre d'utilisation de l'optimisation convexe est proposé comme heuristique pour résoudre le problème d'optimisation des largeurs. Cette nouvelle technique améliore non seulement la qualité de la solution, mais permet de résoudre le problème plus rapidement que les approches itératives classiques. L'application des techniques proposées permet non seulement de réduire les coûts du système mais aussi une réduction de plusieurs ordres de grandeur dans le temps nécessaire pour optimiser les systèmes utilisant l'arithmétique virgule fixe.

Les systèmes logiciels sont devenus omniprésents se substituant à l'homme pour des tâches délicates, souvent critiques, mettant en jeu des coûts importants voire des vies humaines. Les conséquences des défaillances imposent la recherche de méthodes rigoureuses pour la validation. L'approche par automates du model-checking est la plus classique des approches de vérification automatique. Elle prend en entrée un modèle du système et une propriété, et permet de savoir si cette dernière est vérifiée. Pour cela un model-checker traduit la négation de la propriété en un automate et vérifie si le produit du système et de cet automate est vide. Hélas, bien qu'automatique, cette approche souffre d'une explosion combinatoire du nombre d'états du produit.Afin de combattre ce problème, en particulier lors de la vérification des propriétés insensibles au bégaiement, nous proposons la première évaluation d'automates testeur (TA) sur des modèles réalistes, une amélioration de l'algorithme de vérification pour ces automates et une méthode permettant de transformer un TA en un automate (STA) permettant une vérification en une seule passe.Nous proposons aussi une nouvelle classe d'automates: les TGTA. Ces automates permettent une vérification en une seule passe sans ajouter d'états artificiels. Cette classe combine les avantages des TA et des TGBA (automates de Büchi). Les TGTA permettent d'améliorer les approches explicite et symbolique de model-checking. Notamment, en combinant les TGTA avec la saturation, les performances de l'approche symbolique sont améliorées d'un ordre de grandeur par rapport aux TGBA. / Software systems have become ubiquitous in our everyday life. They replace humans for critical tasks that involve high costs and even human lives. The serious consequences caused by the failure of such systems make crucial the use of rigorous methods for system validation. One of the widely-used formal verification methods is the automata-theoretic approach to model checking. It takes as input a model of the system and a property, and answers if the model satisfies or not the property. To achieve this goal, it translates the negation of the property in an automaton and checks whether the product of the model and this automaton is empty. Although it is automatic, this approach suffers from the combinatorial explosion of the resulting product. To tackle this problem, especially when checking stutter-invariant LTL properties, we firstly improve the two-pass verification algorithm of Testing automata (TA), then we propose a transformation of TA into a normal form (STA) that only requires a single-pass verification algorithm.
 We also propose a new type of automata: the TGTA. These automata also enable a check in a single-pass and without adding artificial states : it combines the benefits of TA and generalized Büchi automata (TGBA). TGTA improve the explicit and symbolic model checking approaches. In particular, by combining TGTA with the saturation technique, the performances of the symbolic approach has been improved by an order of magnitude compared to TGBA. Used in hybrid approaches TGTA prove complementary to TGBA.
 All the contributions of this work have been implemented in SPOT and LTS-ITS, respectively, an explicit and a symbolic open source model-checking libraries.