Abstract
Workflow processes are represented as Petri nets with special entry and exit places and labeled transitions. The transition labels represent actions. We give a semantics for such nets in terms of transition systems. This allows us to describe and verify properties like termination: the guaranteed option to terminate successfully. We describe the composition of complex WF nets from simpler ones by means of certain operators. The simple operators preserve termination, giving correctness by design. Only the advanced communication operators are potentially dangerous. A strategy for verification of other properties is described.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W.M.P. van der Aalst. Verification of Workflow Nets. In Application and Theory of Petri Nets 1997, 18th. International Conference, Proceedings, volume 1248 of Lecture Notes in Computer Science, Toulouse, France, 1997. Springer-Verlag, Berlin, Germany.
J.C.M. Baeten and C. Verhoef. Concrete Process Algebra. In A. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 4, pages 149–268. Oxford University Press, Clarendon, UK, 1995.
E. Best, R. Devillers, and J. Hall. The Petri Box Calculus: a New Causal Algebra with Multilabel Communication. In G. Rozenberg, editor, Advances in Petri Nets 1992, volume 609 of Lecture Notes in Computer Science, pages 21–69. Springer-Verlag, Berlin, Germany, 1992.
R.J. van Glabbeek and U. Goltz. Equivalence Notions for Concurrent Systems and Refinement of Actions. In A. Kreczmar and G. Mirkowska, editors, Mathematical Foundations of Computer Science 1989, 14th. International Symposium, Proceedings, volume 379 of Lecture Notes in Computer Science, pages 237–248. Springer-Verlag, Berlin, Germany, 1989.
M. Hennesy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM, 32(1):137–161, 1985.
R. Milner. Communication and Concurrency. Prentice-Hall, London, UK, 1989.
W. Reisig. Petri Nets. Springer-Verlag, Berlin, Germany, 1985.
H.M.W. Verbeek, T. Basten, and W.M.P. van der Aalst. Diagnosing Workflow Processes using Woflan. Computing Science Reports 99/02, Eindhoven University of Technology, 1999.
W. Vogler. Bisimulation and Action Refinement. Theoretical Computer Science, 114(1):173–200, 1993.
M. Voorhoeve. State Event Net Equivalence. Computing Science Reports 98/02, Eindhoven University of Technology, 1998.
WFMC. Workflow Management Coalition Terminology and Glossary. Technical Report WFMC-TC-1011, Workflow Management Coalition, Brussels, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Voorhoeve, M. (2000). Compositional modeling and verification of workflow processes. In: van der Aalst, W., Desel, J., Oberweis, A. (eds) Business Process Management. Lecture Notes in Computer Science, vol 1806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45594-9_12
Download citation
DOI: https://doi.org/10.1007/3-540-45594-9_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67454-2
Online ISBN: 978-3-540-45594-3
eBook Packages: Springer Book Archive