Université de Rennes Parameterized verification of distributed shared-memory systems Vérification paramétrée de systèmes distribués à mémoire partagée vérification paramétréesystèmes infinisalgorithmes distribués parameterized verificationinfinite-state systemsdistributed algorithms Systèmes à paramètres répartis Algorithmes parallèles Mémoire partagée répartie Les systèmes distribués sont constitués de plusieurs composantes informatisés (que nous appelons processus) qui interagissent pour accomplir une tâche commune. Un exemple de tâche est le consensus, où tous les processus doivent se mettre d’accord sur une valeur commune. Dans cette thèse, nous nous intéressons aux systèmes à mémoire partagée, où les processus interagissent en lisant et en écrivant dans une mémoire partagée. Nous ne travaillons pas directement sur des systèmes distribués, mais plutôt sur des modèles de ces systèmes, où nous considérons des questions de vérification automatique. Nos modèles sont paramétrés : le nombre de processus n’est pas fixé à l’avance et peut être arbitrairement grand, ce qui nous permet de vérifier le système pour tout nombre de participants. Cette hypothèse permet également des propriétés de monotonicité qui simplifient l’analyse. Notre modèle, inspiré par des algorithmes de consensus de la littérature, est à ronde : chaque processus évolue de manière incrémentale en un nombre appelé ronde, et où chaque ronde a sa propre mémoire partagée. Nous étudions de plus l’impact d’un ordonnanceur stochastique sur ce modèle à rondes. Notre approche est théorique et nous nous intéressons principalement à l’analyse de nos modèles et à la classification de nos problèmes en termes de classes de complexité. Distributed systems consist in several computerized components (called processes) interacting with one another to perform a common task. An example of such a task is consensus, where all processes must agree on a common value. In this thesis, we are interested in shared-memory systems where the processes interact via reading from and writing to a shared memory. We do not work directly on distributed systems, but rather on models of such systems, and we consider questions related to the automated verification of these models. Our models are parameterized: the number of processes is not fixed beforehand and may be arbitrarily large, so that we are able to verify the system regardless of the number of participants. They enjoy some monotonicity property, called copycat property, which simplifies the analysis. Motivated by consensus algorithms from the literature, we consider a model where each process evolves incrementally in a number called round and where each round has its own set of registers. Also, we study the impact of a stochastic scheduler on this round-based model. Our approach is theoretical and we are mostly interested in analyzing our models and in classifying our problems of interest in terms of complexity. Electronic Thesis or DissertationText en application/pdf1 : 2108 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/0896106b-647e-4473-96e3-07e85e04c134 Waldburger Nicolas 1997-11-28 FR 282918051 waldburger.nicolas@gmail.com 2024URENS058 http://www.theses.fr/2024URENS058 2024-12-11 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiBertrandNathalieintervenant_1111647339MarkeyNicolasintervenant_2073426482SankurOcanintervenant_817456306XWalukiewiczIgorintervenant_3078177146BertrandNathalieintervenant_1111647339MarkeyNicolasintervenant_2073426482EsparzaJavierintervenant_6110961552SznajderNathalieintervenant_7253130883Bouyer-DecitrePatriciaintervenant_4176675426Kučera‎Antonínintervenant_5146940113 MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 BertrandNathalieMarkeyNicolasWalukiewiczIgorBouyer-DecitrePatriciaKučera‎AntonínEsparzaJavierSznajderNathalieSankurOcanUniversité de RennesMATISSE IRISA ASCII PDF 2158179