Bringing Coq Into the World of GCM Distributed Applications - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Bringing Coq Into the World of GCM Distributed Applications

Résumé

Among all programming paradigms, component-based engineering stands as one of the most followed approaches for real world software devel- opment. Its emphasis on clean separation of concerns and reusability makes it appealing for both industrial and research purposes. The Grid Component Model (GCM) endorses this approach in the con- text of distributed systems by providing all the means to define, compose and dynamically reconfigure component-based applications. While structural re- configuration is one of the key features of GCM applications, this ability to evolve at runtime poses several challenges w.r.t reliability. In this paper we present Mefresa, a framework for reasoning on the struc- ture of GCM applications. This contribution comes in the form of a formal specification mechanized in the Coq Proof Assistant. Our aim is to demon- strate the benefits of interactive theorem proving for the reasoning on software architectures. We provide a configuration and reconfiguration language for the safe instantiation of distributed systems.
Fichier principal
Vignette du fichier
paper.pdf (536.8 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00880533 , version 1 (06-11-2013)

Identifiants

  • HAL Id : hal-00880533 , version 1

Citer

Nuno Gaspar, Ludovic Henrio, Eric Madelaine. Bringing Coq Into the World of GCM Distributed Applications. International Symposium on High-level Parallel Programming and Applications&, HLPP, Jul 2013, Paris, France. ⟨hal-00880533⟩
125 Consultations
311 Téléchargements

Partager

Gmail Facebook X LinkedIn More