Avec l'évolution des machines parallèles, le besoin en protocole de tolérance aux fautes devient de plus en plus important. Les protocoles de tolérance aux fautes existants ne sont pas adaptés à ces architectures car soit ils forcent un redémarrage global (protocoles de sauvegarde de points de reprise coordonnés) soit ils forcent l'enregistrement de tous les messages (protocoles à enregistrement de messages). Nous avons étudié les caractéristiques des protocoles existants. Dans un premier temps, nous avons étudié le déterminisme des applications, étant donné que les protocoles existants supposent des exécutions non déterministes ou déterministes par morceaux. Dans notre étude, nous nous sommes intéressés au modèle par échange de messages, et plus précisément aux applications MPI. Nous avons analysé 26 applications MPI et avons mis avant une nouvelle caractéristique appelée "déterminisme des émissions" qui correspond à la majorité des applications étudiées. Dans un second temps, nous nous sommes intéressés aux schémas de communications des applications afin d'étudier l'existence des groupes de processus dans ces schémas. L'étude a montré que pour la plupart des applications, il est possible de créer des groupes de processus de façon à minimiser la taille des groupes et le volume des messages inter-groupe. A partir de là nous avons proposé deux protocoles de tolérance aux fautes. Le premier est un protocole de sauvegarde de points de reprise non coordonnés pour les applications à émissions déterministes qui évite l'effet domino en n'enregistrant qu'un sous ensemble des messages de l'application. Nous avons également adapté le protocole pour l'utiliser sur des groupes de processus. Par la suite, nous avons proposé HydEE, un protocole hiérarchique fondé sur le déterminisme des émissions et les groupes de processus. Il combine un protocole de sauvegarde de points de reprise coordonnés au sein des groupes à un protocole à enregistrement de messages entre les groupes.

The goal of this thesis is the development of support for test generation and animation based on object-oriented specifications. We aim particularly to take advantage of state-of-the-art satisfiability solving techniques by using an appropriate representation of object-oriented data. While automated test generation seeks a large set of data to execute an implementation on, animation performs computations that comply with a specification based on user-provided input data. Animation is a valuable technique for validating specifications.As a foundation of this work, we present clarifications and a partial formalization of the Object Constraint Language (OCL) as well as some extensions in order to allow for test generation and animation based on OCL specifications.For test generation, we have implemented several enhancements to HOL-TestGen, a tool built on top of the Isabelle theorem proving system that generates tests from specifications in Higher-Order Logic (HOL). We show how SMT solvers can be used to solve various types of constraints in HOL and present a modular approach to case splitting for deriving test cases. The latter facilitates the introduction of splitting rules that are tailored to object-oriented specifications.For animation, we implemented the tool OCLexec for animating OCL specifications. OCLexec generates from operation contracts corresponding Java implementations that call an SMT-based constraint solver at runtime.

Un système technologique piloté est constitué d'une variété de composants interagissant ensemble et combinant de multiples phénomènes physiques. Ces composants, subissant un stress en fonctionnement, finissent par être affectés par des défauts pouvant avoir de graves conséquences pour l'intégrité du système lui-même ou son environnement. Ces défauts sont généralement répertoriés par des techniques de sureté de fonctionnement et classés par ordre de criticité.Une solution, pour réduire les sinistres consécutifs à la survenue d'un défaut critique, est de mettre en place un diagnostiqueur embarqué capable, dans un délai bref, de détecter cette survenue puis d'identifier le défaut, en vue de placer le système dans un mode de fonctionnement plus sûr. Il apparaît alors impératif, durant la conception du diagnostiqueur, d'étudier la diagnosticabilité des défauts, étude consistant à s'assurer que le diagnostiqueur sera toujours capable de détecter et d'identifier sans ambiguïté les défauts préalablement répertoriés.Cette thèse établit une chaîne complète de développement d'un diagnostiqueur embarqué pour les systèmes technologiques pilotés. Y sont décrites, dans un cadre théorique unifié et cohérent basé sur l'utilisation de modèles homogènes, toutes les étapes depuis la conception jusqu'à la réalisation du diagnostiqueur : représentation comportementale du système et modélisation des défauts, étude de la diagnosticabilité de ces défauts, puis génération du diagnostiqueur lui-même. Le lien rigoureux établi entre l'étude de la diagnosticabilité et la génération du diagnostiqueur, qui fonde la correction et la cohérence de l'approche, constitue un aspect saillant et original de ces travaux.Cette thèse résulte d'un projet collaboratif réunissant l'entreprise Sherpa Engineering, le Laboratoire de Recherche en Informatique (LRI) unité mixte de recherche de l'Université Paris-Sud et du CNRS et enfin le Laboratoire d'Ingénierie des Systèmes Embarqués (LISE) du CEA LIST.

L'espace et le temps sont des concepts indissociables et nécessaires à l'analyse de l'évolution d'entités spatio-temporelles. Modéliser ces évolutions passe par la détection des changements et des relations qui modifient et caractérisent ces entités. Ces changements sont en particulier caractérisés par des modifications liées à la position, à l'empreinte spatiale de ces entités, ou même à leur identité. Une modélisation spatio-temporelle nécessite le développement de solutions de représentation qui permettent d'identifier et d'étudier les processus mis en jeu, leurs causes et leurs conséquences. Le fait que la représentation formelle et informatique d'un phénomène entraîne une description plus ou moins simplifiée de la réalité, implique qu'une telle modélisation retienne le niveau de détail disponible et/ou souhaité de cette description. Idéalement, il devrait être possible d'étudier un phénomène à plusieurs niveaux de granularité dans l'espace et dans le temps. Si de nombreux modèles et approches ont été proposés pour modéliser des évolutions d'entités au sein de phénomènes spatio-temporels, aucun ne permet de disposer d'une structure de représentation permettant de saisir complètement la sémantique de ces applications. Cette recherche propose un modèle de graphe spatio-temporel qui permet de caractériser les principales propriétés de l'évolution d'entités spatiales. Nous distinguons dans ce cadre plusieurs concepts structurants comme les notions d'identité et de relations à travers les dimensions spatiales et temporelles. Pour un temps donné, nous catégorisons les relations spatiales et de filiation et, à travers le temps, les filiations temporelles et les relations spatio-temporelles. Les structures de graphe émergeantes permettent non seulement de caractériser l'évolution d'un ensemble d'entités spatiales, mais aussi de découvrir de nouvelles propriétés. Des fonctions de manipulation de graphe sont développées et appliquées au modèle de graphe spatiotemporel. Ces fonctions identifient des processus génériques ( e.g. vie et mort d'une entité) ou liés à une application spécifique et à sa sémantique. Afin de combiner plusieurs sources d'informations au sein d'un même graphe, des fonctions de jointure permettent l'intégration de plusieurs graphes au sein d'une représentation unifiée. Les propriétés des graphes ainsi constitués et le rôle des différentes entités présentes au sein de ces graphes sont étudiés par une qualification des différents types de routes les reliant. La consistance du modèle de graphe spatio-temporel est abordée à partir d'un algorithme de vérification de contraintes. Nous faisons la différence entre les contraintes de domaine intrinsèques au modèle de graphe, et les contraintes sémantiques dépendantes d'une application en particulier. Une extension de la démarche de modélisation est réalisée à partir d'une structure basée sur les bigraphes qui permet de représenter explicitement un phénomène spatio-temporel selon plusieurs niveaux de granularité spatiale.

Cette thèse présente une méthode permettant d'améliorer un régulateur existant relativement à des spécifications multiples formulées en termes de normes de système L*, L2/H2 et H∞. Trois éléments clés distinguent l'approche proposée. Premièrement, un paramétrage des régulateurs à ordre fixé au moyen d'un facteur stable et observable de la boucle fermée. Deuxièmement, un paramétrage minimal de toutes les paires stables observables fondé sur la théorie des systèmes conservatifs et permettant un ajustement infinitésimal du régulateur à améliorer. Et troisièmement, l'utilisation d'une information de sensibilité pour calculer le sous gradient local du critère d'optimisation et construire une suite minimisante.

Les systèmes embarqués sont utilisés dans de nombreux systèmes critiques, depuis les automobiles jusqu'aux les systèmes de contrôle industriels. La plupart des recherches sur ces systèmes embarqués se sont concentrés sur l'amélioration de leur fiabilité face à des fautes ou erreurs de fonctionnent non intentionnelles, moins de travaux on été réalisés considérant les attaques intentionnelles. Ces systèmes embarqués sont de plus en plus connectés, souvent à Internet, via des réseaux sans fils, par exemple pour leur administration à distance. Cela augmente les risques d'attaques à distance ou d'injection de code malicieux. Les fautes de fonctionnement de ces équipements peuvent causer des dommages physiques comme par example rendre des appareils médicaux dangereux. Par conséquent, il est primordial de protéger ces systèmes embarqués contre les attaques. Dans cette thèse nous présentons des attaques et défenses contre les systèmes embarqués contraints. Nous présentons plusieurs attaques contre des techniques d'attestation logicielle utilisées dans les systèmes embarqués. Puis nous présentons la conception et l'implémentation d'une technique d'attestation logicielle qui est résistante aux attaque présentées précédemment. Finalement, nous présentons la conception d'une solution permettant de réaliser l'attestation de code ainsi que la création d'une racine de confiance dynamique (dynamic root of trust) pour les systèmes embarqués. Cette solution est prouvée sure et ne dépend pas d'assomptions fortes faites dans le cas de l'attestation logicielle.

Depuis la fin des années 90, les différentes méthodes issues de l'apprentissage artificiel ont été étudiées et appliquées au problème de classement de messages électroniques (filtrage de spam), avec des résultats très bons, mais pas parfaits. Il a toujours été considéré que ces méthodes étaient adaptées aux solutions de filtrage orientées vers un seul destinataire et non pas au classement des messages d'une communauté entière. Dans cette thèse notre démarche a été, d'abord, de chercher à mieux comprendre les caractéristiques des données manipulées, à l'aide de corpus réels de messages, avant de proposer des nouveaux algorithmes. Puis, nous avons utilisé un classificateur à régression logistique avec de l'apprentissage actif en ligne - pour démontrer empiriquement qu'avec un algorithme simple et une configuration d'apprentissage mieux adaptée au contexte réel de classement, on peut obtenir des résultats aussi bons que ceux que l'on obtient avec des algorithmes plus complexes. Nous avons aussi démontré, avec des ensembles de messages d'un petit groupe d'utilisateurs, que la perte d'efficacité peut ne pas être significative dans un contexte de classement mutualisé.

La première partie propose divers systèmes de réseaux d'interaction (calcul par réécriture muni d'une réduction atomique, locale et parallèle) qui simulent l'exécution des preuves de la logique linéaire (considérées comme des programmes). Les différents fragments de cette logique sont abordés, on y ajoute aussi une récursion pour atteindre l'expressivité des langages de programmation usuels. Ce procédé de simulation permet d'exécuter certains langages à l'aide d'une petite machine d'exécution multi-processeurs. Il s'appuie sur des représentations localisées de boîtes issues des réseaux de preuve ; certaines utilisent avantageusement un canal de contrôle pour ne rien perdre de la structure des preuves représentées. La deuxième partie s'articule autour de la logique linéaire différentielle et de ses ressources à usage unique. On la munit d'une super-promotion, qui se distingue notamment d'une promotion ordinaire parce qu'elle préserve la symétrie originelle de ce formalisme. C'est la pendante côté logique de la réplication qu'on trouve parfois dans les algèbres de processus. On arrive à isoler l'un de ses composants plus primitifs, le co-enfouissement, responsable de leur dynamique incontrôlée (pour l'instant). Cette construction peut être exprimée dans la syntaxe du λ-calcul avec ressources ou dans un système de réseaux. La séquentialisation de ces derniers requiert une présentation originale de la logique, fondée sur un calcul de structures, et qui a potentiellement d'autres intérêts. Il est aussi question de réalisabilité pour les systèmes différentiels et de sémantique relationnelle pour les divers réseaux présentés.

Ce travail vise à présenter des méthodes de construction des dictionnaires électroniques de séquences nominales figées du coréen et de leurs formes fléchies, et à justifier leur validité en appliquant notre dictionnaire dans les domaines appliqués de l'analyse automatique de textes coréens. En vue de la reconnaissance des séquences nominales figées par dictionnaire, nous avons classé celles-ci en trois catégories selon les conventions typographiques : noms compacts (NC), noms figés à espacement facultatif (NFF) et noms figés à espacement obligatoire (NFO). Puisque des formes fléchies des séquences nominales figées apparaissent dans les textes coréens, nous avons construit, d'une part, un dictionnaire électronique des NFF à 45000 entrées et d'autre part, un transducteur des séquences de postpositions nominales avec leur segmentation, et enfin fusionné ces deux ensembles de données à partir de codes flexionnels associés à chaque entrée et de la fonctionnalité de flexion d'INTEX. Notre dictionnaire construit d'après ces méthodes a les principaux avantages suivants par rapport aux systèmes préexistants : 1) Le dictionnaire des formes fléchies de NFF permet la reconnaissance automatique de toutes les variantes de NFF liées à l'espacement 2) Le dictionnaire des formes fléchies de NFF permet la segmentation des formes fléchies des NFF en un NFF et une séquence de postpositions nominales 3) Le dictionnaire des séquences de postpositions nominales sous forme de graphes permet leur segmentation en postpositions nominales 4) Le dictionnaire des NFF sert à la segmentation des séquences nominales libres soudées 5) Le dictionnaire des NFF peut être étendu en un dictionnaire bilingue pour la traduction automatique 6) Chaque entrée du dictionnaire de NFF comporte des codes utiles pour les applications dans le traitement automatique : codes indiquant un trait sémantique, le statut de nom prédicatif, le nom tête de chaque entrée, l'origine et la catégorie grammaticale.

Cette étude constitue une description syntaxique de la construction des verbes dits de communication en coréen, qui se définit par une structure syntaxique N0N2-EKE P-ko V0. IL s'agit d'une structure à deux compléments dont l'un est un complément datif, noté N2-EKE, et l'autre une complétive terminée par le suffixe conjonctif -ko (P-ko). Ce travail a pour modèle théorique le lexique-grammaire, qui a été élaboré par M. Gross (1975) au LADL, sur la base des principes de la syntaxe transformationnelle de Z. S. Harris (1968). Les propriétés syntaxiques, distributionnelles ou transformationnelles, des verbes entrant dans cette construction ont été examinées sur les 546 entrées de verbes de communication que nous avons recensées à partir des dictionnaires. Ce travail contribue à la construction du lexique-grammaire du coréen et fait partie de la classification des construction verbales, en particulier de celles qui entrent dans des structures syntaxiques complexes.