Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Le protocole Pastry réalise une table de hachage distribué sur un réseau pair à pair organisé en un anneau virtuel de noeuds. Alors qu'il existe plusieurs implémentations de Pastry, il n'y a pas encore eu de travaux pour décrire formellement l'algorithme ou vérifier son bon fonctionnement. Intégrant des structures de données complexes et de la communication asynchrone entre des noeuds qui peuvent rejoindre ou quitter le réseau, ce protocole représente un intérêt certain pour la vérification formelle. La thèse se focalise sur le protocole Join de Pastry qui permet à un noeud de rejoindre le réseau. Les noeuds ayant intégré le réseau doivent avoir une vue du voisinage cohérente entre eux. La propriété principale de correction, appelée CorrectDelivery, assure qu'à tout moment il y a au plus un noeud capable de répondre à une requête pour une clé, et que ce noeud est le noeud le plus proche numériquement à ladite clé. Il n'est pas trivial de maintenir cette propriété en présence de churn. Ce travail nous a permis de découvrir des violations inattendues de la propriété dans les versions publiées de l'algorithme. Sur la base de cette analyse, le protocole IdealPastry est conçu et vérifié en utilisant l'assistant interactif à la preuve TLAPS pour TLA+. Le protocole LuPastry est obtenu en assouplissant certaines hypothèses de IdealPastry. Il est montré formellement que LuPastry vérifie CorrectDelivery sous l'hypothèse qu'aucun noeud ne quitte le réseau. Cette hypothèse ne peut être relâchée à cause du risque de perte de connexion du réseau dans le cas où plusieurs noeuds quittent le réseau en même temps / Pastry is a structured P2P algorithm realizing a Distributed Hash Table over an underlying virtual ring of nodes. Several implementations of Pastry are available, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines complex data structures, asynchronous communication, and concurrency in the presence of spontaneous join and departure of nodes, it makes an interesting target for verification. This thesis focuses on the Join protocol of Pastry that integrates new nodes into the ring. All member nodes must have a consistent key mapping among each other. The main correctness property, named CorrectDelivery, states that there is always at most one node that can deliver an answer to a lookup request for a key and this node is the numerically closest member node to that key. This property is non-trivial to preserve in the presence of churn. In this thesis, unexpected violations of CorrectDelivery in the published versions of Pastry are discovered and analyzed using the TLA+ model checker TLC. Based on the analysis, the protocol IdealPastry is designed and verified using the interactive theorem prover TLAPS for TLA+. By relaxing certain hypotheses, IdealPastry is further improved to LuPastry, which is again formally proved correct under the assumption that no nodes leave the network. This hypothesis cannot be relaxed in general due to possible network separation when particular nodes simultaneously leave the network

La propension des systèmes informatiques à subir des défaillances matérielles est à l'origine d'une recherche abondante afin de concevoir des systèmes dits tolérants aux pannes. Le procédé couramment retenu consiste à procéder à des réplications, donnant alors naissance à ce que l'on nomme un système distribué. La question se pose alors de savoir si l'on peut garantir que les multiples copies sont cohérentes entre elles. Ainsi, la recherche d'un accord devient-elle un problème à résoudre, à portée paradigmatique : le Consensus. Or, la complexité des algorithmes de Consensus rend la tache ardue : il n'est donc pas rare que l'on commette des erreurs lors de leur conception. De là découle l'idée, développée depuis plus de trente ans, de recourir à des procédés de vérification mécanique des algorithmes et de leurs preuves de correction. Ces procédés prennent place parmi ce que l'on désigne usuellement comme étant des méthodes formelles. C'est à la croisée des recherches en algorithmique distribuée et en méthodes formelles que se situent nos travaux. Plus spécifiquement, il s'agit de faire usage d'un logiciel de certification formelle, Isabelle/HOL, afin de garantir l'exactitude des preuves de correction d'algorithmes de Consensus exprimés dans un cadre formel uniforme du nom de Heard-Of, proposé en 2009 par Charron-Bost et Schiper. Nous montrons que, du fait de leur expression dans un même cadre formel, et du fait de leur proximité, suivant les cas, soit de conception (nombre de rondes, recours à des mécanismes de vote, ...) soit de forme syntaxique, soit d'hypothèses de fonctionnement (synchronisme partiel, ...), ces algorithmes présentent des preuves dont une part conséquente d?arguments sont communs. Cela permet de copier certains d'entre eux d'une preuve à l'autre, afin de réduire l'effort de certification : ces arguments peuvent alors être automatiquement évalués par la machine pour chacun d'entre eux, l'utilisateur n'ayant à intervenir que là où celle-ci est en peine, c'est-à-dire lorsque les différences algorithmiques induisent qu'il faille réviser les détails de l'argumentation. L'exposé que nous faisons de la certification que nous avons effectuée pour six algorithmes distribués dédiés à la résolution du problème du Consensus illustre cette démarche. Par conséquent, nous présentons d'abord les portions communes des démonstrations, puis détaillons ce qui est propre à chacune, l'objectif n'étant pas de permettre une lecture linéaire de chaque démonstration mais de mettre en évidence notre proposition / Computer systems fail. Whatever the reason of these failures, it has been a widespread approach to try and increase the faults-tolerance of a computer system through its replication. The resulting system is said to be a distributed one, in which replicas have to be kept consistent with each others. Hence, reaching agreement, and Consensus in particular, becomes the problem to solve - indeed, the paradigm. Solving Consensus (under various assumptions) is a hard task : algorithms designed on this purpose are subtle and proving their being correct is error-prone - whenever they are, which occasionally appears not to be the case. For more that thirty years, researchers interested in what is called Formal Methods have been working on mechanizing the verification process, in order to increase confidence in the correctness of (distributed) algorithms. The work we present here is at the intersection of distributed algorithms and formal methods. We use the Isabelle/HOL software to certify the correctness proof of various Consensus algorithms expressed in a uniform framework based on the Heard-Of Model, introduced by Charron-Bost and Schiper in 2009. Expressed in a common model, these algorithms, which, depending on the case, share some common mecanisms (number of steps, intermediate votes, ...), some elements of syntax, or types of assumptions (partial synchronism...), can be proved using some common arguments. As a consequence, the certification effort can be reduced by copying some intermediate lemmas from one proof to another and let the computer automatically parse them until some manual adaptation is required. This lead to the idea of certifying the correctness of multiple algorithms all together, instead of proving them one after the other, as one would do on paper in a traditional way. The effort of translation in the formal language of the proof assistant is then possibly reduced. Of course, each proof will also contain specific arguments, which will have to be isolated and translated into the software. Here, we illustrate this proposition through the presentation of formal certificates of correctness for six Consensus algorithms. As a consequence, on should not expect to find here a comprehensive linear presentation of each proof : we first show the arguments shared by multiple proofs, followed by those which are specific to each o them

Ces travaux de recherche ont été réalisés dans le cadre du projet régional Com-SLoT (Communauté de Services Logistiques sur l'Internet des Objets) qui s'inscrit dans l'axe des "outils numériques pour la performance industrielle" (2013-2016). Com-SLoT vise à mettre en place une communauté de services pour la gestion des objets logistiques. Il s'agit précisément de récolter et de partager toutes les informations nécessaires à la planification, l'exécution et la coordination des flux. Le problème qui est posé dans cette thèse est la "Modélisation des flux logistiques : vers une plate-forme d'interopérabilité des objets logistiques". Le modèle de flux de marchandises que nous cherchons à modéliser a donc pour objectif et défi principal de faciliter le développement et la mise en place des systèmes de gestion collaboratives de flux de marchandises basés sur l'Internet des objets et les plateformes cloud Computing. Ce défi scientifique et technologique peut se décliner en sous objectifs comme suit : (1) Proposer un modèle générique de flux logistique centré sur l'entité logistique en tant qu'entité autonome et communicante. (2) Passer de l’échange au partage : Collecter les données sur l'entité et le flux logistique, stocker et partager ces données à l'ensemble des acteurs de la supply chain. (3) Gérer l'hétérogénéité des données et les droits d'accès pour l'interopérabilité des flux. (4) Intégrer le flux de marchandises avec les technologies de l'internet des objets et des plateformes Cloud. (5) Réaliser une vrai plateforme collaborative en mode SaaS : dans ce cadre, il est plus question d'architecture et d'intégration / This research project was carried out within the framework of the regional project COM-SLoT (Community of Logistics Services on the Internet of Things). This project is in the field of "Digital tools for industrial performance". COM-SLoT aims to set up a community of services for the management of logistics workflows and related business entities. It is a matter of collecting and sharing all information necessary for the planning, the execution and the coordination of workflows. The problem to solve in this thesis is the "Modeling of logistic flows : towards a platform for business entities interoperability". The workflow model we are going to seek therefore has as main goal and challenges to facilitate the design of collaborative management of workflows, based on Internet of Things and Cloud Computing technologies. This challenge can be broken down into sub-goals as follows : (1) Propose a generic workflow model focused on the logistics entity as an autonomous and communicating entity. (2) Switching from peer to peer (PoP) data exchange to information sharing : collecting data on entities and workflows, storing and sharing to supply chain stakeholders. (3) Manage data heterogeneity and access rights to enable workflow interoperability. (4) Integrate Internet of Things technologies in the business entities. (5) Design a SaaS based collaborative platform to overcome existing architectural failures

Cette thèse se situe dans la problématique de la conduite en convoi de véhicules autonomes : des ensembles de véhicules qui se déplacent en conservant une configuration spatiale, sans aucune accroche matérielle. Ses objectifs sont d'abord, la définition d'une approche de prise de décision pour les systèmes de convois de véhicules, puis, la définition d'une approche de vérification, adaptée à la preuve de propriétés relatives aux convois de véhicules, avec une attention particulière envers les propriétés de sûreté.L'approche pour la prise de décision est décentralisée et auto organisée : chaque véhicule détermine son comportement de façon locale, à partir de ses propres capacités de perception, sans avoir recours à une communication explicite, de telle sorte que l'organisation du convoi, son maintien et son évolution soient le résultat émergeant du comportement de chaque véhicule. L'approche proposée s'applique a des convois suivant plusieurs types de configuration, et permet des changements dynamiques de configuration.L'approche proposée pour la vérification de propriétés de sûreté des convois de véhicules, adopte le model-checking comme technique de preuve. Pour contourner le problème de l'explosion combinatoire, rencontré dans la vérification des systèmes complexes, nous avons proposé une méthode compositionnelle de vérification, qui consiste a décomposer le système en sous systèmes et à associer une propriété auxiliaire à chacun des sous systèmes. La propriété globale sera ensuite déduite de l'ensemble des propriétés auxiliaires, par l'application d'une règle de déduction compositionnelle. La complexité calculatoire est mieux maîtrisée car le model-checking s'applique aux sous-systèmes. Nous proposons une règle de déduction adaptée aux systèmes de conduite en convoi, en particulier ceux qui sont basés sur des approches décentralisées. La règle considère chaque véhicule comme un composant. Elle est consistante sous la condition que l'ajout d'un nouveau composant au système n'a pas d'influence sur le comportement du reste du système. L'approche décentralisée proposée pour la conduite en convoi satisfait cette condition. Deux propriétés de sûreté ont été vérifiées : absence de collision et évolution confortable pour les passagers / This thesis places in the framework of Platoons, sets of autonomous vehicles that move together while keeping a spatial configuration, without any material coupling. Goals of the thesis are: first, the definition of a decision making approach for platoon systems. Second, the definition of a method for the verification of safety properties associated to the platoon system.The proposed decision making approach is decentralized and self-organized. Platoon vehicles are autonomous, they act based only on their perception capabilities. The configuration emerges as a result of the individual behavior of each of the platoon vehicle. The proposed approach can be applied to platoon with different configurations, and allows for dynamic change of configuration.The proposed verification method uses the model-checking technique. Model checking of complex system can lead to the combinatory explosion problem. To deal with this problem, we choose to use a compositional verification method. Compositional methods decompose system models into different components and associate to each component an auxiliary property. The global property can then be deduced from the set of all the auxiliary properties, by applying a compositional deduction rule. We define a deduction rule suitable for decentralised platoon systems. The deduction rule considers each vehicle as a component. It is applicable under the assumption that adding a new component to an instance of the system does not modify behavior of the instance. Two safety properties have been verified : collision avoidance.

Ce travail de thèse présente une méthode originale pour la simulation symbolique des circuits décrits au niveau algorithmique. Tout d'abord, la description VHDL du circuit est modélisée sous le forme d'un ensemble d'équations récurrentes (SER) qui décrivent l'état du système à un instant donné en fonction des états précédents. Après une extraction automatique du SER du circuit, l'algorithme de simulation VHDL est exécuté pendant un nombre fixe de cycles déterminé par le concepteur. Pendant la simulation, un scénario de test et une simplification par règles de substitution sont appliqués pour obtenir les expressions symboliques ou numériques de chaque objet du circuit (registre, signal ou port de sortie). Trois modes de test (raisonnement, exécution et mixte) sont définis et expliqués en se basant sur la distinction entre la partie opérative et la partie contrôle de circuit. Le simulateur symbolique et le compilateur sont implémentés avec l'aide du système Mathematica. <br />Une méthodologie de vérification autour de la simulation symbolique avec SER est proposée. Plusieurs paradigmes de vérification (la correspondance de forme, la démonstration de théorèmes et SAT) sont employés sur les résultats de la simulation symbolique pour valider ou prouver les propriétés du circuit. La méthodologie est montrée sur deux circuits de taille réelle (un filtre numérique et une mémoire) et sur de nombreux cas académiques.

Cette thèse présente un modèle formel représentant toute architecture de communication sur la puce. Ce modèle est mathématiquement décrit par une fonction nommée GeNoC. La correction de GeNoC est exprimée par un théorème montrant que tout message émis atteint sa destination sans modification de l'information qu'il transporte. Le modèle identifie les composantes communes à toute architecture et leurs propriétés essentielles, à partir desquelles est déduite la preuve du théorème sur GeNoC. Chaque composante est représentée par une fonction sans définition explicite, mais contrainte de satisfaire ses propriétés essentielles. Ainsi, la validation de toute architecture particulière consiste en la preuve que les définitions concrètes de ses composantes satisfont les propriétés essentielles. En pratique, ce formalisme a été réalisé dans la logique du démonstrateur de théorèmes ACL2. Une méthodologie associée au modèle fournit un support systématique pour la spécification et la validation des architectures de communication sur la puce à un haut niveau d'abstraction. Pour valider notre approche, nous avons exhibé différentes architectures constituant autant de concrétisations du modèle générique GeNoC. Ces concrétisations comprennent<br />notamment des systèmes industriels, comme le bus AMBA AHB ou le réseau Octagon de ST Microelectronics.

Cette thèse a pour but d'extraire tous les adjectifs coréens qui entrent dans la relation suivante : La trompe de l'éléphant est longue = L'éléphant est long de trompe et de les classer de manière formelle. Cette relation est appelée l'opération de restructuration. Le lexique déclenchant cette opération n'est rien d'autre qu'une des classes d'adjectifs que les linguistes coréens connaissent depuis longtemps. Ce sont les adjectifs sôngsang : mot composé de sông (nature) et sang (état). Leur nombre est considérablement élevé : parmi 5300 adjectifs, plus de 3000 entrent dans cette classe. La plupart des études concernant les adjectifs sôngsang sont concentrées sur une description sémantique ou une analyse d'une de ses sous-classes. Aucune étude ne porte sur une classification globale de manière formelle. C'est un des résultat de cette thèse : en nous fondant sur des propriétés syntaxiques, nous avons obtenu neufs principales classes syntaxiquement et sémantiquement homogènes.

La fouille de données est définie comme le traitement d'une grande quantité de données afin d'y extraire des connaissances non triviales et utiles. Cette analyse permet de dégager de la masse d'informations des tendances, des regroupements de données et de formuler des hypothèses. Un des domaines de la fouille de données est la recherche de règles d'association. Les algorithmes utilisés en recherche de règles d'association ont généralement l'inconvénient de ne pouvoir identifier des règles dont un des termes est infréquent, mais qui appartient à une catégorie qui, elle, l'est. Les règles d'association multi-niveaux permettent d'identifier les associations impliquant des termes dont les niveaux de généralisation/spécialisation diffèrent. Les algorithmes de recherche de règles d'association multi-niveaux présentés à ce jour ont en commun la génération d'un nombre souvent très grand de règles redondantes. Notre contribution dans cette étude est constituée de la conception de deux algorithmes de recherche de règles d'association mutli-niveaux basés sur l'analyse formelle de concepts, ce qui permet de restreindre la génération des règles d'association aux seules règles informatives maximales. Nous avons également réalisé l'implémentation de ces deux algorithmes, en plus de celle d'un autre algorithme utilisé aux fins de comparaison dans la littérature. Nous avons finalement comparé expérimentalement ces trois implémentations et les résultats obtenus confirment l'intérêt de l'approche basée sur l'analyse formelle de concepts, tout en illustrant l'effet des optimisations apportés au traitement. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Treillis de Galois (treillis de concepts), Analyse formelle de concepts, Fouille de données (data mining), Règles d'association, Base de règles, Règles d'association multi-niveaux (règles d'association généralisées), Base de règles multi-niveaux (bases de règles généralisées).