Le pôle MathStic de l'université Paris 13 organise une journée "Conception et Vérification Formelle de Protocoles Distribués" le 26 Novembre 2013.
La journée aura lieu en salle L322/324, Institut Galilée, Université Paris 13.
La journée aura lieu en salle L322/324, Institut Galilée, Université Paris 13.
Le programme de la journée est le suivant:
09h00 Accueil
09h15 Fabrice Kordon (Professeur, LIP6-UPMC) : Verification of a Quasi certification Protocol over a Distributed Hash Table (DHT).
10h00 Pause
10h30 Isablle Augé-Blum (MdC, CITI - INSA Lyon) : Validation formelle de protocoles temps réel pour réseaux de capteurs sans fil.
11h15 François Vernadat (Professeur, LAAS) : Fiacre/TINA: Un environnement pour la description et vérification de systèmes temps réel.
12h00 Buffet
13h30 Saadi Boudjit (MdC, L2TI-UP13) : SN-MPR: Protocole de Routage Optimisé pour Réseaux de Capteurs Sans Fil à Large Echelle.
14h15 Laure Petrucci (Profeseur, LIPN-UP13) : Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs.
15h00 Pause
15h30 Salim Allal (Doctorant, L2TI-UP13), Saadi Boudjit (MdC, L2TI-UP13) : GeoSUZ: A Geocast Routing Protocol in SubZORs for Vanets.
16h15 Sami Evangelista (MdC, LIPN-UP13) : Formal Analysis of the NEO Protocol for Large Scale Distributed Database.
17h00 Table ronde et clôture.
Pour des raisons d'organisation, merci de nous prévenir par mail si vous souhaitez venir (
Saadi BOUDJIT, Kaïs KLAI (organisateurs de la journée).
Résumés:
1- Fabrice Kordon (Professeur, LIP6-UPMC) : Verification of a Quasi certification Protocol over a Digital Hash Table (DHT)
Résumé: Building a certification authority (CA) that is both decentralized and fully reliable is impossible. However, the limitation thus imposed on scalability is unacceptable for many types of information systems, such as e-government services. This paper presents a potential solution to this problem and its verification by means of Petri Nets.
2- Isablle Augé-Blum (MdC, CITI - INSA Lyon) : Validation formelle de protocoles temps réel pour réseaux de capteurs sans fils.
Résumé: à venir
3- François Vernadat (Professeur, LAAS) : Fiacre/TINA: Un environnement pour la description et vérification de systèmes temps réel.
Résumé: Les réseaux de Petri temporels enrichissent les transitions d’un réseau de Petri par des intervalles de temps qui spécifient les retards
temporels admissibles entre la sensibilisation des transitions et leur tir effectif. Parmi les extensions temporisées des réseaux de Petri, ce modèle
est le plus utilisé; Il bénéficie en outre de techniques d’analyse automatiques bien établies (graphes de classes).TINA (TIme Petri Net Analyzer) est
un environnement logiciel permettant l’édition et l’analyse de réseaux de Petri temporels étendus avec des priorités et un traitement de données
externes synchronisé avec l’évolution du réseau. Sur ces modèles, TINApermet la vérification de propriétés par model-checking pour, notamment, la
logique temporelle à temps linéaire State/Event LTL.
Fiacre — Format Intermédiaire pour les Architectures de Composants Répartis Embarqué — est un langage formel pour la description de systèmes
temps réel. Fiacre a été initialement développé en collaboration avec IRIT/Acadie et INRIA/Vasy dans le cadre de l’ACIéponyme et du projet
Topcased, avec pour objectifs de servir de modèle “pivot” pour la traduction, en vue de leur vérification, des formalismes utilisateurs tels que AADL ou
UML dans les modèles de bas niveau compris par les outils de vérification (comme Tina ou CADP). Le langage FIACRE décrit des composants. Les
composants élémentaires sont des machines à états étendues; des composants plus complexes sont décrits hiérarchiquement, et de façon
compositionnelle, par assemblage de composants plus simples dont les interactions peuvent être contraintes par des exigences temporelles et des
priorités. À des fins de vérification, les descriptions Fiacre, enrichies de déclarations de propriétés, peuvent être traduites dans le formalisme des
réseaux temporels accepté par la boîte à outils TINA par un compilateur dédié (frac). Les propriétés temporisées sont traduites par le compilateur en
propriétés non temporisées (donc vérifiables avec les outils disponibles) après instrumentation automatique des descriptions Fiacre par des observateurs.
4- Saadi Boudjit (MdC, L2TI-UP13) : SN-MPR: Protocole de Routage Optimisé pour Réseaux de Capteurs Sans Fil à Large Echelle.
Résumé: Ces dernières années, beaucoup d'efforts ont été fournis pour destravaux de recherche sur le routage dans les réseaux ad hoc. Cela a aboutit à l’avènement de standards tels que OLSR[RFC 3626] et AODV[RFC 3561].Cependant, des études précédentes ont montré que ces protocoles de routagene sont pas adaptés dans le cas des réseaux de capteurs sans fil (WSNs) où laconsommation d’énergie des noeuds est un facteur clé dans la durée de vie duréseau de manière générale. Dans ce travail, nous nous sommes focalisés sur la conception de protocolesde routage pour les réseaux de capteurs sans fil avec optimisation de la consommation d’énergie. Nous avons étudié le problème de dissémination des donnéesdans les réseaux de capteurs sans fil à large échelle et dans lesquels le collecteurde données, appelé communémentsink, est mobile. on aproposé deux algorithmes de routage distribués. Le premier algorithme, appeléSN-MPR, permet de limiter la propagation des messages de contrôle sur la localisation du sink aux seules zones affectées par la mobilité de ce dernier. Ledeuxième algorithme, appelé duty-cycle SN-MPR, permet d’économiser l’énergiedes capteurs en permettant à ceux qui ne sont pas MPR d’éteindre leurs radiosrespectives quand ils n’ont pas de données à transmettre vers le sink.
5- Laure Petrucci (Profeseur, LIPN-UP13) : Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs.
Résumé: Quantifier la robustesse d'un système temps-réel consiste à mesurer l'étendue maximale des délais temporels pour laquelle le système satisfait toujours sa spécification. Dans ce travail, nous introduisons une notion de robustesse plus précise, en mesurant les variations de délais admises dans leur voisinage. Nous considérons ici le formalisme des réseaux de Petri temporels avec arcs inhibiteurs. Nous utilisons la méthode inverse, définie initialement pour les automates temporisés. Ses résultats se présentent sous la forme de contraintes linéaires paramétrées reliant tous les délais. Nous exhibons aussi une condition et une construction pour obtenir un système robuste à partir d'un système non robuste.
6- Salim Allal (Doctorant, L2TI-UP13), Saadi Boudjit (MdC, L2TI-UP13) : GeoSUZ: A Geocast Routing Protocol in SubZORs for Vanets.
Résumé: Vehicular Ad Hoc Networks (Vanets) are characterized by highly speed nodes, highly dynamic topology and frequent link disconnections. This raises a number of challenges especially in the field of data dissemination. Our study focuses on Geocast routing which consists on routing a message from a unique source vehicle to all vehicles located in a well geographically defined destination area called ZOR (Zone Of Relevance). While in literature ZORs are often assumed to be of any form and still chosen according to the scenarios and motivation needs of the authors, in this work we consider a ZOR as a set of sub-ZORs and we choose simple geometrical forms for each sub-ZOR so that they would be easy to implement and to represent mathematically. We then provide a geometrical vision angle based technique to define if two sub-ZORs are in the same direction in order to send them a single message, and hence, reduce messages overhead. Finally, we introduce a new routing protocol in Sub-ZORs for VANETs callaed GeoSUZ and based on our geometrical vision angle and greedy forwarding techniques.
7- Sami Evangelista (MdC, LIPN-UP13) : Formal Analysis of the NEO Protocol for Large Scale Distributed Database.
Résumé: The NEO system, designed by the Nexedi company, is a distributed database management system which aims at supporting large scale distributed databases. The system targets software of which security data is a critical issue that must be ensured before the software can be released on the market. Thus, special care has been given during the design of this system to prevent faults such as node failures. In this talk we describe the formal analysis of this system that has been carried out within the Neoppod project. This analysis followed a reverse engineering approach from the Python code to extract a coloured Petri net model. We then used several analysis tools to perform verification so as to verify that the system has the desired behaviour.