Sciweavers

Share
FMCO
2009
Springer

A Framework for Reasoning on Component Composition

9 years 1 months ago
A Framework for Reasoning on Component Composition
The main characteristics of component models is their strict structure enabling better code reuse. Correctness of component composition is well understood formally but existing works do not allow for mechanised reasoning on composition and component reconfigurations, whereas a mechanical support would improve the confidence in the existing results. This article presents the formalisation in Isabelle/HOL of a component model, focusing on the structure and on basic lemmas to handle component structure. Our objective in this paper is to present the basic constructs, and the corresponding lemmas allowing the proof of properties related to structure of component models and the handling of structure at runtime. We illustrate the expressiveness of our approach by presenting component semantics, and properties on reconfiguration primitives. Key words: Components, mechanised proofs, futures, reconfiguration.
Ludovic Henrio, Florian Kammüller, Muhammad U
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Where FMCO
Authors Ludovic Henrio, Florian Kammüller, Muhammad Uzair Khan
Comments (0)
books