Méthodes formelles, Systèmes distribués, Tests, Apprentissage par renforcement, Tests unitaires, Fuzzing

La croissance de l'internet moderne est rendue possible par des systèmes distribués à grande échelle, hautement disponibles et résilients. Ces systèmes permettent de répliquer les données à l'échelle mondiale tout en garantissant leur disponibilité en cas de défaillance. Pour garantir la fiabilité et la disponibilité en cas de défaillance, les systèmes s'appuient sur des protocoles distribués complexes. Pourtant, dans la pratique, des bogues dans la mise en oeuvre de ces protocoles distribués ont été la source de nombreux temps d'arrêt dans les bases de données distribuées les plus populaires. Garantir la correction des implémentations reste un défi de taille en raison du vaste espace d'états. Au fil des ans, de nombreuses techniques ont été mises au point pour garantir la correction des implémentations, allant de la vérification systématique des modèles à l'exploration aléatoire. Cependant, un développeur qui teste l'implémentation avec les techniques actuelles n'a aucun contrôle sur l'exploration. En effet, les techniques ne tiennent pas compte de la connaissance qu'a le développeur de l'implémentation. En outre, très peu d'approches utilisent les modèles formels des protocoles lors des tests de leurs implémentations. Les efforts consacrés à la modélisation et à la vérification de la correction du modèle ne sont pas mis à profit pour garantir la correction de l'implémentation. Pour remédier à ces inconvénients, nous proposons dans cette thèse trois nouvelles approches pour tester les implémentations de protocoles distribués - Netrix, WaypointRL, et ModelFuzz. Les deux premières techniques - Netrix et WaypointRL - sont des approches d'exploration biaisées qui prennent en compte l'input du développeur. Netrix est un nouvel algorithme de test unitaire qui permet aux développeurs de biaiser l'exploration d'un algorithme de test existant. Un développeur écrit des filtres de bas niveau dans un langage spécifique au domaine pour fixer des événements spécifiques dans une exécution qui sont appliqués par Netrix. WaypointRL améliore Netrix en acceptant des prédicats d'état de haut niveau comme points de passage et utilise l'apprentissage par renforcement pour satisfaire les prédicats. WaypointRL est efficace pour orienter l'exploration tout en exigeant moins d'efforts de la part du développeur. En utilisant des implémentations de protocoles distribués populaires, nous montrons qu'une contribution supplémentaire du développeur conduit à une exploration biaisée efficace et à des capacités améliorées de recherche de bogues. La troisième technique - ModelFuzz - est un nouvel algorithme de fuzzing qui comble le fossé entre le modèle et la mise en oeuvre du protocole. Nous utilisons les états du modèle comme couverture pour guider la génération d'entrées qui sont ensuite exécutées sur l'implémentation. Nous montrons, à l'aide de trois benchmark industriels, que les notions de couverture existantes sont insuffisantes pour tester les systèmes distribués et que l'utilisation de la couverture du modèle TLA+ pour tester les implémentations entraîne la decouverte de nouveaux bogues.