Approches formelles pour l'analyse de la performabilité des systèmes communicants mobiles : Applications aux réseaux de capteurs sans fil

• Main Author: Abo, Robert
• Language: fra
• Published: Conservatoire national des arts et metiers - CNAM 2011
• Subjects: [INFO:INFO_OH] Computer Science/Other; [INFO:INFO_OH] Informatique/Autre; Systèmes communicants mobiles; Performabilité; Méthodes formelles; Algèbres de processus; Model checking; Chaînes de Markov; Automates temporisés probabilistes; Prism
• Online Access: http://tel.archives-ouvertes.fr/tel-00816392; http://tel.archives-ouvertes.fr/docs/00/81/63/92/PDF/ThA_se_-_R._-_Abo.pdf

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles.