8739 articles  [version française]

hal-00761073, version 1

Behavioural Semantics for Asynchronous Components

Rabéa Ameur-Boulifa () 1, Ludovic Henrio (, http://www-sop.inria.fr/oasis/Ludovic.Henrio/) a2, Eric Madelaine (Author to contact preferably) 2, Alexandra Savu () b2

N° RR-8167 (2012)

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.

  • a –  CNRS
  • b –  INRIA
  • 1:  Institut Télécom - Télécom ParisTech
  • Télécom ParisTech
  • 2:  OASIS (INRIA Sophia Antipolis / Laboratoire I3S)
  • INRIA – Université Nice Sophia Antipolis (UNS) – CNRS : UMR7271
  • Domain : Computer Science/Distributed, Parallel, and Cluster Computing
  • Keywords : Behavioural specification – software components – asynchronous communications – futures
  • Internal note : RR-8167
  • hal-00761073, version 1
  • oai:hal.inria.fr:hal-00761073
  • From: 
  • Submitted on: Wednesday, 5 December 2012 11:39:18
  • Updated on: Wednesday, 5 December 2012 15:04:33