• Home
  • Page : 'emploi' inconnue (menus.php)

 Thesis : Analyse et vérification de réseaux paramétrés (avec broadcast)

PhD school thesis
Nous nous intéresserons dans cette thèse à des systèmes distribués correspondant à des réseaux d’entités communicantes dont le nombre n’est pas fixé a priori et est donc considéré comme un paramètre. En effet, de nombreux algorithmes distribués sont conçus pour fonctionner avec un nombre arbitraire de processus, et les techniques habituelles de vérification automatique ne peuvent s’adapter immédiatement à de tels systèmes. Ils peuvent aussi être utilisés pour représenter des systèmes biologiques comme le modèle proposé dans [BDG+19] où toutes les entités du réseau réagissent à une information commune. Finalement les techniques développées pour leur analyse peuvent être utilisées pour l’amélioration de systèmes industriels dans lesquels les tâches sont assimilées aux entités du réseau et les synchronisations entre tâches sont simulées par les communications ; l’utilisation de méthodes formelles dans ce contexte permet ainsi de mieux comprendre les systèmes, mais aussi d’améliorer leur organisation en fournissant par exemple des méthodes pour planifier les tâches (ce qui correspondrait à la synthèse d’un ordonnanceur paramétré dans le cadre du réseau).
Dans ces réseaux, on suppose que toutes les entités exécutent le meme protocole (c’est-à-dire le meme programme). Selon le modèle utilisé pour la description du protocole (par exemple, un automate fini, un système à pile ou un automate équipé de choix probabilistes pour représenter l’incertitude), ou les moyens de communication entre les entités (passage de message, synchronisation par rendez-vous, broadcast de messages), l’expressivité du modèle change et les résultats sur la vérification de tels systèmes varient (voir par exemple [Esp14] pour une présentation détaillée des différences entre ces modèles).

Ce projet de recherche doctoral fait l’objet d’une demande de financement auprès de « Ecole Doctorale d‘Informatique, Télécommunication et d‘Electronique (EDITE) », le candidat retenu par son porteur devra donc participer au concours correspondant (prévoir un dossier et une audition) en vue d’obtenir le financement effectif.

More details here

Contact :Christine Tasson, Nathalie Sznajder