Behavioural Semantics for Asynchronous Components

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.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