Vérification formelle, Vérification, Test, Consistance, Concurrence, Consistance séquentielle, Tso, Consistance causale, Systèmes distribués

Aujourd'hui, nous sommes tous des utilisateurs de systèmes distribués. Un système distribué est un ensemble d'ordinateurs afin d'améliorer les performances par le partage des ressources. En effet, avec l'explosion massive d'Internet, ces systèmes sont devenus nécessaires. Malheureusement, en raison du parallélisme et de la latence de communication sur les grands réseaux, les systèmes distribués peuvent produire des comportements inattendus (incohérents) s'ils ne sont pas correctement conçus et implémentés. Par exemple, un siège dans un vol peut être attribué à deux utilisateurs d'un système de réservation de vol au même temps. Cette thèse aborde le problème de vérifier qu'une implémentation d'un système concurrent / distribué offre à ces clients les garanties de consistance attendues (consistance forte, faible ou éventuelle). En particulier, nous considérons le problème du test des systèmes concurrents / distribués pour déterminer s'ils offrent le niveau de consistance attendu par leurs utilisateurs. Pour une exécution d'un système concurrent / distribué donnée, le test confirme la consistance ou l'inconsistance du système lors de cette exécution. Nous proposons des approches de vérification dynamique par rapport à certains modèles de consistance très connus, i.e., en exécutant un grand nombre de programmes de test et en les vérifiant par rapport à un modèle de consistance donné. Le principal critère de consistance que nous considérons dans cette thèse est un modèle fondamental appelé la consistance séquentielle. Le problème de vérification de ce modèle est connu pour être NP-difficile. La raison est que, pour prouver qu'une exécution est conforme à ce modèle de consistance, il faut trouver un ordre total sur les opérations d'écriture qui l'explique. Par conséquent, il faut énumérer tous les ordres totaux possibles, dans le pire des cas. Au début, nous nous intéressons à vérifier la conformité à des modèles de consistance vérifiables en temps polynomial à l'aide de techniques basées sur la saturation. Nous considérons le modèle de la consistance causale dans ses différentes variantes. Ensuite, nous nous appuyons sur ces travaux pour proposer une approche de vérification de la consistance séquentielle en se basant sur une variante plus forte de la consistance causale. Cette approche est améliorée par la suite en proposant un autre modèle faible basé sur des règles de saturation plus naturelles et plus simples. Ces approches permettent d'éviter de tomber systématiquement dans le pire des cas i.e., énumérer explicitement le nombre exponentiel des ordres totaux possibles entre les écritures de l'exécution. Ces deux approches sont ensuite généralisées pour couvrir un autre modèle de consistance qui est une relaxation de la cohérence séquentielle appelée "Total Store Ordering" (TSO). Le problème de la vérification de ce modèle est également connu pour être NP-difficile. En effet, la généralisation proposée utilise des modèles convenables pour approximer le modèle TSO. Nous avons implémenté toutes ces approches et réaliser des benchmarks sur des applications réelles.