Analyse Formelle des Protocoles de Communication des Réseaux de Capteurs sans Fil Corporels

Abstract

Cette thèse porte sur l'évaluation des performances des protocoles de contrôle d'accès au support (MAC) pour le réseau de capteurs corporel sans fil (WBAN) par le biais des méthodes de la vérification formelle. L'importance des WBAN a incité les chercheurs à proposer de nouveaux protocoles MAC afin de satisfaire les exigences des WBAN, ce qui nous a conduits à élaborer, dans un premier travail, une analyse comparative, quantitative/qualitative, des protocoles MAC existants pour les WBAN. Selon nos résultats de comparaison, le protocole MAC de la norme IEEE 802.15.6 prend en compte la majorité des exigences des WBAN. Pour valider l'utilité de ce protocole pour les WBAN, nous avons proposé d'évaluer, comme partie centrale de cette thèse, ses performances par une analyse formelle. Nous avons évalué les performances de ses méthodes d'accès Posting/CSMA/CA via le Model-Checker UPPAAL-SMC. Ensuite, nous avons amélioré les performances de la méthode d'accès CSMA/CA en termes de compteur d'attente (BC)/de fenêtre de contention (CW). Le Model-Checker UPPAAL-SMC peut fournir une interprétation stochastique du comportement stochastique des systèmes complexes/temps réel, tels que les WBAN. La modélisation/l'évaluation du comportement des protocoles MAC via les spécifications des automates temporisés stochastiques (STA)/de la logique temporelle d'intervalle métrique (MITL) adoptées par UPPAAL-SMC, nécessitent un certain niveau d'expertise. La chose qui n'est pas disponible pour de nombreux concepteurs de protocoles MAC. Pour faciliter l'utilisation des puissants algorithmes d'analyse d'UPPAAL-SMC, nous avons proposé de définir un prototype d'une approche d'ingénierie dirigée par les modèles (MDE) qui utilise un langage de modélisation spécifique au domaine (DSML) comme point de départ/UPPAAL-SMC comme cible.