Vérification formelle d'un algorithme générique et hiérarchique d'exclusion mutuelle

National audienceDans un environnement distribué, l'exclusion mutuelle des accès aux ressources partagées est un problème fondamental. En s'adaptant aux contraintes des nouvelles topologies de type GRID, les algorithmes d'exclusion mutuelle deviennent de plus en plus complexes et donc de plus en plus difficiles à prouver. Dans un cadre systématique et formel, nous proposons ici une nouvelle approche générique reposant sur la composition d'algorithmes existants et déjà prouvés ainsi que sur l'exploitation de la topologie physique du réseau. Notre composition permet un passage à l'échelle dans cet environnement hétérogène, tout en facilitant la preuve des algorithmes. Notre étude formalise les propriétés fondamentales de ce paradigme et montre par « model cheking » que notre algorithme de composition préserve bien les propriétés des algorithmes composés