From Formal Specification to Optimized Implementation of Distributed Systems : A Multi-Formalism Approach

A. Diagne, F. Kordon

LIP6 1997/039: Rapport de Recherche LIP6 / LIP6 research reports
22 pages - Décembre/December 1997 - Document en anglais.

PostScript : 94 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Systèmes Répartis et Coopératifs

Titre français : Depuis les Spécifications Formelles à l'Implémentation de Systèmes Répartis: Une approche Multi-Formalisme
Titre anglais : From Formal Specification to Optimized Implementation of Distributed Systems : A Multi-Formalism Approach

Résumé : Cet article présente une méthodologie pour la construction de systèmes répartis sûrs. Cette méthodologie considère à la fois les aspects conceptuels et opérationnels de la description d'un système. Au niveau conceptuel, nous insistons sur les propriétés de vivacité et de sûreté attendues. De telles propriétés doivent être posées puis vérifiées. Au niveau opérationnel, nous insistons sur les propriétés permettant d'optimiser l'application correspondante. La traçabilité entre ces deux niveaux est supportée de manière semi-automatique. Elle préserve les propriétés prouvées et écarte l'information irrelevante pour la génération de code. Cet article, après avoir présenté les principes de la méthodologie, propose une application sur un exemple simple.

Abstract : This paper proposes a methodology to build safe distributed systems that considers both conceptual and operational description aspects. At the conceptual level, we focus on the safety and liveness properties expected from the system. Such properties are stated and then verified. At the operational level, we focus on properties addressing the optimization of the generated code. Traceability between the two levels is managed in a satisfactory semi-automatic way. It preserves the properties proved at the first level and discards information that are not relevant for code generation. The paper presents the general methodology and proposes an application to a simple example.

Mots-clés : Spécifications Formelles, Réseaux de Petri, Validation, Vérification, Traçabilité de choix de conception, Prototypage, Systèmes Répartis

Key-words : Formal Specification, Petri Nets, Validation, Verification, Design Traceability, Prototyping, Distributed Systems

Publications internes LIP6 1997 / LIP6 research reports 1997

Responsable Éditorial / Editor
webmaster@lip6.fr