On Enabling Data-Aware Compliance Checking of
Business Process Models
?
David Knuplesch
1
, Linh Thao Ly
1
, Stefanie Rinderle-Ma
3
, Holger Pfeifer
2
, and
Peter Dadam
1
1
Institute of Databases and Information Systems
Ulm University, Germany
2
Institute of Articial Intelligence
Ulm University, Germany
3
Faculty of Computer Science
University of Vienna, Austria
david.knuplesch,thao.ly,holger.pfeifer,peter.dadam@uni-ulm.de,
stefanie.rinderle-m[email protected]
Abstract.
In the light of an increasing demand on business process
compliance, the verication of process models against compliance rules
has become essential in enterprise computing. To be broadly applicable
compliance checking has to support data-aware compliance rules as well
as to consider data conditions within a process model. Independently of
the actual technique applied to accomplish compliance checking, data-
awareness means that in addition to the control ow dimension, the
data dimension has to be explored during compliance checking. However,
naive exploration of the data dimension can lead to state explosion. We
address this issue by introducing an abstraction approach in this paper.
We show how state explosion can be avoided by conducting compliance
checking for an
abstract process model
and
abstract compliance rules
.
Our abstraction approach can serve as preprocessing step to the actual
compliance checking and provides the basis for more ecient application
of existing compliance checking algorithms.
Keywords:
Process verication, Compliance rules, Process data, Abstraction
1 Introduction
In many application domains, business processes are subject to compliance rules
and policies that stem from domain-specic requirements such as standardization
or legal regulations [1]. Examples of compliance rules for order-to-delivery pro-
cesses are collected in Table 1. Ensuring compliance of their business processes is
crucial for enterprises today, particularly since auditing and certication of their
business processes has become a competitive edge in many domains. Examples
?
This work was done within the research project SeaFlows partially funded by the
German Research Foundation (DFG).
Table 1.
Examples of compliance rules for order-to-delivery processes
c1
After conrming an order, goods have to be shipped eventually.
c2
Production (i.e., local and outsourced production) shall not start until the order
is conrmed.
c3
Each order shall either be conrmed or declined.
c4
Local production shall be followed by a quality test.
c5
Premium customer status shall only be oered after a prior solvency check.
c6
Orders with a piece number beyond
50,000
shall be approved before they are
conrmed.
c7
For orders of a non-premium customer with a piece number beyond
80,000
a
solvency check is necessary before assessing the order.
c8
Orders with piece number beyond
80,000
require additional shipping insurance
before shipping.
c9
After conrming an order of a non-premium customer with piece number of at
least
125,000
, premium status should be oered to the customer
include certied family-friendly enterprises being more attractive to prospective
employees or clinics proving a certain standard of their audited treatments to
patients. Since process models are the common way to represent business pro-
cesses, business process compliance can be ensured by verifying process models
against imposed compliance rules at process buildtime. Such a priori compliance
checking might help process designers to dene compliant process models and
avoid instantiations of non-compliant processes. Further, legacy process models
can be checked for compliance, when introducing new compliance rules.
Fig. 1 shows a simplied order-to-delivery process
P
which might be subject
to the rules given in Table 1. For brevity we abstain from modeling the complete
data ows of
P
. A closer look at compliance rules
c1
to
c4
reveals that they
basically constrain the execution and ordering of activities and events within a
process model. For example,
c1
being applied to
P
means that event
confirm
order
has to be eventually followed by the activity
ship goods
in all execution
paths of
P
. We can apply approaches from literature to verify
P
against
c1
to
c4
, (e.g., [24]). However, compliance rules
c6
to
c9
obviously do not only refer
to activities and events, but also to process data. In particular, in the context
of
P
process data includes piece number
pn
, customer status
c
, and approved
a
. In order to verify
P
against
data-aware
compliance rules such as
c6
to
c9
,
data ows as well as branching conditions of
P
have to be considered, i.e., any
compliance checking approach should be able to deal with data conditions.
It is notable that although compliance rule
c5
does not contain any references
to process data of
P
, data-awareness of the compliance checking is still needed to
enable correct verication. Verifying
c5
while ignoring the data conditions in
P
would lead to violation of
c5
over
P
since activity
offer premium status
is not
always preceeded by activity
check solvency
. However, when having a closer
look at the data conditions under which these activities are executed (i.e., the
[pn > 50,000]
Process model P
x
[pn > 100,000]
check
solvency
[pn ≤ 50,000]
x
x
[pn > 150,000]
[pn ≤ 150,000]
enable
tracking
x
x
x
[pn ≤100,000]
10%
discount
[c = premium]
x
[c ≠premium]
x
[a = true
OR
pn ≤ 50.000] [a = false AND
pn > 50,000]
x
[pn > 100,000]
receive 30% prepayment
x
[pn ≤100,000]
+
local
production
outsourced
production
+
x
shipping
insurance
x
[pn > 100,000]
receive order
process
order
quality test
split order
c
customer
[new, normal,
premium]
x
[c = premium OR pn ≤150,000 ]
[c ≠premium AND
pn > 150,000]
[pn ≤100,000]
offer premium
status
x
+
+
x
confirmation of receipt
x
a
approved
[true, false]
decline order
comfirm order
confirm shipping
pn
piece number
send invoice
ship goods
local
production
assess
order
Fig. 1.
A simplied order-to-delivery process modeled in BPMN
branching conditions) we can see, that
c5
is satised over
P
. Note that
offer
premium status
is executed only for orders of non-premium customers with
piece number beyond
150,000
. The correlation of the data conditions assigned
to data-based exclusive gateways in
P
guarantee a prior solvency check.
We denote compliance checking mechanisms that are able to deal with corre-
lations of data-based gateways as well as to verify processes against data-aware
compliance rules as
data-aware compliance checking
.
Challenges.
As our examples show, data-awareness is crucial for applying
compliance checking in practice. Independently of
how
compliance checking is
actually accomplished (i.e., which techniques, such as model checking [2], are
applied), data-awareness poses challenges for compliance checking in general.
Data-aware compliance checking has to consider the states that relevant data ob-
jects can adopt during process execution. Activity
offer premium status
from
Fig. 1, for example, can only be executed under data condition
pn >
150,000
.
As this example shows, we may have to deal with arbitrary data such as integers
that have huge domains. When compliance checking is applied in a straight-
forward and naive manner, data-awareness can lead to
state explosion
caused
by the states that relevant data objects can adopt during process execution.
Consider for example data object
pn
representing the piece number in the order-
to-delivery process and compliance rule
c8
. Let us assume, for example, that the
domain of
pn
ranges from
1
to
500,000
. Then, naive exploration of the data
dimension means that process model
P
is veried against
c8
for each possible
state
of
pn
between
1
and
500,000
. This, in fact, means that the complexity
of data-aware compliance checking is
500,000
times the complexity of the non-
A
B
compliance
checking
processing
compliance
report
automatic
abstraction to
reduce complexity
automatic
concretization
for user
feedback
process
model
data-aware
abstract
process model
abstract data-
A
compliance
rules aware
compliance rules
Fig. 2.
The overall process of automatic abstraction based on the analysis of the process
model and the compliance rules to be veried
data-aware case. Hence, to enable ecient compliance checking, strategies are
required that keep the complexity manageable. A further challenge is that data-
aware compliance checking also necessitates advanced concepts for user feedback.
This is necessary since compliance violations that occur only under certain data
conditions are often not as obvious as compliance violations at activity level.
Contributions.
Although the verication of process models has been addressed
by a multitude of recent approaches, data-awareness has not been suciently
supported yet. Only few approaches consider the data perspective at all. While
addressing data-aware compliance rules, [5] only enables data conditions that do
not correlate. However, as the order-to-delivery process in Fig. 1 shows, data-
based gateways may also contain conditions that are correlated. For example,
the data conditions
pn > 100,000
and
pn > 150,000
in
P
correlate (i.e.,
pn >
150,000
implies
pn > 100,000
but not vice versa). In addition, these conditions
correlate with data condition
pn > 80,000
("piece number beyond
80,000
")
resulting from compliance rule
c8
. The limitation to only non-correlating data
conditions facilitates the compliance checking problem. However, as our examples
indicate, this can be too restrictive for many practical applications.
While existing approaches mainly focus on the compliance checking part (cf.
Fig. 2 A), this paper focuses on the pre- and postprocessing steps (cf. Fig. 2
B) that enable data-aware compliance checking by tackling the state explosion
problem. The latter can occur when fully exploring the data dimension dur-
ing compliance checking. In this paper, we introduce abstraction strategies to
reduce the complexity of data-aware compliance checking. This is achieved by
abstracting from concrete states of data objects to abstract states. Based on the
compliance rules to be checked our approach
automatically
derives an
abstract
process model
and
abstract compliance rules
. The latter enable more ecient
exploration of the data dimension when used as input to the actual compli-
ance checking (cf. Fig. 2 B). Moreover, we discuss how a concretization can be
accomplished to provide users with intelligible feedback in case of compliance
violations. Our approach is nally validated by a powerful implementation, the
SeaFlows compliance checker.
This paper is structured as follows. Related work is discussed in Sect. 2. Fun-
damentals are introduced in Sect. 3. Sect. 4 discusses how the abstract process
model and corresponding abstract compliance rules are derived. The applica-
tion of our abstraction approach and the proof-of-concept implementation are
discussed in Sect. 5. We close with a summary and an outlook in Sect. 6.
2 Related Work
Due to its increasing importance compliance verication has been addressed by
numerous approaches. Most of them focus on the compliance checking part (cf.
Fig. 2 A). They propose a variety of techniques to accomplish the verication of
process models against imposed compliance rules, such as model checking [2,69]
or the analysis of the process model structure [3,10]. In our previous work in the
SeaFlows project, we addressed the support of activity-level compliance rules
throughout the process lifecycle [4,10]. So far, however, only few approaches
have addressed data-awareness. The modeling of data-aware compliance rules
is addressed by [4,5,7,11]. Graphical notations that are mapped to logical for-
mulas (e.g., in linear temporal logic) are introduced in [4,5,7]. Basically, these
approaches support the enrichment of activity-related compliance rules by data
conditions. Our work in this paper apply these modeling approaches, since we do
not focus on
how
to model data-aware compliance rules but rather on enabling
their verication.
[12] introduce an approach for semantically annotating activities with pre-
conditions and eects that may refer to data objects. In addition, [12] discusses
an ecient algorithm for compliance verication using propagation. In contrast
to this approach, we focus on deriving suitable abstraction predicates from pro-
cess models and compliance rule. Further [5] allows for verifying process models
against compliance rules with data conditions based on linear temporal logic
(LTL). However, as previously discussed [5] only addresses data conditions that
do not correlate. This is for example not sucient to support proper verica-
tion of the order-to-delivery process from Fig. 1 against compliance rule
c5
from
Table 1, since we have to deal with the correlation of two data-based exclusive
gateways both refering to data object
pn
. In this paper, we propose strategies
to deal with such cases. By applying abstraction techniques, our approach ac-
complishes the basis to apply approaches such as [5].
Orthogonal strategies to reduce complexity of compliance checking are dis-
cussed in [6,7]. [7] sequentializes parallel ows in order to avoid analyzing irrele-
vant interleavings. [6] limits the complexity of compliance checking by reducing
process models to the relevant parts. These abstraction strategies operating at
the structural level are orthogonal to our abstraction approach. They can be
applied to complement the approach introduced in this paper.
3 Fundamentals
Independently of the actual technique applied to accomplish compliance check-
ing, data-awareness means that in addition to the control ow dimension the
data dimension must be explored during compliance checking. However, this can
lead to state explosion since a potentially huge number of states of data objects
has to be explored. In Sect. 4, we show how the state explosion can be avoided
by applying suitable abstraction strategies. Before discussing these, we provide
some fundamentals.
A process domain representing a particular business domain typically consists
of process artifacts (e.g., activities and events). The process domain notion in
Def. 1 provides the basis for both process models and compliance rules.
Denition 1 (Process Domain).
A process domain
D
is a tuple with
D=
(A,E,O,D, dom)
where
A
is the set of activity types,
E
is the set of event types,
O
is the set of data objects,
D
is the set of data domains, and
dom :O→D
is a function assigning a data domain to each data object.
We further dene
ΩD:= SD
as the set of all values (i.e., data states) of
D
.
Example 1.
Consider process model
P
from Fig. 1. The related process domain
may be
D= (A,E,O,D, dom)
, where
A:= {
process order, 10% discount, check solvency, assess order, ...
}
E:= {
receive order, confirmation of receipt, confirm order, ...
}
O:= {pn, c, a}
D:= {N={
0, 1, 2, ...
},{
new, normal, premium
},B={
true, false
} }
dom(pn) := N;dom(c) := {
new, normal, premium
};dom(a) := B
Data-Aware Compliance Rules.
It is not our intention to introduce an ap-
proach to model data-aware compliance rules. Hence, we rely on existing work
such as [4,5,13]. Since our approach is not restricted to a particular compliance
rule modeling language, we come up with a general notion of data-aware com-
pliance rules in Def. 3 that is applicable to a multitude of existing approaches.
Compliance rules typically contain conditions on activities and events of cer-
tain types (e.g., cf. compliance rules
c1
to
c4
). We denote these as
type conditions
.
In addition to type conditions, data-aware compliance rules contain conditions
on the states of data objects, so-called
data conditions
. Formalization of type
conditions and data conditions is given in Def. 2.
Denition 2 (Type Condition, Data Condition).
Let
D= (A,E,O,D, dom)
be a process domain and let
t∈A∪E
be an activity type or an event type. Then
a type condition is an expression of the form:
(type =t)
.
Let further
o∈O
be a data object,
v∈dom(o)
a certain value of the related
domain, and
⊗ ∈ {=,6=, <, >, ≤,≥, . . .}
a relation. Then
a data condition is an expression of the form:
(o⊗v)
.
Moreover, we dene:
TCD⊆ { (type =t)|t∈A∪E}
as the set of all type conditions over
D
.
DCD⊆ { (o⊗v)|o∈O, v ∈dom(o),⊗:= {=,6=, <, >, ...}}
as the set of
all data conditions over
D
.
Example 2.
Consider compliance rule
c9
from Table 1. Here,
c9
yields the
following type conditions (
TCD
) and data conditions (
DCD
) where
pn ∈O
is
the data object representing the piece number and
c∈O
is the data object
representing the customer status (cf. Fig. 1).
Phrase Corresponding condition
After
conrming an order
(type =
confirm order
)∈T CD
of a
non-premium customer
with
(c6=
premium
)∈DCD
piece number of at least
125,000
(pn ≥
125,000
)∈DCD
premium status
should be
oered
(type =
offer premium status
)∈T CD
to the customer
Finally, a general data-aware compliance rule is dened as follows:
Denition 3 (Data-Aware Compliance Rule).
Let
D= (A,E,O,D, dom)
be a process domain. Then, a data-aware compliance rule is a tuple
c= (C, ∆)
,
with:
C=TCc∪DCc
is nite set of conditions that is partitioned into the set of
type conditions
TCc⊆TCD
and the set of data conditions
DCc⊆DCD
.
∆
an expression dening temporal (ordering) and logical relations over the
conditions in
C
.
Further, we dene:
conditionsCRc:O→2DCc, o07→ {(o⊗v)|o=o0∧(o⊗v)∈DCc}
as a
function returning all data conditions of
c
that aect a certain data object.
Example 3.
To illustrate our examples, we use linear temporal logic (LTL).
LTL is applied to model compliance rules by numerous approaches [5,13]. Note,
however, that our approach is not restricted to a particular compliance rule mod-
eling language. Using LTL we can model
c9
from Table 1 as follows:
c9:
G
( ((type =
confirm order
)∧(pn ≥
125,000
)∧(c6=
premium
))
⇒
F
(type =
offer premium status
) )
According to Def. 3 this means
c9= (C9, ∆9)
, where
C9={tc1= (type =
confirm order
), tc2= (type =
offer premium status
)
dc1= (pn ≥
125,000
), dc2= (c6=
premium
)}
∆9=
G
( (tc1∧dc1∧dc2)⇒
F
tc2)
TCc9={(type =
confirm order
),(type =
offer premium status
)}
DCc9={(pn ≥
125,000
),(c6=
premium
)}
Based on the above notion of data-aware compliance rules, we later show how
automatic abstraction is conducted to enable data-aware compliance checking.
Processes.
A process model, commonly represented by a process graph, can
be composed using activities, events, and data objects from a process domain.
Since our approach is not restricted to a particular process denition language,
we provide a general denition of process graphs in Def. 4 following common
notations, such as BPMN:
Denition 4 (Process Graph).
Let
D= (A,E,O,D, dom)
be a process do-
main. Then, a process graph is a tuple with
P= (N, F, O, I, type, con)
, where:
N=AP∪EP∪GP
is a nite set of nodes that is partitioned into the set of
activities
AP
, the set of events
EP
, and the set of gateways
GP
.
F⊆N×N
represents the sequence ow relation between nodes.
O⊆O
is a nite set of data objects.
I⊆O×N∪N×O
is the data ow relation between nodes and data objects.
type :AP∪EP→A∪E
is a function assigning an activity type to each
activity in
P
and an event type to each event in
P
, where holds:
a∈AP⇒type(a)∈A
and
e∈EP⇒type(e)∈E
con :F→2DCD
is a function assigning a (maybe empty) set of data condi-
tions to each sequence ow.
Further, we dene:
DCP:= {(o⊗v)|∃f∈F: (o⊗v)∈con(f)} ⊆ DCD
as the set of data con-
ditions in
P
.
conditionsPGP:O→2DCP, o07→ {(o⊗v)|o=o0∧(o⊗v)∈DCP}
as a
function returning all data conditions of
P
on the associated data object.
Example 4.
Process model
P
from Fig. 1 contains the following data conditions
over
pn
:
conditionsPGP(pn) = {(pn ≤
50,000
),(pn >
50,000
),(pn ≤
100,000
),
(pn >
100,000
),(pn ≤
150,000
),(pn >
150,000
)}
4 On Enabling Data-Aware Compliance Checking
As discussed the full exploration of the data dimension can lead to state ex-
plosion, when conducting compliance checking. The basic idea to achieve more
ecient
data-aware compliance checking
of process models and to limit the state
explosion problem is to abstract from states that are irrelevant for the verica-
tion of a particular compliance rule. Consider, for example, compliance rule
c8
from Table 1. Concerning the satisfaction/violation of
c8
it is not relevant
whether
pn =
120,000
,
pn =
120,001
,
pn =
120,002
,
. . .
,
or
pn =
130,000
holds when executing the order-to-delivery process from Fig. 1. Hence, it is not
necessary to dierentiate between these cases when verifying
P
against
c8
. These
potential states of
pn
, namely
120,000
,
. . .
,
130,000
, could be treated as one
"merged" state. The merged state can be described by the
abstraction predicates
(pn ≥
120,000
)∧(pn ≤
130,000
)
and be applied to data-aware compliance
checking (e.g., by applying model checking techniques). Other irrelevant states
of
pn
can be merged in a similar manner to derive a more compact set of states
that serve as domain of
pn
in the
abstract process model
. In fact, a dierentiation
between the concrete states of
pn
beyond
100,000
is not necessary for verifying
P
against
c8
. Hence, all states of
pn
beyond
100,000
can be merged to one
abstract state
pn >
100,000
.
In general, by abstracting from states of data objects irrelevant for the ver-
ication of a compliance rule, less cases have to be explored in the verication
procedure. This helps to reduce complexity of compliance checking. However,
abstracting from states must not lead to incorrect verication results. Consider,
for example, again the order-to-delivery process
P
and compliance rule
c8
from
Table 1. To verify particularly
c8
it is not sucient to only consider whether
pn >
100,000
or
pn ≤
100,000
holds. The challenge of automatic abstraction
is to identify adequate
abstraction predicates
that enable us to "merge" states
wihtout falsifying verication results
In literature, abstracting from concrete states to abstract predicates is com-
mon practice for dealing with state explosion [1417]. This is particularly relevant
in engineering domains, where large systems have to be veried against safety
properties. In many applications, abstraction constitutes a task that requires
human interaction. In particular, domain experts are required to nd the right
abstraction. By analyzing the dependencies between a process model
P
and a
compliance rule
c
our abstraction approach
automatically
derives an abstract
process model
Pabstract
and an abstract compliance rule
cabstract
. These can
serve as input to the actual compliance checking. We want to nd
conservative
abstraction predicates such that holds:
P|=c⇔Pabstract |=cabstract
The data-based abstraction introduced in this paper can be combined with
structural abstraction strategies (cf. Sect. 2) to achieve further reduction of the
compliance checking complexity.
Automatic Abstraction for Data Conditions
To achieve automatic abstraction, we have to accomplish three steps:
1) Identify data objects potentially relevant to
c
and the data conditions on
them in
c
and in the data-based gateways of
P
2) Identify abstraction predicates for relevant data objects
3) Application of abstraction predicates to obtain
Pabstract
and
cabstract
Altogether, the states of each data object
o
can be represented by a set of
abstraction predicates beeing relevant for proper verication of the associated
compliance rule over the process model. This is accomplished by analyzing the
data conditions in the process model and in the compliance rule. For the iden-
tied set of abstraction predicates we can identify combinations of predicates
whose conjunction is satisable (i.e., evaluated with
true
). Each such combina-
tion represents a potential
abstract state
of the corresponding data object
o
:
Denition 5 (Abstraction for Data Conditions).
Let
D= (A,E,O,D, dom)
be a process domain,
P= (N, F, O, I, type, con)
be a process model, and
c
be a
compliance rule over
D
. Let further
o∈O
be a data object in
P
. Then,
predicatesc
P:O→DCD, o 7→ predicatesc
P(o)
with
predicatesc
P(o) := conditionsCRc(o)∪conditionsP GP(o)
is a function
returning the set of all data conditions in
c
and
P
that aect
o
and, thus,
constitute relevant abstraction predicates.
solve : 2DCD×ΩD→2DCD,(C, v0)7→ solve((C, v0))
with
solve(C, v0) :=
{(o⊗v)|(v0⊗v) =
true
∧(o⊗v)∈C}
is a function returning the partic-
ular subset of predicates that are satised by
v
.
allocationsc
P:O→22DCD, o 7→ allocationsc
P(o)
with
allocationsc
P(o) := {S| ∃v∈dom(o) : S=solve(predicatesc
P(o), v)}
is a
function returning a set of sets of predicates such that for each value
v∈
dom(o)
there is a set in
allocationsc
P(o)
containing all predicates over
o
that
are satised by
v
.
Note that for deriving the abstraction predicates
predicatesc
P(o)
not only
the data conditions of
P
, but also the data conditions of
c
are considered. Based
on the predicates
predicatesc
P(o)
for a data object
o
, we can narrow the data
domain of
o
which has to be explored during data-aware compliance checking.
In particular, instead of exploring the complete domain of
o
, which may cause a
state explosion, only the corresponding set of abstract states (i.e., the elements
of
allocationsc
P(o)
) has to be explored in the compliance checking procedure.
Due to the Def. 5
|allocationsc
P(o)|≤|dom(o)|
always holds. For a large data
domain
dom(o)
typically,
allocationsc
P(o)
contains signicantly less elements.
Hence, to be able to narrow the domain of
o
to the set of abstract states of
o
being relevant for the verication of the actual compliance rule is a crucial step
to avoid the state explosion problem.
Dealing with Large Domains.
Although it is easy to derive
allocationsc
P(o)
for small nite domains by calculating
solve(C, v)
for each
v∈dom(o)
, this
procedure is not feasible for large data domains, such as
D=N
. However, if
D
is a totally ordered domain (e.g.
N
,
Z
, or
R
) and all conditions
(o⊗v)∈
predicatesc
P(o)
are using ordering relations
⊗∈{<, ≤,=,≥, >, 6=}
, as it is the
case with
pn
and corresponding data conditions, we can eciently calculate
allocationsc
P(o)
as follows:
First, we determine
(vi)1≤i≤n=< v1, . . . , vn>
the ascendingly sorted nite
sequence of such values
v
with
∃(o⊗v)∈predicatesc
P(o)
without any multiple oc-
currences. Now it is sucient to limit the calculation of
solve(predicatesc
P(o), v)
to the following cases of
v
1. the values
v1, . . . , vn
that are the limits of the relevant abstraction predicates,
2. for any two successive values
vi
and
vi+1
, a value
wi
with
v1< wi< vi+1
,
3. a value
s < v1
smaller than any
vi
and
b > vn
bigger than any
vi
Obviously, it is sucent to use one
wi
with
vi< wi< vi+1
, since all values of
this interval exactly fulll and violate the same conditions of
predicatesc
P(o)
.
For the same reason the use of one
s
and one
b
is sucent. Note that sometimes
there may be no
s∈D
with
s < v1
or no
wi∈D
with
vi< wi< vi+1
(i.e.
D=N
and
v1= 0, v2= 1
). Then, the corresponding cases have to be ignored.
The calculation of
allocationsc
P(o)
may also be delegated to a SMT-Solver
(e.g., Yices [18]) that is even able to deal with large domains and conditions
using linear arithmetics.
Example 5.
Consider process model
P
from Fig. 1 and compliance rule
c9
from
Table 1 over process domain
D
. As described above, to calculate
allocationsc9
P(pn)
it is sucient to consider
50,000, 100,000, 125,000, 150,000
as well as
75,000, 112,500, 137,500
and
49,999, 150,001
. So we receive the follow-
ing abstraction predicates for the data object
pn
.
predicatesc9
P(pn) = conditionsCRc9(pn)∪conditionsP GP(pn)
={(pn ≥
125,000
)} ∪ {(pn ≤
50,000
),(pn >
50,000
),(pn ≤
100,000
),
(pn >
100,000
),(pn ≤
150,000
),(pn >
150,000
)}
={(pn ≥
125,000
),(pn ≤
50,000
),(pn >
50,000
),(pn ≤
100,000
),
(pn >
100,000
),(pn ≤
150,000
),(pn >
150,000
)}
allocationsc9
P(pn) = {α, β, γ, δ, }
, where
α:= {(pn ≤
50,000
),(pn ≤
100,000
),(pn ≤
150,000
)}
β:= {(pn >
50,000
),(pn ≤
100,000
),(pn ≤
150,000
)}
γ:= {(pn >
50,000
),(pn >
100,000
),(pn ≤
150,000
)}
δ:= {(pn ≥
125,000
),(pn >
50,000
),(pn >
100,000
),(pn ≤
150,000
)}
:= {(pn ≥
125,000
),(pn >
50,000
),(pn >
100,000
),(pn >
150,000
)}
The sets of predicates in
allocationsc9
P(pn)
constitute properties describing
the "merged" sets of original states of
pn
.
{α, β, γ, δ, }
may be used as
abstract
data domain
of
pn
for verication against
c9
. During compliance checking of
P
against
c9
, only these abstract states have to be explored. Compared to the
original domain of
pn
, this constitutes a signicant reduction of the complexity
for exploring the data dimension.
In Def. 6 we transfer the above results into process domain, process graph
and compliance rule and, therefore, formalize the
abstract process domain
, the
abstract process graph
, and the
abstract compliance rule
(cf. Fig. 2).
Denition 6 (Abstract Process Domain, Abstract Process Graph, Ab-
stract Compliance Rule).
Let
D= (A,E,O,D, dom)
be a process domain with
a process graph
P= (N, F, O, I, type, con)
and a compliance rule
c= (C, ∆)
.
The abstract process domain
Dabstract
of
D
with respect to
P
and
c
is dened as
Dabstract = (A,E,O,Dabstract, domabstract)
, where
Dabstract := {allocationsc
P(o)|o∈O}
domabstract(o) := allocationsc
P(o)
Then the abstract process graph
Pabstract
of
P
with respect to
c
is dened as
Pabstract = (N, F, O, I, type, conabstract)
, where for
f∈F
holds
conabstract(f) := {(00(o⊗v)00 ∈o)|00(o⊗v)00 ∈con(f)}
The abstract compliance rule
cabstract
of
c
with respect to
P
, is dened as
cabstract =
(Cabstract, ∆)
where:
Cabstract := TCc∪ { (00(o⊗v)00 ∈o)|00(o⊗v)00 ∈DCc)}
Example 6.
Consider process model
P
from Fig. 1 and compliance rule
c9
over process domain
D
(cf. Example 1). Due to space limitation, we apply the
abstraction only for data object
pn
. Based on Example 5 we obtain the abstract
process domain
Dabstract = (A,E,O,Dabstract, domabstract)
, with
Dabstract := {allocationsc9
P(pn), . . .}
={ {α, β, γ, δ, }, . . . }
dom(pn)abstract := allocationsc9
P(pn) = {α, β, γ, δ, }
The corresponding abstract process graph
Pabstract = (N, F, O, I, type, conabstract)
is depicted in Fig. 3). Further, we obtain the corresponding compliance rule
cabstract = (Cabstract, ∆)
, where:
Cabstract := TCc∪ { ((o⊗v)∈o)|(o⊗v)∈DCc)}
={tc1= (type =
confirm order
), tc2= (type =
offer premium status
)
dc1abstract = ((pn ≥
125,000
)∈pn), . . . }
5 Analyis and Implementation
We applied our approach to enable data-aware compliance checking of process
models without running into intractable state explosion problems. To accomplish
the actual compliance checking step (cf. Fig. 2 A), we applied model checking
techniques (e.g., by using SAL [19]). Model checking is applied to compliance
verication by numerous approaches in literature [2,6,7]. It comprises techniques
for automatic verication of a model specication against predened properties.
Process model P
x
check
solvency
x
x
enable
tracking
x
x
x
10%
discount
[c = premium]
x
[c ≠premium]
x
[a = false AND
(pn > 50,000) є pn]
x
receive 30% prepayment
x
+
+
x
shipping
insurance
x
receive order
process
order
quality test
split order
c
customer
[new, normal,
premium]
x
offer premium
status
x
+
+
x
confirmation of receipt
x
a
approved
[true, false]
decline order
comfirm order
confirm shipping
pn
piece number
send invoice
ship goods
local
production
assess
order
[(pn > 100,000) є pn]
[(pn ≤ 50,000) є pn]
[(pn > 150,000) є pn]
[(pn ≤ 150,000) є pn]
[(pn ≤100,000) є pn]
[a = true OR
(pn ≤ 50.000) є pn]
[(pn > 100,000) є pn]
[(pn ≤100,000) є pn]
[(pn > 100,000)
є pn]
[ c = premium OR (pn ≤150,000) є pn]
[ c ≠premium AND
(pn > 150,000) є pn]
[(pn ≤100,000) є pn]
[(pn > 50,000) є pn]
local
production
outsourced
production
abstract
Fig. 3.
The abstract order-to-delivery process after applying abstraction to
pn
SeaFlows
Seite 2
process domain
process
model
data-aware
compliance rule
counterexample
process trace
automatic
abstraction abstraction
mappings
model
compliance
rule
process
trace
automatic
concretization
abstract process domain
abstract
process model abstract data-aware
compliance rule counterexample
abstract process trace
transformation retransformation
transformation
mappings
state transition system
i
state transition
system temporal-logic
property
i
counterexample
state trace
co
nv
e
r
s
i
o
n
SAL
ifi d l h k
convers
i
on
SAL in
p
ut file
pars
i
ng
counterexample
SAL output stream
conversion
mappings
spec
ifi
c mo
d
e
l
c
h
ec
k
e
r
model checking with SAL
p
SAL
output
stream
true
false
Fig. 4.
Data-aware compliance checking and generation of counterexample
In order to apply model checking, we have to provide a state transition system
and a logic property model to the model checker (cf. Fig 4). Therefore, we
transform the abstract process model into a state representation and the abstract
compliance rule into a logic property. To provide both to the model checker, a
conversion with respect to the model checker's specic syntax and restrictions is
required. The model checker then performs automatic exploration of the state
space and checks for conformance to the compliance rule. In case of a violation,
the model checker provides an incompliant execution trace as counterexample.
As previously discussed, a major challenge of data-aware compliance checking
is to provide meaningful feedback in case of compliance violations (e.g., data
conditions under which a violation occurs). To tackle this we have to memorize
the steps taken during the transformation procedure and we need to conduct a
retransformation. Fig. 4 shows the steps accomplished by our implementation.
Our proof-of-concept implementation, the SeaFlows compliance checker, is
implemented as Java-plug-in for the Aristaow Process Template Editor which
is part of the Aristaow BPM Suite [20]. 17.000 lines of code and the class
hierarchy comprising about 70 interfaces and 210 classes indicate the complexity
of the implementation. The SeaFlows compliance checker enables modeling of
LTL-based data aware compliance rules using a tree-based editor. Automatic
abstraction as discussed in Sect. 4 is supported for domains of numbers. The
SeaFlows compliance checker conducts the automatic abstraction, transforms a
AristaFlow process model into a state representation, and pass it to the model
checker SAL [19]. Counterexamples obtained from SAL can be shown as process
logs or visualized as process graph as shown in Fig. 5.
6 Summary and Outlook
Enabling process-aware information systems to support the compliance of pro-
cess models with imposed data-aware compliance rules can be regarded as one
original
process graph
counterexample as
process graph
counterexample
as process log
data-aware
compliance rules
visualization of the
counterexample’s steps
Fig. 5.
Aristaow Process Template Editor with the SeaFlows compliance checker plug-
in for data-aware compliance rule checking
step towards installing business process compliance management in practice.
In this paper, we introduced an abstraction approach that enables data-aware
compliance checking in a more ecient manner by limiting the state explosion
problem that can occur when fully exploring the data dimension during verica-
tion. The approach serves as preprocessing step to actual compliance checking
and provides the basis for ecient application of existing compliance check-
ing algorithms. Being indepedent of a particular process meta-model and of a
particular compliance rule modeling language, our approach is applicable to a
variety of existing approaches. To accomplish data-aware compliance checking in
a comprehensive manner, we also address the challenge of providing users with
intelligible feedback in case of compliance violations. To our best knowledge, we
are the rst to apply automatic data abstraction in the context of compliance
checking of business process models. In future, we will further research on au-
tomatic abstraction for other types of domains, also considering relationships
among them. Further we will go on in rening the verication output to provide
more intelligible feedback to users.
References
1. Sadiq, S., Governatori, G., Naimiri, K.: Modeling control objectives for business
process compliance. In: Proc. of the 5th Int'l Conf. on Business Process Manage-
ment. Volume 4714 of LNCS., Springer (2007) 149164
2. Ghose, A., Koliadis, G.: Auditing business process compliance. Service-Oriented
ComputingICSOC 2007
4749
(2007) 169180
3. Sadiq, S., Orlowska, M., Sadiq, W.: Specication and validation of process con-
straints for exible workows. Information Systems
30
(5) (2005) 349378
4. Ly, L.T., Rinderle-Ma, S., Dadam, P.: Design and verication of instantiable com-
pliance rule graphs in process-aware information systems. In: Proc. of the 22nd
Int'l Conf. on Advanced Information Systems Engineering. Volume 6051 of LNCS.,
Springer (2010)
5. Awad, A., Weidlich, M., Weske, M.: Specication, verication and explanation of
violation for data aware compliance rules. In: Proc. of the 7th Int'l Joint Conf. on
Service-Oriented Computing. Volume 5900 of LNCS., Springer (2009) 500515
6. Awad, A., Decker, G., Weske, M.: Ecient compliance checking using BPMN-Q
and temporal logic. In: Proc. of the 6th Int'l Conf. on Business Process Manage-
ment. Volume 5240 of LNCS., Springer (2008) 326341
7. Liu, Y., Müller, S., Xu, K.: A static compliance-checking framework for business
process models. IBM Systems Journal
46
(2) (2007) 335261
8. Yu, J., et al.: Pattern based property specication and verication for service com-
position. In: Proc. of the 7th Int'l Conf. on Web Information Systems Engineering.
Volume 4255 of LNCS. (2006) 156168
9. Förster, A., Engels, G., Schattkowsky, T.: Activity diagram patterns for mod-
eling quality constraints in business processes. In: Proc of the 8th Int'l Conf.
on Model Driven Engineering Languages and Systems. Volume 3713 of LNCS.,
Springer (2005) 216
10. Ly, L.T., Rinderle, S., Dadam, P.: Semantic correctness in adaptive process man-
agement systems. In: Proc. of the 4th Int'l Conf. on Business Process Management.
Volume 4102 of LNCS., Springer (2006) 193208
11. Weber, I., Homann, J., Mendling, J.: Semantic business process validation. In:
Proc. of the 3rd Int'l Workshop on Semantic Business Process Management. (2008)
2236
12. Governatori, G., et al.: Detecting regulatory compliance for business process mod-
els through semantic annotations. In: Business Process Management Workshops.
Volume 17 of LNBIP., Springer (2008) 517
13. van der Aalst, W., Pesic, M.: DecSerFlow: Towards a truly declarative service
ow language. In: Proc. of the 3rd Int'l Workshop on Web Services and Formal
Methods. Volume 4184 of LNCS., Springer (2006) 123
14. Cousot, P., Cousot, R.: Abstract interpretation: A unied lattice model for static
analysis of programs by construction or approximation of xpoints. In: Proc. of
the 4th ACM Symp. on Principles of Programming Languages, ACM Press (1977)
238252
15. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Proc. of
the 9th Int'l Conf. on Computer Aided Verication, Springer (1997) 7283
16. Das, S.: Predicate Abstraction. PhD thesis, Stanford University (2003)
17. Model, F.S., Clarke, E., Lu, Y.: Counterexample-guided abstraction renement.
In: Computer Aided Verication. Volume 1855 of LNCS., Springer (2000) 154169
18. Dutertre, B., De Moura, L.: The YICES SMT solver. Tool paper at http://yices.
csl. sri. com/tool-paper. pdf (2006)
19. Bensalem, S., et al.: An overview of SAL. In: Proc. of the 5th NASA Langley
Formal Methods Workshop, NASA Langley Research Center (2000) 187196
20. Dadam, P., Reichert, M.: The ADEPT project: a decade of research and devel-
opment for robust and exible process support. Computer Science-Research and
Development
23
(2) (2009) 8197
