Développement incrémental prouvé de systèmes répartis : le cas Mondex

Nazim Benaissa 1 Dominique Méry 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Notre travail se situe dans le cadre du développement incrémental prouvé de systèmes distribués communiquant par des canaux non fiables, en particulier des protocoles de communication utilisés dans les porte-monnaie électroniques. L'approche B événementielle est mise en application sur une étude de cas réputée du Grand Challenge et appelée Mondex. Ce travail met en avant une explication des mécanismes sous-jacents qui permettent à ce système de satisfaire les exigences initiales résumées sous la forme suivante: il n'y a pas de perte d'argent ni de création d'argent lors des transferts. Le développement permet de préserver cette propriété de sûreté attendue du système final et identifie des relations de communication spécifiques pour assurer la mise en oeuvre du protocole. Ainsi, un premier modèle énonce la spécification globale de sûreté; un second modèle raffiné décrit le comportement détaillé des différents protagonistes; un troisième modèle localise les données; un quatrième modèle élimine des variables utiles pour faciliter les preuves. Cette étude nous permet de vérifier la robustesse du protocole à la perte de messages.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00336655
Contributor : Nazim Benaissa <>
Submitted on : Tuesday, November 4, 2008 - 4:38:05 PM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM
Long-term archiving on : Tuesday, October 9, 2012 - 3:01:04 PM

File

benaissamery.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00336655, version 1

Collections

Citation

Nazim Benaissa, Dominique Méry. Développement incrémental prouvé de systèmes répartis : le cas Mondex. [Rapport de recherche] 2008, pp.13. ⟨inria-00336655⟩

Share

Metrics

Record views

159

Files downloads

91