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.

La morphologie de la surface du sol conditionne le ruissellement et réciproquement. Cette étude a été menée dans le but de mieux comprendre les mécanismes de contrôle et leurs interactions. Elle s'est focalisée sur le ruissellement diffus de type inter-rigoles. Ce travail s'appuie sur un modèle numérique basé sur la technique des marcheurs conditionnés. La dynamique du stockage de l'eau en surface est finement analysée en termes de genèse et de propagation du ruissellement. Nous montrons que la propagation du ruissellement, considérée comme un développement de connexions entre dépressions, peut être assimilée à un processus de percolation. Une relation formelle entre la taille du système et la dynamique du ruissellement est proposée. Des surfaces numériquement générées permettent l'examen des dynamiques externes, à partir du calcul du coefficient de ruissellement, et internes, à partir d'un calcul de la distance de transfert. La distance de transfert est une mesure pertinente pour comprendre le comportement du système, le coefficient de ruissellement n'y suffisant pas. Les effets des différentes rugosités dépendent principalement de leurs amplitudes. La corrélation observée à courte distance ne modifie pas le développement des connexions. En étant le moteur des redistributions de particules, l'écoulement d'eau aboutit à des évolutions non triviales de la géométrie des surfaces. Ce sont les processus affectant localement la morphologie de la surface qui ont les plus fortes conséquences sur le déclenchement du ruissellement. Toutefois, les méthodes courantes ne peuvent pas mettre en évidence ce type de modifications. Essentiellement focalisée sur les transferts d'eau et de particules, la redistribution de substances dissoutes est aussi abordée.