Specification, Verification and Explanation of Violation for Data Aware Compliance Rules

  • Ahmed Awad
  • Matthias Weidlich
  • Mathias Weske
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5900)


Compliance checking is becoming an inevitable step in the business processes management life cycle. Languages for expressing compliance requirements should address the fundamental aspects of process modeling, i.e. control flow, data handling, and resources. Most of compliance checking approaches focus on verifying aspects related to control flow. Moreover, giving useful feedback in case of violation is almost neglected. In this paper, we demonstrate how data can be incorporated into the specification of compliance rules. We call these rules data aware. Building upon our previous work, we extend BPMN-Q, a query language we developed, to express these rules as queries and formalize these rules by mapping them into PLTL. In addition, whenever a compliance rule is violated, execution paths causing violations are visualized to the user. To achieve this, temporal logic querying is used.


Compliance Checking Business Process Querying Violation Explanation Temporal Logic Querying 


  1. 1.
    Weske, M.: Business Process Management. Springer, Heidelberg (2007)Google Scholar
  2. 2.
    United States Senate and House of Representatives in Congress: Sarbanes-Oxley Act of 2002. Public Law 107-204 (116 Statute 745) (2002)Google Scholar
  3. 3.
    Kharbili, M.E., de Medeiros, A.K.A., Stein, S., van der Aalst, W.: Business Process Compliance Checking: Current State and Future Challenges. In: MobIS, GI. LNI, vol. P-141, pp. 107–113 (2008)Google Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  5. 5.
    Awad, A., Decker, G., Weske, M.: Efficient compliance checking using bpmn-q and temporal logic. In: Dumas, M., Reichert, M., Shan, M.-C. (eds.) BPM 2008. LNCS, vol. 5240, pp. 326–341. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Awad, A.: BPMN-Q: A Language to Query Business Processes. In: EMISA, GI. LNI, vol. P-119, pp. 115–128 (2007)Google Scholar
  7. 7.
    Zuck, L.: Past Temporal Logic. PhD thesis, Weizmann Intitute, Israel (1986)Google Scholar
  8. 8.
    Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Awad, A., Decker, G., Lohmann, N.: Diagnosing and Repairing Data Anomalies in Process Models. In: 5th International Workshop on Business Process Design. LNBIP. Springer, Heidelberg (to appear, 2009)Google Scholar
  10. 10.
    Küster, J.M., Ryndina, K., Gall, H.: Generation of Business Process Models for Object Life Cycle Compliance. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 165–181. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. 11.
    Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50, 1281–1294 (2008)CrossRefGoogle Scholar
  12. 12.
    Chechik, M., Gurfinkel, A.: TLQSolver: A temporal logic query checker. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 210–214. Springer, Heidelberg (2003)Google Scholar
  13. 13.
    Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: A tool for model exploration. IEEE Trans. Softw. Eng. 29, 898–914 (2003)CrossRefGoogle Scholar
  14. 14.
    Bruns, G., Godefroid, P.: Temporal logic query checking. In: LICS, p. 409. IEEE Computer Society, Los Alamitos (2001)Google Scholar
  15. 15.
    Lu, R., Sadiq, S.W., Governatori, G.: Compliance aware business process design. In: ter Hofstede, A.H.M., Benatallah, B., Paik, H.-Y. (eds.) BPM Workshops 2007. LNCS, vol. 4928, pp. 120–131. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  16. 16.
    Goedertier, S., Vanthienen, J.: Designing Compliant Business Processes from Obligations and Permissions. In: Eder, J., Dustdar, S. (eds.) BPM Workshops 2006. LNCS, vol. 4103, pp. 5–14. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Goedertier, S., Vanthienen, J.: Compliant and flexible business processes with business rules. In: BPMDS. CEUR Workshop Proceedings,, vol. 236 (2006)Google Scholar
  18. 18.
    Milosevic, Z., Sadiq, S.W., Orlowska, M.E.: Translating business contract into compliant business processes. In: EDOC, pp. 211–220. IEEE Computer Society, Los Alamitos (2006)Google Scholar
  19. 19.
    Yu, J., Manh, T.P., Han, J., Jin, Y., Han, Y., Wang, J.: Pattern based property specification and verification for service composition. In: Aberer, K., Peng, Z., Rundensteiner, E.A., Zhang, Y., Li, X. (eds.) WISE 2006. LNCS, vol. 4255, pp. 156–168. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Lui, Y., Müller, S., Xu, K.: A static compliance-checking framework for business process models. IBM Syst. J. 46, 335–362 (2007)CrossRefGoogle Scholar
  21. 21.
    Governatori, G., Milosevic, Z.: Dealing with contract violations: formalism and domain specific language. In: EDOC, pp. 46–57. IEEE Computer Society, Los Alamitos (2005)Google Scholar
  22. 22.
    Governatori, G., Milosevic, Z., Sadiq, S.: Compliance checking between business processes and business contracts. In: EDOC, pp. 221–232. IEEE Computer Society, Los Alamitos (2006)Google Scholar
  23. 23.
    Sadiq, S.W., Governatori, G., Namiri, K.: Modeling control objectives for business process compliance. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 149–164. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  24. 24.
    Ryndina, K., Küster, J.M., Gall, H.C.: Consistency of Business Process Models and Object Life Cycles. In: Kühne, T. (ed.) MoDELS 2006. LNCS, vol. 4364, pp. 80–90. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  25. 25.
    Lu, R., Sadiq, S., Governatori, G.: Measurement of Compliance Distance in Business Processes. Inf. Sys. Manag. 25, 344–355 (2008)CrossRefGoogle Scholar
  26. 26.
    Ghose, A., Koliadis, G.: Auditing business process compliance. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 169–180. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  27. 27.
    Flender, C., Freytag, T.: Visualizing the soundness of workflow nets. In: Algorithms and Tools for Petri Nets (AWPN 2006), University of Hamburg, Germany, Department Informatics Report 267, pp. 47–52 (2006)Google Scholar
  28. 28.
    Schroeder, A., Mayer, P.: Verifying interaction protocol compliance of service orchestrations. In: Bouguettaya, A., Krueger, I., Margaria, T. (eds.) ICSOC 2008. LNCS, vol. 5364, pp. 545–550. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Ahmed Awad
    • 1
  • Matthias Weidlich
    • 1
  • Mathias Weske
    • 1
  1. 1.Hasso-Plattner-InstituteUniversity of PotsdamGermany

Personalised recommendations