Parameterized verification of networks of many identifical processes
Vérification paramétrée de réseaux composés d'une multitude de processus identiques
Paulin Fournier
http://people.irisa.fr/Paulin.Fournier/
Advisors: Nathalie Bertrand and Thierry Jerron
Soutenance de thèse - Jeudi 17 décembre 2015
Les transparents
PAROSH ABDULLA Professeur Université d’Uppsala , Rapporteur
JÉROME LEROUX Directeur de recherche CNRS LaBRI, Rapporteur
SADDEK BENSALEM Professeur Université Joseph Fourier Grenoble, Examinateur
JOOST-PIETER KATOEN Professeur RWTH Université de Aachen, Examinateur
SOPHIE PINCHINAT Professeur Université Rennes 1, Examinatrice
THIERRY JÉRON Directeur de recherche INRIA, Directeur de thèse
NATHALIE BERTRAND Chargée de recherche INRIA, Co-directrice de thèse
ARNAUD SANGNIER Maître de conférence Université Paris Diderot, Co-directeur de thèse
Ce travail s'inscrit dans le cadre de la vérification formelle de programmes. La vérification de modèle permet de s'assurer qu'une propriété est vérifiée par le modèle du système. Cette thèse étudie la vérification paramétrée de réseaux composés d'un nombre non borné de processus identiques où le nombre de processus est considéré comme un paramètre.
- Concernant les réseaux de protocoles probabilistes temporisés nous montrons que les problèmes de l'accessibilité et de synchronisation sont indécidables pour des topologies de communication en cliques. Cependant, en considérant des pertes et créations probabiliste de processus ces problèmes deviennent décidables.
- Pour ce qui est des réseaux dans lequel les messages n'atteignent qu'une sous partie des composants choisie de manière non-déterministe, nous prouvons que le problème de l'accessibilité paramétrée est décidable grâce à une réduction à un nouveau modèle de jeux à deux joueurs distribué pour lequel nous montrons que l'on peut décider de l'existence d'une stratégie gagnante en co-NP.
- Finalement, nous considérons des stratégies locales qui permettent d'assurer que les processus effectuent leurs choix non-déterministes uniquement par rapport a leur connaissance locale du système. Sous cette hypothèse de stratégies locales, nous prouvons que les problèmes de l'accessibilité et de synchronisation paramétrées sont NP-complet.