Université de Rennes 1 Parameterized verification of networks of many identical processesVérification paramétrée de réseaux composés d'une multitude de processus identiques Vérification paramétrée de réseaux composés d'une multitude de processus identiques Vérification paramétréevérification de modèlescomplexitéprobabilitéprotocoles de diffusion model checkingparameterized verificationcomplexityprobabilitybroadcast protocols Logiciels -- Vérification Thèses et écrits académiques 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 coNP. 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. This thesis deals with formal verification of distributed systems. Model checking is a technique for verifying that the model of a system under study fulfills a given property. This PhD investigates the parameterized verification of networks composed of many identical processes for which the number of processes is the parameter. Considering networks of probabilistic timed protocols, we show that the parameterized reachability and synchronization problems are undecidable when the communication topology is a clique. However, assuming probabilistic creation and deletion of processes, the problems become decidable. Regarding selective networks, where the messages only reach a subset of the components, we show decidability of the parameterized reachability problem thanks to reduction to a new model of distributed two-player games for which we prove decidability in coNP of the game problem. Finally, we consider local strategies that enforce all processes to resolve the non-determinism only according to their own local knowledge. Under this assumption of local strategy, we were able to show that the parameterized reachability and synchronization problems are NP-complete. Electronic Thesis or DissertationText en application/pdf1 : 1593 Kohttps://ecm.univ-rennes1.fr/nuxeo/site/esupversions/dcf39425-9237-417d-9590-0f5ba29a68eb Fournier Paulin 1989-09-19 FR 194641805 paulin.fournier@gmail.com 2015REN1S170 http://www.theses.fr/2015REN1S170 2015-12-17 Informatique Université de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiJéronThierryintervenant_1095612777BertrandNathalieintervenant_2111647339 MATISSEecoleDoctorale_1 139007164 Université européenne de BretagnepartenaireRecherche_1 139075119 IRISA partenaireRecherche_2 026386909 ddc:004 JéronThierryBertrandNathalieUniversité de Rennes 1Sciences et technologie, médecine, pharmacie, odontologie, droit, économie, gestion, philosophieMATISSEÉcole doctorale Mathématiques, informatique, signal, électronique et télécommunications (Rennes)Université européenne de Bretagne Pôle de recherche et d'enseignement supérieur de Bretagne IRISA ASCII PDF 1631408