Master 2013 2014
Stages de la spécialité SAR
Vérification formelle d’un protocole de routage distribué pour réseaux de capteurs sans fil à large échelle


Site :LIPN
Lieu :Université Paris 13, LIPN (UMR 7030 CNRS) et L2TI
Encadrant : Laure Petrucci (laure.petrucci@lipn.univ-paris13.fr) Saadi Boudjit(boudjit@univ-paris13.fr)
Dates :standard
Rémunération :standard
Mots-clés : Parcours SAR autre qu’ATIAM, recherche, Parcours SAR, aussi pour STL

Description

Les nœuds constituant un réseau de capteurs sans fil (WSNs) sont capables de communiquer en mode ad hoc en utilisant un protocole de routage et d’envoyer des informations sur leur environnement (température, détection d’incendie, mesures effectuées dans un champ agricole, ...). Cependant, l’utilisation des protocoles de routage proposés à l’origine pour les réseaux sans fil ad hoc n’est pas souhaitable dans un réseau de capteurs sans fil où la consommation d’énergie des nœuds est un facteur clé dans la durée de vie du réseau. En effet, bon nombre de fonctions dans les protocoles de routage pour réseaux sans fil ad hoc sont liées à la gestion de la mobilité or les nœuds dans un réseau de capteurs sans fil sont souvent statiques. De plus, dans un réseau de capteurs sans fil le collecteur de données, appelé communément Sink, est la seule destination pour les données. Dans ce contexte, l’équipe réseau du L2TI s’est focalisée sur le problème de dissémination des données avec économie d’énergie dans les réseaux de capteurs sans fil à large échelle avec Sink mobile. Un protocole de routage distribué appelé SN-MPR a été proposé. Ce protocole 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. Une autre variante du protocole, appelée duty-cycle SN-MPR, permet d’économiser l’énergie des capteurs en permettant à ceux qui ne sont pas MPR d’éteindre leurs radios respectives quand ils n’ont pas de données à transmettre vers le Sink. Les résultats de simulation ont montré que le protocole permet une consommation d’énergie parfaitement distribuée dans un réseau de capteurs sans fil avec Sink mobile et permet d’augmenter ainsi la durée de vie du réseau.

Ce stage s’inscrit autour du protocole de routage pour réseaux de capteurs sans fil précédemment mentionné. L’objectif est de compléter l’évaluation de performances obtenue par simulation, par une vérification formelle du protocole. Dans un premier temps, le stagiaire se familiarisera avec le protocole SN-MPR et avec le routage dans les réseaux de capteurs sans fil de manière générale. Dans un second temps et avec l’aide de l’équipe LCR du laboratoire LIPN, le stagiaire se verra attribuer la tâche de vérifier le bon fonctionnement du protocole et d’en quantifier la robustesse par des méthodes de vérification formelle pour protocoles distribués. La vérification consistera à prouver la bonne adéquation du routage. La quantification consiste à mesurer la vitesse maximale du Sink pour laquelle le protocole satisfait toujours sa spécification. Le formalisme des réseaux de Petri temporels sera employé.