Contrats Comportementaux pour Composants

Behavioural Contracts for Components

Résumé

Abstract

Cette conception par composition pose cependant plusieurs problèmes. Les services non uniformes impliquent que les messages échangés entre les composants le soient selon un dialogue bien précis, qui doit être respecté. Les liens d'interconnection entre les composants évoluent au gré de leur comportement: création, suppression et modification de ces liens ne sont pas forcément détectables à l'assemblage des composants, donc a priori non vérifiables. Survient alors le problème des "messages non compris", qui a pour conséquence que certaines requêtes peuvent ne pas être traitées par les composants.

Notre but est de fournir un cadre formel pour la vérification compositionnelle des systèmes à base de composants.

Nous définissons un langage de type d'interfaces comportementales. Ce langage s'inspire des types réguliers, selon une sémantique de messages. Nous introduisons également la notion d'actions permises et obligatoires, qui imposent des contraintes non seulement au composant, mais aussi à son environnement. Ce langage constitue un contrat comportemental à partir duquel nous définissons deux vérifications.

La première vérification impose que le composant respecte son contrat d'interface. Nous avons choisi d'avoir une sémantique de composant la plus abstraite possible, pour étudier les contraintes minimales imposées par le contrat. Notre abstraction inclut les notions de ports, références vers ces ports, et tâches d'exécution. La dynamique de notre modèle repose essentiellement sur les notions d'état du port (émission/réception), de son activité (actif/suspendu), et les relations entre les ports (par exemple attente de résultat sur un autre port).

La deuxième vérification est utilisée lors de l'assemblage des composants, ou lors de leur déploiement sur une plate-forme d'exécution. Les contrats sont utilisés pour vérifier que deux interfaces interconnectées sont compatibles: compatibilité des services modalisés respectifs, qui se propage récursivement aux arguments des messages échangés. Cette vérification est faite sans prendre en compte le comportement interne du composant; elle s'avère donc précieuse dans le cadre des composants sur étagères, où le composant n'arbore que sa spécification, et non son calcul interne.

Cette double vérification nous assure que l'application évoluera sainement: tout message envoyé sera consommé, et il n'y aura pas d'interblocage externe entre les composants.

This conception by composition gives rise to several problems. Non uniform services implies that messages are exchanged between components according to a well-defined dialogue, which must be honoured. Interconnection links between components evolve at the liking of their behaviour: creation, deletion and modification of those links are not necessarily determined at the assembly of the components, thus not verifiable. Then, the "message not understood" problem occurs, which consequence is that some requests may not be processed by the components.

Our goal is to provide a formal framework for compositional verification of component based systems.

We define a behavioural interface type language. This language takes inspiration from regular types, with message semantics. We also bring in the concept of allowed and obligatory actions, which enforces constraints on both the component and its environment. This language forms a behavioural contract from which we define two verifications.

The first verification imposes the component honours its interface contract. We chose a component semantics which is as abstract as possible, to study minimal constraints demanded by the contract. This abstraction encompasses concepts of ports, references towards those ports, and threads. The dynamic of our model primarily uses concepts of port states (sending/receiving), its activity (active/suspended), and relations between ports (for instance, waiting a result on another port).

The second verification is used during the assembly of the components, or during their deployment on an executing platform. Contracts are used to check that two interconnected interfaces are compatible: compatibility of respective modal services, which recursively propagates to arguments of exchanged messages. This verification is made without taking into account the internal behaviour of the component; hence, it is precious when used with components off-the-shelf, where each component shows only its specification, not its internal calculus.

This double verification ensures that the application will evolve soundly: every sent message will be consumed, and there will be not external deadlock between components.

• Le rapport: postcript compressé, ~600ko   ou   PDF, 2Mo
• Les transparents (PDF, ~450ko): en couleur   ou   en grisé