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 26/7 - 2007  - pp.853-882  - doi:10.3166/tsi.26.853-882
TITRE
Propriétés de vivacité dans les systèmes B. Application à l’algorithme de Ricart-Agrawala

RÉSUMÉ
Dans cet article, nous présentons une approche de spécification, preuve et raffinement de modalités, dans le cadre du B événementiel sans hypothèses d'équité. L'approche utilise les relations ensures et leads-to de la logique UNITY. La méthode est illustrée par le développement d'un système distribué qui met en oeuvre l'algorithme d'exclusion mutuelle de Ricart-Agrawala. L'exercice permet aussi de donner les principes de raffinement pour implémenter des algorithmes parallèles distribués avec communication asynchrone par canaux.


ABSTRACT
In this paper, we present an approach to specification, proof and refinement of modalities, in the framework of event-B without fairness assumption. The approach uses relations ensures and leads-to of the UNITY logics. The method is exemplified by the development of a distributed system, which carries out the mutual exclusion algorithm of Ricart and Agrawala. The exercise is a way to provide refinement principles to implement distributed parallel algorithms, with asynchronous communication by channels.


AUTEUR(S)
Didier BERT, Héctor Ruíz BARRADAS

Reçu le 15 mars 2006.    Accepté le 18 janvier 2007.

MOTS-CLÉS
B événementiel, UNITY, vivacité, progrès minimal, algorithme distribué.

KEYWORDS
event B, UNITY, liveness, minimal progress, distributed algorithm.

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  (400 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier