Modélisation, vérification et analyse des performances du protocole « Directed Diffusion » (Les réseaux de capteurs sans fils)

Abstract

Les réseaux de capteurs sans fils (RCSF) sont utilisés de plus en plus dans notre vie quotidienne ainsi que dans les domaines médicaux, militaires, agricoles et technologiques. Pour faire fonctionner un RCSF, on doit définir des protocoles de communication. Ces pƌotoĐoles doiveŶt gaƌaŶtiƌ uŶ ďoŶ foŶĐtioŶŶeŵeŶt de tels ƌĠseaudž, ŵais Đe Ŷ’est pas toujouƌs le Đas. OŶ doit doŶĐ ġtƌe sûƌ Ƌue l’iŶfoƌŵatioŶ ĐiƌĐule edžaĐteŵeŶt Đoŵŵe pƌĠvu dans le réseau. Pour garantir vraiment un bon fonctionnement de ces réseaux, on doit faire subir ces protocoles à des tests. Le ŵeilleuƌ ŵoLJeŶ pouƌ testeƌ Đes pƌotoĐoles est l’utilisatioŶ des ŵĠthodes foƌŵelles. Nous avons spécifié formellement le protocole de routage «Directed Diffusion» en utilisaŶt l’outil UPPAAL qui adopte le modèle des automates temporisés comme un modèle formel de spĠĐifiĐatioŶ. Nous avoŶs aussi passĠ Đe ŵodğle paƌ le Model CheĐkeƌ de l’outil UPPAAL pour vérifier certaines propriétés exprimées dans la logique temporelle. Afin de valider notre travail, nous avons analysé les performances de ce protocole par UPPAAL puis nous avons les comparés avec ceux du simulateur NS2 qui est l'un des simulateurs les plus utilisés dans le domaine des réseaux de communications.