Abstract
Workflow management systems will change the architecture of future information systems dramatically. The explicit representation of business procedures is one of the main issues when introducing a workflow management system. In this paper we focus on a class of Petri nets suitable for the representation, validation and verification of these procedures. We will show that the correctness of a procedure represented by such a Petri net can be verified by using standard Petri-net-based techniques. Based on this result we provide a comprehensive set of transformation rules which can be used to construct and modify correct procedures.
Preview
Unable to display preview. Download preview PDF.
References
W.M.P. van der Aalst. Putting Petri nets to work in industry. Computers in Industry, 25(1):45–54, 1994.
W.M.P. van der Aalst. A class of Petri net for modeling and analyzing business processes. Computing Science Reports 95/26, Eindhoven University of Technology, Eindhoven, 1995.
W.M.P. van der Aalst. Petri-net-based Workflow Management Software. In A. Sheth, editor, Proceedings of the NFS Workshop on Workflow and Process Automation in Information Systems, pages 114–118, Athens, Georgia, May 1996.
W.M.P. van der Aalst. Three Good reasons for Using a Petri-net-based Workflow Management System. In S. Navathe and T. Wakayama, editors, Proceedings of the International Working Conference on Information and Process Integration in Enterprises (IPIC'96), pages 179–201, Camebridge, Massachusetts, Nov 1996.
W.M.P. van der Aalst and K.M. van Hee. Business Process Redesign: A Petri-net-based approach. Computers in Industry, 29(1–2): 15–26, 1996.
W.M.P. van der Aalst and K.M. van Hee. Workflow Management: Modellen, Methoden en Systemen (in Dutch). Academic Service, Schoonhoven, 1997.
G. Berthelot. Transformations and decompositions of nets. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Advances in Petri Nets 1986 Part I: Petri Nets, central models and their properties, volume 254 of Lecture Notes in Computer Science, pages 360–376. Springer-Verlag, Berlin, 1987.
E. Best. Structure theory of Petri nets: the free choice hiatus. In W. Brauer, W. Reisig, and G. Rozenberg, editors, Advances in Petri Nets 1986 Part I: Petri Nets, central models and their properties, volume 254 of Lecture Notes in Computer Science, pages 168–206. Springer-Verlag, Berlin, 1987.
A. Cheng, J. Esparza, and J. Palsberg. Complexity results for 1-safe nets. In R.K. Shyamasundar, editor, Foundations of software technology and theoretical computer science, volume 761 of Lecture Notes in Computer Science, pages 326–337. Springer-Verlag, Berlin, 1993.
J. Desel. Reduction and design of well-behaved concurrent systems. In J.C.M. Baeten and J.W. Klop, editors, Proceedings of CONCUR 1990, Volume 458 of Lecture Notes in Computer Science, pages 166–181. Springer-Verlag, Berlin, 1990.
J. Desel. A proof of the Rank theorem for extended free-choice nets. In K. Jensen, editor, Application and Theory of Petri Nets 1992, volume 616 of Lecture Notes in Computer Science, pages 134–153. Springer-Verlag, Berlin, 1992.
J. Desel and J. Esparza. Free choice Petri nets, volume 40 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1995.
C.A. Ellis and G.J. Nutt. Modelling and Enactment of Workflow Systems. In M. Ajmone Marsan, editor, Application and Theory of Petri Nets 1993, volume 691 of Lecture Notes in Computer Science, pages 1–16. Springer-Verlag, Berlin, 1993.
J. Esparza. Synthesis rules for Petri nets, and how they can lead to new results. In J.C.M. Baeten and J.W. Klop, editors, Proceedings of CONCUR 1990, Volume 458 of Lecture Notes in Computer Science, pages 182–198. Springer-Verlag, Berlin, 1990.
K. Gostellow, V. Cerf, G. Estrin, and S. Volansky. Proper Termination of Flow-of-control in Programs Involving Concurrent Processes. ACM Sigplan, 7(11):15–27, 1972.
V. Gruhn. Validation and Verification of Software Process Models. In A. Endres and H. Weber, editors, Software Development Environments and CASE Technology, volume 509 of Lecture Notes in Computer Science, pages 271–286. Springer-Verlag, Berlin, 1991.
M.H.T. Hack. Analysis production schemata by Petri nets. Master's thesis, Massachusetts Institute of Technology, Cambridge, Mass., 1972.
T.M. Koulopoulos. The Workflow Imperative. Van Nostrand Reinhold, New York, 1995.
A.V. Kovalyov. On complete reducability of some classes of Petri nets. In Proceedings of the 11th International Conference on Applications and Theory of Petri Nets, pages 352–366, Paris, June 1990.
T. Murata. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, 77(4):541–580, April 1989.
J.L. Peterson. Petri net theory and the modeling of systems. Prentice-Hall, Englewood Cliffs, 1981.
C.A. Petri. Kommunikation mit Automaten. PhD thesis, Institut für instrumentelle Mathematik, Bonn, 1962.
T. Schäl. Workflow Management for Process Organisations, Volume 1096 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1996.
P.A. Straub and C. Hurtado. The Simple Control Property of Business Process Models. In XVInternational Conference of the Chilean Computer Science Society, 1995.
R. Valette. Analysis of Petri Nets by Stepwise Refinements. Journal of Computer and System Sciences, 18:35–46, 1979.
WFMC. Workflow Management Coalition Terminology and Glossary (WFMC-TC-1011). Technical report, Workflow Management Coalition, Brussels, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van der Aalst, W.M.P. (1997). Verification of workflow nets. In: Azéma, P., Balbo, G. (eds) Application and Theory of Petri Nets 1997. ICATPN 1997. Lecture Notes in Computer Science, vol 1248. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63139-9_48
Download citation
DOI: https://doi.org/10.1007/3-540-63139-9_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63139-2
Online ISBN: 978-3-540-69187-7
eBook Packages: Springer Book Archive