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 metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-00880533
Contributor : Ludovic Henrio <>
Submitted on : Wednesday, November 6, 2013 - 1:47:36 PM
Last modification on : Monday, February 11, 2019 - 10:10:04 AM
Long-term archiving on : Friday, April 7, 2017 - 10:09:14 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00880533⟩

Share

Metrics

Record views

268

Files downloads

324