MeFoSyLoMa
Méthodes Formelles pour les Systèmes Logiciels et Matériels
Vendredi 30 septembre 2011C. Démoulins (LIP6, Alligator) ; E. Best (Univ. Oldenburg); A. Dedova
09h00-10h30: Alligator, la plate-fome d'outils MeFoSyLoMa
Introduction
- Objectifs de la plate-forme Alligator
- Architecture d'Alligator
- Un exemple d'intégration d'outils: Crocodile
11h00-12h30: Travaux pratiques - intégration d'un outil dans Alligator
- Intégration pas-à-pas d'un outil de statistique
Prérequis à installer sur vos machines pour ce TP: - Eclipse 3.6 version RCP/RAP
- Plugin m2eclipse
- Plugin Coloane (utiliser les "night updates" et prendre les composants "Core" et "Alligator external platform") Java6
- maven 3 (sous Unix, "mvn -version" permet de tester la version de maven)
14h00-15h00: E. Best, Univ. Oldenburg, "Distributable Petri Nets" (collaboration work with P. Darondeau)
Abstract: A Petri net is distributed if, given an allocation of transitions to (geographical) locations, no two transitions at different locations share a common input place. A system is distributable if there is some distributed Petri net implementing it.
This talk addresses the question of which systems can be distributed, while respecting a given allocation. The problem is stated formally as well as by examples, and the current status of this work is outlined.
15h00-15h30 : A. Dedova, LIPN, "Modelling of the NEO distributed storage protocol"
Abstract: De nos jours, les bases de données sont d'une taille de plus en plus conséquente du fait du rôle qu'elles jouent dans pratiquement tous les domaines de la vie. Par conséquence, la gestion d'une base de données doit être très efficace. En effet, plusieurs techniques de gestion de bases de données existent mais leur efficacité dépend généralement de la taille et de la structure de la base de données. Dans cette perspective et dans le cadre du projet NEOPPOD, un nouveau protocole (appelé NEO) a été proposé pour les bases de données distribuées de grand taille. Le protocole NEO a été développé pour la gestion d'une base de données distribuée. Il tourne sur un ensemble de machines (nœuds) qui constituent le cluster. 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ître qui vont élire l'un d'eux (maître primaire) qui aura la tâche de contrôler l'ensemble du cluster, les autres peuvent prendre le relais en cas de panne, et enfin les nœuds client servant à l'envoi et à la réception des différentes requêtes.
Dans le cadre de mes travaux de thèse, j’ai proposé un modèle de réseaux de Petri colorés symétriques 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 la mesure où aucune information n’est perdue (aussi dans le cas où il y a des transactions où les objets absents)..
15h30-16h00: pause café
16h00-16h30: vie du groupe
16h30-17h30: point sur l'organisation de FM'2012
Plus d'informations ici …
Fabrice.Kordon (at) nulllip6.fr