Refinement of Synchronizable Places with Multi-workflow Nets

• Autorzy: Hee, K. N. v. , Sidorova, N. , Werff, J. M. v. d.
• Języki publikacji: EN

Abstrakty

EN

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 weak termination is preserved under the refinement of places with multiworks if and only if the refined places are synchronizable. We give a method to decide if a given set of places is synchronizable.

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 122, nr 1-2
• Strony: 59--83
• Opis fizyczny: Bibliogr. 18 poz., rys., wykr.

Twórcy

autor

Hee, K. N. v.

• Department of Mathematics and Computer Science Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, The Netherlands,

autor

Sidorova, N.

• Department of Mathematics and Computer Science Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, The Netherlands,

autor

Werff, J. M. v. d.

• Department of Mathematics and Computer Science Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, The Netherlands,

Bibliografia

• [1] W.M.P. van der Aalst, K.M. van Hee, A.H.M. ter Hofstede, N. Sidorova, H.M.W. Verbeek, M. Voorhoeve, and M.T. Wynn. Soundness of workflow nets: classification, decidability, and analysis. Formal Aspects of Computing, pages 1–31, 2010.
• [2] T. Basten and W.M.P. van der Aalst. Inheritance of Behavior. Journal of Logic and Algebraic Programming, 47(2):47–145, 2001.
• [3] G. Berthelot. Transformations and decompositions of nets. In Petri Nets, central models and their properties, volume 254 of LNCS, pages 360–376. Springer, 1987.
• [4] E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logics of Programs, volume 131 of LNCS, pages 52–71. Springer, 1982.
• [5] J. Desel and J. Esparza. Free Choice Petri Nets, volume 40 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1995.
• [6] R.J. van Glabbeek. The Linear Time - Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves. In Proceedings of CONCUR 1993, volume 715 of LNCS, pages 66–81. Springer, 1993.
• [7] K.M. van Hee, A.J Mooij, N. Sidorova, and J.M.E.M. van der Werf. Soundness-preserving refinements of service compositions. In Web Services and Formal Methods 10, volume 6551 of LNCS, pages 131-145. Springer, 2011.
• [8] K.M. van Hee, N. Sidorova, and M. Voorhoeve. Soundness and separability of workflow nets in the stepwise refinement approach. In Application and Theory of Petri Nets 2003, volume 2679 of LNCS, pages 335 – 354. Springer, 2003.
• [9] K.M. van Hee, N. Sidorova, and J.M.E.M. van der Werf. Construction of asynchronous communicating systems: Weak termination guaranteed! In Proceedings of the 9th International Conference on Software Composition (SC 2010), volume 6144 of LNCS, pages 106 – 121. Springer, 2010.
• [10] K.M. van Hee, N. Sidorova, and J.M.E.M. van der Werf. Refinement of synchronizable places with multiworkflow nets - weak termination preserved! In Applications and Theory of Petri Nets, volume 6709 of LNCS, pages 149–168. Springer, 2011.
• [11] K.G. Larsen. Modal specifications. In Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 232–246. Springer, 1990.
• [12] K.G. Larsen and B. Thomsen. A modal process logic. In Logic in Computer Science, pages 203–210. IEEE Computer Society, 1988.
• [13] T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580, April 1989.
• [14] T. Murata and I. Suzuki. A method for stepwise refinement and abstraction of Petri nets. Journal of Computer and System Sciences, 27(1):51 – 76, 1983.
• [15] W. Reisig. A strong part of concurrency. In Advances in Petri Nets 1987, volume 266 of LNCS, pages 238–272. Springer, 1987.
• [16] N. Sidorova, C. Stahl, and N. Trˇcka. Workflow soundness revisited: Checking correctness in the presence of data while staying conceptual. In Advanced Information Systems Engineering, 22nd Int. Conference, CAiSE 2010, volume 6051 of LNCS, pages 530–544. Springer, 2010.
• [17] I. Suzuki and T. Kasami. Three measures for synchronic dependence in petri nets. Acta Informatica, 19:325–338, 1983.
• [18] W. Vogler. Modular Construction and Partial Order Semantics of Petri Nets, volume 625 of LNCS. Springer, 1992.