A static compliance-checking framework for business process models

Modern businesses face a broad number of challenges. While striving to please their customers, they must meet the expectations of their shareholders and remain profitable. Due to globalization and digitization, they are typically confronted with increased and highly dynamic competition. Consequently, investments in information technology (IT) have become a necessary condition to stay competitive and remain in business. As a result, many enterprises have recently shown a growing interest in business process management (BPM), which refers to all activities performed by businesses to model, automate, optimize, monitor, and adopt their businesses processes.^1,2 Thus, there has been an increased acceptance and adoption of business process management systems (BPMSs) in order to efficiently support, execute, and monitor business processes.

The above development has been paralleled by a growing number of regulatory requirements imposed on businesses. Prominent examples in the United States are the Gramm-Leach-Bliley Act,³ the Sarbanes Oxley Act (SOX),⁴ and the USA Patriot Act.⁵ While these United States regulations have very broad coverage, many industry-specific regulations—such as the international Basel II accord,⁶ European Money Laundering Regulation,⁷ and the Law of the People's Republic of China on the People's Bank of China⁸—have been enacted around the globe. Demonstrating compliance with legal requirements and international standards generally requires that affected companies document their business processes. Although many enterprises try to regard such documentation requirements as an opportunity to identify their informal processes and to render their execution more efficient, for large enterprises with thousands of different business processes, this alone represents a considerable challenge.

Enterprises operating in heavily regulated industries, such as financial services, health care, government, and national defense, are likely governed by a large number of regulatory requirements. As these requirements must be implemented and enforced by a multitude of internal business and IT controls, many regulations now recommend the use of respected standards, such as COBIT** (Control Objectives for Information and Related Technologies)⁹ and ITIL** (Information Technology Information Library),¹⁰ for the implementation of an enterprise IT system. These standards consist of well-defined abstract process definitions that can be tailored according to a company's individual needs.

Because of the increasing number of regulations and standards, enterprises need a comprehensive compliance-management approach, as discussed in Abrams et al.¹¹ and Giblin et al.¹² They need to be able to understand the implications of new regulations for their business and its processes. As business processes are increasingly managed using BPMSs, regulatory requirements that necessitate changes to the structure of particular workflows directly impact business process modeling. Thus, whenever a new regulatory requirement is enacted, a company needs to know what its impact is. Three effects are possible: existing business processes must be adapted or removed; new business processes must be introduced; or there is no impact because all business processes are already compliant with the new requirement.

Business processes that are automated through BPMS can be used to implement IT processes and controls, as defined by ITIL or COBIT, and thereby address existing regulations. The impact of new regulatory requirements, however, cannot be assessed using these frameworks. For large enterprises with thousands of business processes deployed on the BPMS and stored in specific repositories, the assessment of which existing process definitions comply with a new regulatory requirement is of utmost importance. In this paper, we describe an approach that allows for the static verification of business process models against a set of formally expressed regulatory requirements, which include constraints on the state and execution order of process activities. We call these formally expressed regulatory requirements compliance rules. Our approach helps a company with the identification of noncompliant business processes before their execution and, in the case of noncompliance, indicates the nature of the problem.

To ensure compliance, the impact of each new regulatory requirement on existing business process models needs to be identified. Although BPM does not help here, our approach indicates which processes are compliant and which are not, hence providing a valuable tool to ensure that new requirements are incorporated into the company's process models. Hence, the benefit of our method is threefold:

1. Through automated verification of a large set of business process models, our approach increases efficiency during deployment and lowers the risk of implementing and activating noncompliant processes.

2. By automating a tedious task that must otherwise be done manually, our method reduces the cost associated with inspecting business process models for compliance.

3. Used as a tool during modeling of new business processes, our approach ensures compliance of new models before their execution and thereby increases the reliability of business operations in general.

We now introduce a case study, which we shall use as a running example throughout this paper. We assume the existence of a Chinese bank called SimpleBank, whose managers want to know whether its business operations conform to a set of relevant compliance rules. For the sake of simplicity, we focus only on SimpleBank's account-opening process, whose process definition is portrayed in Figure 1.

Figure 1

We further assume that at some point SimpleBank is confronted with a set of new compliance rules corresponding to the Rules for Anti-Money Laundering by Financial Institutions,¹³ as published by the People's Bank of China. The two relevant articles are Article 11 and Article 13. Article 11 states in part: “When opening deposit accounts or providing settlement service for individual customers, financial institutions shall verify the customers' IDs and record the names and ID numbers.” Article 13 states: “Financial institutions shall abide by relevant rules and report to the People's Bank of China and/or the State Administration of Foreign Exchange of any large-value transactions detected in the process of providing financial services to customers.

For example, if a customer deposits a large amount of money into his account, the respective transaction must be reported. Compliance with this rule requires an adequate interpretation of large value according to the relevant rules made by the People's Bank of China and the State Administration of Foreign Exchange. For the sake of simplicity, we shall assume this is a parameter that can be flexibly adjusted.

Given the business process in Figure 1 and a set of compliance rules, we demonstrate in this paper how a set of well-defined model transformations enables the use of model-checking technology to verify whether the definition of a business process complies with a set of relevant compliance rules. We call our method compliance checking.

Overall, our compliance-checking method includes six major steps (Figure 2).

Figure 2

In Step 1, we model our business processes using BPEL (Business Process Execution Language).¹⁴ In Step 2, we use the visual BPSL¹⁵ to specify relevant compliance rules. (In the section “Modeling business processes and compliance rules,” we provide both the BPEL process model and the compliance rules formalized in BPSL (Business Property Specification Language) for the SimpleBank case study.) We transform the BPEL process model into a representation using pi-calculus¹⁶ in Step 3.1. Then, in Step 3.2, the pi-calculus is transformed into a finite state machine (FSM). In Step 4, the BPSL compliance rules are transformed into linear temporal logic (LTL).¹⁷ (Steps 3.1, 3.2, and 4 are described in the section “Model transformations.”) Having thus formalized both the business processes and compliance rules, in Step 5 we use model-checking technology¹⁸ to statically verify whether the business processes comply with the imposed regulations. In Step 6, counterexamples (i.e., execution orders of process activities that demonstrate how the compliance rules can be violated) are fed back to the business process layer to demonstrate how the compliance rules have been violated. (Details about the model checking, counterexample tracing, and specific optimization approaches for compliance checking are presented in the sections “Compliance-checking framework and case study results” and “Advanced features of the compliance-checking framework.”)

Before introducing the details of our compliance-checking method, we briefly explain how to model business processes with BPEL and how to specify compliance rules with BPSL.

In the earlier section “Case study,” we introduced a conceptual account-opening process for SimpleBank. Assuming that SimpleBank wants to take advantage of a BPMS to manage this process, the process should be specified with an executable business process modeling language. BPEL is such a language. It is a de facto standard for business application integration and business-to-business processing based on XML (Extensible Markup Language), with a specific focus on Web services. It synthesizes essential aspects of Web Services Flow Language (e.g., support for graph-oriented processes)¹⁹ and XLANG²⁰ (e.g., structural constructs for processes) into one cohesive language to support implementing business processes in a natural manner. Although there is no formal proof that BPEL is powerful enough to express all requirements related to business processes, BPEL has been applied in many real customer cases and enjoys broad industry acceptance. Because of this and its characteristic features, BPEL has been the business process modeling language of choice in our compliance-checking method.

A BPEL process, also called a BPEL program, consists of four major elements: The Variable section defines the data variables used by the process, providing their definitions in terms of Web Services Description Language (WSDL) message types, XML schema simple types, or XML schema elements. The PartnerLinks section defines the different parties that interact with the business. The FaultHandler elements define the activities that must be performed in response to faults during process execution. The rest of the process definition contains the description of normal behavior with BPEL activities, including BasicActivity, StructuredActivity, and ScopeActivity. The BPEL program corresponding to the account-opening process is given in Figure 3. (It shows only the behavior definition section, whose essence is self-explanatory.) The precise semantics of BPEL activities and variables are explained in the section “Model transformations.”

Figure 3 (Part 1 of 2) Figure 3 (Part 2 of 2)

As writing BPEL code manually is relatively cumbersome, process designers often model business processes visually by using a process modeling tool such as IBM WebSphere* Business Integration Modeler (WBI Modeler).²¹ In addition to providing a visual user interface, these tools allow graphical process models to be exported as BPEL programs. We do not focus on the transformation from Unified Modeling Language (UML**) to BPEL here; refer to Mantell²² for more detailed information. (The visual process modeling language provided by WBI Modeler is partially compatible with UML activity-diagram notation.)

Temporal constraints in compliance rules can be specified formally with temporal logic formulas, such as LTL and computation tree logic (CTL). However, for people without a background in formal logic systems, temporal logic systems are rather difficult to understand and use. The purpose of BPSL is to provide a more intuitive formalism to express such properties. Therefore, in our compliance-checking method, we use BPSL for specifying compliance rules.

Four main features of BPSL simplify the specification and understanding of temporal properties:

1. Obscure logical operators are replaced with an intuitive visual notation.

2. Recurring logical patterns from a business or regulatory domain are defined as dedicated operators.

3. Domain-specific templates (e.g., the property patterns²³) can be predefined and reused in BPSL to help increase the efficiency of property specification.

4. BPSL has a direct semantic interpretation in both LTL and CTL.

In this paper, we focus more on LTL because we agree with the argument by Vardi²⁴ that the branching-time formalism of CTL is unintuitive to business analysts and does not support compositional reasoning, as does LTL. The complete syntax, semantics, and notation of BPSL have been described by Xu et al.¹⁵ To ease understanding, in Figure 4 we present the visual BPSL specification of Article 11 and Article 13 of our case study. (The precise semantics of these BPSL properties are explained in the next section.)

Figure 4

In Figure 4, Article 11 is specified by the first two BPSL properties, Article11_part1 and Article11_part2, while Article 13 is specified by the third property, Article13. The rectangles denote Boolean blocks, which may represent the performing of business activities (e.g., AcceptCustomerReq, ObtainCustomerInfo, and VerifyCustomerInfo) or the processing of data (e.g., names and IDs in the ParaList). Annotated arrows are used as temporal operators to define the temporal dependency between the Boolean blocks. For example, the temporal operator ExistWithin [inf] specifies that the next Boolean block must hold within an infinite amount of time after the previous Boolean block holds. The combination of these temporal dependencies thus forms a visual temporal sequence in BPSL. There are simple and compound temporal sequences. A simple temporal sequence specifies a chain of temporal relations among different Boolean blocks or any other BPSL properties (e.g., Article11_part2 and Article13 are simple ones). A compound temporal sequence is a logical combination of simple temporal sequences (e.g., Article11_part1 is a compound temporal sequence that consists of two other simple temporal sequences combined by a logical AND relation).

The BPSL properties in Figure 4 thus possess the following semantics: Before a customer account may be opened, the customer information must first be obtained and verified (Article11_part1): Whenever a customer request for opening a deposit account is received, the customer information must be obtained and the customer name and ID must be later verified. Finally, the customer information must be recorded (Article11_part2). Whenever a customer request for opening a deposit account is received, the deposit must be checked as to its amount. If it is a large-value deposit, it must be reported later.

In previous work, Giblin et al.¹² developed REALM (regulations expressed as logical models), a metamodel and method to formally specify regulations. While REALM, which builds on real-time temporal object logic, is more expressive than BPSL, BPSL supports visual, and thus more intuitive, property specification. As REALM properties cannot be verified by existing model-checking algorithms, we use BPSL as the specification language in our static compliance-checking work.

In this section we introduce the essential model transformations of our compliance-checking method. To reuse existing model-checking algorithms, a series of transformations are performed. We first explain the transformation from BPEL to pi-calculus and the transformation from pi-calculus to FSM (see Steps 3.1 and 3.2 in Figure 2). Then we show how BPSL properties are transformed into LTL formulas (see Step 4 in Figure 2).

Some elementary knowledge of pi-calculus is necessary to understand the content of this section. Before introducing the transformation from BPEL to pi-calculus, we thus present an introduction to pi-calculus.

Pi-calculus
Pi-calculus¹⁶ is a model of concurrent communicating processes that allows complex communication patterns to be modeled. We chose pi-calculus as the formal method to formalize BPEL programs. A detailed discussion justifying this choice can be found in the section “Related work.”

The syntax of Milner's polyadic pi-calculus is as follows:

The simplest entities of pi-calculus are names (denoted by lowercase) and processes (denoted by uppercase). Processes can evolve by performing actions. Syntactically, x < y > denotes an output action that sends name y via x, and x(y) is an input action, which receives a name y via x. Further, is a silent action that expresses unobservable behavior. A sum ₁.P₁ + ₂.P₂ + ··· + _n.P_n denotes a nondeterministic choice of process execution. In the restriction new x P, the scope of name x is bound to P. In the composition P|Q, the processes P and Q can proceed independently and can interact by means of shared names. The replication !P can be thought of as an infinite composition P|P|P|··· of processes. Finally, P represents a process that is guarded by a Boolean expression evaluated by name matching.

Transforming BPEL to pi-calculus
The transformation from BPEL to pi-calculus requires a semantic translation of BPEL. The overall semantics are very complex. Having described the complete transformation from BPEL to pi-calculus in our previous work,²⁵ in this paper we present only the important basic and structured activities.

BPEL contains program variables to which values can be assigned. We adopt the approach proposed by Jacobs and Piessens²⁶ to formally define a programming variable as a storage location. Accordingly, a variable holding a value of x (Variable(x)) is defined by a register (Reg) as follows (the expression =_def is used as a definition symbol):

The above formalization means that the stored value x of the variable can be read from the storage location by using get<x>, and a new value y can be written into the location with put(y).

The basic BPEL activities (Receive, Reply, Invoke, Assign, Empty, and Termination) define how message communication, service invocation, and variable assignment are done in a process model. Link name, Partner name, and Operation name are three elements in the activities of BPEL, and they often appear at the same time. Therefore, here the three elements are denoted as a unified name: â„“. The partner links and data sharing in these BPEL activities are mapped to the input and output prefixes of â„“, get, and put in pi-calculus. In addition, two special names, start and done, are used to indicate common internal communication in a BPEL process.

There are some challenges in the transformation, such as the handling of timeout, synchronizing with links, message correlation, global termination of activity, and fault handling and compensation. We discussed how to solve these problems in another paper.²⁵ Because they are not critical to understanding our compliance-checking method, we do not cover them in this paper. We take Receive(start,â„“,put,done) as an example to explain the semantics of the pi-calculus formalization. The process of Receive contains some free names (e.g., put and done), which are defined as the communication channels of this process. The names start and done are used to start and terminate the activity. The communication among different activities through these two channels thus forms the control flow of the BPEL process. When the Receive process is triggered by its start channel, an input action of â„“(v) is enacted to receive a message through a specific partner link. The output action of put<v> is then enacted to put the received message (i.e., v) into the corresponding variable. Finally, the action done is enacted to indicate the termination of the Receive activity and to trigger another activity in the BPEL process.

Structured activities imply different control relations between the executions of activities in BPEL. We let function fn define a mapping from a pi-calculus process  to a  set of  free names,  where fn(P) indicates the set of all free names contained in process P. Consequently, the semantics of the structured activities Sequence, Switch, While, Pick, and Flow are defined as the following:

In the formalization, {start/done} is a basic name substitution operation, which means that the name done is replaced by start so that an internal interaction can occur between processes P and Q. The formalization of Switch above implies that in the case when several branching conditions hold at the same time, the branches are taken in the order in which they appear, which reflects exactly the semantics of BPEL in its specification. Pick is a nondeterministic choice between process P and Q. Switch, While, Sequence, and Flow are self-explanatory.

Scope is an important concept in BPEL for defining an effective scope of the definition and use of variables, compensation handlers, fault handlers, and other activities. As these BPEL elements can all be associated with a scope, we collect all the free names in a scope with a predefined function, GetNames(s), where s is the scope. Therefore, the restriction operator new can be used to restrict the access to these elements according to their effective scope. The following is the formalization of Scope:

P_i (i = 1, ··· ,n) can be a pi-calculus process of basic activities, structured activities, variables, fault handlers, or compensation handlers. Furthermore, restnames is defined as a free name set:

Because everything is a process in pi-calculus, the semantics of a BPEL process can be formalized as the composition of the above pi processes for all considered BPEL activities:

The application of model checking to verify business process models against compliance rules requires the transformation of business process models into a formalism that can be accepted by a model-checking algorithm. Most current model-checking tools require FSM as an input format. We thus first translate from BPEL to pi-calculus and then from pi-calculus to FSM. Having the processes formalized in pi-calculus as an intermediary formalism provides us the opportunity to apply other verification techniques, such as structural verification (including, for example, deadlock detection) and bisimulation. Furthermore, it also helps the future integration of more practical and efficient model-checking algorithms and tools into our compliance-checking approach. Despite the detour through pi-calculus, the static verification result is the same as if the process models had been transformed into FSM directly.

The transformation from pi-calculus to FSM yields the total behavior of the BPEL process by reducing the pi processes into their corresponding state spaces. Previous works by Ferrari et al.²⁷ and Pistore²⁸ have already shown the approach and feasibility of how to correctly transform finitary pi-calculus processes into the corresponding finite state automata such that a wide range of powerful formal verification techniques can be smoothly reused in the case of mobile processes. In our compliance-checking method, we exploit the results obtained by Ferrari et al.²⁷ to transform a pi process into a corresponding FSM, based on the early operational semantics of pi-calculus. The mapping between the early operational semantics²⁹ of pi-calculus to the state transitions in FSM is presented as a set of transformation rules. For better understanding, each transformation rule is illustrated with an example (see Figure 5).

Figure 5

For each transition triggered by an action in pi-calculus, three attributes are used to record the necessary information of . The action attribute records its port name port(); the paralist attribute records the set of parameters para() passed through the port; and the type attribute is one of the values of input, output, or tau, which indicates that is an input, output, or an invisible action in pi-calculus.

The choice of pi-calculus as the mediation between high-level business process models and very formal models yields several benefits. Specifically, state space generation from pi processes and not directly from the business process model provides us with the following advantages:

• While transforming from the pi process to FSM, two properties can be directly checked: deadlock and redundant activities of the BPEL process. A deadlock exists if there is a pi process that cannot generate its state space before it changes to an empty process (“0”). If a pi process cannot communicate with any other pi process, then there is a redundant activity in the corresponding BPEL process.

• Using pi-calculus and FSM as the formal models of business processes renders the business process verification method independent of a specific model checker. Thus, more practical and efficient model checkers can be integrated into our compliance-checking method.

Though BPSL supports semantic mapping to both LTL and CTL, in this section we explain the mapping from BPSL specifications to LTL formulas based on the three compliance rules given earlier in the section “Compliance rule modeling using BPSL” as examples. Before discussing the mapping from BPSL to LTL, an overview of LTL is given as preliminary information.

LTL
LTL^17,18 is a widely used language for specifying temporal properties of software or hardware designs. In LTL, time is treated as if each moment has just one possible future. Accordingly, linear temporal formulas are interpreted over linear state sequences, and we regard them as describing the behavior of a single computation of a system.

LTL uses formulas of the form Af, where: first, A is the universal path quantifier, which means that f has to be true on all possible paths in the future; and second, f is a path formula (which is true along a specific path) in which the only state subformulas permitted are atomic propositions. More precisely:

If p ∈ AP (AP is a nonempty set of atomic propositions), then p is a path formula.

If f and g are path formulas, then ¬f, f∨g, f∧g, Xf, Ff, Gf, and f U g are path formulas.

The four basic operators of X, F, G, and U are explained informally as follows:

• X (“next time”): a formula (f) is true in the second state of the path.

• F (“eventually”): a formula (f) will be true at some future state on the path.

• G (“always”): a formula (f) is true at every state on the path.

• U (“until”): there is a state on the path where the second formula (g) is true, and at every successive state on the path the first formula (f) is true.

Take the formula G (AcceptCustomerReq → F VerifyCustomerId) as an example. This formula is true in a computation precisely if every state in the computation in which AcceptCustomerReq holds is followed by some state in the future in which VerifyCustomerId holds. Here, AcceptCustomerReq and VerifyCustomerId represent atomic propositions.

Mapping from BPSL to LTL
Referring to Figure 4, we start with Article11_part2. As explained, Article11_part2 (and Article13) is a simple temporal sequence that specifies the temporal relation among a sequence of Boolean blocks or other BPSL properties along paths in which time advances monotonically. The name of each Boolean block in Article11_part2 represents a business activity being performed and the data associated with it. For example, the Boolean block AcceptCustomerReq is interpreted as action = AcceptCustomerReq, and the Boolean block of ObtainCustomerInfo with the parameter list (ParaList) of name and ID is interpreted as action = ObtainCustomerInfo & ParaList = {name, ID}. Note the diamond symbol under the Boolean block of AcceptCustomerReq. This is a special feature of BPSL named compensation property (cp). A cp specifies that when the Boolean block associated with the cp does not hold, the whole BPSL property is still deemed to be correct if cp holds. For this example, the diamond stands for a shortcut to the cp being True. It specifies that Article11_part2 will be evaluated only when a customer request is accepted (because it is always allowable for AcceptCustomerReq not to hold). The key word Always in the formula of Article11_part2 is a global temporal operator, which has a direct interpretation in LTL as the G operator.

Four types of global temporal operators are supported by BPSL: (Possible) Always, (Possible) Eventually, Repeat, and Never. (Possible) Always is equal to G or AG(EG); (Possible) Eventually is equal to F or AF(EF). Repeat and Never mean that the temporal sequence must hold at least n times or that it must not hold at all. Different Boolean blocks are associated with the temporal operators in BPSL. For example, in Figure 6A ExistWithin [inf] specifies that after a customer request is accepted (AcceptCustomerReq), the customer information including the customer name and ID must be obtained. Here inf is the scope parameter for the operator ExistWithin with the value of infinity. Seventeen stereotypes of temporal operators with different semantics are supported in BPSL to specify temporal relations in different situations. While some of the temporal operators have a direct mapping to LTL temporal operators (e.g., Next [3] for XXX and AllWithin [inf] for G), others can be used to express rather complex temporal relations in a simple and compact manner (e.g., the MultiWithinOnEvt [scope] [n] operator specifies the scenario that a Boolean block must hold for n times when a certain event occurs within the scope). Consequently, the final LTL formula corresponding to Article 11_part2 is:

The mapping of this formula to the BPSL notations is shown in Figure 6A.

Figure 6

As to Article13, two new elements need to be introduced. The rectangle TRUE indicates a Boolean block that will always hold. The notation of LargeDeposit, on the other hand, is a post-condition associated with this Boolean block. In BPSL, a post-condition specifies whether it is necessary to further evaluate the rest of the temporal sequence after a Boolean block. For example, in Article13, the post-condition of LargeDeposit specifies that ReportLargeDeposit will (only) be performed after a LargeDeposit is detected (i.e., action = LargeDeposit → F (action = AcceptCustomerReq)). Consequently, the final LTL formula corresponding to Article13 is:

The mapping of this formula to the BPSL notations is shown in Figure 6B.

Finally, Article11_part1 is captured using a compound temporal operator which specifies the logical relation (And) between two simple temporal sequences. Here a new temporal operator Precede appears. The Precede relation (a Precede b) specifies that either b never occurs or that there is no occurrence of b before a holds, that is,

Consequently, the final LTL formula corresponding to Article11_part1 is:

The mapping of this formula to the BPSL notations is shown in Figure 6C. The above mapping follows exactly the semantics of BPSL¹⁵ and thus ensures its correctness.

With FSM and LTL, model-checking technology can be used to verify whether the business process complies with the compliance rules. We briefly explain the basic concepts of model checking and then introduce our compliance-checking framework.

Finally, we present a case study result to illustrate the practical feasibility of this framework.

Model checking¹⁸ is an automatic technique for verifying finite state systems. It has been successfully applied to many systems, including hardware designs and communication protocols. The main idea of model checking is to search the state space of a system model and to verify that it satisfies some user-defined properties (e.g., temporal constraints, such as liveness or safety properties). The advantage of model checking over traditional simulation and testing is that it can exhaustively search the whole state space of a system and can prove the system is indeed error-free. The advantage of model checking over deductive verification is that it requires less expertise and experience in logical reasoning on the part of users. In fact, the procedure of model checking needs little user intervention; it can be performed automatically and results in a final yes or no answer.

Model checking generally includes three steps:

1. Transforming the target system that is to be checked into a formal system model—In our case, the target is the business process model expressed in BPEL, and the formal model we chose is pi-calculus.^16,29 The total behavior of the business process can thus be obtained in an FSM expressing the operational semantics of pi-calculus.

2. Specifying the properties that the formal system model is expected to satisfy—LTL is often used to capture such specifications. As writing correct statements in temporal logic is relatively difficult, for our compliance-checking method, we developed BPSL, a visual property specification language, to formally express such properties. BPSL properties are then automatically translated into LTL formulas.

3. Performing the verification of the formal system model against desired properties with model-checking algorithms—The generated result indicates whether the system satisfies the properties. Our compliance-checking framework, Open Process AnaLyzer (OPAL), integrates the binary decision diagram (BDD)-based symbolic model-checking algorithm implemented in NuSMV2.³⁰ The validity and effectiveness of the algorithm has already been proven from both the academic and industrial sides. In addition, OPAL also provides a counterexample tracing capability for business process models and offers its own optimization approach for compliance checking.

Figure 7 is an overview of the OPAL toolkit, our implementation of the compliance-checking framework. While OPAL supports compliance checking of different business process models against compliance rules, the OPAL framework is independent of a specific business-process modeling approach and model-checking method. OPAL offers an open framework to integrate different business-process modeling tools (e.g., WBI Modeler) and model-checking engines (e.g., NuSMV2³⁰ and Rule Base³¹) by means of the process-model-to-pi transformer and the model-checker adapter, respectively. The component-process-model-to-pi transformer generates the pi processes for different business process models. Compliance rules are specified in the BPSL editor. Because the elements in a compliance rule are closely related to the business process model, there is a graphical user interface (GUI) adapter between the BPSL editor and the process modeling tool. For example, some activity elements can be directly dragged into the BPSL editor from the process modeling tool through the respective adapter.

Figure 7

As introduced earlier, we use pi-calculus as the method to formalize business process models, and LTL is used to specify temporal properties. The details of the BPSL-to-LTL transformer, the process model-to-pi transformer, and pi-to-FSM transformer were introduced earlier. The model-checker adapter is used to integrate existing model-checking engines, such as NuSMV2 and Rule Base, with OPAL. The framework uses the counterexample tracer to trace counterexamples in the business process model. Further, compliance checking results can be generated as compliance reports using the compliance-checking reporting module.

Because this framework is intended for use by business people for business-process model checking, two aspects must be addressed. The first aspect is the understandability of the checking results. For example, if a business process model does not comply with a compliance rule, business people require help to position error points in the process model. The counterexample tracer can help solve this problem. The other aspect is how to ensure an acceptable performance of the compliance-checking method. If a business process model is very complex, optimization helps improve the performance of compliance checking. These important OPAL features are discussed later.

Recall the SimpleBank account-opening process that was described in the introduction. It has been used as a running example throughout the paper to illustrate our compliance-checking method. We have applied OPAL to check the compliance of the account-opening process in Figure 3 against the compliance rules defined in Figure 4. As explained in the section “Model transformations,” the account-opening process was automatically transformed to pi-calculus and further into an FSM with the help of OPAL. Likewise, the regulatory requirements of Article 11 and Article 13 were formalized as compliance rules using the OPAL BPSL modeler, and were then automatically transformed into LTL.

OPAL was developed as a plug-in for the Eclipse** platform, which allows for the integration with different business process modelers, such as WBI Modeler and other Eclipse-based BPEL editors.³² We tested our case study using OPAL on a Microsoft Windows** platform with an Intel** Pentium** 4 processor, 3.0 GHz, and 2.5 GB random access memory (RAM), and obtained the following results: OPAL took 0.056 seconds to transform the account-opening process expressed in BPEL into pi expressions, as introduced in the section “Model transformations.” The time consumed for transforming the pi-calculus formalization into its corresponding FSM was 49.959 seconds. The final FSM contained 11,832 (i.e., 2^13.5304) reachable states out of 535,840 (i.e., 2^19.0314) states after OPAL applied its opimization by means of sequentialization of interleaving actions to compact the FSM (introduced later in the section “Sequentialization of interleaving actions”). The checking of the three compliance rules in Figure 4 consumed 121.0 seconds of CPU time. This also included an additional 21.0 seconds to generate the needed counterexamples for the violated compliance rules. The peak memory use was 71.960 MB.

As the final compliance-checking results showed, the account-opening process complies with the two compliance rules Article11_part1 and Article13. However, it does not comply with the compliance rule Article11_part2. The counterexample for Article11_part2 contains the state trace of 54 states, which shows there is a possible execution path in the account-opening business process in Figure 1 in which the customer information was already recorded in the banking system before it was verified for correctness.

As we have explained so far, OPAL is capable of automatically checking the compliance of our account-opening process model against the three compliance rules in the example. Thus, OPAL users realize that the current account-opening process is noncompliant before deployment, which helps increase deployment efficiency and lowers the risk of installing noncompliant processes.

Our experience with OPAL has shown that our current implementation can handle a state space with 10⁶ reachable states out of 10⁸ total states within 15 minutes.

Two important features of the framework, counterexample tracing and performance optimization, are addressed in this section.

If a regulation rule is not satisfied by a business process model, normally a counterexample would be generated only in the corresponding FSM of the process model because the model-checking algorithm is executed based on FSM. However, for business people, a counterexample based on an FSM is meaningless. Hence, we must provide a mechanism to trace the counterexample back to the business process model. We have developed such a mechanism for OPAL.

As the previous counterexample in our running example is too large (a state trace of 54 states), we now present a simpler example to explain how the OPAL counterexample tracing mechanism works. The BPEL program of the account-opening process in Figure 3 is simplified to the BPEL program SimpleAC, given in Figure 8A.

This simple BPEL process can be transformed to the pi process shown in Figure 8B by using the BPEL-to-pi transformation rules introduced earlier. (For simplification, some channel names have been shortened, for example, AcceptCustomerReq is abbreviated as ACR.)

Figure 8

In the formalism shown in Figure 8B, allnames represents all free names in AccountOpeningProcess, thus making AccountOpeningProcess a closed system with all its names restricted to itself. The formalization of Variable_acq, Variable_oci, and Variable_vci is done as explained earlier in the section “Model transformations,” where we also introduced how to transform a pi process to an FSM. Accordingly, the pi process can be transformed into the FSM shown in Figure 9 with the help of OPAL.

Figure 9

Figure 9 shows only part of the FSM of the entire SimpleAC Process model, which in total contains 69 states as the transformation result of OPAL. Using OPAL, we may now check the following property, and we are thus informed that the result is wrong.

OPAL visualizes the transformed FSM and the counterexample generated by NuSMV2. The counterexample is indicated by the state transitions in orange lines in Figure 9, showing a possible execution path in SimpleAC Process where the customer information may be verified before it is obtained in the first place.

Because the counterexample in the preceding diagram is given at a state machine level and contains information about many redundant actions, such as start_ac and ack, it is hard for business people to comprehend what the counterexample stands for from a business perspective. Therefore, OPAL provides a counterexample mapping from the FSM to the BPEL process model. Such mapping is implemented by preserving only the actions that have a direct connection with the corresponding BPEL activities (e.g., AcceptCustomerReq, ObtainCustomerInfo, VerifyCustomerInfo) and remove any other redundant information in the counterexample. The mapped counterexample in BPEL is the following:

The basic idea of model checking is to exhaustively search the state space of formal system models to discover potential violations of specific logical constraints that a user specifies. To make model checking more applicable to realistic large-scale models, performance tuning and improvement of model checking is a critical research area. OPAL reuses optimized, state-of-the-art model-checking algorithms and focuses primarily on the business process level with its own optimizations. Specifically, it improves the performance of compliance checking by concentrating on the following two aspects:

1. State space reduction of the business process when transforming it to an FSM—States that do not influence the checking result in the FSM are identified and removed so that the state space of the business process can be decomposed or radically reduced. In OPAL, sequentialization of interleaving actions, explained in the next section, is one of the methods implemented to remove redundant states from the state space.

2. Controlled state-space searching using business bug patterns—Compliance checking can be rendered more efficient by a guided search for bugs in the business process.

Sequentialization of interleaving actions
As we know, concurrency is a major cause of state-space explosion. Accordingly, unnecessary concurrencies in business process models may be eliminated to avoid redundant states. Inspired by the idea of partial order reduction,¹⁸ OPAL tries to remove unnecessary concurrencies in the pi-calculus specification that do not affect the semantics of the corresponding business process. We call this approach sequentialization of interleaving actions. When a business process is formalized in pi-calculus and transformed to an FSM, the state space can thus be made as compact as possible.

To explain the rationale of our approach, we take the formalization of SimpleAC as an example. In our SimpleAC example, there are two parallel activities: ObtainCustomerInfo and VerifyCustomerInfo. It seems reasonable to model the triggering of the two activities in a concurrent form, that is, start_oci|start_vci in the formalism of Sequence, as these two activities are executed independently and in an arbitrary order. However, it is easy to note that start_oci and start_vci play only the role of triggering the execution of two pi processes, but do not affect the execution order of the two activities ObtainCustomerInfo and VerifyCustomerInfo. Consequently, even if start_oci|start_vci are sequentialized as start_oci.start_vci the internal behavior of the two activities (such as the retrieval and assignment of variables by means of Get and Put and the invocation of PartnerLinks â„“) is still interpreted in an interleaving form. To be intuitive, the execution of start_oci and start_vci in either order can result in the same global state in the FSM of SimpleAC. Therefore, we can safely replace this concurrency with a sequence and reduce the redundant states caused by the concurrency. The same situation also holds for the formalism of Flow, where done_oci and done_vci are modeled as done_oci|done_vci.

Thus OPAL avoids unnecessary concurrencies in the formalization of a business process model when transforming it into an FSM. Typical sequentializations are implemented in OPAL, including the formalism of the Fork nodes, Join nodes, multiple inputs and outputs for an activity in the UML activity diagrams and compatible models, the Flow structure, and multiple incoming and outgoing links for an activity in BPEL models. The sequentialization in the pi-calculus processes does not mean that the corresponding activities in the BPEL process are sequentialized.

As an example, the state-transition diagram of SimpleAC can be simplified. In Figure 10, the states numbered from 62 to 65 and their transitions indicated by orange dashed lines show the part of the FSM that can be reduced by optimization. The optimized FSM is reduced to 43 states. Internal experiments have demonstrated the practical value of state-space reduction using sequentialization of interleaving actions, especially for complex process models with many unnecessary parallelisms.

Figure 10

Guided state searching for business bug patterns
Despite great improvements in the performance of model checking, the exploitation of domain knowledge is crucial to further improve the efficiency of compliance checking. Because model checking is more useful to probe hidden bugs in a system than to prove its correctness, we have developed business bug patterns, that is, a set of antipatterns corresponding to the well-known workflow patterns³³ to represent common behavioral violations in a business process. A guided search mechanism is then implemented to more efficiently search for these business bugs in a business process model.

To explain the main idea of business bug patterns,³⁴ we take the simple sequential pattern between two activities, A and B, as an example. To falsify the semantics that activity A and B are executed in a sequential order, a business bug pattern SequentialBug(A, B) is shown below:

/*After a certain number of steps, a state is reached in the process where B is started while the execution of A does not yet take place.

NoResponse(A, B) = {[*];A.InExecution; A.Exit}  {B.InExecution[= 0]}

/*If A is finished in the process, no B will be executed afterwards.

The semantics of the SequentialBug pattern are formally captured with the IEEE Property Specification Language (PSL).³⁵ Contrary to Sequential(A, B), the sequential bug pattern tries to find that either both A and B start their execution simultaneously or that B is never executed after A is done. The above two aspects can be defined with two more atomic bug patterns, SimultaneousStart(A, B) and NoResponse(A, B), respectively. The symbol ∨ indicates that the SequentialBug pattern holds when either SimultaneousStart or NoResponse is satisfied. Here, the SequentialBug pattern does not necessarily check whether A is possibly executed after B, as this is acceptable (e.g., when B loops back to A).

In the above definition, the form of A.Exit indicates that the execution of activity A is terminated. The execution status (e.g., Start, InExecution, and Exit) can be encoded in the FSM model of the business process according to the actions in the pi-calculus process that has been enacted. Figure 10 shows an example of such a mapping for the Receive activity.

A full reference of all the business bug patterns can be found in our previous work.³⁴

To more efficiently probe the potential existence of such bugs in a business process model, our idea is to always follow a subset of interesting states while traversing the state space. Interesting states are those that can lead to the detection of a targeted business bug pattern within the least number of transitions. More specifically, we define the following:

M(m): the complete state space (universe) of a business process m, with its initial state in which all of the activities are NotStarted;

S(m) = {s(act1),s(act2),…}: A state in M(m) that is encoded as the states of all activities in m, where act_i ∈ m & s(act_i) ∈ {act_i.NotStarted, act_i.Start, act_i.InExecution, act_i.Cancel, act_i.Failed, act_i.Exit};

The distance between two activity states D(s(act)1, s(act)2) is thus defined as the least number of transitions from one state s(act)₁ to another state s(act)₂. For example, if D(act.Start, act.Exit) = 2, it means that at least two steps are needed from state Start to state Exist for action act. Therefore, the distance between two states in the process is defined as the weighted average of D:

D_S(S(m)1, S(m)2) = iD(s(act)li, s(act)2i)/|S(m)|

The interesting states for a given commitment state CS in state set SS are thus:

S(m)_CS = {S(m)|S(m) ∈ SS,S’(m) ∈ SS D_S(S(m), CS)< D_S(S’(m), CS)}

A more detailed reference of our guided searching mechanism and its algorithms can be found in our previous work.³⁴ Our experiments have shown that the guided reasoning of business bug patterns can help improve the performance of compliance checking in OPAL. Table 1 shows a set of experimental results on the compliance checking of the account-opening process in Figure 1, which has a total state space of 8,361 (2^13.0295) reachable states. The guided business bug-searching algorithm has been implemented in OPAL. The test environment was again a Windows platform with an Intel Pentium 4 processor, 3.0 GHz, and 2.5 GB RAM.

The results show that our guided business-bug searching approach can improve the performance of finding potential violations in a business process compared to the original approach. Intuitively speaking, the reason for the improvement is that our approach takes advantage of the pre-identified activity status and always follows the shortest path that may lead to the detection of a targeted bug. Uninteresting state traces are neglected to narrow down the state space that needs to be traversed. Therefore, the guided business-bug searching approach is useful to check the compliance of complex large-scale business processes. However, the approach is not perfect; its merits come at some cost too:

• It can be used only to falsify a business process because it does not ensure the full traversal of the state space of the business process. Because model checking is more useful for finding system bugs than to prove them correct,³⁶ the approach is still valuable for checking compliance of real industrial business designs that are too large for classical model checking to run to completion.

• It is not suitable for application in small-scale business processes. On the one hand, it is totally affordable to have a thorough and precise checking of simple business processes with model checking. On the other hand, the computation of the interesting states in the approach is not negligible for the compliance checking of a simple business process; thereby, giving away the performance advantage of the approach.

With the rapid growth of complexity in existing business applications and their supporting IT infrastructures, ensuring highly secure and reliable business process development is becoming a critical task. In the past few years, there has been a lot of work modeling business processes and developing verification techniques and tools for them. A recent survey was done by Breugel and Koshkina.³⁷ In this section, we identify three aspects pertaining to the compliance checking of business process models. We report on the literature in each area and clarify how our work is different.

Many researchers generally agree that formal models should be used as a basis for complex business-process modeling languages, such as BPEL.³⁸ According to Sid Askary, “It will allow us to not only reason about the current specification and related issues, but also uncover issues that would otherwise go unnoticed.”³⁹ In this context, tremendous focus has been concentrated on Petrinet and pi-calculus. However, this has also led to a long debate on what is the most suitable formal foundation for business process models. Smith supports pi-calculus and argues that “… workflow is just a pi-calculus.”⁴⁰ The design of Web Services composition languages, such as XLANG and BPEL, is also claimed to be based on pi-calculus. Van der Aalst, on the other hand, has appealed that more solid work should be done to prove the effectiveness of pi-calculus in modeling business processes.³⁸ In fact, there has been some previous work on formalizing various business process models with pi-calculus, including UML statechart diagrams,^41,42 UML (2.0) activity diagrams,^43,44 and workflow patterns.⁴⁵ Previous work has also shown that pi-calculus is a suitable formal composition language for software composition and Web service composition.^46–48 In our work, we have formalized BPEL process models with pi-calculus instead of using Petrinets or automata (and their extensions).

We rely on pi-calculus for the following reasons. First, automata and Petrinets are often used to model closed systems, whose behavior is completely determined and controlled by the state of the system. However, pi-calculus, aside from its mobility feature, is designed to model open communicating systems whose behavior is determined by the state of the system and interaction with the behavior of the environment.^29,49 For example, FSM model is under complete control of its transitions, whereas in pi-calculus, all observable actions are under the joint control of the process and its environment. Therefore, one may regard FSM as the processes in pi-calculus with only internal actions.

We favor pi-calculus over BPEL because, although BPEL can be regarded as a fully controllable orchestration of various services, there are also cases when the behavior of a BPEL process (e.g., a service invocation according to the WSDL specification) needs an interactive feedback from the environment of the process (e.g., a dynamically changing service portfolio). For example, when BPEL is used as an abstract service-composition language with the automatic discovery and mapping of the target services for invocation, it becomes critical to consider the communication with the environmental information, such as the available service candidates in the service portfolio and service selections (which can be best modeled by the mobility feature of pi-calculus).

Another advantage of pi-calculus is its mobility and compositionality. Here compositionality means that there is a natural composition operator in pi-calculus to model a system from its subcomponents. This operator does not exist in Petrinets. Therefore, for composing various Web services by BPEL to form a process, it is more natural and beneficial to use a compositional language like pi-calculus instead of FSM or Petrinet, which involve additional operations and computations for the composition.

Pi-calculus is theoretically sound and supports bisimulation analysis and model checking. It enjoys increasing acceptance and tool support in the industry. It has also been used as the formal foundation for business-process modeling languages such as BPEL and XLANG. However, as pointed out by van der Aalst,³⁸ more work needs to be done to provide formal models, verification approaches, and automatic tools for business processes based on pi-calculus. Our work can be regarded as a response to this appeal.

Based on the formal semantics, there has been previous work on the formal verification of BPEL process models. Fu et al.⁵⁰ first translate BPEL processes into (guarded) automata, and LTL model checking can thus be performed with SPIN⁵¹ with an additional transformation from (guarded) automata to Promela (the input language used by the free model checker of SPIN, developed by Bell Laboratories).⁵¹ Besides, Fu et al.⁵⁰ studied the so-called synchronizability and realizability analysis for the composition of Web services. Kovács and Gönczy⁵² also exploit the model checker of SPIN, although the intermediate model between BPEL and Promela is a model of a dataflow network. Foster et al.,⁵³ on the other hand, take the BPEL process and translate it into the form of finite state process calculus and then compile it into a labeled transition system. The formal verification is then performed by the existing labeled-transition-system analyzer tool suite. Ouyang et al.⁵⁴ and Lohmann et al.⁵⁵ both provide a semantic transformation from BPEL to Petrinet. However, whereas Ouyang et al.⁵⁴ focus on the analysis of specific process properties, such as reachability analysis, competing message-consuming activities, and garbage collection of queued messages, Lohmann et al.⁵⁵ focus on the controllability of the process; that is, whether a strategy can be constructed to impose the weak termination property on the corresponding workflow net. Finally, instead of dealing with the BPEL model, Koehler et al.⁵⁶ propose a pattern-based mapping approach to model a general business process. Two typical properties in a process model, reachability and termination, are formulated with the temporal logic of CTL, which can be verified later by existing model checkers.

Our compliance-checking approach differs from these works in two ways:

1. The theoretical foundation is different. We have used a pi-calculus-based approach instead of an automata- or Petri-net-based approach. The benefits of our selection were addressed in the previous subsection.

2. The completeness of the approach is different. We focused on the verification of our formalized BPEL models against specific structural errors. More important, our work involves a more detailed proposal of subjects—including counterexample guiding, performance enhancement, and visualization of temporal logics—which are critical to making the formal verification of business processes practical and usable.

Specifying user-desired properties with logical formulas is an important step in the formal verification of business process models. The intuitiveness and convenience in the property specification thus becomes a key issue in making the formal verification approach more applicable to business analysts, who may not be logical experts. The LTL model checker plug-in in ProM⁵⁷ exploits a textual form of LTL formula directly. The work in Giblin et al.¹² extends a timed propositional temporal logic and is devoted to the specification of regulatory rules in a textual form. REALM¹² provides several easy-to-use features, such as a predefined set of business entity types (e.g., Artifact, Resource, and Principle) and relations (e.g., Do, Input, and Output) whose syntax conforms to a UML profile. Unfortunately, there is still no tool support for the verification of REALM specifications.

On the other hand, visual extension to existing logical languages is an important research direction to help business analysts understand and specify logical formulas intuitively. Related visualization works can be found for commonly used temporal logics, including CTL,⁵⁸ LTL,⁵⁹ and interval temporal logics.⁶⁰ Especially in DecSerFlow,⁶¹ a graphical representation of the so-called Declarative Service Flow Language is proposed, which can be mapped onto LTL and enables the LTL verification of Web-service flow models.

As explained earlier, our OPAL toolkit contains an editor for BPSL to visually specify various regulatory rules. BPSL is different from the preceding works in the following aspects:

• It is a visual specification language which supports the temporal logics of both LTL and CTL. It is also compatible with the IEEE standard, Property Specification Language.³⁵

• It enables the intuitive and convenient specification of regulatory rules by customizing predefined property templates in BPSL. The source of these templates comes from existing work on patterns such as business property specification patterns²³ and business bug patterns.³⁴

We have introduced OPAL, a compliance-checking framework, and related tools, including a static method to check business process models against compliance rules. Compliance-checking tools enable one to quickly assess the compliance of business process models in batch mode. The use of high-level specification languages, such as BPEL (as opposed to pi-calculus or FSMs directly) and BPSL (as opposed to LTL specifications) and the definition of transformations that can be automated into low-level formalisms yields easier, more intuitive, and less error-prone process modeling, thus reducing the risk of implementation errors and noncompliant operations. If noncompliant business process models are discovered, counterexamples can be generated on the level of the business process model. This capability provides a better understanding of the nature of the problem and enables a quicker reaction to address and rectify the noncompliant processes. These capabilities make it possible for business people to use the compliance-checking tool.

Our compliance-checking method builds on classical model-checking technology. After a business process model has been formalized with pi-calculus, it can be transformed into an FSM representation. The intermediate models of pi-calculus and FSM enable our compliance-checking framework to be scalable to both the future emergence of new business-process modeling techniques and the reuse of more powerful model-checking tools. As a matter of fact, although this paper mainly addresses the application of the framework in BPEL processes, our current implementation of the compliance-checking framework (the OPAL toolkit) has also been applied in the verification of WBI process models. As performance is always a critical problem in the area of model checking, we have also proposed the method of sequentialization of interleaving actions to reduce the overall state space. The approach of guided state searching for business bug patterns can further help improve the efficiency of compliance checking. As conducted experiments illustrated, these two optimization approaches can greatly help improve the performance of compliance checking.

We plan to extend the existing compliance-checking method to support the verification of resource and data constraints that are related to business process models. Additionally, we plan to focus on performance optimization. Finally, we intend to apply our compliance-checking method to more real cases to further validate the capabilities and usability of our compliance-checking framework.

The authors in the author list contributed equally to this paper. The ordering of the author list follows the principle of alphabetical ordering according to the first character of family name. We would like to express our sincere thanks to Jun Zhu for his great help in improving this paper.

*Trademark, service mark, or registered trademark of International Business Machines Corporation in the United States, other countries, or both.
**Trademark, service mark, or registered trademark of Information Systems Audit and Control Association, Government Agency of UK, Object Management Group, Inc., The Eclipse Foundation, Microsoft Corporation, or Intel Corporation in the United States, other countries, or both.

Accepted for publication October 24, 2006; Published online May 2, 2007.