Semantics and Controllability of Time-Aware Business Processes

• Autorzy: De Angelis Emanuele , Fioravanti Fabio , Meo Maria Chiara , Pettorossi Alberto , Proietti Maurizio

Identyfikatory

DOI

10.3233/FI-2019-1783

• Języki publikacji: EN

Abstrakty

EN

We present an operational semantics for time-aware business processes, that is, processes modeling the execution of business activities, whose durations are subject to linear constraints over the integers. We assume that some of the durations are controllable, that is, they can be determined by the organization that executes the process, while others are uncontrollable, that is, they are determined by the external world. Then, we consider controllability properties, which guarantee the completion of the execution of the process, satisfying the given duration constraints, independently of the values of the uncontrollable durations. Controllability properties are encoded by quantified reachability formulas, where the reachability predicate is recursively defined by means of constrained Horn clauses (CHCs). These clauses are automatically derived from the operational semantics of the process. Finally, we present two algorithms for solving the so called weak and strong controllability problems. Our algorithms reduce these problems to the verification of a set of quantified integer constraints, which are simpler than the original quantified reachability formulas, and can effectively be handled by state-of-the-art CHC solvers.

Słowa kluczowe

EN

controllability; systems engineering; semantics; integers

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 165, nr 3-4
• Strony: 205--244
• Opis fizyczny: Bibliogr. 41 poz., rys., tab.

Twórcy

autor

De Angelis Emanuele

• University of Chieti-Pescara, Viale Pindaro 42, 65127, Pescara, Italy

autor

Fioravanti Fabio

• University of Chieti-Pescara, Viale Pindaro 42, 65127, Pescara, Italy

autor

Meo Maria Chiara

• University of Chieti-Pescara, Viale Pindaro 42, 65127, Pescara, Italy

autor

Pettorossi Alberto

• University of Rome Tor Vergata, Via del Politecnico 1, 00133 Rome, Italy

autor

Proietti Maurizio

• IASI-CNR, Via dei Taurini 19, 00185 Rome, Italy

Bibliografia

• [1] van der Aalst WMP. The Application of Petri Nets to Workflow Management. Journal of Circuits, Systems, and Computers, 1998;8(1):21-66. URL https://doi.org/10.1142/S0218126698000043.
• [2] Bagheri Hariri B, Calvanese D, De Giacomo G, Deutsch A, and Montali M. Verification of relational data-centric dynamic systems with external services. Proc. PODS ’13, ACM, 2013 pp. 163-174. doi:10.1145/2463664.2465221.
• [3] Berthomieu B, and Vernadat F. Time Petri nets analysis with TINA. Proc. QEST ’06, IEEE Computer Society, 2006 pp. 123-124. doi:10.1109/QEST.2006.56.
• [4] Bjørner N, Gurfinkel A, McMillan KL, and Rybalchenko A. Horn clause solvers for program verification. In: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich, LNCS 9300. Springer, 2015 pp. 24-51. doi:10.1007/978-3-319-23534-9_2.
• [5] Bradley AR, and Manna Z. The Calculus of Computation. Springer, 2007. ISBN-978-3-540-74112-1, 978-3-642-09347-0.
• [6] Cheikhrouhou S, Kallel S, Guermouche N, and Jmaiel M. The temporal perspective in business process modeling: a survey and research challenges. Service Oriented Computing and Applications, 2015;9(1):75-85. doi:10.1007/s11761-014-0170-x.
• [7] Cimatti A, Hunsberger L, Micheli A, Posenato R, and Roveri M. Dynamic controllability via timed game automata. Acta Informatica, 2016;53(6):681-722. doi:10.1007/s00236-016-0257-2.
• [8] Cimatti A, Micheli A, and Roveri M. Solving strong controllability of temporal problems with uncertainty using SMT. Constraints, 2015;20(1):1-29. doi:10.1007/s10601-014-9167-5.
• [9] Cimatti A, Micheli A, and Roveri M. An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty. Artif. Intell., 2015;224:1-27. URL https://doi.org/10.1016/j.artint.2015.03.002.
• [10] Combi C, Oliboni B, Zerbato F. Modeling and handling duration constraints in BPMN 2.0. Proc. SAC ’17, ACM, 2017 pp. 727-734. ISBN-978-1-4503-4486-9.
• [11] Combi C, and Posenato R. Controllability in Temporal Conceptual Workflow Schemata. Proc. BPM ’09, LNCS 5701, Springer, 2009 pp. 64-79. doi:10.1007/978-3-642-03848-8_6.
• [12] Damaggio E, Deutsch A, and Vianu V. Artifact systems with data dependencies and arithmetic. ACM Transactions on Database Systems, 2012;37(3):1-36. doi:10.1145/2338626.2338628.
• [13] De Angelis E, Fioravanti F, Meo MC, Pettorossi A, and Proietti M. Verification of time-aware business processes using Constrained Horn Clauses. Proc. LOPSTR ’16, LNCS 10184, Springer, 2017 pp. 38-55. doi:10.1007/978-3-319-63139-4_3.
• [14] De Angelis E, Fioravanti F, Pettorossi A, and Proietti M. Veri MAP: A tool for verifying programs through transformations. Proc. TACAS ’14, LNCS 8413, Springer, 2014 pp. 568-574. doi:10.1007/978-3-642-54862-8_47.
• [15] De Angelis E, Fioravanti F, Pettorossi A, and Proietti M. Semantics-based generation of verification conditions via program specialization. Science of Computer Programming, 2017;147:78-108. URL https://doi.org/10.1016/j.scico.2016.11.002.
• [16] de Moura LM, and Bjørner N. Z3: An efficient SMT solver. Proc. TACAS ’08, LNCS 4963, Springer, 2008 pp. 337-340. doi:10.1007/978-3-540-78800-3_24.
• [17] Etalle S, and Gabbrielli M. Transformations of CLP modules. Theoretical Computer Science, 1996;166(1-2):101-146. URL https://doi.org/10.1016/0304-3975(95)00148-4.
• [18] Fioravanti F, and Pettorossi A, and Proietti M, and Senni V. Improving Reachability Analysis of Infinite State Systems by Specialization. Fundamenta Informaticae, 2012;119(3-4): 281-300. doi:10.3233/FI-2012-738.
• [19] Formal Systems (Europe) Ltd. Failures-Divergences Refinement, FDR2 User Manual. www.fsel.com, 1998.
• [20] ter Hofstede AM, van der Aalst WMP, Adams M, and Russell N, Eds. Modern Business Process Automation: YAWL and its Support Environment. Springer, 2010. ISBN-978-3-642-03120-5, 978-3-642-42490-8.
• [21] Jaffar J, and Maher M. Constraint logic programming: A survey. Journal of Logic Programming, 1994;19/20:503-581. URL https://doi.org/10.1016/0743-1066(94)90033-7.
• [22] Jaffar J, Maher M, Marriott K, and Stuckey P. The semantics of constraint logic programs. Journal of Logic Programming, 1998;37(1-3):1-46. URL https://doi.org/10.1016/S0743-1066(98)10002-X.
• [23] Kowalski RA, and Sergot MJ. A Logic-based Calculus of Events. New Generation Comput., 1986;4(1):67-95. doi:10.1007/BF03037383.
• [24] Kumar A, Sabbella SR, and Barton RR. Managing controlled violation of temporal process constraints. BPM ’15, LNCS 9253, Springer, 2015 pp. 280-296. doi:10.1007/978-3-319-23063-4_20.
• [25] Lanz A, Posenato R, Combi C, and Reichert M. Controlling time-awareness in modularized processes. Proc. BPMDS/EMMSAD ’16, LNBIP 248, Springer, 2016 pp. 157-172. doi:10.1007/978-3-319-39429-9_11.
• [26] Larsen KG, Pettersson P, and Yi W. UPPAAL in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1997;1(1-2):134-152. doi:10.1007/s100090050010.
• [27] Makni M, Tata S, Yeddes MM, and Ben Hadj-Alouane N. Satisfaction and coherence of deadline constraints in inter-organizational workflows. Proc. OTM ’10, LNCS 6426, Springer, 2010 pp. 523-539. doi:10.1007/978-3-642-16934-2_39.
• [28] Malcolm DG, Roseboom JH, Clark CE, and Fazar W. Application of a Technique for Research and Development Program Evaluation. Operation Research, 1959;7(5):646-669. doi:10.1287/opre.7.5.646.
• [29] McCarthy J, and Hayes PJ. Some Philosophical Problems from the Standpoint of Artificial Intelligence. In: B. Meltzer and D. Michie (eds.), Machine Intelligence 4, Edinburgh University Press, 1969 pp. 463-502. ISBN: 978-0852240625.
• [30] OMG. Business Process Model and Notation. URL http://www.omg.org/spec/BPMN/.
• [31] Peintner B, Venable KB, and Yorke-Smith N. Strong Controllability of Disjunctive Temporal Problems with Uncertainty. Proc. CP ’07, LNCS 4741, Springer, 2007 pp. 856-863. doi:10.1007/978-3-540-74970-7_64.
• [32] Pritsker AAB. GERT: Graphical Evaluation and Review Technique. Memorandum RM-4973-NASA. National Aeronautics and Space Administration, 1966. URL https://ntrs.nasa.gov/search.jsp? R=19670022025.
• [33] Proietti M, and Smith F. Reasoning on data-aware business processes with constraint logic. Proc. SIMPDA ’14, CEUR, Vol. 1293, 2014 pp. 60-75. URL http://ceur-ws.org/Vol-1293/paper5.pdf.
• [34] Smith F, and Proietti M. Rule-based behavioral reasoning on semantic business processes. In: Proc. ICAART ’13, Vol. II, SciTePress, 2013 pp. 130-143. ISBN:978-989-8565-39-6.
• [35] Thielscher M. From Situation Calculus to Fluent Calculus: State update axioms as a solution to the inferential frame problem. Artif. Intell., 1999;111(1-2):277-299. URL https://doi.org/10.1016/S0004-3702(99)00033-8.
• [36] Venable KB, Volpato M, Peintner B, and Yorke-Smith N. Weak and dynamic controllability of temporal problems with disjunctions and uncertainty. Proc. COPLAS ’10, Association for the Advancement of Artificial Intelligence, 2010 pp. 50-59. URI http://hdl.handle.net/10938/12112.
• [37] Vidal T, and Fargier H. Handling contingency in temporal constraint networks: from consistency to controllabilities. J. Exp. Theor. Artif. Intell., 1999;11(1):23-45. URL https://doi.org/10.1080/095281399146607.
• [38] Watahiki K, Ishikawa F, and Hiraishi K. Formal verification of business processes with temporal and resource constraints. Proc. SMC’11, IEEE, 2011 pp. 1173-1180. doi:10.1109/ICSMC.2011.6083857.
• [39] Weber I, Hoffmann J, and Mendling J. Beyond soundness: On the verification of semantic business process models. Distrib. Parallel Databases, 2010;27(3):271-343. doi:10.1007/s10619-010-7060-9.
• [40] Weske M. Business Process Management: Concepts, Languages, Architectures. Springer, 2007. doi:10.1007/978-3-540-73522-9.
• [41] Wong PYH, and Gibbons J. A relative timed semantics for BPMN. Electronic Notes Theoretical Computer Science, 2009;229(2):59-75. URL https://doi.org/10.1016/j.entcs.2009.06.029.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).