Propriétés de vivacité dans les systèmes B. Application à l’algorithme de Ricart-Agrawala
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.
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.
D.BERT, H.BARRADAS
Reçu le 15 mars 2006.
Accepté le 18 janvier 2007.
B événementiel, UNITY, vivacité, progrès minimal, algorithme distribué.
event B, UNITY, liveness, minimal progress, distributed algorithm.
Français
|
