Date : 2012
Editeur / Publisher : [S.l.] : [s.n.] , 2012
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : anglais / English
Résumé / Abstract : Le protocole NEO a été développé pour la gestion d’une base de données distribuée à grande échelle. Il est executé sur un ensemble de machines (nœuds) qui constituent un cluster de machines. Ce dernier contient plusieurs types de nœuds : des nœuds de stockage qui servent à stocker la base de données, plusieurs nœuds maîtres qui vont élire l’un d’eux (maître primaire) ayant la tâche de contrôler l’ensemble du cluster, et enfin les nœuds clients servant à l’envoi et à la réception des différentes requêtes. Dans le cadre des travaux de thèse, un modèle de réseaux de Petri coloré est proposé pour le protocole NEO. Ce modèle a été élaboré dans le but de spécifier et vérifier des propriétés attendues du protocole. Les phases d’élection du maître primaire ainsi que de démarrage ont été modélisées et vérifiées avec succès dans plusieurs configurations de base des données et du cluster. Les proprietés importantes de protocole ont été formalisées et verifiées automatiquement sûr plus d’une centaine des configurations initiales. Les résultats négatifs ont été soumis à l’analyse inverse. Dans le même temps, une nouvelle methodologie de modélisation été proposée. La méthode comprend plusieurs étapes présis à suivre pour obtenir un réseau de Petri coloré à partir du code source de haut niveau orienté objet.
Résumé / Abstract : The NEO protocol was developed to manage a large scale distributed data base. It is executed on a set of machines (nodes) that form a cluster. The cluster consists of nodes of different types: storage nodes, which store the database, several master nodes, which choose one among them (the primary master) that will control the whole cluster, and, finally, client nodes which send and receive different requests from users. As part of the thesis work, a coloured Petri net model was proposed for the NEO protocol. This model was constructed for the purpose of specification and verification of the expected properties of the protocol. The phases of the election of the primary master as well as the bootstrap phase was modelled and successfully verified on various cluster and database configurations. The important properties of the protocol were found, formalised and automatically verified on more than a hundred initial configurations. The negative results were subjected to backward analysis. At the same time, a new modelling methodology was proposed. The method consists of precise steps to follow in order to get a coloured Petri net model from high level object oriented source code, thus achieving retro-engineering.