Behavioural and Structural Composition Rules Preserving Liveness by Synchronization for Coloured FIFO Nets

M.-L. Benalycherif, C. Girault

Masi-IBP 1996/21: Rapport de Recherche Masi / Masi research reports
21 pages - Juillet/July 1996 - Document en anglais.

PostScript : 117 Ko /Kb

Titre français : Règles de Composition Comportementales et Structurelles Préservant la Vivacité par Synchronisation pour les Réseaux à Files Colorés
Titre anglais : Behavioural and Structural Composition Rules Preserving Liveness by Synchronization for Coloured FIFO Nets

Résumé : L'objet de cet article est la compositionalité de la vivacité pour la synchronisation de deux réseaux à files colorés. L'opérateur de composition permet la fusion de transitions ainsi que celle de places et de files adjacentes.
Une condition comportementale suffisant à la compositionalité de la vivacité repose sur une relation mutuelle de non contraignance entre les réseaux composants.
Une condition structurelle suffisant à la préservation de la vivacité par synchronisation est alors exprimée. Nous considérons des réseaux composants dont l'interface des éléments fusionnés avec ceux non fusionnés est une machine à états. La condition nécessite que les transitions colorées en conflit dans les machines à états d'interface satisfassent la relation structurelle de blocage ou celle de libération.
En dernier lieu, un exemple montre comment ces conditions simplifient l'analyse d'un protocole au sein d'une architecture en couches.

Abstract : This paper deals with the compositionality of liveness when synchronizing two coloured FIFO nets. The composition operator allows to merge transitions as well as some adjacent places or queues.
A behavioural sufficient condition for liveness compositionality relies on a mutual non constraining relation between component nets.
A structural sufficient condition for synchronization preserving liveness is then given in the case of a state machine at the interface of the merged elements with the non merged ones of each component net. It requires that the conflictual coloured transitions of the interface state machines satisfy the structural freeing or blocking relations.
Finally an example shows how these conditions simplify the analysis of a protocol within a layered architecture.

Mots-clés : compositionalité, égal conflit, machine à états, médium de synchronisation, relation de blocage, relation de libération, relation de non contraignance, réseaux à files colorés, synchronisation, vivacité

Key-words : blocking relation, coloured FIFO nets, compositionality, equal conflict, freeing relation, liveness, non constraining relation, state machine, synchronization, synchronization medium

Publications internes Masi 1996 / Masi research reports 1996