La vérification en ligne de spécifications formelles permet de créer des détecteurs d'erreur dont le pouvoir de détection dépend en grande partie du formalisme vérifié à l'exécution. Plus le formalisme est puissant plus la séparation entre les exécutions correctes et erronées peut être précise. Cependant, l'utilisation des vérifieurs en-ligne dans le but de détecter des erreurs est entravée par deux problèmes récurrents : le coût à l'exécution de ces vérifications, et le flou entourant les propriétés sémantiques exactes des signaux d'erreur ainsi générés. L'objectif de cette thèse est de clarifier les conditions d'utilisation de tels détecteurs dans le cadre d'applications " temps réel " critiques. Dans ce but, nous avons donné l'interprétation formelle de la notion d'erreur comportementale " temps réel". Nous définissions la propriété de détection " au plus tôt " qui permet de d'identifier la classe des détecteurs qui optimisent la latence de détection. Pour illustrer cette classe de détecteurs, nous proposons un prototype qui vérifie un comportement décrit par un automate temporisé. La propriété de détection au plus tôt est atteinte en raisonnant sur l'abstraction temporelle de l'automate et non sur l'automate lui-même. Nos contributions se déclinent dans trois domaines, la formalisation de la détection au plus tôt, sa traduction pour la synthèse de détecteurs d'erreur à partir d'automate temporisés, puis le déploiement concret de ces détecteurs sur une plate-forme de développement temps réel, Xenomai.

Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées

La planification du mouvement connait une utilisation croissante dans le contexte industriel. Qu'elle soit destinée à la programmation des robots dans l'usine ou au calcul de l'assemblage d'une pièce mécanique, la planification au travers des algorithmes probabilistes est particulièrement efficace pour résoudre des problèmes complexes et difficiles pour l'opérateur humain. Cette thèse CIFRE, effectuée en collaboration entre le laboratoire de recherche LAAS-CNRS et la jeune entreprise Kineo CAM, s'attache à résoudre la problématique de planification de mouvement dans l'usine numérique. Nous avons identifié trois domaines auxquels s'intéressent les partenaires industriels et nous apportons des contributions dans chacun d'eux: la détection de collision, le volume balayé et le mouvement en collision. La détection de collision est un opérateur critique pour analyser des maquettes numériques. Les algorithmes de planification de mouvement font si souvent appel à cet opérateur qu'il représente un point critique pour les performances. C'est pourquoi, il existe une grande variété d'algorithmes spécialisés pour chaque type de géométries possibles. Cette diversité de solutions induit une difficulté pour l'intégration de plusieurs types de géométries dans la même architecture. Nous proposons une structure algorithmique rassemblant des types géométriques hétérogènes pour effectuer les tests de proximité entre eux. Cette architecture distingue un noyau algorithmique commun entre des approches de division de l'espace, et des tests spécialisés pour un couple de primitives géométriques donné. Nous offrons ainsi la possibilité de facilement ajouter des types de données nouveaux sans pénaliser la performance. Notre approche est validée sur un cas de robot humanoïde qui navigue dans un environnement inconnu grâce à la vision. Concernant le volume balayé, il est utilisé pour visualiser l'étendue d'un mouvement, qu'il soit la vibration d'un moteur ou le geste d'un mannequin virtuel. L'app roche la plus innovante de la littérature repose sur la puissance du matériel graphique pour approximer le volume balayé très rapidement. Elle est toutefois limitée en entrée à un seul objet, qui lui-même doit décrire un volume fermé. Afin d'adapter cet algorithme au contexte de la conception numérique, nous modifions son comportement pour traiter des " soupes de polygones " ainsi que des trajectoires discontinues. Nous montrons son efficacité sur les mouvements de désassemblage pour des pièces avec un grand nombre de polygones. Une soupe de polygones est plus difficile à manipuler qu'un volume bien formé. Le calcul du volume balayé introduit des opérateurs d'agrandissement et de rétrécissement des objets discrétisés. Le rétrécissement peut être utilisé pour d'autres applications dans la planification du mouvement à condition que la topologie de l'objet soit conservée pendant la transformation. Afin de préserver celle-ci, nous définissons le calcul du squelette qui préserve l'équivalence topologique. En gardant le squelette, nous employons l'opérateur de rétrécissement pour chercher les passages étroits des problèmes difficiles de planification de mouvement. Enfin, nous abordons le problème de la planification de mouvement en collision. Cette antilogie exprime la capacité d'autoriser une collision bornée pendant la recherche de trajectoire. Ceci permet de résoudre certains problèmes d'assemblage très difficiles. Par exemple, lors du calcul des séquences de désassemblage, il peut être utile de permettre à des "pièces obstacles" telles que les vis de se déplacer pendant la planification. De plus, en autorisant la collision, nous sommes capables de résoudre des problèmes de passage en force. Cette problématique se pose souvent dans la maquette numérique où certaines pièces sont " souples " ou si le problème consiste à identifier la trajectoire "la moins pire" quand aucun chemin sans collision n'existe. Nous apportons dans ce travail plusieurs contributions qui s'appliq uent à la conception numérique pour la robotique industrielle. Nous essayons de marier une approche scientifique avec des critères de fonctionnalités strictes pour mieux s'adapter aux utilisateurs de la conception numérique. Nous cherchons à exposer les avantages et les inconvénients de nos approches tout au long du manuscrit.

Les entreprises de transport font face à des problèmes de taille grandissante où l'utilisation de transbordement peut avoir un impact significatif sur les coûts. ILOG TPO est un logiciel capable de résoudre de tels problèmes, mais il lui est difficile de prendre de bonnes décisions concernant le transbordement. De plus, le processus de résolution d'ILOG TPO est basé sur la recherche locale, et il peut être aidé pour certaines décisions globales comme le transbordement. Cette thèse se place dans ce contexte, et son objectif est d'aider ILOG TPO à trouver de meilleures solutions. Pour cela, une formulation complète est d'abord proposée pour résoudre les plus petites instances, et avec une technique de plans coupants, les solutions optimales sont généralement trouvées en un temps raisonnable. Ensuite, un algorithme à deux phases qui inclut un programme en variables mixtes (MIP) sur une relaxation de type réseau du problème est donné pour de plus grandes instances. Cet algorithme est une coopération entre le MIP et ILOG TPO, où le MIP donne à ILOG TPO, pour chaque ordre de transport, le chemin de hubs par lequel il devrait être acheminé. Cette heuristique trouve des solutions similaires à ILOG TPO seul, mais le temps de calcul est réduit de façon significative.

Cette thèse traite de la préservation de l'intégrité des systèmes d'exploitation courants. L'objectif est de répondre aux menaces actuelles et futures que représentent les logiciels malveillants qui s'implantent dans le noyau de ces systèmes (comme les rootkits "noyau") ou du moins en altèrent l'intégrité (comme les rootkits "hyperviseur"). La première partie de ce document se focalise sur ces logiciels malveillants. Tout d'abord, les attaques logiques sur les systèmes informatiques sont présentées dans leur globalité. Ensuite est proposée une classification des actions malveillantes qui provoquent la perte de l'intégrité d'un noyau. Enfin, les résultats d'une étude sur les rootkits "noyau" sont donnés et la création d'un rootkit original est expliquée. La seconde partie s'intéresse à la protection des noyaux. Après une description de l'état de l'art, une approche originale est proposée, fondée sur le concept de préservation de contraintes. En premier lieu, les éléments essentiels sur lesquels reposent un noyau sont identifiés et les contraintes sur ces éléments, nécessaires à un fonctionnement correct du noyau, sont exposées. Un hyperviseur léger (Hytux) a été conçu pour empêcher la violation de ces contraintes en interceptant certaines des actions du noyau. Sa mise en oeuvre est décrite pour un noyau Linux 64 bits sur architecture x86 qui dispose des technologies Intel VT-x et VT-d.

Cette thèse s'inscrit dans une thématique pluridisciplinaire explorant les liens existants entre la théorie de la commande et les réseaux informatiques. L'idée consiste à appliquer les outils de l'Automatique pour la stabilisation du trafic dans les réseaux de communication. Premièrement, nous nous sommes intéressés à l'analyse de stabilité des systèmes à retards variables au travers de deux approches temporelles. D'une part, nous avons considéré la méthode de Lyapunov-Krasovskii dans laquelle nous avons élaboré des fonctionnelles en adéquation avec de nouvelles modélisations du système (segmentation du retard, dérivée temporelle). D'autre part, la stabilité a également été abordée avec une approche entrée-sortie, empruntant alors les outils de l'analyse robuste. Le système à retard est alors réécrit comme l'interconnexion d'une application linéaire avec une matrice constituée d'opérateurs définissant le système original. Après avoir revisité le principe de séparation quadratique, nous développons des opérateurs auxiliaires afin de caractériser au mieux la dynamique retardée et proposer des critères moins pessimistes. Deuxièmement, la méthodologie développée est ensuite utilisée pour le problème de contrôle de congestion d'un routeur lors de communications TCP. Ce protocole de bout en bout est sensible à la perte de paquet et modifie en conséquence son taux d'émission selon l'algorithme du AIMD. Il s'agit alors de commander le taux de perte par l'intermédiaire d'un mécanisme d'Active Queue Management situé au niveau du routeur afin de réguler le trafic. Les résultats théoriques sont ensuite évalués à l'aide du simulateur de réseaux NS-2.

Les agents mobiles peuvent physiquement migrer à travers un réseau informatique dans le but d'effectuer des tâches sur des machines, ayant la capacité de leur fournir un support d'exécution. Ces agents sont considérés comme composants autonomes, une propriété qui leur permet de s'adapter à des environnements dynamiques à l'échelle d'un réseau large. Ils peuvent également échanger des informations entre eux afin de collaborer au sein de leur groupe, nous parlerons ainsi d'une communauté d'agents mobiles. Nous avons développé ce concept de communauté, en se référant aux recherches et aux études précédentes pour définir un nouveau modèle comportemental d'agent mobile. Ce modèle est utilisé pour répondre aux besoins de la surveillance logicielle. Celle ci consiste à collecter des événements à partir de plusieurs sources de données (Log, événements système...) en vue de leur analyse pour pouvoir détecter des événements anormaux. Cette démarche de surveillance s'appuie sur plusieurs types d'agents mobiles issus du même modèle. Chaque type d'agent gère un domaine fonctionnel précis. L'ensemble des ces agents constitue une communauté pouvant collaborer avec différentes autres communautés lorsqu'il existe plusieurs sites à surveiller. Les résultats de cette approche nous ont permis d'évoquer les limites liées à la taille des données collectées, ce qui nous amène à de nouvelles perspectives de recherche et à penser un agent mobile "idéal". Enfin, nous nous intéressons également à l'application de la communauté d'agent mobile pour les systèmes de détection d'intrusion et la remontée d'anomalie

Le monde du protocole de transport a fortement évolué depuis la création de l'internet. On retrouve désormais une grande diversité de liens avec des caractéristiques hétérogènes en termes de débit, taux de pertes et délais. Plus récemment, le caractère ubiquitaire des périphériques sans fil a permis d'envisager un nouveau mode de transfert prenant en compte la mobilité des utilisateurs pour propager l'information dans le réseau. Ce paradigme de communication rompt définitivement avec les hypothèses de conceptions des protocoles de transport classique. Les applications qui utilisent l'internet ont également évolué. Les réseaux best effort sont maintenant utilisés pour transporter des flux à contrainte de délai tels que la voix sur IP et la vidéo conférence. Cependant, malgré ces changements importants, le principe de fiabilité utilisé n'a guère évolué et se base toujours sur des retransmissions. C'est dans ce contexte que s'inscrit cette thèse qui vise à fournir une brique de fiabilité novatrice pour le support de tout type d'application sur les réseaux best effort et les challenged neworks qui font de plus en plus partie du paysage de l'internet. A cette fin, nous proposons un mécanisme de codage dénommé Tetrys. Ce code est sans rendement et ses symboles de redondance sont générés à la volée. Il permet à la fois une fiabilité totale et un délai de reconstruction quasi-optimal. Après une étude détaillée de ses propriétés, nous illustrons la généricité de ce mécanisme. Nous verrons que ses caractéristiques mènent à des contributions aussi bien sur le transport de flux de vidéo-conférence que sur le support du streaming dans les DTN ou encore la fiabilisation des handovers. De manière plus prospective, cette thèse reconsidère les hypothèses initiales du contrôle de congestion. Tetrys est utilisé comme code optimal dans le cas de réseaux dit "anarchiques" (i.e. caractérisés par une absence totale de contrôle de congestion). Nous montrons que le concept de réseau anarchi que est une alternative viable au contrôle de congestion et qu'il le remplace mÆeme avantageusement.

La classification de données (ou apprentissage non-supervisé) vise à regrouper un ensemble d'observations sous la forme de classes homogènes et contrastées. Lorsque les données sont caractérisées par un grand nombre de variables, il devient nécessaire d'adapter les méthodes classiques, notamment au niveau des métriques, afin de maintenir des classes pertinentes ; ce phénomène est connu sous le nom de "malédiction de la dimension". Dans cette thèse, nous proposons une mesure de co-similarité basée sur la notion de co-occurrences d'ordre supérieur, directement extraites à partir des données. Dans le cas de l'analyse de texte, par exemple, les similarités entre documents sont calculées en prenant en compte les similarités entre mots, qui simultanément prennent en compte les similarités entre documents. Par cette approche " circulaire ", nous parvenons à mettre en correspondance des documents sans mots communs mais ayant juste des mots similaires. Cette approche s'effectue de manière purement numérique sans nécessiter de thesaurus externe. En outre, notre méthode peut également être étendue pour tirer parti de connaissances "a priori" afin de réaliser des tâches de catégorisation de textes : l'étiquette des documents est utilisée pour influencer les mesures de similarité entre les mots afin de classer de nouvelles données. Ainsi, le même cadre conceptuel, exprimable en terme de théorie des graphes, peut être utilisé à la fois pour les tâches de classification et de catégorisation en fonction de la quantité d'information initiale. Nos résultats montrent une amélioration significative de la précision, par rapport à l'état de l'art, à la fois pour le co-clustering et la catégorisation sur les jeux de données qui ont été testés.

Les logiciels s'orientent de plus en plus vers des architectures évolutives, capables de s'adapter facilement aux changements et d'intégrer de nouvelles fonctionnalités. Ceci est important pour plusieurs classes d'applications qui ont besoin d'évoluer sans que cela implique d'interrompre leur exécution. Des plateformes dynamiques à composants autorisent ce type d'évolution à l'exécution, en permettant aux composants d'être chargés et exécutés sans requérir le redémarrage complet de l'application en service. Toutefois, la flexibilité d'un tel mécanisme introduit de nouveaux défis qui exigent de gérer les possibles erreurs dues à des incohérences dans le processus de mise à jour, ou en raison du comportement défectueux de composants survenant pendant l'exécution de l'application. Des composants tiers dont l'origine ou la qualité sont inconnus peuvent être considérées à priori comme peu fiables, car ils peuvent potentiellement introduire des défauts d'applications lorsqu'il est combiné avec d'autres composants. Nous sommes intéressés à la réduction de l'impact de ces composants considérés comme non fiables et qui sont susceptibles de compromettre la fiabilité de l'application en cours d'exécution. Cette thèse porte sur l'application de techniques pour améliorer la fiabilité des applications dynamiques à composants. Pour cela, nous proposons l'utilisation des frontières d'isolation pouvant fournir du contingentement de fautes. Le composant ainsi isolé ne perturbe pas le reste de l'application quand il est défaillant. Une telle approche peut être vu sous trois perspectives présentées: (i) l'isolement des composants dynamiques, régi par une politique d'exécution reconfigurable, (ii) l'autoréparation de conteneurs d'isolement, et (iii) l'utilisation des aspects pour séparer les préoccupations de fiabilité à partir du code fonctionnel.