Description
Date depot: 1 janvier 1900
Titre: Modèles et Algorithmes pour les Systèmes Emergents
Directeur de thèse:
Sébastien TIXEUIL (LIP6)
Directrice de thèse:
Maria POTOP-BUTUCARU (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Les réseaux de capteurs statiques et/ou mobiles ont reçu récemment une attention considérable et constituent un pole de recherche émergent dans le domaine plus général de l'algorithmique distribuée. En effet, l'ère des robots coûteux dédiés à une seule tâche est passée. La tendance aujourd'hui est au déploiement de réseaux de capteurs mobiles qui sont collectivement en mesure d'exécuter diverses tâches complexes.
Une application possible de ces réseaux est par exemple d'optimiser la couverture de zones en situation de catastrophe naturelle ou humaine, et d'aider dans les tâches de recherche et de sauvetage. Dans les opérations de secours, les sauveteurs doivent travailler rapidement pour être en mesure de sauver les victimes, mais ils sont souvent limités par une main d'œuvre insuffisante, par leur incapacité à atteindre des espaces confinés et par le manque d'informations sur l'emplacement et l'état des victimes. Dans ce contexte, les réseaux de capteurs mobiles peuvent être un précieux atout pour la recherche des victimes et l'aide aux équipes de sauvetage.
Le trait caractéristique des réseaux de capteurs mobiles est le dynamisme extrême de leur structure, de leur contenu et de leur charge. Dans ces systèmes, les nœuds peuvent rejoindre, quitter et changer leur position physique à volonté avec un impact très fort sur la topologie du système. En outre, la fluctuation de la quantité d'énergie dans leur batteries induit également un dynamisme très fort du système (c.à.d. la taille du système et sa topologie sont susceptibles de changer au cours de tout calcul qui pourrait avoir lieu).
Le projet 'PACTOLE' vise à proposer une plateforme formelle basée sur les avancées récentes dans les preuves automatiques et les domaines liés, afin de prouver l'exactitude des protocoles distribués localisés dans les réseaux de capteurs mobiles. Jusqu'à présent, l'exactitude de ces systèmes a été partiellement explorée, soit via des simulations et des expérimentations restrictives ou via des outils analytiques construits sur des hypothèses restrictives (par exemple les caractéristiques et le statut des nœuds ne changent pas au cours de toute l'exécution du système, etc.).
Ces hypothèses peuvent être complètement irréalistes dans les réseaux actuels, et donc désastreuses en pratique. Etudier formellement et automatiquement l'impact du dynamisme des réseaux sur les protocoles localisés n'a jamais été réalisé. Les preuves d'exactitude des systèmes susmentionnés devraient être fondées sur un modèle théorique, capable d'encapsuler le comportement dynamique de ces systèmes qui doivent résister à des changements fréquents. En effet, l'exactitude de ces systèmes ne peut être basée uniquement sur les périodes non dynamiques, car elles peuvent être absentes ou très courtes.
Doctorant.e: Bouzid Zohir