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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00426835
Contributor : Olga Kouchnarenko <>
Submitted on : Wednesday, October 28, 2009 - 10:23:13 AM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Identifiers

  • 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, Humboldt University, Sep 2009, Kraków-Przegorzały, Poland. ⟨inria-00426835⟩

Share

Metrics

Record views

251