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.
Type de document :
Rapport
[Rapport de recherche] 2008, pp.13
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00336655
Contributeur : Nazim Benaissa <>
Soumis le : mardi 4 novembre 2008 - 16:38:05
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : mardi 9 octobre 2012 - 15:01:04

Fichier

benaissamery.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

147

Téléchargements de fichiers

66