Le développement de systèmes distribués présente des défis significatifs, principalement en raison de la complexité introduite par la concurrence non déterministe et les pannes. Pour y remédier, nous proposons un cadre de développement piloté par spécifications. Notre méthode comprend trois étapes clés. La première étape définit les spécifications du système et les invariants en utilisant TLA^+. Cela nous permet de réaliser une vérification de modèle sur la fiabilité de l'algorithme et de générer des cas de test pour les phases de développement suivantes. Dans la deuxième étape, sur la base des spécifications établies, nous écrivons du code pour garantir la cohérence et l'exactitude de l'implémentation. Enfin, après avoir terminé le processus de codage, nous testons rigoureusement le système en utilisant les cas de test générés lors de la première étape. Ce processus garantit la qualité du système en maintenant une forte connexion entre la conception abstraite et l'implémentation concrète par le biais d'une vérification continue.
Hua et al. (Mon,) ont étudié cette question.