Abstract
The last decade has witnessed an increasing transformation in the design, engineering, and mining of processes, moving from a pure control-flow perspective to more integrated models where also data and decisions are explicitly considered. This calls for methods and techniques able to ascertain the correctness of such integrated models. Differently from previous approaches, which mainly focused on the local interplay between decisions and their corresponding outgoing branches, we introduce a holistic approach to verify the end-to-end soundness of a Petri net-based process model, enriched with case data and decisions. In addition, we present an effective, implemented technique that verifies soundness by translating the input net into a colored Petri net with bounded color sets, on which standard state space analysis techniques are subsequently applied. Experiments on real life illustrate the relevance and applicability in real settings.
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
Notes
- 1.
\(\mathbb {B}(X)\) indicates the set of all multisets of elements of X.
- 2.
In the remainder, given a transition \(t \in T\), we denote by \({}^\bullet t=\{p \in P. \exists a \in A. N(a)=(p,t)\}\) and \({t}^\bullet =\{p \in P. \exists a \in A. N(a)=(t,p)\}\) the usual notions of preset and postset of t.
- 3.
Notation \(a_{(p,t^i)}\) denotes the arc \(a \in A\) s.t. \(N(a)=(p,t^i)\) and cannot be employed if such an arc does not exist. The set-difference operator \(\setminus \) is overridden for multisets: given two multisets A and B, for each element \(x \in B\) with cardinality \(b_x>0\) in B and cardinality \(a_x \ge 0\) in A, the cardinality of x in \(B \setminus A\) is \(\max (0,b_x - a_x)\); moreover, if \(x \not \in B\) then \(x \not \in B \setminus A\).
- 4.
For dense domains such as real numbers such intervals are always nonempty, whereas for non-dense domains they might be empty. In this case, we consider pick undefined.
References
Decision model and notation (DMN) v1.1 (2016). http://www.omg.org/spec/DMN/1.1/
van der Aalst, W.M.P.: The application of petri nets to workflow management. J. Circ. Syst. Comput. 8(1), 21–66 (1998)
Batoulis, K., Haarmann, S., Weske, M.: Various notions of soundness for decision-aware business processes. In: Mayr, H.C., Guizzardi, G., Ma, H., Pastor, O. (eds.) ER 2017. LNCS, vol. 10650, pp. 403–418. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-69904-2_31
Batoulis, K., Weske, M.: Soundness of decision-aware business processes. In: Carmona, J., Engels, G., Kumar, A. (eds.) BPM 2017. LNBIP, vol. 297, pp. 106–124. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-65015-9_7
Calvanese, D., De Giacomo, G., Montali, M.: Foundations of data aware process analysis: a database theory perspective. In: Proceedings of PODS 2013. ACM (2013)
Calvanese, D., Dumas, M., Laurson, Ü., Maggi, F.M., Montali, M., Teinemaa, I.: Semantics and analysis of DMN decision tables. In: La Rosa, M., Loos, P., Pastor, O. (eds.) BPM 2016. LNCS, vol. 9850, pp. 217–233. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45348-4_13
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
de Leoni, M., Felli, P., Montali, M.: A holistic approach for soundness verification of decision-aware process models. CoRR Technical report arXiv:1804.02316, arXiv.org e-Print archive (2018). https://arxiv.org/abs/1804.02316
Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281–1294 (2008)
Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems, 1st edn. Springer, Heidelberg (2009)
Kalenkova, A.A., van der Aalst, W.M.P., Lomazova, I.A., Rubin, V.A.: Process mining using BPMN: relating event logs and process models. Softw. Syst. Model. 16(4), 1019–1048 (2017)
Knuplesch, D., Ly, L.T., Rinderle-Ma, S., Pfeifer, H., Dadam, P.: On enabling data-aware compliance checking of business process models. In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y. (eds.) ER 2010. LNCS, vol. 6412, pp. 332–346. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16373-9_24
Mannhardt, F.: Multi-perspective process mining. Ph.D. thesis, Department of Mathematics and Computer Science (2018). https://pure.tue.nl/ws/portalfiles/portal/90463927
Mannhardt, F., de Leoni, M., Reijers, H.A., van der Aalst, W.M.P.: Decision mining revisited - discovering overlapping rules. In: Nurcan, S., Soffer, P., Bajec, M., Eder, J. (eds.) CAiSE 2016. LNCS, vol. 9694, pp. 377–392. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39696-5_23
Montali, M., Calvanese, D.: Soundness of data-aware, case-centric processes. Int. J. Softw. Tools Technol. Transf. 18(5), 535–558 (2016)
Ratzer, A.V., et al.: CPN tools for editing, simulating, and analysing coloured petri nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 450–462. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44919-1_28
Sidorova, N., Stahl, C., Trčka, N.: Soundness verification for conceptual workflow nets with data: early detection of errors with the most precision possible. Inf. Syst. 36(7), 1026–1043 (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
de Leoni, M., Felli, P., Montali, M. (2018). A Holistic Approach for Soundness Verification of Decision-Aware Process Models. In: Trujillo, J., et al. Conceptual Modeling. ER 2018. Lecture Notes in Computer Science(), vol 11157. Springer, Cham. https://doi.org/10.1007/978-3-030-00847-5_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-00847-5_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00846-8
Online ISBN: 978-3-030-00847-5
eBook Packages: Computer ScienceComputer Science (R0)