Refinement of synchronizable places with multi-workflow nets. Weak termination preserved!

K.M. Hee, van, N. Sidorova, J.M.E.M. Werf, van der

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)
1 Downloads (Pure)


Stepwise refinement is a well-known strategy in system modeling. The refinement rules should preserve essential behavioral properties, such as deadlock freedom, boundedness and weak termination. A well-known example is the refinement rule that replaces a safe place of a Petri net with a sound workflow net. In this case a token on the refined place undergoes a procedure that is modeled in detail by the refining workflow net. We generalize this rule to component-based systems, where in the first, high-level, refinement iterations we often encounter in different components places that represent in fact the counterparts of the same procedure "simultaneously" executed by the components. The procedure involves communication between these components. We model such a procedure as a multi-workflow net, which is actually a composition of communicating workflows. Behaviorally correct multi-workflow nets have the weak termination property. The weak termination requirement is also applied to the system being refined. We want to refine selected places in different components with a multi-workflow net in such a way that the weak termination property is preserved through refinements. We introduce the notion of synchronizable places and show that a sufficient condition for preserving weak termination is that the places to be refined are synchronizable. We give a method to decide if a given set of places is synchronizable.
Original languageEnglish
Title of host publicationApplications and Theory of Petri Nets (32nd International Conference, PETRI NETS 2011, Newcastle, UK, June 20-24, 2011. Proceedings)
EditorsL.M. Kristensen, L. Petrucci
Place of PublicationBerlin
ISBN (Print)978-3-642-21833-0
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Refinement of synchronizable places with multi-workflow nets. Weak termination preserved!'. Together they form a unique fingerprint.

Cite this