Please use this identifier to cite or link to this item: http://archives.univ-biskra.dz/handle/123456789/10979
Full metadata record
DC FieldValueLanguage
dc.contributor.authorbenaoune, siham-
dc.date.accessioned2018-09-02T09:39:26Z-
dc.date.available2018-09-02T09:39:26Z-
dc.date.issued2017-06-20-
dc.identifier.urihttp://archives.univ-biskra.dz/handle/123456789/10979-
dc.description.abstractNous 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.en_US
dc.description.sponsorshipuniv-biskra.dzen_US
dc.language.isoaren_US
dc.publisheruniv-biskraen_US
dc.subjectType des paquets MQTTen_US
dc.subjectComportement de synchronisation des méthodes qui donnent lieu à des requêtes au brokeren_US
dc.subjectDiagramme du client MQTTen_US
dc.subjectDiagramme du broker MQTTen_US
dc.subjectModèle d’un broker phase de publication côté Publisheren_US
dc.subjectModèle de Subscriberen_US
dc.titleEvaluation de performance de protocoles dans l’internet des objets à base de méthodes formellesen_US
dc.typeMasteren_US
Appears in Collections:Faculté de Droit et des Sciences Politiques (FDSP)



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.