Skip to Main content Skip to Navigation

Behavioural Semantics for Asynchronous Components

Rabéa Ameur-Boulifa 1 Ludovic Henrio 2 Eric Madelaine 2, * Alexandra Savu 2 
* Corresponding author
2 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Software components are a valuable programming abstraction that enables a compositional design of complex applications. In distributed systems, components can also be used to provide an abstraction of locations: each component is a unit of deployment that can be placed on a di fferent machine. In this article, we consider this kind of distributed components that are additionally loosely coupled and communicate by asynchronous invocations. Components also provide a convenient abstraction for verifying the correct behaviour of systems: they provide structuring entities easing the correctness veri fication. This article aims at providing a formal background for the generation of behavioural semantics for asynchronous components. We use the pNet intermediate language to express the semantics of hierarchical distributed components communicating asynchronously by a request-reply mechanism. We also formalise two crucial aspects of distributed components: recon figuration and one-to-many communications. This article both demonstrates the expressiveness of the pNet model and formally speci fies the complete process of the generation of a behavioural model for a distributed component system. The behavioural models we build are precise enough to allow veri fication by finite instantiation and model-checking, but also to use veri fication techniques for infi nite systems.
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Eric Madelaine Connect in order to contact the contributor
Submitted on : Wednesday, December 5, 2012 - 11:39:18 AM
Last modification on : Saturday, June 25, 2022 - 11:09:01 PM
Long-term archiving on: : Wednesday, March 6, 2013 - 4:55:52 PM


Files produced by the author(s)


  • HAL Id : hal-00761073, version 1


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⟩



Record views


Files downloads