A Framework for Reasoning on Component Composition

Ludovic Henrio 1 Florian Kammüller 2 Muhammad Uzair Khan 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 : 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.
Type de document :
Communication dans un congrès
FMCO, Nov 2009, Eindhoven, Netherlands. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00490380
Contributeur : Muhammad Uzair Khan <>
Soumis le : mardi 8 juin 2010 - 12:49:01
Dernière modification le : mercredi 14 décembre 2016 - 01:06:44
Document(s) archivé(s) le : vendredi 19 octobre 2012 - 15:45:10

Fichier

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

Identifiants

  • HAL Id : inria-00490380, version 1

Collections

Citation

Ludovic Henrio, Florian Kammüller, Muhammad Uzair Khan. A Framework for Reasoning on Component Composition. FMCO, Nov 2009, Eindhoven, Netherlands. 2010. <inria-00490380>

Partager

Métriques

Consultations de
la notice

212

Téléchargements du document

256