Formalizing and appling compliance patterns for business process compliance

Abstract

Today’s enterprises demand a high degree of compliance of business processes to meet diverse regulations and legislations. Several industrial studies have shown that compliance management is a daunting task, and organizations are still struggling and spending billions of dollars annually to ensure and prove their compliance. In this paper, we introduce a comprehensive compliance management framework with a main focus on design-time compliance management as a first step towards a preventive lifetime compliance support. The framework enables the automation of compliance-related activities that are amenable to automation, and therefore can significantly reduce the expenditures spent on compliance. It can help experts to carry out their work more efficiently, cut the time spent on tedious manual activities, and reduce potential human errors. An evident candidate compliance activity for automation is the compliance checking, which can be achieved by utilizing formal reasoning and verification techniques. However, formal languages are well known of their complexity as only versed users in mathematical theories and formal logics are able to use and understand them. However, this is generally not the case with business and compliance practitioners. Therefore, in the heart of the compliance management framework, we introduce the Compliance Request Language (CRL), which is formally grounded on temporal logic and enables the abstract pattern-based specification of compliance requirements. CRL constitutes a series of compliance patterns that spans three structural facets of business processes; control flow, employed resources and temporal perspectives. Furthermore, CRL supports the specification of compensations and non-monotonic requirements, which permit the relaxation of some compliance requirements to handle exceptional situations. An integrated tool suite has been developed as an instantiation artefact, and the validation of the approach is undertaken in several directions, which includes internal validity, controlled experiments, and functional testing.

1 Introduction

In the light of the recent high-profile business scandals and failures, such as Enron and Countrywide Financial, today’s business entities are faced by an ever-growing number of laws and regulations, such as Sarbanes-Oxley [1] and Basel III [2]. These require organizations to audit their business processes and ensure that they meet compliance requirements set forth in laws and regulations. Without explicit business process (BP) definitions and effective internal control structures, organizations may face litigation risks and even criminal penalties. In 2012, banks had to pay exponentially increasing fines as a result of their failure to show their full compliance with anti-money laundering directives [3]. Nine international institutions were sanctioned (e.g. HSBC, Standard Chartered, ING, ABN Amro), where HSBC had the highest rank of 1,920 million dollars of a fine. Executives and analysts of diverse industry sectors identified regulation and compliance as the top business risk [4, 5].

We define compliance as the process of ascertaining the adherence of business processes and applications to relevant compliance requirements, which may emerge from laws, legislation, regulations, standards and code of practices (such as ISO 9001), internal policies, and business partner contracts (such as service level agreements—SLAs). From a structural perspective, compliance requirements may fall into four classes that pertain to the basic structure of business processes, which are [6] as follows: (i) workflow constraints (control-flow requirements), (ii) information usage (data validation and requirements), (iii) employed resources (task allocation and access rights), and (iv) temporal constraints.

With the ultimate objective of having absolute compliance assurances, many organizations implement compliance solutions on an ad hoc and per case basis. These solutions are generally handcrafted for a particular compliance problem, which creates difficulties for reuse and evolution. These solutions usually lack the flexibility needed to rapidly adapt to ever-changing business imperatives, as they usually involve hard-coded implementations across multiple systems. This makes it difficult to verify and ensure continuous guaranteed compliance. Having recognized these problems and their implications for organizations and firms, major enterprise software vendors have developed commercial products that provide a bundled set of compliance solutions (e.g. Oracle GRC Accelerators, SAP BusinessObjects, and GRC IBM OpenPages). However, these commercial products usually suffer from being highly proprietary (vendor lock-in) and technology-specific as they are usually tightly interweaved with pre-existing enterprise systems.

Efficiently addressing these problems represents an emergent business need that fundamentally requires a framework for managing business process compliance. This framework should be sustainable throughout the complete business process life cycle. A preventive focus is essentially required such that compliance is considered from the early stages of the business process design, thus enforcing compliance by design [7], which must further be taken up by compliance monitoring and adaptation of the running process instances. Accordingly, we consider design-time and run-time compliance checking and monitoring to be complementary and indispensable to ensure preventive compliance. This responds to today’s business environment that strives for a pro-active compliance approach; where a violation is avoided and in case it occurs, recovery action(s) should (semi-)automatically take place to mitigate/minimize the impacts of these violations. In that respect, the main focus of this paper is on design-time aspects of BP compliance as a first key step towards a preventive compliance support

It is generally acceptable that compliance requirements should be based on a formal foundation of a logical language to enable automatic reasoning and analysis that assist in verifying and ensuring business process compliance in a sound, complete, and predictable manner. However, it is a well-known phenomenon that the use of formal languages creates difficulties for end-users, particularly in terms of usability and comprehensibility. This problem represents one of the main obstacles for the utilization of sophisticated verification and analysis tools associated with these languages. To surmount such problems, in the heart of the framework, we propose the Compliance Request Language (CRL) for the abstract specification of compliance requirements that is grounded on temporal logic, more specifically linear temporal logic (LTL). CRL incorporates and integrates a series of compliance patterns, which supports shielding the complexity of logical formalizms from business and compliance experts and facilitates their abstract specification. By applying the proposed mapping scheme, formal LTL rules, capturing applicable compliance requirements, can be automatically generated and directly forwarded to associated verification tools (i.e. model checkers [8]) for automated compliance assurance.

The contributions presented in this paper can be summarized as follows:

• We propose a design-time compliance management framework. The heart of the framework is the Compliance Request Language (CRL), which is a visual pattern-based language that is grounded on LTL and encompasses a series of compliance patterns in its core. Compliance patterns are high-level abstractions of frequently used compliance requirements, which help non-technical users to abstractly represent desired properties and constraints. They span three out of four structural classes of business process aspects; control flow, employed resources, and temporal (data/information aspect is left as a future work). As will be shown later in this paper, this enables to address a wide range of compliance requirements in different application domains.

• Furthermore, CRL provides two efficient mechanisms to allow the relaxation of some less-stringent compliance requirements, i.e. non-monotonicity and compensations.

• To investigate the applicability and expressiveness of CRL, we have developed an integrated software tool suite¹ and employed it in two case studies that deal with business processes of companies in two different industry sectors.

The reminder of this paper is organized as follows: Related work is discussed in Sect. 2. Section 3 summarizes the overall approach for design-time compliance management, pinpointing the main focus of this paper. Section 4 introduces the case studies conducted and gives a simplified scenario used as a running example throughout this paper. Section 5 discusses the compliance request language in detail. Section 6 presents the software toolset as a prototypical implementation of CRL and proof- of-concept. The evaluation and the findings of the case studies are discussed in Sect. 7. Conclusions and a set of lessons that are gained from our research and development experience are portrayed in Sect. 8. Finally, ongoing and future work is highlighted in Sect. 9.

2 Related work

In the area of design-time business process compliance management, we discuss the related work in two broad categories; temporal logic approaches and Deontic logic approaches, corresponding to the formal model of compliance requirements. Key work examples from each class are discussed below and compared to the approach proposed in this paper. In addition to this categorization, we also discuss key graph pattern matching approaches that can also be applied in the context of BP compliance.

An abstract compliance management framework is provided in [9] that incorporates the fundamental requirements for a comprehensive lifetime support of compliance constraints. This framework can serve as a reference model for the open research challenges in this area. In this article, we address the research challenges that are related to design-time compliance management and propose solutions to address these issues. The research problems that we consider will be discussed in detail in Sect. 3, pinpointing the main focus of this paper.

2.1 Approaches based on temporal logic

Temporal logic has been successfully utilized in the literature to formalize and reason about the correctness of software and hardware designs and their adherence to desired properties and constraints in diverse application domains.

Proposals based on temporal logic follow either a bottom-up or a top-down verification approach. The core idea underpinning bottom-up approaches is on one side, to use a logical language (e.g. linear temporal logic—LTL, computational tree logic—CTL) to formally represent compliance requirements; and is on the other side, to transform low-level business process specifications (e.g. modelled using BPEL—Business Process Execution Language) to a corresponding formal representation (e.g. a finite state automata, Petri net, or a process algebraic representation). Next, model checking and other verification techniques are utilized to verify the compliance between the two specifications.

For example, in [10], an extension to computational tree logic (CTL) is proposed to capture data-dependent constraints, i.e. CTL-FO+. Next, CTL-FO+ formulas are mapped into pure CTL formulas and NuSMV model checker is utilized to ensure the conformance against BPEL specifications. In [11], real-time temporal object logic is utilized for the formal specification of compliance requirements based on a pre-defined domain ontology. Real-time temporal logic is a powerful logic; however, no verification approach is provided for design-time compliance checking. In [12], UML activity diagrams is considered, and then, PLTL (past LTL) is exploited to capture desired properties and constraints. Similarly, [13] utilizes first-order logic (FOL) to formally capture both workflow systems and desired constraints for the detection of any constraint anomalies.

In top-down temporal logic approaches, business process models are first represented using an abstract high-level language. Compliance requirements and desired properties are formalized using a temporal logic language. Next, model checkers and other verification techniques are also utilized for compliance checking. If the abstract BP model is compliant with the set of compliance rules, a corresponding BP model may be (semi-)automatically synthesized, e.g. as a BPEL or BPMN (Business Process Modelling and Notation) model. For example, [14] employs $\pi$-logic to formally represent compliance requirements. BP models are abstractly modelled using BP-calculus, which is a formal business process modelling language based on $\pi$-calculus. If business and compliance specifications are compliant, an equivalent BPEL program is automatically generated from the abstract BP-calculus model.

Similarly, authors in [15] follow a top-down approach such that LTL is exploited as the formal foundation of compliance requirements. From a set of LTL rules (capturing applicable compliance requirements) and by applying process-mining techniques, process templates are synthesized semi-automatically. Similarly, a business process synthesis approach is proposed in [16] based on temporal business rules.

The framework proposed in this article falls in this category and follows a bottom-up approach. We differentiate our work by the fact that the above approaches assume experienced users who are familiar with formal languages and mathematical theories, which is hardly the case in practice. To overcome the usability concern of formal languages, which represents the main obstacle of the utilization and application of sophisticated formal analysis and verification tools, we introduce a series of high-level (visual) compliance patterns as an intermediate abstract representation to their corresponding formal rules. In addition, none of these approaches addresses three structural classes of compliance requirements in a single unified approach, e.g. in [11] workflow and real-time constraints are supported, in [10] workflow and data requirements are addressed. Moreover, compensations and non-monotonic requirements, which enable the handling of exceptional situations, are also not addressed in these works. Additionally, we consider Business Process Execution Language (BPEL), which is the standard language for the specification of executable and abstract business processes.

2.1.1 Graphical/pattern-based approaches

To address the usability concern of temporal logic, several research efforts propose pattern-based and/or graphical languages to model desired properties and constraints (e.g. [17, 18] and [19]). Authors in [18] propose the BPMN-Q language, which extends BPMN to graphically represent compliance requirements analogously to the way business processes are modelled in BPMN. BPMN-Q is then mapped into past LTL (PLTL) and a model checking approach is utilized. Similarly, Extended Process Pattern Specification Language (EPPSL) is proposed in [20] focusing on quality constraints.

The study in [21] utilizes Dwyer’s property specification patterns [22] for the verification of service compositions and introduces the logical compositions of these patterns via Boolean operators. The CHARMY framework is proposed in [23] for modelling and verifying designs in UML. CHARMY uses Property Sequence Chart (PSC) as a visual scenario-based language for representing required properties and constraints, which is then mapped into LTL formulas.

In [24], a compliance checking approach is proposed that utilizes a set of Petri net patterns. The compliance checking is performed by means of aligning these patterns with event logs of completed business process executions. This approach focuses mainly on offline business process monitoring of completed business process instances. The same path is adopted in [25] focusing on cloud-based business processes for the purpose of compliance certification, where a number of Petri net patterns are introduced. In [26], Petri net is used focusing on information flow analysis of business process models.

The approach we propose in this paper is closely related to the efforts discussed above. However, our work introduces a wider set of compliance patterns coupled with a graphical notation to enhance its usability. Besides, only workflow and data requirements classes are considered in the above approaches. We also consider design-time compliance checking as first key step towards preventive compliance support. Furthermore, non-monotonicity is not addressed in any of these works. Compensations is only addressed in [17].

DECLARE [27] and ConDec [28] are graphical pattern constraint languages for the declarative specification of workflow systems to improve their flexibility and to enable the management of dynamic processes. DECLARE and ConDec are translated into LTL and are built on the concept of workflow patterns.

While we share the same interest of using a high-level pattern-based language for constraint specification, the approach we propose in this paper considers the BPEL standard. Furthermore, the language we propose (CRL) incorporates a wider range of compliance patterns that supports the employed resources and temporal facets of business process specifications.

The specification and verification of temporal constraints is an important aspect in various application domains, e.g. real-time embedded systems. Studies in [29, 30] and [31] extend Dwyer’s property specification patterns [22] with real-time related patterns. For example, in [29], five real-time patterns are proposed based on an analysis performed on real-time requirements emerging from real-time embedded systems. The timed pattern class as one of the integral parts of the language (CRL) introduced in this paper supports a wider range of timed constraints. Furthermore, these studies only focus on the temporal aspect, and no support is provided for non-monotonic requirements and compensations.

2.1.2 Resource allocation approaches

The modelling and verification of task allocation and authorization constraints have also gained significant interest, particularly in the information systems security field. Task allocation and authorization constraints represent one of the four structural aspects of compliance requirements. Some studies in this area merely focus on the modelling and visualization of authorization constraints inside business process models, without offering a means for their verification. Works in [32] and [33] fall into this category. Wolter et al. [32] propose extensions to BPMN notations to enable the modelling and visualization of task-based authorization constraints.

Our approach is distinguished by having a rigorous verification method to reason about compliance requirement violations. We also agree with the argument in [7] that business and compliance specifications are to be handled separately if we aim to automatically verify their compliance. This is mainly because business and compliance specifications have different objectives (business perspective vs. ownership and governance perspectives), nature (procedural vs. declarative), and lifecycles and may conflict with each other resulting in a highly complicated BP models. Therefore, it should be possible for any of these specifications to be treated independently. However, it is also necessary for these two specifications to be aligned, and their interconnections are established and maintained carefully. This can be possible by having a close collaboration between compliance experts and business process designers, which could be effectively supported by tools that enable sharing and aligning concepts and constructs that are common to both specifications.

In this context, our current work² focuses on the development of a compliance management knowledge base (CMKB) that incorporates and interrelates a set of ontologies capturing various perspectives of the compliance and business spheres. This will further facilitate the communication between different stakeholders with diverse backgrounds, as it will also be possible to annotate business process models with related compliance requirements and visualize them in a unified platform. For the purpose of the main objective of this article, i.e. automating the verification of business process models against applicable compliance requirement in a user-friendly manner, we assume that compliance and business specifications exist independently yet be aligned carefully.

2.2 Approaches based on deontic logic

Deontic logic is also common in specifying compliance constraints, especially in the context of business partner contracts, e.g. SLAs. Key works include [6, 7] and [34]. The study in [34] provides the foundations of the FCL (formal contract language) focusing on business partner contracts. Compliance between business and compliance specifications can be verified based on the idealness notion [34]. In [7], FCL is used to express different types of requirements emerging from laws and regulations. FCL could express compliance requirements in the four compliance structural classes. FCL also supports the specification and verification of non-monotonic requirements.

In [35], an extension is proposed to FCL to incorporate real-time compliance dimension, i.e. temporalized violation logic. LKIF rule language [36] is extended with defeasible logic (FCL) in [37] for the formal specification of compliance requirements. The work in [38] proposes to extend FCL with the notion of goals (i.e. goal compliance), such that BP models could satisfy at the same time the goals of the organization, and the compliance requirements governing the business. In particular, they extend and combine FCL for modelling contracts and regulatory compliance, and the defeasible BIO (Belief–Intention–Obligation) logic for modelling agents [39]. In [38], first, an abstract BP model is specified and checked for compliance and goals satisfaction, which is followed by the automated generation of corresponding concrete compliant BP model.

The approaches referred above implicitly assume users who are experienced in formal theories and definitions. Furthermore, associated verification techniques are not as mature and heavily experimented as the sophisticated verification and analysis techniques associated with temporal logic

2.3 Graph pattern matching approaches

Designing and re-designing business processes from scratch is a highly complex, time-consuming, and error-prone task [40]. An important challenge is to enable the querying of business process artefacts for reusability purposes. This can be basically achieved through the exploitation of graph matching techniques. Dominant studies in this direction are [40–43], and [44]. Although the motivation underlying many of these approaches is to propose solutions for problems regarding process similarity and process substitution, it has been shown in [41] and [44] that these solutions could also be employed for compliance checking.

BP-QL [41] is a novel query language for querying business processes. It is an abstraction of the BPEL standard that allows users to query business processes visually in a way analogous to how business processes are specified. Compliance requirements are represented as queries in BP-QL, which describe the pattern of activities/dataflow of interest, and then, a graph matching approach is utilized. Similarly, the study in [42] proposes an approach that applies graph-based rules for identifying problems in business process models.

A pattern specification and matching approach is proposed in [43], which is based on the set theory and operations. The approach is generic in the sense that it doesn’t assume a specific modelling language, such that any conceptual model is treated as a graph. The approach only focuses on the specification and matching of structural patterns. The work presented in this article is distinguished by the introduction of a wider range of patterns supporting the specification and verification of control flow, employed resources, and timed compliance constraints. In addition, compliance checking is not considered in [43]; therefore, the approach’s applicability on compliance checking of business process models is unstudied.

Since the main focus of these approaches is not necessarily on compliance management, it is unclear which forms of compliance requirements (i.e. regarding control flow, data validation, employed resources, and real time) are supported. In addition, their support for the two compliance-related concepts—non-monotonicity and compensations are inherently not considered.

2.4 Summary and evaluation of related-work approaches

Table 1 presents a summary of the comparison between the key approaches that are discussed in the sections above. ‘Comp. req. abstract specification’ column in Table 1 contains the abstract/visual language used to represent compliance requirements (if any). ‘Structural BP support’ column indicates which BP structural facet the approach supports, i.e. control flow, data, employed resources, and/or temporal. ‘Non-Mon.’ column indicates if the approach provides a support to the handling of non-monotonic requirements. ‘?’ in table indicates that it is unclear if the approach supports the relevant criteria.

Table 1 Summary and evaluation of related work

3 Overview of the design-time business process compliance management

Figure 1 depicts an overview of the key practices and components of our design-time business process compliance management approach, and highlights the parts that outline the scope of this paper. The approach depicted in the figure is a concretized and detailed version of the generic approach that we previously introduced in [45].

Fig. 1

Design-time business process compliance management approach

There are two primary abstract roles involved in this approach: (i) a business expert, who is responsible for defining and managing business processes in an organization while taking compliance constraints into account, and (ii) a compliance expert, who is responsible for refining, internalizing, specifying, and managing compliance requirements stemming from external and internal sources in close collaboration with the business expert.

The approach encompasses two logical repositories: the business process repository and the compliance requirements repository, which may reside in a shared environment. Process models including service descriptions are defined and maintained in the BP repository, while compliance requirements and all relevant concepts are defined, maintained, and organized in the compliance requirements repository. These repositories foster the reusability of business and compliance specifications. We assume that these two specifications (BPs and compliance requirements) share the same constructs—mainly BP elements residing in the BP repository.

The BP definition (the right-hand side of Fig. 1) involves the specification of process models using the Business Process Execution Language (BPEL). However, as BPEL specifications are not grounded on a formal model, they should be transformed into some formal representation to enable their automated verification and analysis against formally specified compliance rules. The automated mapping of process specifications into a formal representation have been intensively studied in the literature (e.g. [11, 14, 17, 46]). For this transformation, we have adopted and integrated the mapping framework proposed in [46] (and its prototypical implementation [47]). We have specifically chosen to exploit this approach due to its support to handle rich data manipulations via XPath expressions. This allows the analysis and validation of data exchanged as messages between participating services. Following this approach, a BPEL specification is first mapped into an intermediate representation (guarded automata—GA), and then to Promela code—the verification language accepted by SPIN model checker [8] (Part C in Fig. 1). A brief description of this BPEL mapping is presented in Sect. 6.2.

On the other side (left-hand side in Fig. 1), compliance management practices commence with the refinement of compliance constraints originating from various compliance sources into a set of organization-specific compliance requirements (Part A in Fig. 1). This involves not only compliance but also business process domain knowledge. Our work on this part is presented in detail in [48] and [49]. The proposed refinement approach is based on the COSO [50] framework, which is the de facto framework used for establishing efficient internal control systems in organizations. The refinement approach briefly involves the following major steps:

• I. Identification of the objectives and the abstract requirements enforced by compliance sources with which the organization has/agrees on to comply with.

• II. Performing ‘risk assessment’ to identify the risks to the achievement of these objectives/abstract requirements imposed by the identified compliance sources.

• III. Identifying, designing, and implementing ‘controls’ to mitigate the identified risks. Controls are concrete and organization-specific norms to be verified, enforced, or tested in order to ensure that compliance requirements are satisfied.

• IV. Specifying formal compliance rules for those controls that can be formally represented and be used for automated process verification at design time and later phases.

For a more detailed discussion about this refinement methodology and its application on two real-life case studies, we refer the reader to [48] and [49]. To address the fourth step in the refinement methodology, compliance expert may apply and combine compliance patterns using the proposed high-level pattern-based Compliance Request Language (CRL) to render organization-specific compliance requirements (Part B in Fig. 1). This serves as an auxiliary step to represent internalized compliance requirements into formal statements (as LTL formulas for our case). These CRL expressions are then automatically transformed into LTL formulas. The verification of business process specifications (Part C in Fig. 1) mainly involves checking formal business process specifications (i.e. Promela code) against formal compliance rules (LTL rules) using the SPIN model checker [8]. SPIN is a popular open source software tool that is intensively used in both academia and industry for the formal verification of large-scale distributed software and hardware systems. The expected inputs to SPIN are as follows: a Promela code that captures the behaviour of the BPEL specification; and a set of LTL rules capturing relevant compliance requirements. The outcome of SPIN is a ‘yes-no’ answer indicating whether each LTL rule is satisfied or violated. In case of violations, the root-cause analysis approach that we have proposed in [51] and [52] may be conducted to analyse and reason about the root causes of design-time compliance violations and provide the user with suggestive guidelines of how to resolve the compliance anomalies. The business experts then alter the process specifications taking these guidelines into consideration, which is followed by the automated re-mapping of the BPEL specification into their formal forms (GA and Promela) and re-verifying against the set of applicable formal compliance rules. This process iterates until all violations are resolved and a statically compliant business process model is produced.

The parts in Fig. 1 enclosed with dotted lines and tagged as ‘Part B’ and ‘Part C’ illustrates the main focus of this paper. In particular, it concerns with the high-level representation of the refined compliance requirements as compliance patterns using CRL, the automatic mapping of CRL expressions into LTL formulas, and automatically verifying the resultant formal rules against BP models for design-time compliance assurance.

4 Case studies

In this section, we introduce two case studies that were conducted within the scope of the EU funded research project (http://www.compas-ict.eu). The case studies were performed in companies operating in different industry sectors and covered processes taking place in the e-business and banking domains. Taking into account the demands for strong regulation compliance schemes, such as Sarbanes-Oxley (SOX), ISO 27000 and sometimes contradictory needs of the different stakeholders, such business environments raise several interesting compliance requirements.

The first case study involved an Internet reseller company that offers products through online systems. The study covered a wide range of BPs, such as order processing, invoicing, cash receipting, and delivery. The second case study covered ‘loan origination and approval’ process that takes place in the banking domain. We use the second case study as a running example throughout this paper. The conducts and the overall findings of both studies are discussed later in Sect. 7.

A simplified model for the loan origination and approval process is depicted in Fig. 2 using BPMN (Business Process Model and Notation). BPMN is used in this section for illustration and presentation purposes; however, we consider BPEL for process specifications. The process flow can be described as follows: Once a customer loan request is received, the credit broker checks customer’s banking privileges status. If privileges are not suspended, the credit broker accesses the customer information and checks whether all loan conditions are satisfied. Next, a loan threshold is calculated, and if the threshold amount is less than 1M Euros, the post-processing clerk checks the credit worthiness of the customer by outsourcing to a credit bureau service. Next, the post-processing clerk initializes the loan form and approves the loan. If the threshold amount is greater than 1M Euros, the supervisor is responsible for performing the same activities instead of the post-processing clerk. Next, the manager evaluates the loan risk, after which she normally signs the loan form and sends the form to the customer to sign. A legal waiting time of 7 days is provided to the customer to send back the signed contract. If a timeout occurs, which means that 7 days have passed and the customer has not sent the signed contract, the relevant loan approval application is closed by the system and the process terminates.

Fig. 2

BPMN model of the loan origination and approval process (simplified)

Table 2 shows an excerpt of the compliance requirements imposed on this loan approval scenario. This table is populated after applying our refined methodology [48, 49] we summarized in Sect. 3 (identified potential risks and other related concepts are omitted for simplicity). The first and second columns of the table allocate a unique reference and an organization-specific interpretation of the requirement, respectively. The third column gives the high-level and abstract compliance requirements as they appear in the compliance sources (such as laws and regulatory documents), from which they originate. Finally, the fourth column refers to the associated compliance sources.

Table 2 An excerpt of the compliance requirements relevant to the case scenario

5 Compliance request language

In [53], we have analysed a wide range of compliance legislations and frameworks, including Sarbanes-Oxley [1], Basel III [2], IFRS [54], FINRA (NASD/SEC) [55], COSO [50], COBIT [56], and OCEG [57], and examined a variety of relevant works on the specification of associated compliance requirements. Based on this analysis and our joint work with two industrial companies (PriceWaterHouseCoopers—PwC, the Netherlands and Thales Services, France), we have iteratively and incrementally identified structural patterns of frequently recurring (compliance) requirements imposed on business processes. Based on the findings of the analysis, we have also identified a set of features a formal language for compliance requirements should possess, which is reported in detail in [58] and [59]. This paper builds on this work by providing an abstract pattern-based language (CRL) that spans over three structural aspects (out of four) of compliance requirements (control flow, employed resources, and temporal) and addresses the usability concern of temporal logic. In addition, it supports the specification and verification of non-monotonic requirements and compensations.

Our analysis also revealed different categorizations of compliance requirements. Requirements can be applicable to controls (checks) that pursue either a preventive or detective approach. Preventive controls help to keep violations from occurring. Examples include authorizations, segregation of duties, and supervisory approval. Detective controls, on the other hand, often produce information regarding an occurred violation to help understand its causes. Examples are management reviews and reconciliations.

With respect to the instruments used for the control, the compliance requirements can also be categorized as process, technical, and physical [57]. Process -related requirements are relevant to the policies and practices concerning the design and execution of BPs. Authorizations, approvals, inspections, segregation of duties applied through business tasks, and other elements are examples of such requirements. Technical requirements involve the use of devices or systems mainly for authentication, encryption, or security purposes. Examples include firewalls and intrusion prevention/detection systems. Physical requirements involve largely the institution of physical means, such as locks, fences, and alarms, to guard critical assets. In identifying the patterns, we focused on preventive-process controls that can be applied for automated design-time verification. The compliance patterns studied in this paper are not applicable or effective for representing the compliance requirements that are applied following a detective approach, or those that are classified as technical or physical.

5.1 CRL meta-model

Figure 3 presents the meta-model of the Compliance Request Language (CRL) represented by UML class diagram. The compliance pattern class is the core element of the language, and each pattern is a sub-type of it. A compliance pattern is a high-level domain-specific template used to represent frequently occurring compliance constraints. The compliance pattern class is sub-divided into four main sub-classes of patterns, namely atomic, resource, composite, and timed.

Fig. 3

Compliance request language meta-model

Atomic patterns deal with occurrence and ordering constraints. Some patterns (those ‘non-shaded’ in Fig. 3) are adopted from Dwyer’s property specification patterns [22]. Resource patterns capture recurring requirements related to task assignments and authorizations, such as segregation of duties.Composite patterns are built up from combinations (nesting) of multiple atomic patterns via Boolean operators to allow for the definition of complex requirements. Timed patterns are used in combination with other compliance patterns to capture time-dependent constraints. We elaborate these types of patterns in Sects. 5.2 through 5.6.

As shown in Fig. 3, an expression mainly comprises compliance patterns (patterns in short) and operands. Expressions can combine multiple (sub-)expressions by using Boolean operators. For example, the expression [(P Precedes Q) And (R Exists)] comprises two sub-expressions, where:

Precedes and Exists are atomic patterns.

$P,\, Q$, and $R$ are operands (that typically represent BP elements).

‘And’ represents the conjunction Boolean operator.

Operands take the form of BP elements (such as activities, events, business objects), their attributes, or conditions on them. For example, the expression ‘CreateOrder LeadsTo ApproveOrder’ has two operands (activities in this case) connected via the LeadsTo atomic pattern. Similar to expressions, operands can also be combined and nested via Boolean operators, e.g.:

An expression built from compliance patterns and operands has a direct mapping to LTL formulas. The formal description of the CRL grammar defining its syntax can be found in [60]. CRL has formally defined operational semantics given by the mapping into LTL formulas [61]. In the following, we describe compliance patterns classes in more detail by exemplifying them using the running scenario introduced in Sect. 4.

5.2 Atomic patterns

Atomic patterns can be used to describe the requirements that involve basic occurrence and ordering of BP elements. They are founded on Dwyer’s property specification patterns [22]. We extended Dwyer’s patterns with four atomic patterns: Else, ElseNext, DirectlyFollowedBy ,and Frees. The Else and ElseNext atomic patterns are used to represent compensations in a way analogous to If-then-else statements. These two patterns are discussed in detail in a separate section (Sect. 5.6). Atomic patterns can be summarized as follows (given $P$ and $Q$ as operands):

Occurrence patterns

• P isAbsent indicates that $P$ should never hold throughout the BP model.

• P isUniversal indicates that $P$ should always hold throughout the BP model.

• P Exists mandates that $P$ must hold at least once within the BP model.

• P BoundedExists (atLeast/Exactly/atMost) $k$ indicates that $P$ must hold at least/exactly/at most $k$ times, respectively, within the BP model.

• P ExistsOften indicates that $P$ must hold more than once within the BP model.

Order patterns

• P Precedes $Q$ indicates that $Q$ must always be preceded by $P$.

• P LeadsTo Q indicates that $P$ must always be followed by $Q$.

• $(P_{1}, \ldots , P_{n})$ ChainPrecedes $(Q_{1}, \ldots , Q_{m})$ indicates that the sequence $Q_{1}, \ldots , Q_{m}$ must be preceded by the sequence of $P_{1}, \ldots , P_{n}$.

• $(P_{1}, \ldots , P_{n})$ ChainLeadsTo $(Q_{1}, \ldots , Q_{m})$ indicates that the sequence $P_{1}, \ldots , P_{n}$ must be followed by the sequence $Q_{1}, \ldots , Q_{m}$.

• P DirectlyFollowedBy Q represents a strict case of the LeadsTo pattern, which requires $P$ to be directly followed by $Q$.

• P Frees Q indicates that the second operand $Q$ has to be true until and including the point where the first operand $P$ first becomes true. For example, a requirement stated as: ‘the status of the loan request should always be pending until the check of the loan risk returns a positive response’, can be specified in CRL as:

  $$\begin{aligned}&Loan.Approved=\hbox {`}Yes\hbox {'} Frees \,Loan.Status\\&=\hbox {`}Pending\hbox {'}. \end{aligned}$$

Atomic patterns exemplified:

Returning back to our running example introduced in Sect. 4, we can represent requirements Req.1 and Req.2 given in Table 2 in CRL as follows:

Regarding Req.1, customer information is collected by conducting a credit bureau service to check the credit worthiness of the customer. In case the loan requester is already a customer of the bank, the credit broker can directly access her personal information from the bank database by invoking ‘request bank information’ activity (as shown in Fig. 2). The pattern expression $R1$ ensures that the customer will be notified immediately after her data has been accessed.

$R2$ uses the ChainPrecedes pattern of Dwyer’s property specification patterns [22], which mandates the sequence of CheckCustomerBankPrivilege and CheckCreditWorthiness to precede EvaluateLoanRisk activity.

5.2.1 From atomic patterns to LTL

LTL [61] is a logic used to formally specify temporal properties of software or hardware designs. In LTL, each state has one possible future and can be represented using linear state sequences, which corresponds to describing the behaviour of a single execution of the system. The formulas take the form Af, where $A$ is a universal path quantifier and $f$ is a path formula. A path formula must contain only atomic propositions as its state sub-formulas. The formation rules of LTL formulas are as follows [61]:

• $\top$ and $\bot$ are formulas (where $\top$ represents tautology and $\bot$ represents contradiction).

• If $P\in AP$, where AP is a non-empty set of atomic propositions, then $P$ is a path formula.

• If $f$ and $g$ are path formulas, then $\lnot f,\, f\vee \,g,\, f \wedge g$, Xf, Ff, Gf, $f U g$, $f W g$, and $f R g$ are path formulas (where ‘$\vee$’ represents ‘or’ and ‘$\Lambda$’ represents ‘and’ logical operators), such that:

  • $G$ (always) indicates that formula $f$ must be true in all the states of the path.

  • X (next time) indicates that the formula $f$ must be true in the next state of the path.

  • F (eventually) indicates that formula $f$ will be true at some state in the future.

  • U (until) indicates that if at some state in the future the second formula $g$ will be true, then, the formula $f$ must be true in all the subsequent states within the path.

  • $W$ (weak until) represents the same semantics as until; however, it is evaluated to true if the second formula $g$ never occurs.

  • R (release) indicates that the second formula $g$ has to be true until and including the point where the first formula $f$ first becomes true; if $f$ never becomes true, $g$ must remain true forever. R (release) is the dual of U (Until).

The mapping scheme from a compliance pattern into LTL enables the automated transformation of CRL expressions into a set of LTL formulas. Table 3 lists the mapping rules to transit from atomic patterns into LTL.

Table 3 Mapping rules from atomic patterns to LTL

Applying the mapping rules given in Table 3 automatically generates the LTL formulas that correspond to the CRL expressions $R1$ and $R2$ given above. The generated LTL formulas of $R1$ and $R2$ are:

5.3 Resource patterns

‘Employed resources’ involves mainly the task allocations, access control, and authorization constraints, and constitutes one of the important structural facets of BP compliance. CRL addresses this dimension through the resource patterns, which typically involve some basic BP concepts, in particular role, user, and task (or BP activity). We assume that tasks are assigned to roles and users perform the tasks through the roles they are assigned to. As shown in Fig. 3, we introduce eight resource patterns that are described in Table 4.

Table 4 Resource pattern descriptions and their mapping rules into LTL

Compliance requirements on employed resources typically require run-time information to be verified. That is, many of such requirements can only be partially verified for compliance at design time. Although the main focus of this paper is on design-time compliance, our underlying motivation is to establish a preventive viewpoint in compliance management. This requires efficient integration of design-time and run-time verification techniques. Accordingly, we found it meaningful to discover and propose patterns that can also be used to specify requirements that may only be checked at the subsequent run-time monitoring phase. In that respect, we mark the rules involving users to be checked and monitored at run-time, since the assignment of specific users to particular roles might not be known until such information is available at run-time. This applies to rules that are generated by using the following resource patterns: SegregatedFrom, USegregatedFrom, BoundedWith, RBoundedWith MU-Segregated, and M-Bounded.

To give an example, consider the mapping rule of the SegregatedFrom pattern as given in Table 4. It is comprised of two rules, i.e.

• $f_1: G\left( {t_{1}.Role\left( R \right) \rightarrow \lnot (t_{2} .Role\left( R \right) )} \right.$: This LTL rule ensures that activities $t_{1}$ and $t_{2}$ are performed by different roles.

• $f_{2}:G\left( {t_{1}. User\left( U\right) \rightarrow \lnot (t_{2}.User\left( U\right) )}\right.$: This LTL ensures that that activities $t_{1}$ and $t_{2}$ are performed by different users.

Rule $f_{1}$ can be verified during design time, while rule $f_{2}$ is generated and marked for subsequent run-time monitoring due to the absence of this specific contextual information during design time.

Resource patterns exemplified

Compliance requirements Req.3 of the running scenario as described in Table 2 represents a resource allocation and authorization constraint that can be represented in CRL as follows:

Req.3 represents the typical segregation of duties compliance requirement. First, $R3.1$ and $R3.2$ ensure that CheckCustomerBankPrivilege and CheckCreditWorthiness activities are assigned to the appropriate personnel. Then, $R3.3$ checks if these two activities are adequately segregated.

Applying the mapping rules given in Table 4, the LTL formulas that correspond to the pattern expressions R3.1 to R3.3 can be automatically generated as follows:

As discussed above, the generated LTL rules $R3.1',\, R3.2'$, and $R3.3'$ are checked during design time, while rule $R3.4'$ is reserved for run-time monitoring.

5.4 Composite patterns

To facilitate the definition of more complex requirements, composite patterns utilize Boolean logical operators (Not, And, Or, Xor, Imply, and Iff) to enable the nesting of multiple patterns. For example, PLeadsTo pattern is an ‘And’ composition of ‘$P$ Precedes $Q$’ And ‘$P$ LeadsTo $Q$’ [21], which indicates that operands $P$ and $Q$ should ‘occur’ and must take place sequentially. Table 5 presents details regarding the CRL composite patterns.

Composite patterns exemplified

Table 5 Mapping rules from composite patterns into LTL

Compliance requirement Req.4 of the running scenario (Table 2) forms a combination of task allocation and composite compliance requirement. It can be represented in CRL as follows:

Compliance requirement Req.4 can be represented using five expressions. $R4.1$ checks if JudgeHighRiskLoan activity takes place. Then, expressions $R4.2,\, R4.3$, and $R4.4$ ascertain that corresponding activities are assigned to the proper roles. Finally, $R4.5$ checks whether JudgeHighRiskLoan is followed by either SignOfficiallyLoanContract or DeclineDueToHighRisk (but not both or neither of them).

Applying the mapping rules given in Tables 3, 4, and 5, the LTL formulas that correspond to the pattern expressions R4.1 to R4.5 can be automatically generated as follows:

5.5 Timed patterns

Time dimension is another key aspect in BP compliance and CRL addresses time-related requirements with eight patterns. Timed patterns should be used in conjunction with other compliance patterns (atomic or composite patterns) forming a ‘timed composite pattern’ expression. However, not every timed pattern can be composed with all compliance patterns. In total, we defined 51 possible combinations, from which a subset is presented in Table 6. For the complete list of combinations, the reader is referred to [60].

Table 6 Mapping rules from combinations of compliance/timed patterns into MTL

Regarding the mapping from timed patterns to corresponding formal statements, LTL lacks the support to such requirements. Various extensions to LTL, such as metrical temporal logic (MTL) and ForSpec temporal logic (FTL) [62] have been proposed in the literature to overcome this limitation.

We have selected MTL for this purpose as MTL extends LTL and thus holds the same semantics (and formation rules). MTL is interpreted over a discrete time domain (over the set of natural numbers $\aleph$). Its temporal operators can be annotated with a real-time expression $I$ that represents a specific time interval. For example, $F_{\ge 5}\emptyset$ represents that in some future state after at least a delay of 5 time units, $\emptyset$ must hold. MTL uses the digital-clock model [63], such that an external, discrete clock progresses at a fixed rate. The granularity of the time can be set by the user.

Similar to the case in resource patterns, many of the rules generated using timed patterns can be fully checked only at run-time as we typically lack the time information at design time. Thus, respective compliance rules are reserved for subsequent run-time compliance monitoring. In some cases, however, the process specification can be enriched with time relevant information. Timeouts that are defined in BPEL models are of such kind. In these cases, verification of such rules at design time is also possible to make sure that the process is specified properly. Req.5 in Table 2 is an example of such a requirement.

Timed patterns exemplified:

Compliance requirement Req.5 given in Table 2 can be represented in CRL as follows:

Req.5 can be represented by two expressions $R5.1$ and $R5.2$, which use the combination of LeadsTo—Within patterns, and Substitutes—ExactlyAfter patterns, respectively. $R5.1$ states that SendSignedLoanContract should always be followed by RecieveCustomerSignedContract within a time interval less than or equal to 7 time units (days in the running scenario) from the start of the first activity. The expression $R5.2$ indicates that CloseLoanContract substitutes the absence of RecieveCustomerSignedContract in the next state after the elapse of 7 days.

By applying the mapping rules given in Tables 3, 5, and 6, the LTL/MTL formulas that correspond to $R5.1$ and $R5.2$ are as follows:

5.6 Capturing compensations with Else and ElseNext patterns

It is important to specify compensations to the violations of certain compliance requirements to handle certain exceptional situations. For example, a requirement may necessitate ‘sending a confirmation message to the customer via e-mail after receiving her application’. A technical failure may prevent this task to be performed and lead to the violation of the requirement. In this case, it may be desirable to define compensation actions (for example, sending a confirmation via SMS) to repair this violation.

The compensation actions can be defined in the form of chains such that each action repairs the violation of its predecessor. This kind of requirements is analogous to if-then-else statements, which impose a prioritization on the order of evaluation of its conditions and actions. We call the action that appears just after the ‘then’ part of the if-then-else statement as the primary action, and every action after each ‘else’ part is called compensation action. If the primary action holds, none of its compensations would take place. Similarly, one and only one action from the primary action and compensation actions should hold. Such a requirement is considered violated if neither of its primary action nor compensation actions holds.

To enable the specification and verification of such requirements in CRL, we use Else and ElseNext atomic patterns in conjunction with LeadsTo and DirectlyFollowedBy atomic patterns (explained in Sect. 5.2). Accordingly, a compensable CRL expression can be formed as:

$$\begin{aligned}&\!\!\!P \left( {LeadsTo\left| {DirectlyFollowedBy)\,P_{1} (Else} \right| ElseNext} \right) \\&\quad P_{2} \ldots (Else|ElseNext)\,P_{n} \end{aligned}$$

Where:

• $P$ is the rule condition.

• $P_{1}$ is the primary action.

• $P_{2}{\ldots }P_{n}$ are the compensation actions.

‘$P\, (LeadsTo{\vert }DirectlyFollowedBy)\,P_{1}$’ captures the ‘if-then’ part of the if-then-else statement. Accordingly, the primary action $P_{1}$ should take place either immediately after P holds (by the DirectlyFollowedBy pattern) or sometime eventually (by the LeadsTo pattern). To capture the ‘else’ part, either ElseNext or Else patterns are used, indicating that a compensation action should take place either immediately after its predecessor action (that fails to compensate the failure) or sometime eventually, respectively.

For example, the requirement Req.6 given in Table 2 can be represented in CRL using LeadsTo, Else, and ElseNext patterns as follows:

During design-time verification, the objective is to ensure that the sequence of the primary action and compensation actions is structurally encoded in the BP model, and there is a transition from one action (primary or compensation) to the next only if the first action could not be completed successfully. This necessitates checking the existence of a decision point after each action that checks whether the action is completed successfully or not. Thus, the mapping rule of a compensable expression for design-time verification can be defined as follows:

Based on this mapping rule, the generated LTL formula from the expression $R6$ is as follows:

In regard to $R6'$, checkCreditWorthinessNotSucceed represents the checking point of the success of the previous activity, i.e. checkCreditWorthiness.Role(‘Supervisor’). Similarly, CreateSuspenseFileNotSucceed is the checking point of the success of CreateSuspenseFile activity. The generated LTL formula captures the static semantics of compensable compliance rules and ensures that it is structurally modelled in the relevant business process model.

5.7 Support for non-monotonic requirements

In real-life scenarios, business processes are also subject to (non-monotonic) requirements that are less strict and can be overridden under certain pre-defined conditions. In these cases, a non-monotonic requirement is still considered satisfied if it is overridden by one of its pre-defined exceptions. We consider CRL’s support to such requirements necessary to enable relaxations and thereby handling exceptional situations. With respect to the strictness of the condition, exceptions has two types [64]:

• A strong exception on the primary rule mandates that whenever the strong exception holds, the primary rule must not hold. For example, for a compliance requirement that demands ‘checking of customer’s bank privileges when a new loan request is received’ can have a strong exception that mandates ‘the check’ to be skipped if the loan requester is a trusted customer (e.g. a customer to the bank for more than 10 years with a good history).

• A weak exception on the primary rule indicates that whenever the weak exception holds, the primary rule may or may not hold. For the same example, where the requirement demands ‘checking of the customer’s bank privileges when a new loan request is received’ can have a weak exception that allows ‘the check’ to be performed as an optional task ‘if the loan amount is less that 1 million Euro and the requester is a trusted customer’.

Following the approach in [64], in CRL, the exceptions are specified as separate rules and linked to the primary rule via labels (i.e. label and exception label constructs in Fig. 3). For example, compliance requirement Req.7 in Table 2 is a non-monotonic requirement and can be represented in CRL as follows:

$R7$ captures the primary rule, and $R_{7}^{1}$ and $R_{7}^{2}$ represent weak and strong exceptions of the primary rule $R7$, respectively. ($R_{7}^{1}$ is put in a single square brackets indicating that it is a weak exception, while $R_{7}^{2}$ is enclosed between double square brackets indicating that it is a strong exception).

The transformation of a non-monotonic expression results in a single LTL formula that combines the primary rule with its exceptions. To simplify the presentation of the mapping, it is illustrated in two steps. First, the non-monotonic expression (the primary rule and its exception rules) is mapped to the LTL rules augmented by exception labels. For example, applying the mapping rules from Table 3 on the expression $R7$, the generated (augmented) LTL rules are as follows:

Second, (augmented) LTL rules are mapped into plain LTL formula following Algorithm 1 (which extends [64]) given below based on the following definitions:

• Assume that $L$ is the set of labels to be used to define corresponding strong and weak exceptions.

• Let $R$ be the label of the primary rule.

• Primary and exception rules constitute a set of rules in the form of $<e:f>$, where $e$ is the label, and $f$ is the body of the rule.

• Let $<e_{1}:f_{1}>$ be an augmented LTL rule. If $e_{2}\rightarrow L$ occurs in the body of $<e_{1}:f_{1}>$, then $e_2$ depends on $e_{1}$. The dependency relation is a transitive relation.

• An augmented LTL rule is Loop Free if and only if no label in $L$ depends on itself. Based on these concepts, Algorithm 1 can be specified as:

Applying Algorithm 1 to $R7$ and its exceptions, step 1 (in Algorithm 1) is skipped since no exceptions have the same label in the exception rules set. By applying step 2 (in Algorithm 1) to replace the weak exception $R_{7}^{1}$ in $R7$, the resulting LTL formula is as follows:

Next, by applying step 3 to replace the strong exception $R_{7}^{2}$ in $R7'$, the resulting LTL formula is as follows:

Steps 4 and 5 of the algorithm are skipped as $R7'$ does not contain more exceptions. The resulting $R7'$ is a pure LTL formula that can be fed into the subsequent design-time verification phase for compliance checking (Sect. 6).

6 Prototypical implementation

An implementation of the proposed design-time compliance management framework is a challenging yet necessary step to help validating the soundness of our approach. We have developed a comprehensive experimental tool suite³ for design-time BP compliance management, implementing the approach described in the above sections. Figure 4 presents three main components of the tool suite and their relationships: Compliance Rule Manager (CRM), Design-time Compliance Verification Manager (DCVM), and Web Service Analysis Tool (WSAT).

Fig. 4

A high-level architectural view of the interacting components of the tool suite

6.1 Compliance Rule Manager (CRM)

The Compliance Rule Manager is a standalone application developed with Microsoft Visual Studio environment (with Visual Studio 2008 SDK) using C# programming language. The upper left-hand side part of Fig. 4 depicts the internal architecture of the Compliance Rule Manager, its components, and their interaction with the business process and compliance repositories. Although conceptually separated, these repositories reside in a shared environment, which is implemented using Oracle database (version.9i).

The CRM comprises two sub-components: Compliance Rule Modeller and Text Template Transformation Toolkit. The Compliance Rule Modeller is a graphical modeller that is used to visually design and create pattern-based expressions of compliance requirements in a drag-and-drop fashion. A screenshot from the Compliance Rule Modeller is shown in Fig. 5. The patterns and the operand types are situated on the left side of the interface on the toolbox. The users drag and drop these constructs on the drawing canvas to build pattern-based expressions. The drawing canvas is divided into swimlanes, each belonging to a refined compliance requirement retrieved from the Compliance Repository. As described in Sect. 5.1, patterns and operands are the main elements that comprise pattern-based expressions. The operands are in the form of business process elements (such as activities, roles, data objects, events), their attributes, or conditions on them.

Fig. 5

A user interface from the compliance rule manager

When an operand type, such as an activity, is selected from the toolbox and dragged onto the swimlane, the Compliance Rule Modeller retrieves the selected type of business process elements available in the Business Process Repository and presents the list to the user for selection (e.g. ‘Select an Activity’ dialogue box shown in Fig. 5).

Figure 5 shows the pattern-based representations of compliance requirements Req.3 and Req.7 of Table 2. Each requirement is represented with one or more pattern-based expressions that capture its semantics and each expression is enclosed in a sub-expression container. For example, the upper swimlane in Fig. 5 graphically represents requirements Req.3 of the running example as described in Table 2 and as represented in expressions R3.1 to R3.3 in Sect. 5.3 in textual form.

The Text Template Transformation Toolkit enables the automatic generation of formal compliance rules (as LTL/MTL formulas) based on the visual pattern-based expressions. This component is implemented using Microsoft Visual Studio 2008—T4. The output is an XML document that contains compliance rules as LTL/MTL formulas and their properties, as well as pattern-based expressions in text formats. The output file is parsed and resulting data is forwarded to the compliance repository together with the references to relevant compliance requirements.

Examples of formal compliance rules generated using the Text Template Transformation Toolkit is shown in Fig. 6. These sample LTL formulas are based on the pattern-based expressions given in Fig. 5 (originated from Req.3 and Req.7 in Table 2). As shown in Fig. 4, generated formal compliance rules are input to the subsequent compliance verification and monitoring phases of the business process compliance management framework.

Fig. 6

Examples of generated compliance rules (in LTL) to be transferred to the compliance repository

6.2 Web Service Analysis Tool (WSAT)

WSAT [47] is an open source tool that implements the BPEL mapping approach proposed in [46]. Accordingly, a BPEL specification is first abstracted to a Guarded Automaton (GA) representing the global sequence of messages exchanged between participating services. GA is a finite state automaton (FSA) augmented with an unbounded queue for incoming messages. Guards can be specified on transitions that are represented as XPath expressions, which enable rich data manipulation and analysis.

Next, GA is mapped to Promela code. Promela (program meta language) is the input language accepted by SPIN model checker [8]. As advocated in [46], having BPEL specifications specified as GA as an intermediate step decouples the BP specification languages and formal verification tools from the translator. In addition, it enables the application of other static analysis techniques, e.g. synchronisability and realisability analysis (we refer the reader to [46] and [47] for further details). To be able to verify resource allocation and authorization constraints, Roles are captured from the ‘PartnerRole’ attribute of the ‘partnerLink’ element in the BPEL specification. Partner links are used to link a BPEL specification to its interacting services. The corresponding partner link is then linked to BPEL basic activities (i.e. Invoke, Receive, and Reply) via the ‘partnerLink’ attribute.

6.3 Design-Time Compliance Verification Manager (DCVM)

DCVM is a web-based environment (http://eriss.uvt.nl/compas), coded in ‘PHP’ (scripting language). It interacts with the Compliance and BP Repositories, which share the same environment running Oracle database (version.9i). As shown in Fig. 4, DCVM comprises two sub-components; firstly, the Verification Handler enables users to formulate compliance verification requests. It retrieves formal compliance rules (in LTL) from the compliance repository and BP specifications encoded in Promela code (WSAT output) and feeds those to SPIN for formal compliance checking. Secondly, the Verification Handler retrieves the checking results from SPIN and reports the possible underlying causes and caveats of detected violations based on the root-cause analysis approach we previously proposed in [51, 52]. SPIN implements exhaustive state search as well as multiple optimized evaluation algorithms, e.g. partial-order reduction, hash-compact searches, which help to solve the typical state explosion problem.

Delivery of results in acceptable time is of utmost important for the proposed automated BP compliance verification approach to be adopted in practice. In order to investigate the performance of the tool suite, we conducted an experiment over the running scenario that we used in this paper. The experiment was conducted on a machine with an Intel Pentium 4 processor 1.7 GHz, and 4 GB RAM, with Microsoft Windows 7 operating system installed. The following results are reported: WSAT took around 49 s on the average to transform the BPEL process of the running scenario into its corresponding Promela code. The checking of the generated LTL rules capturing compliance requirements Req.1–7 presented in Table 2 consumed between 0.035 and 15 s for each of the rules. It is worth noting that 15 s were only consumed in the checking of the compensation compliance requirement R6. The average time of all other rules is 4.6 s.

The peak memory use was 1,026 MB. We believe that the results we received for the scenario are acceptable in terms of time performance. However, considering the complexity of real-life cases with large models and more complex compliance rules, the need for more efficient verification and analysis tools running on more powerful platforms is evident.

With regard to the satisfaction of each of the LTL rules, SPIN indicated the following verification results:

• Compliance requirement Req.1 is violated.

• Compliance requirement Req.2 is satisfied.

• Compliance requirement Req.3 is satisfied.

  • Compliance rule R3.1 is satisfied.

  • Compliance rule R3.2 is satisfied.

  • Compliance rule R3.3 is satisfied.

  • Compliance rule R3.4: could not be checked (details are given below)

• Compliance requirement Req.4 is satisfied.

  • Compliance rule R4.1 is satisfied.

  • Compliance rule R4.2 is satisfied.

  • Compliance rule R4.3 is satisfied.

  • Compliance rule R4.4 is satisfied.

  • Compliance rule R4.5 is satisfied.

• Compliance requirement Req.5:

  • Compliance rule R5.1 is satisfied.

  • Compliance rule R5.2: could not be checked (details are given below)

• Compliance requirement Req.6 is violated.

• Compliance requirement Req.7 is violated.

It was not possible to check the compliance rule R5.2, since the exact time where each BP activity takes place is not modelled in BPEL, which is considered as a limitation. Timeouts, however, can be modelled in BPEL, which enabled us to verify such rules (e.g. R5.1). An extension to BPEL is required to capture these time annotations that capacitate the checking of these time-dependent compliance constraints during design time, which is considered as an open research point. Nevertheless, compliance rule R5.2 and similar time-dependent compliance constraints can be specified using CRL timed patterns and can be reserved for the subsequent run-time monitoring, where time information is available. Analogously, compliance rule R3.4 could not be checked due to the absence of user’s information and the same rule can be reused for run-time verification.

7 Evaluation

The utility of a design artefact must be rigorously demonstrated via well-executed evaluation methods [65]. Observational methods, such as case studies and field studies, allow an in-depth analysis of the artefact and the monitoring of its use in multiple projects within the technical infrastructure of the business environment.

In Sect. 4, we have introduced two case studies that involved processes operating in e-business and banking domains. The case studies involved the specification of the compliance requirements (using the CRL) that are applied on companies’ processes with the main objective of investigating the applicability and expressiveness of compliance patterns that have been introduced as an integral part of the compliance management approach and implemented in the Compliance Rule Manager Software tool. The case studies also allowed us to experiment with the use of the Compliance Rule Manager for building graphical representations of pattern-based expressions and automatically generating corresponding formal compliance rules.

For each case study, the case study team—comprising both compliance and business experts—followed a three-phased approach, which involves the following activities:

• In the first phase, the team analysed the normative specifications (i.e. compliance sources, such as regulations, legislations, domain standards, internal policies) that the companies in the case studies were to comply with and identified high-level compliance requirements imposed on the processes. This phase resulted in 52 high-level requirements for the first case and 7 requirements (some of which are listed in Table 2 as examples) in the second case study.

• In the second phase, grounded on the high-level requirements that were identified and the current design of the processes, the team iteratively refined company-specific interpretation of these requirements in textual forms (examples of these refined/internalized compliance requirements are also given in Table 2). The requirements are also categorized with respect to the control approach (preventive or detective) and control means (process, technical, or physical). The team generated 122 refined requirements in the first and 13 requirements in the second case study.

• The final phase involved the construction of pattern-based expressions (of process requirements that are applicable to preventive approach) through the use of the Compliance Rule Manager Software tool.

Table 7 gives the type and number of compliance requirements covered within the case studies and whether the case study participants were able to express these requirement effectively using patterns introduced in this paper.

Table 7 Categories and numbers of compliance requirements covered in the case studies

As shown in Table 7, the requirements that are classified as process and can be handled using preventive control approaches constituted the majority. These requirements were of particular interest to us, as this type of constraints is the main target for the pattern-based representations and formalization. They involved rules concerning mainly segregation of duties, access rights, condition-based sequencing of activities, and data processing requirements. Under this category of requirements (i.e. preventive process), the case study teams were successful in expressing all segregation-of-duties requirements in both case studies. Requirements concerning access rights / authorizations, activity sequencing were also successfully expressed using the CRL, as it has rich constructs to capture the constraints on the control flow and resource (e.g. role/user assignments) aspects of processes.

Participants were able to express 72 of such requirements (out of 82) using the Compliance Rule Modeller tool, while 10 requirements that were tagged as ‘preventive process’ could not be expressed using available patterns. These requirements mainly involved constraints regarding data processing, e.g. rules that are related to the structure and integrity of the data manipulated within the processes. They typically demanded for sequential numbering of certain business objects, such as orders or invoices.

Despite the limitations discussed above, we can conclude that within the preventive-process category of compliance requirements, the proposed patterns were effective means for expressing compliance requirements of certain concerns. In particular, the concerns that influence the control flow, resource (roles, actors, etc.) and temporal aspects of BP are accurately expressed by patterns.

The process requirements that are controlled following the detective approaches involved mainly management reviews,reconciliations andperformance monitoring. The support by the CRL patterns for the representation and formalization of such requirements is inherently missing, as their verification often requires manual checks to guarantee assurance. Technical requirements were preventive and involved the use of specific techniques for data encryption, data retention and authentication mechanisms. Physical requirements were also preventive in nature that demanded locks or guards to protect against unauthorized access to physical assets. CRL is not designed to address these types of requirements.

In addition, we can compare our approach to major related-work efforts that are discussed in Sect. 2 (and is drawn as a comparison in Table 1). Accordingly, we can conclude that our approach is the only one that satisfies all the criteria considered for the comparison. More specifically:

• The approach presented in this paper incorporates a high-level graphical pattern-based compliance specification language that addresses the usability concern of formal languages.

• The approach is based on a rigour formal foundation of temporal logic (i.e. LTL), which is widely experimented on large-scale systems in various application domains, and incorporates sophisticated verification and analysis tools, such as model checkers.

• The approach considers the Business Process Execution Language (BPEL) standard, which is the de fact standard for web services orchestration.

• The approach supports the specification and verification of three out of four classes of compliance requirements, i.e. control flow, employed resources and time constraints. Support of data constraints is an ongoing work.

• The approach provides efficient solutions to support non-monotonic requirements and compensations, and to reason about root causes of detected compliance violations and guide the user in their resolution.

Furthermore, as part of the EU COMPAS project, we have received positive feedback from COMPAS industrial partners (PricewaterhouseCoopers Netherlands and Thales Services France) with whom we worked closely to validate and evaluate the proposed solutions. The feedback we received was based on their continual meetings with their customers, mainly from the banking domain. Carrying out surveys to investigate the perceived usefulness of the approach is considered one of the future work directions which we highlighted in Sect. 9.

8 Conclusions and lessons learnt

Business processes form the foundation for all organizations, and as such, are impacted by industry regulations. Without explicit BP definitions, effective and expressive compliance frameworks, organizations face litigation risks and even criminal penalties. Compliance management should be one of the integral parts of BPM, such that compliance requirements should be based on a formal foundation of a logical language to enable future reasoning techniques for verifying and ensuring BP compliance starting from the early stages of the business process design.

This paper contributes by a comprehensive design-time compliance management framework that encompasses in its core a high-level and rich pattern-based compliance specification language for facilitating the formal specification of compliance requirements on BPs. The case studies we conducted showed the expressive power of the patterns that we proposed. We believe that using graphical patterns could significantly facilitate the work of the compliance and BP experts by shielding the complexity of the formalizms off from the end-users.

CRL is formally based on temporal logic, i.e. LTL/MTL. We consider CRL as an extensible open language as mapping rules from CRL pattern classes into other formal languages may also be defined. This will enable the specification of some requirements that are not expressible in LTL. Since the expressive power of CRL is limited to the expressive power of LTL, then these requirements are also inexpressible in CRL.

As a proof-of-concept, an integrated tool suite has been developed, where CRL is implemented as a graphical prototype, which enables the specification of compliance requirements intuitively using patterns in a drag-and-drop fashion and automates the process of transforming these definitions into logical formulas. The approach is further evaluated and validated by its application on two case studies performed with two industrial companies.

Managing compliance of business processes requires a multi-faceted approach as the problem involves not only technical aspects rooted in various fields that have to be bridged (such as computer science, business process management, formal methods, and legal studies) but also social and organizational aspects as it highly involves knowledge work. No matter how sophisticated the offered solutions and the underlying technologies are, BP compliance management cannot be fully automated. Having efficient techniques and solutions in place can only facilitate and improve the quality of the work involved.

As also shown by the case studies we conducted, the automated verification and monitoring of compliance is possible only for a certain segment of requirements. Several technical and process- related requirements necessitate checks and controls that have to be performed manually by compliance experts.

Automated tools and techniques should also allow for flexible solutions and human intervention to cope with the non-monotonicity of real life with frequent exceptions. Besides, wide adoption by the industry is only possible if the automated techniques and solutions allow compliance to be managed (cost) effectively. In addition, such solutions should not only provide plain verification results but also give insight into the root causes of compliance violations and propose alternative solutions as remedies.

9 Future work

Future research and development work is ongoing in several directions to enhance and fully support the comprehensive compliance management framework. Ongoing work focuses on the integration of the design-time compliance management approach proposed in this article with the subsequent run-time monitoring and management. In particular, the work presented in this paper will be integrated with the compliance monitoring approach introduced in [66] on the basis of the Compliance Request Language. That is, from pattern-based CRL expressions, design-time and run-time formal rules can be automatically generated for both design-time and run-time compliance assurances.

Ongoing work also involves basing the compliance management framework on semantic repositories. This involves building a set of inter-related semantic ontologies (e.g. business process ontology, compliance ontology) using the Ontology Web Language (OWL2.0) standard as part of a central compliance management knowledge base. This will allow us to conduct a set of preliminary structural analysis using the reasoning tools associated with these technologies and ensures the ontological alignment between compliance and business specifications.

To facilitate the communication between different stakeholders, we are working on the interpretation and encoding of the anti-money laundering regulation using the Semantics of Business Vocabulary and Business Rules (SBVR) standard [67]. Future work will include the integration of the resultant SBVR specifications [68] with the compliance management approach presented in this paper to facilitate the compliance refinement process we previously proposed in [48] and [49].

On a more fine-grained perspective, our analysis of LTL with respect to a set of desired features of CRL [59] revealed a number of limitations. In particular, a support for checking the consistency among compliance requirements is required, as conflicts and contradictions may rise between compliance rules, especially when they originate from various compliance sources.

The case studies we conducted investigated the applicability and expressiveness of the compliance patterns that we proposed in this paper. Our future work should also consider experiments to explore their perceived usefulness and efficiency, possibly through application of some prominent technology adoption models. The validation of the proposed approach will be further intensified by its application on various case studies on prospective users of the patterns and developed tool suite.