We propose a framework grounded in Constraint Logic Programming for representing and reasoning about business processes from both the workflow and data perspective. In particular, our goal is twofold: (1) define a logical language and a formal semantics for process models where data object manipulation and interactions with an underlying database are explicitly represented; (2) provide an effective inference mechanism that supports the combination of reasoning services dealing with process behavior and data properties. To this end we define a rule-based process representation coping with a relevant fragment of the popular BPMN modeling notation, extended with annotations that model data manipulation. The behavioral semantics of a process is defined as a state transition system by following an approach similar to the Fluent Calculus, and allows us to specify state change in terms of preconditions and effects of the enactment of activities. Our framework provides a wide range of reasoning services, which can be performed by using standard Constraint Logic Programming inference engines.
The penetration of Business Process (BP) Management solutions into production
realities is constantly growing, due to its potential for an effective support to enterprise
actors and business stakeholders along the entire BP life-cycle. In this frame,
modeling languages such as BPMN [
However, standard process-centric approaches focus on the procedural
representation of a BP as a workflow graph that specifies the planned order of operations, while
the interactions of individual operations with the underlying data layer is often left
implicit or abstracted away. Indeed, the automated analysis issue is addressed in the
workflow community mainly from a control flow perspective (see, for instance, the notion
of soundness [
In order to provide an integrated account of the workflow and data modeling, several
approaches have been proposed both in industrial realities (e.g., [
In this paper we propose a logic-based framework for representing and reasoning
about data-aware BP models, where the workflow perspective, specified according to
BPMN, is enriched by annotations defining preconditions and effects of individual
process elements in terms of data objects, used to store information that is read and
modified by the process enactment. We also consider the existence of an underlying database,
which can be queried during the enactment, retrieving values to be used for data object
manipulation. The behavioral semantics of a process is defined as a state transition
system by following an approach derived from the Fluent Calculus [
In this work we do not propose yet another business process modeling language, but we assume a pragmatic perspective aiming at supporting process-related knowledge expressed by means of de-facto standards for BP modeling, like BPMN. To the best of our knowledge, this is one of the first attempts to provide a formal execution semantics for expressive BPMN workflows in the presence of data and arithmetic constraints. Notably, the CLP formalization directly provides an executable semantics, which enables the implementation of analysis and verification tasks relying on established automated reasoning methods and tools. Due to the presence of data, the state space of the modeled systems is potentially infinite and most verification problems are undecidable. However, the symbolic representation of data values by means of constraints achieves the termination of a number of reasoning services in many cases of practical relevance also in the presence of an infinite state space.
The paper is organized as follows. After presenting a motivating scenario and introducing the modeling framework in Section 2, we provide a formal account of the behavioral semantics in Section 3. In Section 4 we show how automated reasoning methods developed in the field of CLP can be directly applied to perform analysis and verification tasks. In Section 5 we present a proof-of-concept prototype, and, finally, in the concluding section we give a critical discussion of our approach, along with directions for future work. 2
A data-aware Business Process Schema (DAPS) is an activity workflow model, where
each task can additionally operate on data objects used to store information that is read
and modified by process enactment. In our approach, data objects are essentially
regarded as variables, and hence at any time during execution there is a single instance
of a given data object that may be read or (over-)written by some activity. We consider
two main types of relationships between activities and data objects. Firstly, the
enactment of an activity may be guarded by a condition involving a number of data objects.
Secondly, the enactment of an activity can modify the value of a data object, hence
producing a new value, possibly related to other data objects’ values by an arithmetic
constraint over the real numbers R. We also consider the presence of a database (DB)
that can be queried during process enactment, hence retrieving values to be used for data
object manipulation. For the scope of this work, we assume that DB cannot be updated
by activity executions. Furthermore, we assume to deal with BPs whose state space,
considering the control flow only, is finite. However, since the data objects can assume
infinitely many values, the state space of the overall system is in general infinite.
For the representation of the workflow-related perspective, we mainly refer to the BPMN
standard [
A DAPS consists of a set of flow elements and relations between them, and it is associated with a unique start event (e.g., s) and a unique end event (e.g., e), which are flow elements that represent the entry point and the exit point, respectively, of the process. An activity is a flow element that represents a unit of work performed within the process. It can be modeled as a task, representing an atomic activity no further decomposable (e.g., choose prod), or as a compound activity, representing the execution of a sub-processes (not exemplified here). The sequencing of flow elements is specified by the sequence flow relation (corresponding to solid arrows), and the branching/merging of the control flow is specified by using three types of gateways: exclusive (XOR, e.g., x1), inclusive (OR, e.g., o1), and parallel (AND, not exemplified here).
The item flow relation (corresponding to dotted arrows) specifies that a flow element uses as input or manipulates as output particular data objects. In our setting, the input and output of a flow element can be enriched by declarative descriptions of preconditions and effects, respectively, formulated in terms of arithmetic constraints, value assignments (denoted by :=), and database queries (following the j symbol). For instance, the task apply coupon requires (precondition) a value of item price greater than 0, while upon its execution (effect), the value of item price is decreased by the amount of coupon. More complex effects can be specified, as in the case of choose prod, where the values assigned to item price and item weight are retrieved by performing the conjunctive database query product price(X ; P); weight(X ;W ). Uppercase letters denote variables, representing values not known at design-time that are introduced during the enactment, e.g., retrieved by database queries or produced after interactions with external systems or users. The values that variables are allowed to assume at run-time can be characterized in terms of arithmetic constraints, as exemplified by the payment effect where, due to the constraint 0 < X amount, the possible values of X after each execution of payment range from 0 to the current value of amount (representing any admissible paid amount). Similarly to activity preconditions, guards can be attached to outgoing sequence flows of inclusive and exclusive gateways, as in the case of o1 and x2. Whenever a guard is not defined, a non-deterministic behavior is assumed.
The depicted BP is started by the user log-in, which triggers the execution of the start event leading to the initialization of the involved data objects. The user can select a number of products, by choosing for each of them a shipment compatible with the item weight and optionally applying a coupon, which decreases the item price. When the amount due exceeds the plafond associated with the user, a selected product cannot be added to the order and it is refused. In order to proceed with the shipment, the full amount due has to be paid, possibly through several subsequent payments. 3
Now we present a formal definition of the behavioral semantics, or enactment, of a
DAPS, by following an approach derived from the Fluent Calculus, a well-known
rulebased calculus for action and change (see [
We will consider CLP programs with constraints over the set R of the real numbers. We will denote variables by upper case letters X1; X2; : : : ; while we will denote constants, predicate and function symbols by lower case letters, a; p; f ; : : : Constraints are inductively defined as follows. An atomic constraint is either a formula of the form p1 p2 or a formula of the form p1 > p2, where p1 and p2 are polynomials with real variables. We will also use the equality ‘=’ and the inequalities ‘ ’ and ‘<’ defined in terms of ‘ ’ and ‘>’ as usual. A constraint is either true, or false, or an atomic constraint, or a conjunction of constraints.
An atom is an atomic formula of the form p(t1; : : : ; tm), where p is a predicate symbol not in f ; >g and t1; : : : ; tm, with m 0, are terms. A literal is either an atom A or a negated atom :A. A goal is a (possibly empty) conjunction of atoms. A constrained goal c ^ G is a conjunction of a constraint c and a goal G. A CLP program is a finite set of rules of the form A c ^ G (to be understood as “A if c and G”), where A is an atom and c ^ G is a constrained goal. Given a rule A c ^ G, A is the head of the rule and c ^ G is the body of the rule. A rule with empty body is called a fact. A term or a formula is ground if no variable occurs in it.
Let TR denote the set of ground terms built from R and from the set of function
symbols in the language. An R-interpretation is an interpretation that: (i) has universe
TR, (ii) assigns to +; ; >; the usual meaning in R, and (iii) is the standard Herbrand
interpretation [
We consider the standard operational semantics of CLP programs based on
resolution extended with constraint solving [
A DAPS is formally represented by a triple hWF; DC; DBSi, where WF is a workflow specification, DC (data constraints) is a specification of the preconditions and effects of activities on data objects, and DBS is a database schema.
The workflow specification WF is a set of ground facts of the form p(a1; : : : ; an), where a1; : : : ; an are constants denoting individual flow elements and p is a predicate symbol representing a BPMN construct (e.g., activity, gateway, sequence flow). For instance, the formal specification of the eProcurement BP in Figure 1 will contain facts such as: bp(eProc; s; e), stating that eProc is a process starting with s and ending with e; task(choose prod), stating that choose prod is an atomic activity within the workflow; exc branch(x2), stating that x2 is an exclusive branch point, i.e., a decision point; seq(choose prod; choose ship; eProc), stating that a sequence flow relation is defined between choose prod and choose ship in eProc.
The data constraints DC specify the way data objects are manipulated during process enactment, by means of the following relations: Precondition: pre(A;C; Proc), which specifies an enabling condition C that the data objects must satisfy to enable the execution of an activity A in the process Proc; Effect: eff(A; E; Proc), which specifies the effect expression E describing the effect on the data objects of executing A in the process Proc; Guard: guard(C; B;Y; Proc), which specifies a conditional sequence flow used to select the set of successors of decision points, where the enabling condition C must hold in order to enable the flow element Y , successor of B in the process Proc. Enabling conditions and effect expressions are formally defined as follows. Let DO denote the set of data objects occurring in the DAPS. An arithmetic expression is an expression constructed from DO, (CLP) variables, real numbers, +, and . A constraint expression is an expression of the form a1 rel a2, where a1, a2 are arithmetic expressions and rel 2 f ; >g (i.e., a constraint expression is an atomic constraint on data objects and CLP variables). A db-query is an atom whose predicate is defined in the database schema DBS. A data update is an expression of the form o := a, where o 2 DO and a is an arithmetic expression. An enabling condition is the conjunction of n 0 constraint expressions. An update condition is either a constraint expression or a db-query. An effect expression is a pair data-updates 8 conds, where data-updates is a sequence of data updates and conds is a conjunction of update conditions.
Returning to the eProcurement example of Section 2, a precondition associated with the payment activity is:
pre(payment; [amount > 0]); eProc) meaning that the task payment can be executed only if the data object amount has a positive value. In the above example and in the sequel, both sequences and conjunctions appearing as predicate arguments are represented using lists. The specification of the effect associated with the choose ship activity is: eff(choose ship; [item price := item price + P] 8
[ship price(S; P); max weight(S;W );W > item weight]; eProc) meaning that the effect of the execution of the task choose ship is that the value of the data object item price is incremented by a quantity P, where P is the price of a shipment type S and the value of item weight is below the maximum weight allowed for S.
The specification of the guard associated with the flow from x2 to refuse item is: guard([amount + item price > plafond];x2; refuse item; eProc) meaning that the control flow can proceed from the gateway x2 to the refuse item task only if the sum of the values of amount and item price exceeds the value of plafond.
The database schema DBS consists of a set of predicate symbols (with arity) representing the relations stored in the database, together with a set of formulas of the form p(X1; : : : ; Xn) ! c, where p is a predicate symbol in the schema and c is a constraint whose variables are among X1; : : : ; Xn, representing integrity constraints (for simplicity we do not consider more complex integrity constraints). A database instance of DBS is a finite set of ground facts p(a1; : : : ; an) that satisfies all formulas in DBS. 3.3
Similarly to the Fluent Calculus, we represent the state of the world as a set of fluents,
i.e., terms denoting atomic properties that hold at a given instant of time. The
execution of a flow element may cause a change of state, i.e., an update of the collection of
fluents associated with it. In particular, a change of state can be determined by the
effects of activities specified by DC. A fluent is represented by an expression of the form
f (a1; : : : ; an), where f is a fluent symbol and a1; : : : ; an are constants or variables. We
take a closed-world interpretation of states, that is, we assume that a fluent F holds in
a state S iff F 2 S. Our set-based representation of states relies on the assumption that
the DAPS is safe, that is, during its enactment there are no concurrent executions of the
same flow element [
We will consider the following three kinds of fluents: – cf(E1; E2; Proc), which means that the flow element E1 has been executed and the successor flow element E2 is waiting for execution, during the enactment of the process Proc (cf stands for control flow); – en(A; Proc), which means that the activity A is being executed during the enactment of the process Proc (en stands for enacting). – val(O;V ), which means that the data object O 2 DO has value V .
The truth value of a fluent or update condition depends on the state where it is evaluated. For this reason we introduce the satisfaction relation holds(C; S), which holds if C is true in the state S, where C is either a fluent or a conjunction of update conditions. 1. holds([ ]; S) 2. holds([CjCs]; S) holds(C; S) ^ holds(Cs; S) 3. holds(p(X1; : : : ; Xn); S) p(X1; : : : ; Xn) for every p declared in DBS 4. holds(F; S) fluent(F) ^ F 2 S 5. holds(val(X ;V ); S) constant(X ) ^ V = X 6. holds(val(X ;V ); S) variable(X ) ^ V = X 7. holds(A1 > A2; S) V1 > V2 ^ holds(val(A1;V1); S) ^ holds(val(A2;V2); S) 8. holds(val(A1 +A2;V ); S) V = V1 +V2 ^holds(val(A1;V1); S)^holds(val(A2;V2); S) Recall that in this paper we assume that the database does not change during process enactment, and hence in Rule 3 the evaluation of the db-query p(X1; : : : ; Xn) does not depend on the state S. Rule 4 has one instance for each kind of fluents, and a particular instance is the following rule for retrieving the value of a data object O in a state S: holds(val(O;V ); S) val(O;V ) 2 S. Rules 5 and 6 express the fact that the value of logical variables and constants is independent of the state. Rules 7 and 8 are needed to define the value of constraint expressions by structural induction. We have omitted the rules for and , which are similar to rules 7 and 8, respectively.
The change of state determined by the execution of an action will be formalized by a relation result(S1; A; S2), which holds if action A can be executed in state S1 leading to state S2. For the definition of result(S1; A; S2), we assume that an instance of the database schema DBS is provided. We also assume that the execution of an activity has a beginning and a completion (although we do not associate a duration with activity execution), while the other flow elements execute instantaneously. Thus, we will consider two kinds of actions: begin(A) which starts the execution of an activity A, and complete(E), which represents the completion of the execution of a flow element E (possibly, an activity). The following auxiliary predicate will be used: update(S1; T;U; S2), which holds if S2 = (S1 T ) [ U , where S1; T;U; and S2 are sets of fluents.
Let us now present some of the rules that define the behavioral semantics of a DAPS. The state change determined by the execution of a task is defined by the following two rules, corresponding to the start and the completion of the task, respectively: result(S1; begin(A); S2) task(A) ^ holds(cf(X ; A; P); S1) ^ pre(A;C; P) ^ holds(C; S1) ^ update(S1; fcf(X ; A; P)g; fen(A; P)g; S2) result(S1; complete(A); S2) task(A) ^ holds(en(A; P); S1) ^ seq(A;Y; P) ^ eff(A; DU 8 C; P) ^ holds(C; S) ^ apply(DU; S1; S0) ^ update(S0; fen(A; P)g; fcf(A;Y; P)g; S2)
The first rule states that the execution of task A is started if the control flow has reached it ( holds(cf(X ; A; P); S1) ) and the enabling conditions associated with it hold in the current state ( pre(A;C; P) ^ holds(C; S1) ). The successor state is obtained by asserting that the process is enacting A ( update(S1; fcf(X ; A; P)g; fen(A; P)g; S2) ). The second rule states that the execution of task A can be completed if the update conditions associated with A hold in the current state ( eff(A; DU 8 C; P) ^ holds(C; S) ). The successor state is obtained by applying the sequence DU of data updates, hence updating the values of the data objects ( apply(DU; S1; S0) ), and moving the control flow to the next flow element Y ( update(S0; fen(A; P)g; fcf(A;Y; P)g; S2) ). The relation apply(DU; S1; S0), meaning that state S0 is obtained from state S1 by performing the sequence DU of data updates is defined as follows: apply([ ]; S; S): apply([DUjDUs]; S; T ) apply(DU; S; S0) ^ apply(DUs; S0; T ) apply(O := A; S; S0) holds(val(A;V ); S) ^ update(S; fval(O; X )g; fval(O;V ); S0g)
The following two rules formalize the state changes determined by the execution of an exclusive branch (with a guard associated with an outgoing flow) and an exclusive merge, respectively. result(S1; complete(B); S2) exc branch(B) ^ holds(cf(X ; B; P); S1) ^ seq(B;Y; P) ^ guard(C; B;Y; P) ^ holds(C; S1) ^ update(S1; fcf(X ; B; P)g; fcf(B;Y; P)g; S2) result(S1; complete(M); S2) exc merge(M) ^ holds(cf(A; M; P); S1) ^ seq(M;Y; P) ^ update(S1; fcf(A; M; P)g; fcf(M;Y; P)g; S2)
Note that, in particular, in order to proceed from the exclusive branch B to the next flow element Y , the guard C associated with the flow from B to Y should hold in the current state ( guard(C; B;Y; P) ^ holds(C; S1) ).
The behavioral semantics of other flow elements, e.g., parallel or inclusive
gateways, can be formalized by rules defined in a similar style. For lack of space we omit
those rules and we refer to [
The relation r(S1; S2) holds if a state S2 is immediately reachable from a state S1, that is, some action A can be executed in state S1 leading to state S2: r(S1; S2)
result(S1; A; S2) We say that a state S2 is reachable from a state S1 if there is a finite, possibly empty, sequence of actions from S1 to S2, that is, reachable state(S1; S2) holds, where the relation reachable state is the reflexive-transitive closure of r. 4
The formal semantics of data-aware BP schemas introduced in Section 3 is the basis for developing automated reasoning techniques for the analysis and verification of business processes that manipulate data objects. A major point is that our formal semantics is a CLP program, and hence we can directly apply automated reasoning methods and tools developed in the field of Constrained Logic Programming to perform analysis and verification tasks. Indeed, by using standard CLP systems we are able to provide a framework that supports several reasoning services and, in particular, in this section we will demonstrate some of them and their use for analyzing process enactment, for testing process executions, and for verifying behavioral properties.
Given a DAPS hWF; DC; DBSi and a database instance D of the schema DBS, let K B be the CLP program consisting of: (1) the ground facts WF specifying the workflow, (2) the pre, eff, and guard facts in DC specifying the enabling conditions, effects, and guards associated with the workflow, (3) the ground facts in D, and (4) the rules (introduced in Section 3) that define the behavioral semantics of the DAPS.
Reasoning services will be realized by evaluating queries to the CLP program K B. One major advantage of our approach is that query evaluation relies on a symbolic representation of states, which often avoids the actual exploration of the whole, in general infinite, state space, by covering that space by means of a finite set of constraints. More specifically, a symbolic state is represented as a set of the form:
f f1; : : : ; fk; val(o1;V1); : : : ; val(om;Vm)g satisfying a constraint c on V1; : : : ;Vm.
In the above symbolic state f1; : : : ; fk are ground cf or en fluents and val(o1;V1); : : : ;
val(om;Vm) are fluents that associate data objects o1; : : : ; om with their values V1; : : : ;Vm,
respectively. Thus, a symbolic state represents the, possibly infinite, set of concrete
1 The semantics presented in [
The predicate trace(S1; T; S2; N) defined below holds if T is a sequence of actions of maximum length N that leads from state S1 to state S2: trace(S1; [ ]; S2; N) trace(S1; [AjT]; S2; N)
N = 0 ^ S1 = S2
N > 0 ^ N1 = N
1 ^ result(S1; A;U ) ^ trace(U; T; S2; N1).
In the following we use the abbreviation s0Proc to denote the initial state of a process Proc, where the start event of Proc is enabled to fire. Furthermore, we introduce the following rule to characterize the set of final states, where the end event of Proc is enabled to fire holds(final(Proc); S)
bp(Proc; Estart; Eend) ^ holds(en(Eend; Proc); S).
Our framework provides two services for analyzing process enactment, namely trace compliance and simulation. (1) Trace compliance is the task of verifying whether an execution trace of a process is correct with respect to a given DAPS specification. Execution traces are commonly stored by BP management systems as process logs, representing the evolution of the process instances that have been enacted. Formally, a correct trace T of length N of a process Proc is a trace that leads from the initial state to the final state of Proc, that is: ctrace(T; Proc; N)
trace(s0Proc; T; S f ; N) ^ holds(final(Proc); S f )
The compliance of a trace with respect to a given DAPS can then be verified by evaluating a query of the form ctrace(t; p; n) with respect to program K B, where t is a ground list of length at most n and p is a process name. It is easy to see that such query terminates for every ground t, as the length of the second argument of the trace predicate decreases at each recursive call. An example of correct trace related to our running example is reported below. [comp(s),comp(x1),comp(o1),beg(choose prod),comp(choose prod), beg(choose ship),comp(choose ship), comp(o2),comp(x2),beg(add item), comp(add item),comp(x3),beg(payment),comp(payment), comp(x4),beg(shipment),comp(shipment),comp(e)] The trace is guaranteed to be compliant also with respect to the data constraints associated with the DAPS, even if the information about the actual values of the data objects is not explicitly represented. A more complex representation of traces that also includes information about the data object values can easily be defined, but we omit it for reasons of simplicity. (2) Simulation is the task of generating execution traces that represent possible process enactments. In order to analyze the dynamic behavior of the process in various situations, the process designer can analyze test cases where: (i) data objects are initialized to ground values in R, and (ii) a subset of the database instance D is selected. A query of the form trace(s0Proc; T; S; n), where T is a free variable, can be used to generate the execution traces T of length not larger than n. The query terminates for every fixed integer n, as the last argument of trace decreases at each recursive call, and for each successful derivation from the query, the unification mechanism employed by CLP will bind T to a ground list of actions. Similarly, to the case of trace compliance, we can easily extend our definitions so as to generate traces that also contain explicit information about data values. 4.2
Simulation is performed by selecting a finite set of test cases, that is, by fixing values for initializing the data objects and taking into consideration a specific database instance. However, the generation of test cases is not always straightforward. The mechanisms of symbolic computation provided by CLP (notably, unification and constraint solving) enable us to generate execution traces by only specifying constraints that those values are required to satisfy. Thus, we can initialize a data object to a value in a range, rather than to a concrete value. Furthermore, we can exploit the integrity constraints in the database schema DBS to perform a symbolic evaluation of a trace query without considering a fixed database instance.
For instance, in our eProcurement example, we can evaluate a trace query by initializing the data object coupon to a value X with 0 < X < 10, as specified in Figure 1. Similarly, we can initialize plafond to a value X with 0 < X < 1000. Furthermore, suppose that in our running example the integrity constraints relative to product price and ship price are: product price(X ; P) ! P > 5 ^ P < 100 ship price(X ; P) ! P > 0 ^ P < 15: Then we replace the database instance D in K B by the inverse implications of these integrity constraints, that is, by the rules: product price(X ; P) ship price(X ; P)
P > 5 ^ P < 100
P > 0 ^ P < 15:
In general, for performing a symbolic testing task, we replace the ground facts that constitute the database instance D in K B, by the inverse implications p(X1; : : : ; Xn) c of all integrity constraints p(X1; : : : ; Xn) ! c specified by DBS, hence deriving a new CLP program K B0. Due to the least model semantics of CLP, we will have that M(K B0) j= p(X1; : : : ; Xn) $ c1 ^ : : : ^ ck, where c1; : : : ; ck are the constraints implied by p(X1; : : : ; Xn) in DBS. K B0 is an over-approximation of K B, i.e., M(K B) M(K B0). Then we evaluate a query of the form trace(s0Proc; T; S; n), for a given integer n. This query always terminates and, if it succeeds and returns an answer T = t, then there exists a database instance of DBS such that the DAPS hWF; DC; DBSi has t as a possible execution trace. The converse in not necessarily true, i.e., there may exist database instances that do not generate the trace t.
K B0 can be used to test reachability properties of the DAPS. For instance, the reachability of a deadlock state in n steps can be verified trough a query of the form: trace(s0Proc; T; Sd ; n) ^ :r(Sd ; Sn) If the query succeeds, then the DAPS can reach, for some database instance, a potential deadlock state Sd and T is bound to a trace that leads to that state. If the query fails then, for any database instance satisfying the given database schema DBS, no deadlock is reachable in at most n steps.
In our example, two potential deadlock states are reachable by taking n = 20, both occurring when the control flow reaches payment (i.e., holds(en(payment; eProc); Sd )). In the first case the potential deadlock is due to a negative value of amount caused by a coupon value higher than the price of the product chosen by choose prod, which prevents the execution of payment. Indeed, the following constraint associated with Sd is computed as an answer to the above query: Vamount < 0 ^ Vitem price < 0 ^ Vcoupon > 5 where Vo is the logical variable associated to the data object o in the state Sd through the fluent val (i.e., holds(val(o;Vo); Sd )). In the second case we have that the following constraint associated with Sd is computed as another answer to the above query: Vamount = 0 ^ Vitem price <Vplafond < 115
Here the potential deadlock is due to a value of item price that exceeds the plafond granted to the user. For this reason, no item is added to the order, causing a zero value amount and preventing the execution of payment.
In order to prevent the above potential deadlocks it is sufficient to fix different ranges for the data objects plafond and coupon that make the two constraints unsatisfiable, e.g., 0 < coupon 5 and 115 plafond<1000. In this way, the lowest plafond always covers the purchase of at least one product, and the highest coupon cannot exceed the price of any product. 4.3
Verification aims at checking whether a temporal property holds for all enactments of a
given DAPS. Unlike the trace conformance, simulation, and symbolic testing tasks, for
verification we do not assume a bounded trace length. Thus, due to the presence of data
objects with values in R and arbitrary, unstructured workflow graphs, the state space is
infinite. Most verification problems, and in particular reachability, are undecidable in
this setting. However, since we encode verification tasks as CLP queries, whose
evaluation is based on a symbolic representation of states, by applying state subsumption
we can avoid the actual exploration of the whole state space and terminate in many
concrete verification examples.
(1) A very relevant behavioral property of a DAPS p is that, from any reachable state, it
is possible to complete the process, i.e., reach the final state. This property, also known
as option to complete [
reachable state(s0p; S) ^ :reachable final(S) where reachable final(S) holds if a final state can be reached from S, i.e., reachable final(S) reachable state(S; S f ) ^ holds(final(p); S f )
In our running example, modified as suggested at the end of Section 4.2, the above
query fails, hence enforcing the option to complete property.
(2) Another property that may reveal potential flaws in a DAPS is executability [
^ pre(C; A; p) ^ :holds(C; S)
In our running example we have a case of non-executability whenever apply coupon and choose prod are both scheduled for execution after o1, according to the inclusive gateways semantics. In this case, since apply coupon requires a value of item price greater than 0, it will not begin its execution until the completion of apply coupon. (3) Temporal queries can also be used for the verification of compliance rules, i.e., directives expressing internal policies and regulations aimed at specifying the way an enterprise operates. We report below two such compliance rules related to our running example. The first one requires that in any possible enactment the amount never reaches a negative value. The following query succeeds if it is possible to reach a state of the process where amount < 0.
reachable state(s0eProc; S) ^ holds(amount < 0; S)
In our running example, modified to avoid deadlock as indicated at the end of Section 4.2, this query fails, thus enforcing the compliance rule.
A second example is a compliance rule requiring that it is possible to add an item to the order after the payment of part of the due amount. This property is encoded by the following query, which succeeds in our running example.
reachable state(s0eProc; S1) ^ holds(en(payment; eProc); S1)
^ reachable state(S1; S2) ^ holds(en(add item; eProc); S2)
We implemented the proposed framework in a proof-of-concept tool, extending the
system discussed in [
The inference engine is built upon SWI Prolog2 and is based on a suitable encoding
of the set K B of rules defined in Section 4. The constraints are handled by the built-in
SWI solver for equality and inequality constraints over the reals. While the translation
2 http://www.swi-prolog.org/
of K B is straightforward, additional considerations are needed when dealing with the
evaluation of queries that involve state reachability (i.e., the relation reachable state).
Indeed, similarly to many other Prolog engines, SWI generates derivations from a query
by using a depth-first search strategy that never looks at the queries derived before the
current one. For this reason query evaluation may enter an infinite loop in the presence
of recursive rules. To mitigate this difficulty, at least partially, the definition of the
predicate reachable state (reported below) has been implemented through memoing [
reachable state(X,X). reachable state(X,Z) :result(X, ,Y), constrained state(Y,cs(Y1,CY)), n+ subsumed by visited(cs(Y1,CY)), assert(visited(cs(Y1,CY))), reachable state(Y,Z). where: constrained state(Y,cs(Y1,CY)) holds if Y1 is the set of fluents in Y and CY is the constraint associated with the variables in Y; subsumed by visited(cs(Y1,CY)) holds if a fact visited(cs(W1,CW)) belongs to the program, such that Y1 is an instance of W1 for some substitution and CW entails CY; assert(visited(cs(Y1,CY))) adds the fact visited(cs(Y1,CY)) to the program.
Essentially, during the evaluation of a goal including a reachable state atom (i.e., requiring the state space exploration), for every reached state a subsumption test is performed, in order to verify whether a state that subsumes the current one has been already considered. If it is the case, the sub-goal fails, avoiding redundant computations. Otherwise, the state is added to the set of the visited states and the exploration proceeds.
By exploiting this simple memoing mechanism, we were able to verify many reachability properties of various versions of the eProcurement example, and in particular all properties presented in Section 4.3, which in principle require the exploration of an infinite state space. 6
In this paper we presented a framework, grounded in Constraint Logic Programming, for reasoning on BP models represented through a data-aware extension of the popular BPMN notation. The behavioral semantics of a process is defined as a (possibly infinite) state transition system by following an approach derived from the Fluent Calculus. Data values have a symbolic representation based on arithmetic constraints, which allow us to specify data objects manipulations and database interactions in terms of preconditions and effects of the enactment of activities. We discussed the reasoning tasks the framework enables, dealing with enactment, testing and verification, and how they can be implemented through CLP engines.
Our work is related to a growing stream of research ([
Several approaches have been recently proposed in the workflow community to take
into account process data, extending consolidated results originally conceived for
dealing with control-flow only. Among them, some related problems addressed in literature
concern: run-time support for the enactment of data-aware process models [
Finally, other approaches based on LP that are worth mentioning are [
The preliminary results presented in this paper open up several directions for future research. First of all, we plan to push forward the empirical evaluation of our proposal in each application scenario reported in Section 4. To this end, a relevant aspect to be further elaborated regards the adoption of program optimization techniques to enhance the performances of the reasoning approach. On a more theoretical perspective, we are investigating the class of BPs for which a symbolic finite-state space can be computed, in order to characterize the decidability and complexity of temporal verification tasks.