Raffinements de sous-réseaux

 Le raffinement et l’abstraction sont des méthodes complémentaires dans la conception et l’analyse des systèmes. La conception hiérarchique consiste à partir d’un modèle abstrait qu’on raffine progressivement en remplaçant certaines parties du modèle par des sous-modèles plus détaillés. L’opération inverse (abstraction) est utile quand on veut analyser et comprendre un système déjà réalisé, et alors on construit un modèle abstrait de son comportement. Une telle méthode de conception hiérarchique doit s’appuyer sur une méthode d’analyse hiérarchique: si le modèle M. est transformé par une opération bien définie op, les propriétés de op(Ái) devraient être déduites de celles de A4 et op. L’opération étudiée dans ce chapitre est le remplacement d’un sous-réseau à frontière de places (sous-réseau ouvert) par un réseau: si le réseau de remplacement est plus détaillé que le sous-réseau c’est un raffinement, sinon c’est une abstraction. Si N [Ni «— 7V2] est le réseau obtenu après remplacement du sous-réseau Ni par le réseau 7V2 dans N, nous voulons déduire N [Ni <— N2] = N de Ni =’ N2, pour certaines relations d’équivalence = et =’. On rencontre naturellement les sous-réseaux ouverts quand on modélise un système distribué comme un ensemble d’acteurs communicant par envoi de messages. Pa r exemple, cette méthode d’analyse peut être appliquée aux réseaux HOOD[22] qui possèdent une interface de places, ou à la méthode de conception hiérarchique de Girault[24,25] fondée sur les « acteurs abstraits » où un serveur abstrait est un réseau ayant une interface de places, et les raffinements consistent à remplacer de tels réseaux. Un sous-réseau ouvert est engendré par un sous-ensemble de transitions, alors qu’un sous-réseau fermé (ie à frontière de transitions) est engendré par un sou ensemble de places. Le remplacement de sous-réseaux à frontière de transitions et la composition de réseaux par fusion de transitions ont été largement étudiés au moyen de notions d’équivalences fondées sur l’étiquetage des transitions et l’observation des langages des réseaux (André[3], Baumgarten[6], Bourguet-Rouget[9], Valmari[59], Vogler[61] et voir Pomello[46] pour une synthèse de ces notions d’équivalence). Ces notions sont la plupart du temps inspirées des modèles algébriques tels que CCS et CSP, et jouissent de propriétés mathématiques élégantes et maniables. Le remplacement de sous-réseaux à frontière de places et la composition par fusion de places sont un peu plus laborieux et ne sont pas des opérations libres puisque des restrictions sont nécessaires pour obtenir des propriétés de fermeture ou assurer l’existence de certaines constructions mathématiques (pour obtenir, dans le cadre de la théorie des catégories, que la composition par fusion de places soit une somme, Winskel[66] considère des réseaux 1-bornés). Le raffinement de transition est un cas particulier du remplacement d’un sousréseau à frontière de places: on remplace le sous-réseau engendré par cette transition. Cette opération a été étudiée par Valette[57], Suzuki et Murata[55], Vogler[62], van Glabbeek et Goltz[27], soit en considérant la conservation de propriétés soit en considérant des notions d’équivalence qui sont des congruences pour de tels raffinements. Nous ne cherchons pas à définir une notion d’équivalence conservée par de tels raffinements mais une équivalence entre un réseau et son raffinement. Dans [60], Vogler remplace un sous-réseau, engendré par une transition, par des réseaux particuliers appelés « modules »: nous considérons des opérations de remplacement plus générales et la notion d’équivalence de [60] est inspirée de celle d’André[3] et donc fondée sur l’étiquetage des transitions. 

Réseaux à interface ouverte

Exemple d’introduction

Considérons le modèle client-serveur de base suivant (Figure II-l): un client oisif (CI) envoie une requête (R) et attend l’acquittement (CW); il y a n clients dans le système. Sur réception d’une requête le serveur oisif (SI) exécute la requête (SX); puis il envoie un acquittement au client (A) et redevient oisif. Quand le client reçoit l’acquittement il devient oisif. N CI ( n ) CW I Figure II-l: Modèle Client-Serveur On ajoute un tampon pour recevoir les requêtes quand le serveur est occupé et uniquement dans ce cas: on obtient le réseau N2 de la figure II-2. BB est le nombre de requêtes tamponnées et FB est le nombre de places vides. Le serveur consulte le tampon (SC) avant de redevenir oisif. N2 Clin Figure II-2: Ajout d’un tampon Si on se restreint à l’étiquetage des transitions et aux sous-réseaux à frontière de transitions, on est amené à regarder N2 comme le résultat du remplacement  Figure II-3: Remplacement d’un sous-réseau à frontières de transitions du sous-réseau JV3 engendré par les places SX et 57 (figure II-3) par le réseau ÍV4 (les transitions rr et pb ont la même étiquette rr). Dans TV 4 la séquence rr.rr est franchissable alors qu’elle ne l’est pas dans 7V3 (idem pour AT 1 et ÍV2); mais toutes les notions d’équivalence fondées sur les événements exigent au moins l’égalité des langages: donc ces réseaux ne vérifient aucune de ces équivalences. Cet argument n’est plus valable si on inclut la transition sr dans le réseau remplacé: mais nous ne voulons pas inclure une transition d u client quand nous remplaçons le serveur. C’est pourquoi nous définissons des équivalences fondées sur les transformations d’états et considérons cette transformation de réseau comme le remplacement de N5, le sous-réseau engendré par {rr,sa}, par N6 (figure II-4) car ces deux réseaux effectuent la même transformation sur {R, A): une requête consommée de R est transformée en un acquitement délivré dans A. Par dualité avec le paradigme de l’étiquetage des événements et l’observation des séquences d’événements, on pourrait penser étiqueter les places et observer l’évolution des marquages des places observables, et exiger que le réseau de remplacement présente la même évolution de marquages que le sous-réseau remplacé. Dans notre exemple les places observables—qu’on appelle places d’interface—sont il et A. Ce paradigme observationnel est trop restrictif: le réseau N7 (figure II-4) est une abstraction de 7V5 et il semble raisonnable de vouloir remplacer 7V5 par ÍV7; mais ces deux réseaux ne présentent pas la même évolution de marquages sur {R, A}: dans 7V5, à partir de l’état M(R) = 1,M(A) — 0, on peut atteindre l’état M(R) = M(A) = 0, et ceci est impossible dans N7 à cause de la différence d’atomicité entre ces deux réseaux. Cependant, si on considère uniquement les états de A^5 vérifiant M (SX) = 0 alors on observe les mêmes transformations  Figure II-4: Remplacement d’un sous-réseau à frontières de places d’états sur {R,A}: nous appellerons de tels états des états stables; dans A7 2, les états stables sont ceux vérifiant M{SI) – 1,M(5C) = M(SX) = M(BB) = 0,M(F£) = k. Il existe une séquence infinie de N2 qui n’amène jamais le système dans un état stable mais il est toujours possible d’atteindre un tel état. Donc la comparaison de deux réseaux par rapport à leurs états stables n’est pas une notion observationnelle puisqu’elle ne peut pas être vérifiée par un observateur extérieur: l’équivalence que nous définissons, fondée sur les transformations d’états stables (SST-éq), doit être considérée comme une méthode de preuve et d’analyse hiérarchique de réseaux conçus hiérarchiquement et non une notion observationnelle. Les états stables sont les seuls où l’état de l’interface est définitif et significatif: ils correspondent à des états internes où aucune « action observable » (c-à-d, dont les conséquences sur l’interface sont observables) n’est en cours.