Petri Nets with May/Must Semantics

Olga Kouchnarenko 1 Natalia Sidorova Nikola Trcka
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Many systems used in process managements, like workflow systems, are developed in a top-down fashion, when the original design is refined at each step bringing it closer to the underlying reality. Underdefined specifications cannot however be used for verification, since both false positives and false negatives can be reported. In this paper we introduce colored Petri nets where guards can be evaluated to true, false and indefinite values, the last ones reflecting underspecification. This results in the semantics of Petri nets with may- and must-enableness and firings. In this framework we introduce property-preserving refinements that allow for verification in an early design phase. We present results on property preservation through refinements. We also apply our framework to workflow nets, introduce notions of may- and must-soundness and show that they are preserved through refinements. We shortly describe a prototype under implementation.
Type de document :
Communication dans un congrès
Workshop on Concurrency, Specification, and Programming - CS&P 2009, Sep 2009, Kraków-Przegorzały, Poland. 1, 2009, Concurrency, Specification, and Programming
Liste complète des métadonnées

https://hal.inria.fr/inria-00426835
Contributeur : Olga Kouchnarenko <>
Soumis le : mercredi 28 octobre 2009 - 10:23:13
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : inria-00426835, version 1

Citation

Olga Kouchnarenko, Natalia Sidorova, Nikola Trcka. Petri Nets with May/Must Semantics. Workshop on Concurrency, Specification, and Programming - CS&P 2009, Sep 2009, Kraków-Przegorzały, Poland. 1, 2009, Concurrency, Specification, and Programming. 〈inria-00426835〉

Partager

Métriques

Consultations de la notice

227