On the Formal Specification of Regulatory Compliance: A Comparative Analysis

  • Amal Elgammal
  • Oktay Turetken
  • Willem-Jan van den Heuvel
  • Mike Papazoglou
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6568)


Today’s business environment demands a high rate of compliance of service-enabled business processes with which enterprises are required to cope. Thus, a comprehensive compliance management framework is required such that compliance management must crosscut all the stages of the complete business process lifecycle, starting from the very early stages of business process design. Formalizing compliance requirements based on a formal foundation of an expressive logical language enables the application of associated verification and analysis tools to ensure the compliance. In this paper, we have conducted a comparative analysis between three languages that can be used as the formal foundation of business process compliance requirements, focusing on design time phase. Two main families of languages have been identified, which are: the temporal and deontic families of logic. In particular, we have considered LTL, CTL and FCL. The comparative analysis is based on the capabilities and limitations of each language and a set of required identified features.


Compliance requirements specifications linear temporal logic Regulatory compliance computational tree logic formal contract language 


  1. 1.
    Sadiq, S., Governatori, G., Naimiri, 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
  2. 2.
    Papazoglou, M., Traverso, P., Dustdar, S., Leymann, F.: Service-Oriented Computing: State of the Art and Research Challenges. Computer 40, 38–45 (2007)CrossRefGoogle Scholar
  3. 3.
    Thao, L., Goser, K., Rinderle-Ma, S., Dadam, P.: Compliance of Semantic Constraints- A Requirements Analysis for Process Management Systems. In: 1st GRCIS 2008 Workshop, France, pp. 41–45 (2008)Google Scholar
  4. 4.
    Governatori, G., Milosevic, Z., Sadiq, S.: Compliance Checking Between Business Processes and Business Contracts. In: 10th EDOC 2006, Hong Kong, pp. 221–232 (2006)Google Scholar
  5. 5.
    Pnueli, A.: The Temporal Logic of Programs. In: 18th IEEE Symposium on Foundations of Computer Science, Providence, pp. 46–57 (1977)Google Scholar
  6. 6.
    Clarke, E., Grumberg, J., Peled, D.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  7. 7.
    COMPAS official web site – Project description,
  8. 8.
    COMPAS Project, D 2.1, State-of-the-Art in the Field of Compliance Languages (2008)Google Scholar
  9. 9.
    COMPAS Project, D 6.1, Use Case, Metrics and Case Study Definition (2008)Google Scholar
  10. 10.
    Vardi, M.: Branching vs. Linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Alur, R., Henzinger, T.: Real-time Logics: Complexity and Expressiveness. Information and Computation 104, 35–77 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Alur, R.: Techniques for Automatic Verification of Real-time Systems. vol. Ph.D. thesis. Stanford University (1991)Google Scholar
  13. 13.
    Governatori, G.: Representing Business Contracts in RuleML. International Journal of Cooperative Information Systems (2005)Google Scholar
  14. 14.
    Elgammal, A., Turetken, O., van den Heuvel, W., Papazoglou, M.: Root-cause analysis of design-time compliance violations on the basis of property patterns. In: Maglio, P.P., Weske, M., Yang, J., Fantinato, M. (eds.) ICSOC 2010. LNCS, vol. 6470, pp. 17–31. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Fenech, S., Okika, J., Pace, G., Ravn, A., Schneider, G.: On the Specification of Full Contracts. In: 6th FESCA 2009 workshop, UK (2009)Google Scholar
  16. 16.
    Liu, Y., Muller, S., Xu, K.: A Static Compliance-Checking Framework for Business Process Models. IBM Systems Journal 46 (2007)Google Scholar
  17. 17.
    Abouzaid, F., Mullins, J.: A Calculus for Generation, Verification, and Refinement of BPEL Specifications. In: 3rd WWV 2007 Workshop, Italy, pp. 43–68 (2007)Google Scholar
  18. 18.
    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
  19. 19.
    Namiri, K., Stojanovic, N.: Pattern-based Design and Validation of Business Process Compliance. In: Chung, S. (ed.) OTM 2007, Part I. LNCS, vol. 4803, pp. 59–76. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  20. 20.
    Yu, J., Manh, T., Han, J., Jin, Y.: 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
  21. 21.
    Giblin, C., Liu, A., Muller, S., Piftzmann, B., Zhou, X.: Regulations Expressed As Logical Models. In: 18th JURIX 2005, Belgium, pp. 37–48 (2005)Google Scholar
  22. 22.
    Schumm, D., Turetken, O., Kokash, N., Elgammal, A., Leymann, F., van den Heuvel, W.: Business process compliance through reusable units of compliant processes. In: Daniel, F., Facca, F.M. (eds.) ICWE 2010. LNCS, vol. 6385, pp. 325–337. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  23. 23.
    Lazovik, A., Aiello, M., Papazoglou, M.: Planning and Monitoring the Execution of Web Services Requests. International Journal on Digital Libraries 6, 235–246 (2006)CrossRefGoogle Scholar
  24. 24.
    Goedertier, S., Vanthienen, J.: Designing Compliant Business Processes with Obligations and Permissions. In: Eder, J., Dustdar, S. (eds.) BPM Workshops 2006. LNCS, vol. 4103, pp. 5–14. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  25. 25.
    Dwyer, M., Avrunin, G., Corbett, J.: Property Specification Patterns for Finite-State Verification. In: 2nd International Workshop on Formal Methods on Software Practice, USA, pp. 7–15 (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Amal Elgammal
    • 1
  • Oktay Turetken
    • 1
  • Willem-Jan van den Heuvel
    • 1
  • Mike Papazoglou
    • 1
  1. 1.European Research Institute in Service Science (ERISS)Tilburg UniversityTilburgThe Netherlands

Personalised recommendations