Skip to Main content Skip to Navigation
Conference papers

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 , Laboratoire I3S - 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.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Ludovic Henrio Connect in order to contact the contributor
Submitted on : Wednesday, November 6, 2013 - 1:47:36 PM
Last modification on : Thursday, January 20, 2022 - 5:32:16 PM
Long-term archiving on: : Friday, April 7, 2017 - 10:09:14 PM


Files produced by the author(s)


  • HAL Id : hal-00880533, version 1



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⟩



Les métriques sont temporairement indisponibles