Fondations vérifiées de systèmes de graphes distribués à grande échelle – VERDI

Les bases de données relationnelles font face à la complexité des données interconnectées et hétérogènes. Ainsi, les bases de données graphes ont gagné en popularité dans l'industrie et l'académie. Par exemple, certaines avec des données multiomiques ont été collaborativement conçues pendant la pandémie pour des analyses génomiques et le traçage de contacts (EU Datathon, CovidGraph, Covid-19 Knowledge Graph). Finance, télécommunications, journalisme et transports intelligents sont d'autres utilisations critiques sociétales. Cependant, le traitement à grande échelle de graphes géo-distribués nécessite des modèles qui posent encore des défis : la réplication, pour gérer des réseaux lents et peu fiables, le partitionnement, pour répartir de grands graphes, et la réplication partielle à proximité des clients, pour la localité. Aussi, les modèles local-first offrent une haute disponibilité, combinant partitionnement et réplication, pour accéder à une partie pertinente de données en cas de déconnexion. Si les mécanismes de distribution, tels que les types de données répliqués (RDT), sont utilisés par des bases clés-valeurs local-first, pour les bases de données graphes leur usage est largement inexploré. Cela est plus difficile, car il nécessite la maintenance des invariants de connectivité complexes compositionnels. VERDI propose une méthodologie interdisciplinaire pour concevoir des RDT graphes (GRDT) fiables, recoupant les domaines des bases de données, des systèmes distribués, des méthodes formelles et des langages de programmation. Il comprend quatre packages de travail (WP). WP1 fournira un fondement formel unifié pour le prototypage et l'extraction des GRDT corrects par construction. WP2 les adaptera pour assurer la préservation des invariants complexes dans des modèles à faible cohérence. WP3 étendra les GRDT avec la paramétricité et les transactions, et WP4 évaluera leurs performances sur le cas industriel d’un registre décentralisé basé sur des graphes.