Les systèmes informatiques jouent un rôle essentiel dans la vie actuelle, et leurs erreurs peuvent avoir des conséquences dramatiques. Il existe des méthodes formelles permettant d'assurer qu'un système informatique est fiable. La méthode formelle utilisée dans cette thèse est appelée complétion d'automates d'arbres et permet d'analyser les systèmes à nombre d'états infini. Dans cette représentation, les états du système sont représentés par des termes et les ensembles d'états par des automates d'arbres. L'ensemble des comportements possibles d'un système est calculé grâce à l'application successive d'un système de réécriture modélisant le comportement du système vérifié. On garantit la fiabilité d'un système en vérifiant qu'un comportement interdit n'est pas présent dans l'ensemble des états accessibles. Mais cet ensemble n'est pas toujours calculable, et nous devons alors calculer une sur-approximation calculable de cet ensemble. Mais cette approximation peut s'avérer trop grossière et reconnaître de faux contre-exemples. La première contribution de cette thèse consiste alors à caractériser, par des formules logiques et de manière automatique, ce qu'est une "bonne" sur-approximation : une approximation représentant un sur-ensemble des configurations accessibles, et qui soit suffisamment précise pour ne pas reconnaître de faux contre-exemples. Résoudre ces formules conduit alors automatiquement à une sur-approximation concluante si elle existe, sans avoir recours à aucun paramétrage manuel. Le second problème de la complétion d'automates d'arbres est le passage à l'échelle, autrement dit le temps de calcul parfois élevé du calcul de complétion quand on s'attaque à des problèmes de la vie courante. Dans la vérification de programmes Java utilisant la complétion d'automates d'arbres, cette explosion peut être due à l'utilisation d'entiers de Peano. L'idée de notre seconde contribution est alors d'évaluer directement le résultat d'une opération arithmétique. D'une façon plus générale, il s'agit d'intégrer les éléments d'un domaine infini dans un automate d'arbres. En s'inspirant de méthodes issues de l'interprétation abstraite, cette thèse intègre des treillis abstraits dans les automates d'arbres, constituant alors un nouveau type d'automates. Les opérations sur le domaine infini représenté sont calculées en une seule étape d'évaluation plutôt que d'appliquer de nombreuses règles de réécriture. Nous avons alors adapté la complétion d'automates d'arbres à ce nouveau type d'automate, et la généricité du nouvel algorithme permet de brancher de nombreux treillis abstraits. Cette technique a été implémentée dans un outil appelé TimbukLTA, et cette implémentation permet de démontrer l'efficacité de cette technique. / Computer systems are more and more important in everyday life, and errors into those systems can make dramatic damages. There are formal methods which can assure reliability of a system. The formal method used in this thesis is called tree automata completion and allows to analyze infinite state systems. In this representation, states of a system are represented by a term and sets of states by tree automata. The set of all reachable behaviors (or states) of the system is computed thanks to successive applications of a term rewriting system which represents the behavior of the system. The reliability of the system is assured by checking that no forbidden state is reachable by the system. But the set of reachable states is not always computable and we need to compute an over-approximation of it. This over-approximation is not always fine enough and can recognize counter examples. The first contribution of this thesis consist in characterizing by logical formulae, in an automatic way, what is a good approximation: an over-approximation which does not contain any counter example. Solving these formulae leads automatically to a good over-approximation if such an approximation exists, without any manual setting. An other problem of tree automata completion is the scaling when dealing with real life problems. In verification of Java programs using tree automata completion, this explosion may be due to the use of Peano numbers. The idea of the second contribution of this thesis is to evaluate directly the result of an arithmetic operation. Generally speaking, we integrate elements of an infinite domain in a tree automaton. Based on abstract interpretation, this thesis allows to integrate abstract lattice in tree automata. Operations on infinite domain are computed in one step of evaluation instead of probably many application of rewrite rules. Thus we adapted tree automata completion to this new type of tree automata with lattice, and genericity of the new algorithm allows to integrate many types of lattices. This technique has been implemented in a tool named TimbukLTA, and this implementation shows the efficiency of the technique.

Partant du principe qu'une machine ne sait pas qu'elle est une machine et du présupposé selon lequel un robot n'a pas de conscience, ce travail étudie le parallèle entre la fabrication des créatures de roman et la fabrication des machines. Parmi ces figures, Madame Bovary est un archétype. Comme tout autre machine, Emma Bovary ne sait pas qu'elle en est une. Emma est une machine à texte, elle est faite de livres. Pourtant, elle ne peut pas avoir lu Madame Bovary. Parce qu'Emma n'est pas consciente qu’elle est l'appareil de Flaubert, nous l'avons rapproché des fonctionnements et des disfonctionnements du Monstre de Frankenstein, encore écervelé avant l'épiphanie des livres qu'il découvre au creux d'un chemin. Après avoir défini les enjeux stratégiques de ses lectures, Emma est présentée comme une machine homéostatique, d'une part du point de vue de la thermodynamique, et d'autre part, du point de vue de l'entropie, une résultante du bovarysme, causée par les distorsions entre la vie et la lecture. Dans un premier temps Emma perçoit, puis ressent, par les feedbacks de ses lectures. Elle se transforme alors en une mécanique à émotions, gouvernée par son bovarysme. Ce sentiment renvoie à toutes ses perceptions et ses appétits. Par ses désirs, Emma démontre une capacité à comparer et à se projeter, formulant les prémices d'une conscience autobiographique. De la même manière qu'il représente l'inconscient social à partir d'automates déambulatoires, tels la figure du pied-bot ou de l'aveugle, Flaubert réussit à induire une idée de conscience dans sa créature machine / According to the fact that a machine does not know that it is a machine, and to the supposition that a robot has no conscience, this work explores parallels between the creation of the characters of a novel and the fabrication of machines. Among these figures, Madame Bovary is an archetype. Like any other machine, Emma Bovary does not know that she is one. Emma is machine created from text. She is made from the stuff of books. However, she could not have read the book Madame Bovary. Because Emma is not aware that she is a device of Flaubert, there are some similarities between her and the functions and malfunctions of the Monster of Frankenstein that didn't have a conscience until the moment of epiphany with the books he discovered in the woods. After the definition of the strategic challenges of her readings, Emma is presented as a homeostatic machine, first from the viewpoint of thermodynamics, and secondly from the viewpoint of entropy, a result of the bovarysme caused by distortions between life and reading. Emma's perceptions and feelings depend of the feedback of her readings. She becomes an emotional device, governed by her bovarysme. This feeling is present in all her perceptions and her appetites. Through her desires, Emma demonstrates an ability to compare and project herself, formulating the beginnings of an autobiographical conscience. In the same way as he represents social unconsciousness with ambulatory automatons such as the figure of the club-footed Hippolyte or the blind man, Flaubert is able to induce an idea of consciousness in his machine-creature

La SNCF cherche à mettre en place des solutions innovantes permettant d’améliorer la sécurité et les conditions de travail des chargés d’études lors des travaux d’automatisation. En partant de l’étude théorique du projet jusqu’à sa validation sur site, en passant par la mise en œuvre des programmes, du câblage des armoires, et de leur vérification sur plateforme et en usine, ces différentes tâches s’avèrent souvent être longues, complexes, et répétitives, ce qui a pour effet d’augmenter la charge de travail des chargés d’études. En vue d’améliorer les conditions de travail des chargés d’études, ce projet de recherche vise principalement à améliorer leurs méthodologies de vérification des programmes API (aspects fonctionnels et sécuritaires) et du câblage des armoires électriques. Ce projet intitulé « Vérification formelle et simulation pour la validation des programmes API des EALE » se décompose en deux axes :  la vérification hors ligne des programmes API : basée sur une approche formelle, la méthode s’appuie sur une modélisation de l’installation électrique, des programmes API et du cahier de recette dans le model-checker Uppaal. Le principe consiste à vérifier automatiquement si les programmes satisfont aux tests du cahier de recette.  la vérification en ligne du câblage des armoires de contrôle/commande/ protection grâce à un simulateur de partie opérative interfacé avec les armoires de contrôle/commande/protection (via une armoire de test). La vérification se fera de manière automatique et en ligne, toujours avec les tests du cahier de recette, et permettra de valider le câblage des armoires et les réglages des appareils de protection numérique. / In order to keep its leadership in French rail market and to improve working conditions of its systems engineers during automation projects, the SNCF (French acronym for National Society of French Railways) wants to develop solutions increasing the productivity. One of these improvements focuses on the current methodology used by the systems engineers to verify and validate the control command system of electrical installations. This task remains one of the most important during an automation project because it is supposed to ensure installations safety, but it should be optimized. Through an industrial thesis financed by SNCF, the aim of this research project is to improve this method and reduce time validation of control command system by providing tools which will help systems engineers to verify and validate quickly and automatically the control command system during any automation project. It is composed of two axes : - Offline verification of PLC programs with model checking - Online validation of electrical cabinets with virtual commissioning

En ce qui concerne le développement des technologies informatique, les systèmes et les réseaux informatiques sont intensément utilisés dans la vie quotidienne. Ces systèmes sont responsables de nombreuses tâches essentielles pour notre communauté sociale (par exemple, système de traitement médical, E-Commerce, Système d'avion, système de vaisseau spatial, etc.). Quand ces systèmes cessent de fonctionner ou sont corrompus, les pertes économiques peuvent atteindre des sommes inacceptables. Pour éviter ces situations, les systèmes doivent être sécurisés avant leur installation. Alors que la plupart de ces systèmes sont mis en œuvre à partir de spécifications des protocoles, les problèmes de vérification de la sécurité de systèmes concrets renvient à vérifier la sécurité de l'implémentation de ces protocoles. Dans cette thèse, nous nous concentrons sur les méthodes de vérification de la sécurité des implémentations des protocoles et nous sommes intéressés à deux principaux types d'attaques sur les réseaux : Déni de service (DoS) et attaque de Protocol d’authentification. Nous étudions les caractéristiques de ces attaques et les méthodes de vérification formelles. Puis nous proposons modèle étendu de IOLTS et les algorithmes correspondants à la génération de les cas de test pour la vérification de sécurité automatique. Afin d'éviter les explosions d'état possibles, nous formalisons également les expériences de sécurité du testeur comme le « Objectif de Sécurité » pour contrôler la génération de test sur la volée. Parallèlement, une méthode d'analyse basée sur le modèle pour la Systèmes de Détection d'intrusion Anomalie (Anomaly IDS) est également proposée dans cette thèse, ce qui peut améliorer les capacités de détecter des anomalies de l'IDS. Ces méthodes de vérification proposées sont mises en évidence par l'étude de RADIUS protocole et un outil intégré de graphique est également proposé pour facilement les opérations de la génération de test. / Regarding the development of computer technologies, computer systems have been deeply used in our daily life. Those systems have become the foundation of our modern information society. Some of them even take responsibilities for many essential and sensitive tasks (e.g., Medical Treatment System, E-Commerce, Airplane System, Spaceship System, etc.). Once those systems are executed with problems, the loss on the economy may reach an unacceptable number. In order to avoid these disappointing situations, the security of the current systems needs to be verified before their installations. While, most of the systems are implemented from protocol specifications, the problems of verifying the security of concrete system can be transformed to verify the security of protocol implementation. In this thesis, we focus on the security verification methods of protocol implementations and we are interested with two main types of network attacks: Denis-of-Services (DoS) attacks and Protocol Authentication attacks. We investigate the features of these attacks and the existed formal verification methods and propose two extended models of IOLTS and the corresponding algorithms to generate the security verification test cases automatically. In order to avoid the possible state explosions, we also formalize the security experiences of the tester as Security Objective to control the test generation on-the-fly. Meanwhile, a modeled based Anomaly Intrusion Detection Systems (IDS) analysis method is also proposed in this thesis, which can enhance the detect abilities of Anomaly IDS. These proposed verification methods are demonstrated with the case study of RADIUS protocol and an integrated GUI tool is also proposed to simply the operations of test generation.

La modélisation d'un système intégré sur puce nécessite la spécification de l'application logicielle et la modélisation de l'architecture matérielle puis le déploiement du logiciel sur ce matériel. L'objectif du concepteur de systèmes intégrés est de trouver la meilleure solution de déploiement pour optimiser les critères de surface de silicium, de consommation d'énergie, et de performances. Ces critères sont le plus souvent évalués par simulation. En raison du grand nombre de paramètres de l'architecture matérielle et des choix dans le déploiement du logiciel sur l'architecture, le temps nécessaire pour les simulations est important. Les outils permettant de réduire ce temps présentent un grand intérêt. Cette thèse présente des principes et des outils pour faciliter le développement des architectures matérielles et pour accélérer la simulation de modèles d'architectures synchrones décrites en langage SystemC, précis au cycle près et au bit près. Ce document est constitué de quatre chapitres : • La modélisation de composants matériels en SystemC sous la forme d'automates synchrones communicants (CFSM) ; • La génération de modèles SystemC, pour la simulation, à partir de descriptions synthétisables VHDL au niveau RTL ; • La vérification des règles d'écriture des modèles SystemC ; • La simulation rapide à l'aide d'une technique d'ordonnancement totalement statique. Ces outils permettent au concepteur de construire rapidement une architecture matérielle à l'aide de composants synthétisables au niveau RTL et de composants SystemC, respectant le modèle des CFSM. SystemCASS simule une telle architecture avec une accélération supérieure à un facteur 12 par rapport à un simulateur à échéancier dynamique.

La technologie des services web est aujourd'hui largement utilisée comme support de l'interopérabilité entre les applications. Dans ce cadre, les interactions entre deux applications encapsulées par des services web sont réalisées par le biais d'un ensemble d'échanges de messages appelé conversation. Une conversation peut échouer parce que l'interface fournie d'un participant a été modifiée et n'est plus compatible avec celle requise par l'autre participant. L'étude rapportée dans cette thèse porte sur la réconciliation de telles conversations. La solution proposée est le canevas ArchiMed.<br>Dans un premier temps, une modélisation des interfaces comportementales par des automates est adoptée. Dans cette modélisation, seul le comportement externe (comportement observable) est considéré. En d'autres termes, il n'y a que les opérations d'envoi et de réception de messages qui sont décrites dans les interfaces. Une fois les interfaces comportementales décrites en automates, une étape de détection des incompatibilités entre les différentes définitions de l'interface d'un service est réalisée. La détection des incompatibilités est automatique et portent sur des changements élémentaires dans les interfaces qui sont : l'ajout, la suppression et la modification d'opérations. Une visualisation des incompatibilités entre les interfaces est rendue disponible.<br>Le canevas maintient les descriptions des versions successives de l'interface du service ainsi que l'ensemble minimal de médiateurs pour que les clients puissent interagir avec le service au travers de l'une de ses versions. A l'initiation d'une conversation par un client, si nécessaire, le canevas sélectionne parmi les médiateurs disponibles celui qui résoud les incompatibilités entre le client et le service. La sélection du médiateur est basée sur une mesure de similarité entre les interfaces afin de découvrir la description de l'interface fournie qui est conforme avec l'interface requise du client. La validation expérimentale du canevas, a été effectuée par le traitement d'une collection de tests qui contient les descriptions des interfaces comportementales des services. Une étude quantitative et comparative à des travaux similiaires est réalisée et montre l'apport significatif de notre proposition.

Depuis vingt ans, la capacité d'intégration des technologies MOS double tous les dix-huit mois. Une approche prometteuse pour exploiter cette progression a été introduite récemment par l'invention des “circuits analogiques cellulaires”, qui sont composés de l'assemblage régulier de milliers de cellules analogiques identiques. L'objectif de cette thèse est de contribuer à la conception de ces circuits, en étudiant ceux pour lesquels sont possibles une modélisation statistique à l'aide de Réseaux de Neurones Formels (RNF) et des applications à la reconnaissance des formes. Elle porte plus particulièrement sur la machine de Boltzmann, qui est un modèle de RNF booléen et stochastique, à temps discret. Au chapitre I, je présente les Réseaux de Reurones Formels et les algorithmes de la Machine de Boltzmann Synchrone, qui est un modèle adapté au parallélisme matériel. Au chapitre II, je présente l'état de l'art des réalisations de Machine de Boltzmann et des techniques analogiques utilisées pour les RNF. Au chapitre III, je présente une architecture originale de circuits dédiés aux réseaux multi-couches exécutant la Machine de Boltzmann. Au chapitre IV, je présente la conception et la simulation des cellules et des circuits nécessaires : convertisseurs tension-courant et courant-tension, comparateur, fonction sigmoïde... Ce modèle étant stochastique, je présente aussi deux réalisations originales de générateurs aléatoires : le premier est optoélectronique et tire partie des propriétés du speckle optique, le second est électronique et à base d'automates cellulaires. Le chapitre V est consacré à la description des mesures effectués sur des circuits prototypes de chacune des cellules. En conclusion, je présente les évolutions de ces travaux vers des circuits analogiques à temps continu et à états de neurones continus.

Cette these propose un mecanisme de coordination entre outils pour un environnement integre de developpement de logiciels. Le ro^le d'un tel environnement est d'accroitre la productivite des developpeurs et d'ameliorer la qualite du logiciel developpe en integrant les composants de l'environnement. Le mecanisme que nous proposons integre les outils de developpement, en permettant a` ceux-ci d'echanger des informations pour agir de maniere coherente et homogene. Nous qualifions ces echanges de coordinations. Ce mecanisme se fonde sur un modele de coordination mis en oeuvre par un langage nomme Indra qui comprend des parties declaratives et imperatives. Il presente les caracteristiques suivantes. Pour faciliter l'evolution des composants de l'environnement (outils et coordinations), il permet d'une part d'exprimer les coordinations de maniere modulaire, en dehors du code des outils. Il permet d'autre part d'exprimer explicitement l'evolution dynamique des coordinations, en s'inspirant du concept d'automate d'etats fini. Afin de pouvoir coordonner des outils qui presentent des interfaces de coordination independantes les unes des autres, il definit un espace global de coordinations au travers duquel sont exprimees les liaisons entre les interfaces. Enfin, pour gerer la forte evolution dynamique des outils actifs, il permet de designer les outils sans connaitre leur identite, en fournissant une designation associative fondee sur le concept d'arbre attribue. Ce mecanisme a ete realise au dessus du systeme reparti et oriente objet Guide.

Résumé non disponible

Ce travail de thèse a pour objectif de concevoir et réaliser un module informaticolinguistique apte à effectuer des analyses automatiques de textes thaï sous le système INTEX © . Basé fondamentalement sur les langues indo-européennes écrites avec l'alphabet latin, INTEX © rencontre quelques difficultés pour travailler sur une langue très différente comme le thaï. Le problème crucial est la segmentation en mots et en phrases, étant donné que le thaï n'a pas de séparateur de mot : une phrase est écrite en une séquence de lettres continues, et les séparateurs de phrase sont fréquemment ambigus. Aussi avons-nous développé et évalué deux méthodes de segmentation en mots, par expressions rationnelles et par transducteurs à nombre fini d'états, qui découpent respectivement des textes thaï en lettres et en syllabes. Nous avons également créé les dictionnaires électroniques du thaï qui servent à la fois à reconnaître les mots à partir des lettres ou des syllabes et à les étiqueter avec les codes syntaxiques et sémantiques. Deux méthodes de segmentation en phrases thaï, par la ponctuation et par mots-clés, sont également proposées et évaluées. Nous montrons enfin que, grâce à notre travail, INTEX © est capable d'analyser des documents thaï, malgré toutes les difficultés.