Abstract
Compliance management is important in several industry sectors where there is a high incidence of regulatory control. It must be ensured that business practices, as reflected in business processes, comply with the rules. Such compliance checks are challenging due to (1) the different life cycles of rules and processes, and (2) their disparate representations. (1) requires retrospective checking of process models. To address (2), we herein devise a framework where processes are annotated to capture the semantics of task execution, and compliance is checked against a set of constraints posing restrictions on the desirable process states. Each constraint is a clause, i.e., a disjunction of literals. If a process can reach a state that falsifies all literals of one of the constraints, then that constraint is violated in that state, and indicates non-compliance. Naively, such compliance can be checked by enumerating all reachable states. Since long waiting times are undesirable, it is important to develop efficient (low-order polynomial time) algorithms that (a) perform exact compliance checking for restricted cases, or (b) perform approximate compliance checking for more general cases. Herein, we observe that methods of both kinds can be defined as a natural extension of our earlier work on semantic business process validation. We devise one method of type (a), and we devise two methods of type (b); both are based on similar restrictions to the processes, where the restrictions made by methods (b) are a subset of those made by method (a). The approximate methods each guarantee either of soundness (finding only non-compliances) or completeness (finding all non-compliances). We describe how one can trace the state evolution back to the process activities which caused the (potential) non-compliance, and hence provide the user with an error diagnosis.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
It may seem odd that executability is a prerequisite, since I-propagation was designed to check this same property. The latter can, in fact, be done, by a certain contra-position argument (outlined in Section 3 where we explain I-propagation).
Hence our constants correspond to BPEL “data variables” (OASIS 2007); note that the term “variables” in our context is reserved for variables as used in logics, quantifying over constants.
As indicated, our compliance rules are also clauses; however, their formal interpretation is different. This will be explained in Section 2.2, when we formally introduce constraints bases.
A striking if imprecise illustration is that of gravity vs. traffic rules: any car must drive on the ground, by physical law; whether they use the left or right hand side of the road is a matter of rules.
It may also be puzzling in this context that, as stated above, we designed I-propagation in order to check whether a process is executable. However, I * can actually be used for that purpose: \({\cal G}\) is executable iff, for all \(n \in {\cal N}_T\), \(\mbox{pre}(n) \subseteq I^*(IN(n))\). First, if \({\cal G}\) is executable then by Lemma 1 we have that I * captures exactly the literals which are necessarily true, and hence obviously \(\mbox{pre}(n) \subseteq I^*(IN(n))\) for all n. Second, if n is not executable but all its predecessors are, then the arguments behind the proof of Lemma 1 can be applied up to n, and we get that I * handles IN(n) correctly, and hence \(\mbox{pre}(n) \not \subseteq I^*(IN(n))\) must hold.
Note that this “lucky coincidence” suggests a simple generalization of non-contradicted constraints: a task node may negate one of the constraint’s literals as long as it makes another one true.
Note that we only talk about “reasons for a literal being true”, not about “reasons for a literal being false”. We get the latter for free due to the duality between positive and negative literals. For example, if we want to ask “what are the reasons for a literal l to be necessarily false at an edge e?” then this is the same as question (1) for \(\neg{\kern1pt} l\).
If the start node does not have the effect \(\neg{\kern1pt} paid(o)\), then this is formally interpreted to mean that paid(o) might be true at the beginning already. Consequently, \({R^{\triangleright}}(e_+,paid(o))\) collects all nodes on paths from n 0 to n + that do not contain Accept Payment – i.e., all nodes except Send Invoice and Receive Payment.
In free-choice nets, for every two transitions either the input places are disjoint, or identical. In conflict-free nets, every place either is on the input of only one transition, or is on the output of all such transitions.
One can extend this method to encode compliance checking at an edge e, simply by assigning e as another input place of t. However, this construction is necessarily neither free-choice nor conflict-free, due to the competition between t and the node that consumes the control-flow tokens on e.
References
Aalst, W. (1999a). Formalization and verification of event-driven process chains. Information and Software Technology, 41(10), 639–650.
Aalst, W. (1999b). Interorganizational workflows: An approach based on message sequence charts and petri nets. Systems Analysis Modelling Simulation, 34(3), 335–367.
Ankolekar, A., Burstein, M., Hobbs, J. R., Lassila, O., Martin, D., McDermott, D., et al. (2002). DAML-S: Web service description for the semantic web. In ISWC.
Aspvall, B., Plass, M., & Tarjan, R. (1979). A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters, 8, 121–123.
Awad, A., Decker, G., & Weske, M. (2008). Efficient compliance checking using bpmn-q and temporal logic. In M. Dumas, M. Reichert, & M. C. Shan (Eds.), Business process management, 6th international conference, BPM 2008. Lecture notes in computer science (Vol. 5240, pp. 326–341). New York: Springer.
Baader, F., Lutz, C., Milicic, M., Sattler, U., & Wolter, F. (2005). Integrating description logics and action formalisms: First results. In AAAI.
Berthelot, G. (1987). Transformations and decompositions of nets. In W. Brauer, W. Reisig, & G. Rozenberg (Eds.), Advances in petri nets 1986 part I: Petri nets, central models and their properties. LNCS (Vol. 254, pp. 360–376). New York, Springer.
Chopra, A. K., & Sing, M. P. (2007). Producing compliant interactions: Conformance, coverage and interoperability. Declarative agent languages and technologies IV. In M. Baldoni, & U. Endriss (Eds.), LNAI (Vol. 4327, pp. 1–15). Berlin: Springer.
Coalition, T. O. S. (2003). OWL-S: Semantic markup for web services. In M. Burstein, J. Hobbs, O. Lassila, D. McDermott, S. McIlraith, S. Narayanan, M. Paolucci, B. Parsia, T. Payne, E. Sirin, N. Srinivasan, K. Sycara & D. Martin (Eds.),OWL-S: Semantic Markup for Web Services. OWL-S 1.1. http://www.daml.org/services/owl-s/1.1/. Version 1.1
Desel, J., & Esparza, J. (1995). Free choice Petri nets. New York, NY, USA: Cambridge University Press.
Farrell, A., Sergot, M., Sallé, M., & Bartolini, C. (2005). Using the event calculus for tracking the normative state of contracts. International Journal of Cooperative Information Systems, 14(2–3), 99–129.
Fensel, D., Lausen, H., Polleres, A., Stollberg, M., Roman, D., de Bruijn, J., et al. (2006). Enabling semantic web services: The web service modeling ontology. New York: Springer.
Garcia-Valles, F., & Colom, J. (1999). Implicit places in net systems. In Petri nets and performance Models, 1999. Proceedings. The 8th international workshop (pp. 104–113).
Ghose, A., & Koliadis, G. (2007). Auditing business process compliance. In Service Oriented Computing, ISOC 2007. LNCS (pp. 169–180). New York: Springer.
Giacomo, G. D., Lenzerini, M., Poggi, A., & Rosati, R. (2006). On the update of description logic ontologies at the instance level. In AAAI.
Governatori, G., Hoffmann, J., Sadiq, S., & Weber, I. (2008). Detecting regulatory compliance for business process models through semantic annotations. In BPD-08: 4th international workshop on business process design.
Governatori, G., & Milosevic, Z. (2006). A formal analysis of a business contract language. International Journal of Cooperative Information Systems, 15(4), 659–685.
Governatori, G., Milosevic, Z., Sadiq, S. (2006). Compliance checking between business processes and business contracts. In P. C. K. Hung (Ed.), 10th International Enterprise Distributed Object Computing Conference (EDOC 2006) (pp. 221–232). IEEE Computing Society. doi:10.1109/EDOC.2006.22.
Holzmann, G. (2003). The spin model checker—Primer and reference manual. Reading: Addison-Wesley.
Howell, R., & Rosier, L. (1989). Problems concerning fairness and temporal logic for conflict-free petri nets. Theoretical Computer Science, 64(3), 305–329.
Liu, Y., Müller, S., & Xu, K. (2007). A static compliance-checking framework for business process models. IBM Systems Journal, 46(2), 335–362.
Lutz, C., & Sattler, U. (2002). A proposal for describing services with DLs. In DL.
Ly, L. T., Rinderle, S., & Dadam, P. (2006). Semantic correctness in adaptive process management systems. In BPM06: Proc. 4th int’l conf. on business process management (pp. 193–208). Vienna, Austria.
Ly, L. T., Rinderle, S., & Dadam, P. (2008). Integration and verification of semantic constraints in adaptive process management systems. Data and Knowledge Engineering, 64(1), 3–23.
OASIS (2007). Web services business process execution language version 2.0. http://www.ibm.com/developerworks/webservices/library/ws-bpel/.
OMG (2008). Business process modeling notation—BPMN 1.1. OMG specification. http://www.bpmn.org/.
Roman, D., & Kifer, M. (2007). Reasoning about the behaviour of semantic web services with concurrent transaction logic. In VLDB (pp. 627–638).
Sadiq, S., Governatori, G., & Namiri, K. (2007). Modelling control objectives for business process compliance. In Proc. 5th international conference on business process management. Brisbane, Australia.
Sergot, M. J., Sadri, F., Kowalski, R. A., Kriwaczek, F., Hammond, P., & Cory, H. (1986). The british nationality act as a logic program. Communications of the ACM, 29(5), 370–386.
van der Aalst, W. M. P., de Beer, H. T., & van Dongen, B. F. (2005). Process mining and verification of properties: An approach based on temporal logic. OTM conferences (1). In R. Meersman, Z. Tari, M. S. Hacid, J. Mylopoulos, B. Pernici, Ö. Babaoglu, et al. (Eds.), Lecture notes in computer science (Vol. 3760, pp. 130–147). New York: Springer.
van der Aalst, W. M. P., & van Hee, K. (2002). Workflow management: Models, methods, and systems (cooperative information systems). Cambridge: MIT. http://www.amazon.ca/exec/obidos/redirect?tag=citeulike04-20&path=ASIN/0262011891.
Vanhatalo, J., Völzer, H., Leymann, F. (2007). Faster and more focused control-flow analysis for business process models though sese decomposition. In B. Krämer, K. Lin, P. Narasimhan (Eds.), 5th international conference on service-oriented computing (ICSOC). Lecture notes in computer science (Vol. 4749, pp. 43–55). Berlin: Springer.
Weber, I., Hoffmann, J., Mendling, J. (2008). Semantic business process validation. In Proceedings of the 3rd international workshop on semantic business process management (SBPM’08).
Winslett, M. (1988). Reasoning about actions using a possible models approach. In AAAI.
zur Muehlen, M., Indulska, M., Kemp, G. (2007). Business process and business rule modeling languages for compliance management: A representational analysis. In Proc. 26th international conference on conceptual modelling - ER2007 - tutorials, posters, panels and industrial contributions. Auckland, New Zealand.
Acknowledgements
This work has in part been funded through NICTA and through the SUPER project. SUPER (FP6- 026850, http://www.ip-super.org) is funded through the European Union’s 6th Framework Programme, within Information Society Technologies (IST) priority. NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Hoffmann, J., Weber, I. & Governatori, G. On compliance checking for clausal constraints in annotated process models. Inf Syst Front 14, 155–177 (2012). https://doi.org/10.1007/s10796-009-9179-7
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10796-009-9179-7