Paper Info
Title
Bringing Coq into the World of GCM Distributed Applications
Abstract
Among all programming paradigms, component-based engineering stands as one of the most followed approaches for real world software development. 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 context of distributed systems by providing all the means to define, compose and dynamically reconfigure component-based applications. While structural reconfiguration 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 structure of GCM applications. This contribution comes in the form of a formal specification mechanized in the Coq Proof Assistant. Our aim is to demonstrate 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.
Year
DOI
Venue
2014
10.1007/s10766-013-0264-7
International Journal of Parallel Programming
Keywords
Field
DocType
component-based engineering,the coq proof assistant,formal semantics,interactive theorem proving,formal methods
Programming paradigm,Computer science,Parallel computing,Separation of concerns,Theoretical computer science,Formal specification,Formal methods,Software development,Control reconfiguration,Reusability,Proof assistant,Distributed computing
Journal
Volume
Issue
ISSN
42
4
1573-7640
Citations 
PageRank 
References 
4
0.43
13
Authors
3
Name
Order
Citations
PageRank
Nuno Gaspar141.10
Ludovic Henrio230434.43
Eric Madelaine326125.38