Description
Date depot: 7 avril 2022
Titre: Analyse et vérification de réseaux paramétrés avec broadcast
Directrice de thèse:
Christine TASSON (ISAE-SUPAERO)
Encadrante :
Nathalie SZNAJDER (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Modèles de calcul, preuve, vérification
Resumé: Le cadre de cette thèse est le développement de méthodes formelles pour les réseaux dans lesquels le nombre de participants est a priori non borné, et peut être vu comme un paramètre du système. Les résultats sur ces modèles peuvent être appliqués à différents domaines tels que la vérification de systèmes concurrents/distribués, l'analyse de systèmes biologiques ou encore la planification de tâches industrielles. De nombreux modèles pour ces réseaux paramétrés ont été développés en considérant différents types de communication (rendez-vous, mémoire partagée, broadcast).
Dans cette thèse nous souhaitons étudier les réseaux paramétrés communiquant par broadcast sélectif dans lesquels les configurations sont décrites par des graphes (appelés topologies de communication) et une entité peut recevoir un message si, et seulement si, elle est voisine du noeud émetteur. Pour ces réseaux deux principales hypothèses ont été considérées sur l'évolution de la topologie de communication lors des exécutions, soit elle reste fixe et dans ce cas la plupart des problèmes de vérification sont indécidables, soit elle peut changer de manière complètement non-déterministe ce qui permet de regagner la décidabilité de nombreux problèmes. Cette dernière hypothèse a été introduite afin de modéliser la mobilité dans les réseaux mais elle est assez peu réaliste car elle autorise trop de comportements.
Notre objectif est donc dans un premier temps de proposer un modèle plus réaliste de mobilité, en spécifiant par exemple, les mouvements autorisés à chaque étape (ce qui est une tâche complexe étant donné que le nombre de participants n'est pas connu a priori). Dans un second temps, nous mènerons une étude exhaustive des problèmes de vérification décidables sur ces nouveaux modèles en incluant également des notions de coût sur les actions afin de représenter par exemple la consommation d'énergie des noeuds qui est un facteur critique dans les réseaux ad hoc. Pour finir, nous nous intéresserons à des problèmes d'expressivité afin de mieux comprendre quelles toplogies de réseaux peuvent être extraites avec ces modèles à broadcast sélectif.