Behavioural Models for Hierarchical Components

Tomás Barros 1 Ludovic Henrio 2 Eric Madelaine 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 : We describe a method for the specification and verification of the dynamic behaviour of component systems. Building applications using a component framework allows the developers to specify the architecture, the deployment, the life-cycle of the system with well-defined formalisms, and to gain productivity by reusing existing components. But then one wants to make sure that the application built from existing components is safe, in the sense that its parts fit together appropriately and behave together smoothly. Each component must be adequate to its assigned role within the system, and the update or replacement of a component should not cause deadlock or failure of the rest of the system. The usual notion of type compatibility of interfaces is not sufficient; we need to capture the dynamic interaction between components, and typically to avoid deadlocks or unexpected behaviours in the system. In this work, we focus on hierarchical component systems. We describe both the functional behaviour and the non-functional features (life-cycle management) of components in terms of synchronised transition systems; we define a notion of correct component composition; then we show how we can prove, using (compositional) model-checking techniques, temporal properties of a component system. Transformations of a system, for example replacement of a sub-component, are expressed as transformations of its behavioural semantics, allowing to prove preservation of some properties, or the validity of new properties after transformation.
Type de document :
Communication dans un congrès
SPIN'05, 2005, San Francisco, USA, Spinger Verlag, 2005
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00122933
Contributeur : Ludovic Henrio <>
Soumis le : vendredi 5 janvier 2007 - 17:28:03
Dernière modification le : mardi 12 juin 2018 - 10:04:04
Document(s) archivé(s) le : mercredi 7 avril 2010 - 01:51:09

Fichier

2005-SPIN-Frisco.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00122933, version 1

Collections

Citation

Tomás Barros, Ludovic Henrio, Eric Madelaine. Behavioural Models for Hierarchical Components. SPIN'05, 2005, San Francisco, USA, Spinger Verlag, 2005. 〈inria-00122933〉

Partager

Métriques

Consultations de la notice

258

Téléchargements de fichiers

91