Evaluation de performance de protocoles dans l’internet des objets à base de méthodes formelles

Abstract

Nous nous sommes intéressés, au cours de ce mémoire, à l'étude formelle d'un protocole utilisé dans l’internet des objets qui est le protocole MQTT (Message Queue Telemetry Transport). Cette étude fait appel aux méthodes formelles qui sont exploitées pour assurer la fiabilité des systèmes conçus ou déjà réalisés. Ces méthodes offrent en même temps: des langages pour la spécification des systèmes, des langages pour la spécification des propriétés que l'utilisateur cherche à avoir, et en fin les algorithmes permettant de vérifier ces propriétés sur ces systèmes. Parmi ces méthodes formelles pour la vérification: Model-checking statistique (Stastical Model Checking SMC) permet de rendre certaines propriétés décidables, en limitant l'exploration de l'espace d'états d'un système. Cette méthode permet aussi de produire des probabilités sur la satisfaction ou non de certaines propriétés et donc peut être considérée comme une solution là où le model-checking classique se rend incapable. Ce travail était réalisé en quatre phases: 1. Etudier les caractéristiques essentielles et les notions fondamentales des protocoles de l’internet des objets; 2. Explorer le domaine des méthodes formelles; 3. Etudier les caractéristiques essentielles et les notions fondamentales du protocole sujet de cette étude MQTT V.3.1.1 4. Modéliser et vérifier le protocole choisi en évaluant ses performances avec SMC-UPPAAL. Nous avons rencontré plusieurs obstacles mais, la description du protocole par ses auteurs était trop riche d’après notre point de vue et les forums en répondus à certaines lacunes. Nous sommes limités dans le développement à construire un prototype qui permet de traduire les variables MQTT et de générer un squelette de modélisation UPPAAL. Le présent travail nous a donné plusieurs idées à développer dans le futur et comme perspectives, nous proposons : • D’améliorer le modèle proposé en prenant en considération les fonctions non modélisé comme le filtrage des topics ou la gestion de la retransmission dans le cas de non réception d’acquittement • D’Etudier approfondiment des algorithmes exploités dans l'outil UPPAAL et proposition d'amélioration possible, ou l'implémentation d'autres algorithmes non encore implémentés; par éxemple

• D’étendre ce travail pour pouvoir déceler les fragments de modélisation qui sont la source au non satisfaction des propriétés à vérifier, et pour qu’il puisse prendre en compte d’autres fragments de modélisations que nous n’avons pas pris en considération et de même pour élargir les classes des propriétés à vérifier. • Vérifier d'autres protocoles en utilisant le modèle checking statistique; et surtout établissement de comparaison raffinée avec d’autres protocoles de l’IOT comme COAP (Constrained Application Protocol) qui tente d’adapter HTTP a l’IOT..

À la fin de ce mémoire, nous considérons que nous avions développé plusieurs acquis sur le domaine des techniques de vérification formelle.