Contribution à la modélisation et à la vérification de réseaux de capteurs sans fil

Abstract

Un réseau de capteurs sans fil est constitué d’un ensemble de nœuds autonomes dotés de capteurs, conçus pour collecter des grandeurs physiques et environnementales. Les réseaux de capteurs sans fil ont de nombreuses applications, comme la surveillance de l’environnement ou le monitoring de l’état de santé d’un patient. Leur conception est complexe, car soumise à plusieurs contraintes : l’énergie limitée, les problèmes de concurrence, l’hétérogénéité des nœuds, et dans certains cas, le caractère critique. C’est pourquoi, il est nécessaire de vérifier et de valider ces systèmes, pour garantir que ces contraintes sont satisfaites. Plusieurs approches ont été proposées dans ce sens : – des études de cas qui modélisent de façon ad hoc et vérifient formellement un aspect d’un réseau de capteurs sans fil particulier (e.g., un protocole de communication). – des model checkers de programmes dont le but est de trouver des bugs dans l’implémentation des nœuds. – des langages de modélisation dédiés au domaine (Domain Specific Modeling Languages ou DSMLs) qui fournissent les concepts du domaine et supportent l’analyse ou la génération de code.

Cependant, les études de cas nécessitent une phase d’abstraction manuelle (donc potentiellement génératrice d’erreurs) du réseau par un expert en méthodes formelles et en réseaux de capteurs sans fil. Les model checkers de programmes interviennent tard dans le cycle de développement, ce qui augmente le coût, en cas de détection d’erreur. Les DSMLs supportent généralement la simulation ou la génération de code. La simulation ne permet pas de vérifier exhaustivement les comportements du système et peut donc omettre des scénarios problématiques. A ce stade, il n’existe donc pas de solution satisfaisante pour modéliser et vérifier un réseau de capteurs sans fil.

Nous proposons Verification of Wireless Sensor Networks (VeriSensor) un DSML pour les réseaux de capteurs sans fil, supportant la vérification formelle. VeriSensor est destiné à être utilisé par les experts du domaine en leur fournissant des concepts capturant les cas d’utilisation de ces systèmes : la collecte de données et la détection d’évènements. Il peut être transformé automatiquement en une spécification exprimée dans le langage formel des Instantiable Transition Systems (ITS). La vérification des propriétés est faite par model checking et le résultat est transmis à l’utilisateur.