Behavioural Semantics for Asynchronous Components

Rabéa Ameur-Boulifa 1 Ludovic Henrio 2 Eric Madelaine 2, * Alexandra Savu 2
* Auteur correspondant
2 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
Résumé : Les composants logiciels fournissent une abstraction de programmation intéressante pour la conception modulaire d'applications complexes. Dans les systèmes répartis, les composants peuvent également être utilisés pour fournir une abstraction de la localisation des processus: chaque composant est une unité de déploiement qui peut être placée sur une machine différente. Dans cet article, nous considérons ce type de composants distribuées, faiblement couplés et communiquant par des appels asynchrones. Les composants fournissent également une abstraction commode pour vérifier le bon comportement des systèmes: ils fournissent un concept structurant qui facilite la vérification de ses propriétés. Cet article vise à fournir un support formel pour la génération de la sémantique comportementale des composants asynchrones. Nous utilisons le formalisme intermédiaire pNet pour exprimer la sémantique des composants hiérarchiques distribués communiquant de manière asynchrone par un mécanisme de requêtes. Nous formalisons également deux aspects fondamentaux des composants distribués: la reconfiguration et les communications de groupe. Cet article d'une part démontre l'expressivité du modèle pNet et d'autre part spécifie formellement le processus complet de la génération du modèle comportemental d'un système de composants distribués. Les modèles de comportement que nous construisons sont suffisamment précis pour permettre la vérification par instanciation finie et model-checking, mais aussi pour utiliser des techniques de vérification de systèmes infinis.
Type de document :
Rapport
[Research Report] RR-8167, INRIA. 2012, pp.58


https://hal.inria.fr/hal-00761073
Contributeur : Eric Madelaine <>
Soumis le : mercredi 5 décembre 2012 - 11:39:18
Dernière modification le : samedi 17 septembre 2016 - 01:32:17
Document(s) archivé(s) le : mercredi 6 mars 2013 - 16:55:52

Fichier

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

Identifiants

  • HAL Id : hal-00761073, version 1

Collections

Citation

Rabéa Ameur-Boulifa, Ludovic Henrio, Eric Madelaine, Alexandra Savu. Behavioural Semantics for Asynchronous Components. [Research Report] RR-8167, INRIA. 2012, pp.58. <hal-00761073>

Exporter

Partager

Métriques

Consultations de
la notice

470

Téléchargements du document

190