Riccardo De Masellis
ABSTRACT
Checking the compliance of a business process execution with respect to a set of regulations is an important issue in several settings. A common way of representing the expected behavior of a process is to describe it as a set of business constraints. Runtime verification and monitoring facilities allow us to continuously determine the state of constraints on the current process execution, and to promptly detect violations at runtime. A plethora of studies has demonstrated that in several settings business constraints can be formalized in terms of temporal logic rules. However, in virtually all existing works the process behavior is mainly modeled in terms of control-flow rules, neglecting the equally important data perspective. In this paper, we overcome this limitation by presenting a novel monitoring approach that tracks streams of process events (that possibly carry data) and verifies if the process execution is compliant with a set of data-aware business constraints, namely constraints not only referring to the temporal evolution of events, but also to the temporal evolution of data. The framework is based on the formal specification of business constraints in terms of first-order linear temporal logic rules. Operationally, these rules are translated into finite state automata for dynamically reasoning on partial, evolving execution traces. We show the versatility of our approach by formalizing (the data-aware extension of) Declare, a declarative, constraint-based process modeling language, and by demonstrating its application on a concrete case dealing with web security.
- XES Standard Definition, 2009. www.xes-standard.org.Google Scholar
- C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008. Google ScholarDigital Library
- D. A. Basin, F. Klaedtke, and S. Müller. Policy monitoring in first-order temporal logic. In CAV, pages 1–18, 2010. Google ScholarDigital Library
- A. Bauer, J.-C. Küster, and G. Vegliach. From propositional to first-order monitoring. In RV, pages 59–75, 2013.Google ScholarCross Ref
- A. Bauer, M. Leucker, and C. Schallhart. The good, the bad, and the ugly, but how ugly is ugly? In RV, pages 126–138, 2007. Google ScholarDigital Library
- A. Bauer, M. Leucker, and C. Schallhart. Runtime verification for ltl and tltl. ACM Trans. Softw. Eng. Methodol., 20(4):14:1–14:64, Sept. 2011. Google ScholarDigital Library
- F. Belardinelli, A. Lomuscio, and F. Patrizi. Verification of deployed artifact systems via data abstraction. In ICSOC, pages 142–156, 2011. Google ScholarDigital Library
- J. Chomicki. Efficient checking of temporal integrity constraints using bounded history encoding. ACM Transactions on Database Systems, 20(2):149–186, 1995. Google ScholarDigital Library
- E. Damaggio, A. Deutsch, R. Hull, and V. Vianu. Automatic verification of data-centric business processes. In BPM, pages 3–16, 2011. Google ScholarDigital Library
- M. d’Amorim and G. Rosu. Efficient monitoring of omega-languages. In CAV, pages 364–378, 2005.Google Scholar
- B. D’Angelo, S. Sankaranarayanan, C. Sánchez, W. Robinson, B. Finkbeiner, H. B. Sipma, S. Mehrotra, and Z. Manna. Lola: Runtime monitoring of synchronous systems. In TIME, pages 166–174, 2005. Google ScholarDigital Library
- G. De Giacomo, R. De Masellis, and R. Rosati. Verification of conjunctive artifact-centric services. Int. J. Cooperative Inf. Syst., 21(2):111–140, 2012.Google ScholarCross Ref
- R. De Masellis and J. Su. Runtime enforcement of first-order ltl properties on data-aware business processes. In ICSOC, pages 54–68, 2013.Google ScholarDigital Library
- G. Dong, J. Su, and R. Topor. Nonrecursive incremental evaluation of datalog queries. Annals of Mathematics and Artificial Intelligence, 14:187–223, 1995.Google ScholarCross Ref
- C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. McIsaac, and D. V. Campenhout. Reasoning with temporal logic on truncated paths. In CAV, pages 27–39, 2003.Google Scholar
- M. Fitting and R. L. Mendelsohn. First-Order Modal Logic. Kluwer Academic Press, 1998. Google ScholarDigital Library
- R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In PSTV, pages 3–18, 1995. Google ScholarDigital Library
- D. Giannakopoulou and K. Havelund. Automata-based verification of temporal properties on running programs. In ASE, pages 412–416, 2001. Google ScholarDigital Library
- S. Hallé and R. Villemaire. Runtime monitoring of message-based workflows with data. In EDOC, pages 63–72, 2008. Google ScholarDigital Library
- B. B. Hariri, D. Calvanese, G. De Giacomo, R. De Masellis, and P. Felli. Foundations of relational artifacts verification. In BPM, pages 379–395, 2011. Google ScholarDigital Library
- R. Hull, E. Damaggio, R. De Masellis, F. Fournier, M. Gupta, F. T. Heath, S. Hobson, M. H. Linehan, S. Maradugu, A. Nigam, P. N. Sukaviriya, and R. Vacul´ın. Business artifacts with guard-stage-milestone lifecycles: managing artifact interactions with conditions and events. In DEBS, pages 51–62, 2011. Google ScholarDigital Library
- O. Kupferman and M. Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291–314, 2001. Google ScholarDigital Library
- F. Maggi, M. Montali, M. Westergaard, and W. van der Aalst. Monitoring business constraints with linear temporal logic: An approach based on colored automata. In BPM 2011, volume 6896, pages 132–147, 2011. Google ScholarDigital Library
- F. M. Maggi. Declarative process mining with the declare component of prom. In BPM (Demos), 2013.Google Scholar
- F. M. Maggi, M. Dumas, L. Garc´ıa-Ba˜ nuelos, and M. Montali. Discovering data-aware declarative process models from event logs. In BPM, volume 8094 of Lecture Notes in Computer Science, pages 81–96. Springer, 2013. Google ScholarDigital Library
- F. M. Maggi, M. Westergaard, M. Montali, and W. M. P. van der Aalst. Runtime verification of LTL-based declarative process models. In RV 2011, volume 7186, pages 131–146. Google ScholarDigital Library
- F. M. Maggi, M. Westergaard, M. Montali, and W. M. P. van der Aalst. Runtime verification of ltl-based declarative process models. In RV, pages 131–146, 2011. Google ScholarDigital Library
- M. Montali. Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach, volume 56 of Lecture Notes in Business Information Processing. Springer, 2010.Google Scholar
- M. Montali, F. Chesani, F. M. Maggi, and P. Mello. Towards data-aware constraints in declare. In SAC, pages 1391–1396. ACM Press and Addison Wesley, 2013. Google ScholarDigital Library
- M. Montali, F. M. Maggi, F. Chesani, P. Mello, and W. M. P. van der Aalst. Monitoring business constraints with the event calculus. ACM TIST, 5(1):17, 2013. Google ScholarDigital Library
- M. Montali, M. Pesic, W. M. P. van der Aalst, F. Chesani, P. Mello, and S. Storari. Declarative Specification and Verification of Service Choreographies. ACM Transactions on the Web, 4(1), 2010. Google ScholarDigital Library
- M. Pesic, H. Schonenberg, and W. van der Aalst. DECLARE: Full Support for Loosely-Structured Processes. In Proc. of EDOC, pages 287–300. IEEE, 2007. Google ScholarDigital Library
- W. van der Aalst, M. Pesic, and H. Schonenberg. Declarative Workflows: Balancing Between Flexibility and Support. Computer Science - R&D, pages 99––113, 2009.Google Scholar
- M. Westergaard and F. M. Maggi. Declare: A tool suite for declarative workflow modeling and enactment. In BPM (Demos), 2011.Google Scholar
- M. Westergaard and F. M. Maggi. Looking into the future: Using timed automata to provide a priori advice about timed declarative process models. In OTM, volume 7565 of Lecture Notes in Computer Science, pages 250–267. Springer, 2012.Google Scholar
Index Terms
- Monitoring data-aware business constraints with finite state automata
Recommendations
Monitoring Constraints and Metaconstraints with Temporal Logics on Finite Traces
Runtime monitoring is a central operational decision support task in business process management. It helps process executors to check on-the-fly whether a running process instance satisfies business constraints of interest, providing an immediate feedback ...
Monitoring business constraints with the event calculus
Special Section on Intelligent Mobile Knowledge Discovery and Management Systems and Special Issue on Social Web MiningToday, large business processes are composed of smaller, autonomous, interconnected subsystems, achieving modularity and robustness. Quite often, these large processes comprise software components as well as human actors, they face highly dynamic ...
Monitoring business constraints with linear temporal logic: an approach based on colored automata
BPM'11: Proceedings of the 9th international conference on Business process managementToday's information systems record real-time information about business processes. This enables the monitoring of business constraints at runtime. In this paper, we present a novel runtime verification framework based on linear temporal logic and ...
Comments