Soundness Verification of Data-Aware Process Models with Variable-to-Variable Conditions

• Autorzy: Felli Paolo , de Leoni Massimiliano , Montali Marco

Identyfikatory

DOI

10.3233/FI-2021-2064

• Języki publikacji: EN

Abstrakty

EN

Traditionally Business Process Modeling has only focused on the control-flow perspective, thus allowing process designers to specify the constraints on the activities of the process: the order and potential concurrency of their execution, their mutual exclusivity, the possibility of being repeated, etc. However, activities are executed by different resources, manipulate data objects and are constrained by the state of such objects. This requires that the traditional notion of soundness, typically introduced for control-flow-only models, is extended so as to consider data. Intuitively, a (data-aware) process model is sound if (1) it does not contain deadlocks, (2) no more activities are enabled when the process instance is marked as completed and finally (3) there are no parts of the model that cannot be executed. Although several data-aware notations have been introduced in the literature, not all of these are given a formal semantics. In this paper, we propose a technique for checking the data-aware soundness for a specific class of such integrated models, with a simple syntax and semantics, building on Data Petri Nets (DPNs). These are Petri nets enriched with case variables, where transitions are guarded by formulas that inspect and update such variables, and are of the form variable-operator-variable or variable-operator-constant. Even though DPNs are less expressive than Petri nets where data are carried by tokens, they elegantly capture business processes operating over simple case data, allowing to model complex data-aware decisions. We show that, if a DPN is data-aware sound, the Constraint Graph is a finite-state automaton; however, a finite-state Constraint Graph does not guarantee data-aware soundness, but provides a finite structure through which this property can be checked. Finally, we investigate further properties beyond data-aware soundness, such as the problem of verifying that an actor participating in the business process can unilaterally enforce data-aware soundness by restricting the possible executions of a bounded DPN, assuming this actor to be able to control the firing of some transitions and decide the value of some of the case variables whenever these are updated.

Słowa kluczowe

EN

soundness of process models; data perspective; data petrin nets

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 182, nr 1
• Strony: 1--29
• Opis fizyczny: Bibliogr. 35 poz., rys.

Twórcy

autor

Felli Paolo

• Free University of Bozen-Bolzano Bolzano, Italy

autor

de Leoni Massimiliano

• University of Padova Padova, Italy

autor

Montali Marco

• Free University of Bozen-Bolzano Bolzano, Italy

Bibliografia

• [1] Reichert M. Process and Data: Two Sides of the Same Coin? In: Proc. of OTM, volume 7565 of LNCS. Springer, 2012 pp. 2-19.
• [2] Calvanese D, De Giacomo G, Montali M. Foundations of Data Aware Process Analysis: A Database Theory Perspective. In: Proc. of PODS. ACM, 2013 .
• [3] Decision Model and Notation (DMN) V1.1, 2016. URL http://www.omg.org/spec/DMN/1.1/.
• [4] Calvanese D, Dumas M, Laurson ¨U, Maggi FM, Montali M, Teinemaa I. Semantics and Analysis of DMN Decision Tables. In: Proc. of BPM, volume 9850 of LNCS. Springer, 2016 pp. 217-233.
• [5] Batoulis K, Weske M. Soundness of Decision-Aware Business Processes. In: Proc. of BPM Forum. Springer, 2017 pp. 106-124.
• [6] de Leoni M, van der Aalst WMP. Data-aware Process Mining: Discovering Decisions in Processes Using Alignments. In: SAC 2013. ACM. ISBN 978-1-4503-1656-9, 2013 pp. 1454-1461.
• [7] de Leoni M, Mannhardt F. Decision Discovery in Business Processes. In: Sakr S, Zomaya A (eds.), Encyclopedia of Big Data Technologies. Springer International Publishing. ISBN 978-3-319-63962-8,2018
• [8] Mannhardt F. Multi-perspective process mining. Ph.d. thesis, Eindhoven University of Technology, 2018. https://research.tue.nl/en/publications/multi-perspective-process-mining.
• [9] van der Aalst WMP. The Application of Petri Nets to Workflow Management. Journal of Circuits, Systems, and Computers, 1998. 8(1):21-66.
• [10] Montali M, Calvanese D. Soundness of Data-Aware, Case-Centric Processes. Int. Journal on Software Tools for Technology Transfer, 2016.
• [11] Batoulis K, Haarmann S, Weske M. Various Notions of Soundness for Decision-Aware Business Processes. In: Proc. of ER, volume 10650 of LNCS. Springer, 2017 pp. 403-418.
• [12] Rosa-Velardo F, de Frutos-Escrig D. Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci., 2011. 412(34):4439-4451.
• [13] Lasota S. Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture. In: Proc. of PN, volume 9698 of LNCS. Springer, 2016 pp. 20-36.
• [14] Triebel M, S¨urmeli J. Homogeneous Equations of Algebraic Petri Nets. In: Proc. of CONCUR, LNCS. Springer, 2016 pp. 1-14.
• [15] Fahland D. Describing Behavior of Processes with Many-to-Many Interactions. In: Proc. of PN. Springer, 2019 pp. 3-24.
• [16] Montali M, Rivkin A. DB-Nets: On the Marriage of Colored Petri Nets and Relational Databases. T. Petri Nets and Other Models of Concurrency, 2017. 12:91-118.
• [17] Polyvyanyy A, van der Werf JMEM, Overbeek S, Brouwers R. Information Systems Modeling: Language, Verification, and Tool Support. In: Proc. of CAiSE, volume 11483 of LNCS. Springer, 2019 pp. 194-212.
• [18] Ghilardi S, Gianola A, Montali M, Rivkin A. Petri Nets with Parameterised Data - Modelling and Verification. In: Proc. of BPM, volume 12168 of LNCS. Springer, 2020 pp. 55-74.
• [19] de Leoni M, Munoz-Gama J, Carmona J, van der Aalst WMP. Decomposing Alignment-Based Conformance Checking of Data-Aware Process Models, pp. 3-20. Springer, 2014.
• [20] de Leoni M, Felli P, Montali M. A Holistic Approach for Soundness Verification of Decision-Aware Process Models. In: Conceptual Modeling - 37th International Conference, ER 2018, Xi’an, China, October 22-25, 2018, Proceedings. 2018 pp. 219-235.
• [21] Felli P, de Leoni M, Montali M. Soundness Verification of Decision-Aware Process Models with Variable-to-Variable Conditions. In: 2019 19th International Conference on Application of Concurrency to System Design (ACSD). 2019 pp. 82-91.
• [22] Clarke EM, Grumberg O, Long DE. Model Checking and Abstraction. ACM Trans. Program. Lang. Syst., 1994. 16(5):1512-1542.
• [23] Morimoto S. A Survey of Formal Verification for Business Process Modeling. In: Proceedings of the 8th International Conference on Computational Science, Part II, ICCS ’08. Springer-Verlag, Berlin, Heidelberg. ISBN 978-3-540-69386-4, 2008 pp. 514-522.
• [24] Sadiq S, Orlowska M, Sadiq W, Foulger C. Data Flow and Validation in Workflow Modelling. In: Proceedings of the 15th Australasian Database Conference - Volume 27, Proc. of ADC ’04. Australian Computer Society, Inc., Darlinghurst, Australia, 2004 pp. 207-214.
• 25] Corradini F, Fornari F, Polini A, Re B, Tiezzi F, Vandin A. BProVe: A Formal Verification Framework for Business Process Models. In: Proceedings of the 32Nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017. IEEE Press, 2017 pp. 217-228.
• [26] Corradini F, Fornari F, Polini A, Re B, Tiezzi F. A formal approach to modeling and verification of business process collaborations. Science of Computer Programming, 2018. 166:35 - 70.
• [27] Sidorova N, Stahl C, Trˇcka N. Soundness Verification for Conceptual Workflow Nets with Data: Early Detection of Errors with the Most Precision Possible. Information Systems, 2011. 36(7):1026-1043.
• [28] Knuplesch D, Ly LT, Rinderle-Ma S, Pfeifer H, Dadam P. On Enabling Data-Aware Compliance Checking of Business Process Models. In: Proc. of ER, volume 6412 of LNCS. Springer, 2010 pp. 332-346.
• [29] Cassandras CG, Lafortune S. Introduction to Discrete Event Systems. Springer-Verlag, Berlin, Heidelberg, 2006. ISBN 0387333320. [30] Giua A, Seatzu C. Petri nets for the control of discrete event systems. Software & Systems Modeling, 2015. 14(2):693-701. doi:10.1007/s10270-014-0425-1.
• [31] Iordache M, Antsaklis P. Supervisory control of concurrent systems: A petri net structural approach, pp. 1-278. Springer, 2006.
• [32] Sidorova N, Stahl C, Trˇcka N. Workflow Soundness Revisited: Checking Correctness in the Presence of Data While Staying Conceptual. In: Proceedings of the 22Nd International Conference on Advanced Information Systems Engineering, Proc. of CAiSE 2010. Springer, 2010 pp. 530-544.
• [33] Dijkman RM, Dumas M, Ouyang C. Semantics and analysis of business process models in BPMN. Information & Software Technology, 2008. 50(12):1281-1294.
• [34] Kalenkova AA, van der Aalst WMP, Lomazova IA, Rubin VA. Process Mining Using BPMN: Relating Event Logs and Process Models. In: Proc. of MODELS. ACM, 2016 pp. 123-123.
• [35] Esparza J. Decidability and Complexity of Petri Net Problems - An Introduction. In: Reisig W, Rozenberg G (eds.), Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science. Springer, 1996 pp. 374-428.

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023). (PL)