ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 28/9 - 2009  - pp.1085-1105  - doi:10.3166/tsi.28.1085-1105
TITRE
Vérification formelle d'un algorithme générique et hiérarchique d'exclusion mutuelle

RÉSUMÉ
Dans 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.


ABSTRACT
In distributed environments, the use of mutual exclusion to control the access of shared resources is a key issue. However, the constraints of current large scale distributed systems require more complex mutual exclusion algorithms which are harder to prove. In this article, we propose a formal modeling and verification of a new generic hierarchical approach which is based on the composition of classical already proved and checked algorithms. Such a composition approach overcomes some limitations of the classical algorithms by taking into account the network topology. It thus provides high scalability. Our study formalizes all basic properties of mutual exclusion paradigm and verifies them by "model checking".


AUTEUR(S)
Julien SOPENA, Souheib BAARIR, Fabrice LEGOND-AUBRY

MOTS-CLÉS
composition d'algorithmes distribués, exclusion mutuelle, grille de calculs, réseaux de Petri colorés, vérification de modèle.

KEYWORDS
distributed algorithm composition, mutual exclusion, grid computing, colored Petri nets, model checking.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (418 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier