Dynamic Changes in Concurrent Systems: Modelling and Verification

Eric Badouel 1 Javier Oliver 2
1 PARAGRAPHE - Parallelism and Graphs
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : In this paper we address the issues of modelling and verification of concurren- t systems subject to dynamic changes using Petri net formalisms. As far as the expressivity of the model is concerned a built-in and decentralized mechanism for handling changes is looked for. At the same time the basic decidable properties of Petri nets (Place Boundedness, Reachability, Deadlock, and Liveness) should remain decidable for the extended model. The gain in terms of modelling power is usually paid by a loss of decidable properties. A trade-off needs to be found between expressivity and computability. In a previous study we have introduced a class of high level Petri nets, called reconfigurable nets, that can dynamically modify their own structure by rewriting some of their components. These nets were used for modelling computer supported cooperative work (CSCW) and more precisely workflow systems. In this study we restrict our attention to the subclass of reconfigurable nets, termed reversible, whose structure modifying rules are formally inversible. Such a net may be viewed as the cascaded composition of an automaton with a parametric Petri net; and under some additional assumption it is equivalent to a stratified Petri net. Place boundedness, reachability, deadlock, and liveness are decidable properties of reversible reconfigurable nets. From a practical point of view however the choice of a particular model (Petri nets, selfmodifying or stratified Petri nets, reconfigurable nets ...) depends strongly on the nature of the problem to be modelized.
Type de document :
Rapport
[Research Report] RR-3708, INRIA. 1999
Liste complète des métadonnées

https://hal.inria.fr/inria-00072960
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 11:28:06
Dernière modification le : mercredi 16 mai 2018 - 11:23:04
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:29:28

Fichiers

Identifiants

  • HAL Id : inria-00072960, version 1

Citation

Eric Badouel, Javier Oliver. Dynamic Changes in Concurrent Systems: Modelling and Verification. [Research Report] RR-3708, INRIA. 1999. 〈inria-00072960〉

Partager

Métriques

Consultations de la notice

234

Téléchargements de fichiers

185