Abstract
We report on a case study on control-flow analysis of business process models. We checked 735 industrial business process models from financial services, telecommunications and other domains. We investigated these models for soundness (absence of deadlock and lack of synchronization) using three different approaches: the business process verification tool Woflan, the Petri net model checker LoLA, and a recently developed technique based on SESE decomposition. We evaluate the various techniques used by these approaches in terms of their ability of accelerating the check. Our results show that industrial business process models can be checked in a few milliseconds, which enables tight integration of modeling with control-flow analysis. We also briefly compare the diagnostic information delivered by the different approaches.
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
Mendling, J.: Empirical Studies in Process Model Verification. Trans. Petri Nets and Other Models of Concurrency (ToPNoC) 2, 208–224 (2009)
van der Aalst, W.M.P., Hirnschall, A., Verbeek, H.M.W(E.): An alternative way to analyze workflow graphs. In: Pidduck, A.B., Mylopoulos, J., Woo, C.C., Ozsu, M.T. (eds.) CAiSE 2002. LNCS, vol. 2348, pp. 535–552. Springer, Heidelberg (2002)
Verbeek, H.M.W.E., Basten, T., van der Aalst, W.M.P.: Diagnosing Workflow Processes using Woflan. Comput. J. 44(4), 246–279 (2001)
Wolf, K.: Generating petri net state spaces. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 29–42. Springer, Heidelberg (2007)
Vanhatalo, J., Völzer, H., Leymann, F.: Faster and more focused control-flow analysis for business process models through SESE decomposition. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 43–55. Springer, Heidelberg (2007)
van Dongen, B.F., Jansen-Vullers, M., Verbeek, H.M.W.E., van der Aalst, W.M.P.: Verification of the SAP reference models using EPC reduction, state-space analysis, and invariants. Comput. Ind. 58(6), 578–601 (2007)
Mendling, J., Neumann, G., van der Aalst, W.M.P.: Understanding the occurrence of errors in process models based on metrics. In: Meersman, R., Tari, Z. (eds.) OTM 2007, Part I. LNCS, vol. 4803, pp. 113–130. Springer, Heidelberg (2007)
Mendling, J.: Detection and Prediction of Errors in EPC Business Process Models. PhD thesis, Vienna University of Economics and Business Administration (May 2007)
Mendling, J., Verbeek, H.M.W.E., van Dongen, B.F., van der Aalst, W.M.P., Neumann, G.: Detection and prediction of errors in EPCs of the SAP reference model. Data Knowl. Eng. 64(1), 312–329 (2008)
Wynn, M., Verbeek, H.M.W.E., van der Aalst, W.M.P., ter Hofstede, A.H.M.: Business process verification: Finally a reality! Business Process Management Journal 15(1), 74–92 (2009)
Fahland, D.: Translating UML2 activity diagrams to Petri nets. Informatik-Berichte 226, Humboldt-Universität zu Berlin, Berlin, Germany (2008)
Desel, J., Esparza, J.: Free Choice Petri Nets. Cambridge University Press, New York (1995)
Kiepuszewski, B., ter Hofstede, A.H.M., van der Aalst, W.M.P.: Fundamentals of control flow in workflows. Acta Inf. 39(3), 143–209 (2003)
LoLA v1.11, http://service-technology.org/lola
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991)
UML2oWFN compiler, http://service-technology.org/uml2owfn
Murata, T.: Petri nets: Properties, analysis and applications. Proc. of the IEEE 77(4), 541–580 (1989)
Vanhatalo, J., Völzer, H., Koehler, J.: The refined process structure tree. In: Dumas, M., Reichert, M., Shan, M.-C. (eds.) BPM 2008. LNCS, vol. 5240, pp. 100–115. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fahland, D. et al. (2009). Instantaneous Soundness Checking of Industrial Business Process Models. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds) Business Process Management. BPM 2009. Lecture Notes in Computer Science, vol 5701. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03848-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-03848-8_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03847-1
Online ISBN: 978-3-642-03848-8
eBook Packages: Computer ScienceComputer Science (R0)