Bringing Coq Into the World of GCM Distributed Applications

Nuno Gaspar 1 Ludovic Henrio 1 Eric Madelaine 1
1 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : 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.
Type de document :
Communication dans un congrès
International Symposium on High-level Parallel Programming and Applications&, HLPP, Jul 2013, Paris, France. 2013
Liste complète des métadonnées


https://hal.inria.fr/hal-00880533
Contributeur : Ludovic Henrio <>
Soumis le : mercredi 6 novembre 2013 - 13:47:36
Dernière modification le : mardi 17 décembre 2013 - 17:29:58
Document(s) archivé(s) le : vendredi 7 avril 2017 - 22:09:14

Fichier

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

Identifiants

  • HAL Id : hal-00880533, version 1

Collections

Citation

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. 2013. <hal-00880533>

Partager

Métriques

Consultations de
la notice

167

Téléchargements du document

191