=Paper=
{{Paper
|id=None
|storemode=property
|title=SeaFlows Toolset - Compliance Verification Made Easy
|pdfUrl=https://ceur-ws.org/Vol-592/PaperDemo05.pdf
|volume=Vol-592
|dblpUrl=https://dblp.org/rec/conf/caise/LyKRGRD10
}}
==SeaFlows Toolset - Compliance Verification Made Easy==
https://ceur-ws.org/Vol-592/PaperDemo05.pdf
SeaFlows Toolset
Compliance Veri cation Made Easy?
1 1 2 3
Linh Thao Ly , David Knuplesch , Stefanie Rinderle-Ma , Kevin Göser ,
1 1
Manfred Reichert , and Peter Dadam
Institute of Databases and Information Systems
1
Ulm University, Germany
{thao.ly,david.knuplesch,manfred.reichert,peter.dadam}@uni-ulm.de
2
Faculty of Computer Science
University of Vienna, Austria
stefanie.rinderle-ma@univie.ac.at
3
AristaFlow GmbH, Germany
kevin.goeser@aristaflow.com
Abstract. In the light of an increasing demand on business process
compliance, the veri cation of process models against compliance rules
has become essential in enterprise computing. The SeaFlows Toolset fea-
tured in this tool demonstration extends process-aware information sys-
tem by compliance checking functionality. It provides a user-friendly en-
vironment for modeling compliance rules using a graph-based formalism.
Modeled compliance rules can be used to enrich process models. To ad-
dress a multitude of veri cation settings, SeaFlows Toolset provides two
compliance checking components: The structural compliance checker de-
rives structural criteria from compliance rules and applies them to detect
incompliance. The data-aware compliance checker addresses the state
explosion problem that can occur when the data dimension is explored
during compliance checking. It performs context-sensitive automatic ab-
straction to derive an abstract process model which is more compact
with regard to the data dimension enabling more e cient compliance
checking. Altogether, SeaFlows Toolset constitutes a comprehensive and
extensible framework for compliance checking of process models.
Key words: Compliance rules, Process veri cation, Tool support, Data-awareness
1 Introduction
In the light of an increasing demand on business process compliance [1], the
veri cation of process models within process-aware information systems against
?
This work was done in the research project SeaFlows which is partially funded by
the German Research Foundation (DFG).
2 L.T. Ly, D. Knuplesch, S. Rinderle-Ma, K. Göser, M. Reichert, P. Dadam
compliance rules has become essential in enterprise computing. To ensure com-
pliance with imposed rules and policies, compliance audits for process models
are necessary. Due to increasing complexity of process models [2] manual compli-
ance veri cation is hardly feasible. Tool support is particularly needed in order
to deal with changes at dierent levels. On the one hand, changes and evolution
of regulatories and policies may occur, leading to changes in implemented com-
pliance rules. On the other hand, changes to business processes may take place,
resulting in changes of implemented process models. This further necessitates
tool support for (semi-)automatic compliance veri cation.
The toolset featured in this tool demonstration resulted from our research
in the SeaFlows project. In this project, we aim at providing techniques to
enable compliance with imposed regulatories throughout the process lifecycle.
This inludes compliance cheking of business process models at buildtime but
also compliance monitoring of process instances at runtime [3]. With the im-
plementation of SeaFlows Toolset, so far, we have realized concepts addressing
compliance checking of process models at buildtime. The particular components
shown in this tool demonstration enable modeling compliance rules as visual
compliance rule graphs as well as verifying process models against imposed com-
pliance rules [4]. To support a variety of veri cation scenarios and to exploit
their speci c properties, SeaFlows Toolset comprises several veri cation compo-
nents: a structural compliance checker, enabling e cient compliance veri cation
for block-structured process models and a data-aware compliance checker, en-
abling data-aware compliance checking using model checking techniques.
In the following, the particular components of SeaFlows Toolset are intro-
duced. Related work is discussed in Sect. 3 before we close the paper with an
outlook on future developments in Sect. 4
2 SeaFlows Toolset
SeaFlows Toolset extends process-aware information system (PAIS) by compli-
ance checking functionality. Fig. 1 depicts the interplay between existing infras-
tructure stemming from PAIS (e.g., activity repository, process modeling tool,
and process model repository) and components introduced by SeaFlows Toolset .
2
The SeaFlows Graphical Compliance Rule Editor (cf. Fig. 1) allows to
model compliance rules over process artifacts as compliance rule graphs [4] (cf.
Sect. 2.1). By interacting with the activity repository responsible for organizing
and managing process artifacts relevant within a business domain, the Graphi-
cal Compliance Rule Editor enables compliance rule modeling over exactly the
process artifacts available in the domain. Thus, we can enrich process models by
compliance rules that are imposed on the corresponding business process. This
can be done at an early stage, when the process is modeled to enable compliance
by design. Compliance rules may be also assigned to a completed or released
process model to perform compliance audits.
2
The Rule Graph Execution Engine for executing compliance rule graphs is currently
under implementation
SeaFlows Toolset 3
Activity Process Model
Repository Repository
Process
Execution
Engine
Seaflows Graphical
Process
Compliance Rule
Modeling Tool
Editor
SeaFlows
Compliance Rule Seaflows Compliance Checkers
Repository
Compliance
Process model Structural Data-Aware Rule Graph
rule graphs
enriched by Compliance Compliance Execution
compliance Checker Checker Engine
rule graphs
Fig. 1. Overall infrastructure around the SeaFlows Toolset
SeaFlows Toolset currently comprises two compliance checking components
to verify process models (cf. Fig. 1), namely the Structural Compliance Checker
and the Data-aware Compliance Checker. By interacting with the process model-
ing tool of PAIS, the SeaFlows compliance checkers enable the process designer to
verify process models already during process design. Meaningful compliance re-
ports help the process designer to identify incompliant process behaviour. Based
on them, the process designer may further modify the process model until in-
compliance is resolved.
To transfer our concepts into a comprehensive prototype, we opted to base
our implementation on the commercial process management system AristaFlow
BPM Suite orginated from research activities in the ADEPT project [5].
AristaFlow BPM Suite provides a powerful API which enables us to extend
existing PAIS functionality by compliance checking mechanisms in an elegant
manner. Thus, SeaFlows compliance checking components are smoothly inte-
grated into the process modeling environment of AristaFlow BPM Suite. In the
following, the components of SeaFlows Toolset (cf. Fig. 1) and underlying con-
cepts are discussed in more detail.
2.1 Graphical Compliance Rule Editor and Compliance Rule
Repository
We developed a graph-based compliance rule speci cation language that enables
modeling compliance rules in a manner similar to process modeling. Designed to
support intuitive compliance rules modeling, compliance rule graphs are modeled
by linking nodes representing absence and occurrence of activity executions of
certain types [4]. In particular, (sub-)graphs are used to respresent an antecedent
pattern that activates the compliance rule and corresponding required conse-
quence patterns. This enables modeling frequent compliance rule patterns [6, 7]
in a straightforward manner. Further, compliance rule graphs can be enriched
with annotations of temporal constraints (e.g., minimal temporal distance) as
well as data conditions.
The Graphical Compliance Rule Editor provides a user-friendly environment
for modeling compliance rule graphs (cf. Fig. 2). Nodes of compliance rule graphs
4 L.T. Ly, D. Knuplesch, S. Rinderle-Ma, K. Göser, M. Reichert, P. Dadam
Fig. 2. The SeaFlows Graphical Compliance Rule Editor
are assigned to activity types available in the activity repository (cf. Fig. 1). Mod-
eled compliance rule graphs are exported as separate XML- les which enables
their organization within rule sets in the Compliance Rule Repository. In addi-
tion, versioning of compliance rules is also supported by the repository. Being
implemented based on Eclipse Modeling Framework, modeled compliance rule
graphs are based on a de ned data object model that facilitates their import
and processing in compliance checking tools.
2.2 Structural Compliance Checker
The basic idea underlying the Structural Compliance Checker is to e ciently
verify process models by automatically deriving criteria on the process struc-
ture from compliance rules [8]. Following the dynamic programming paradigm,
for each compliance rule a set of simple binary structural criteria (such as A
excludes B) whose satisfaction ensure compliance with the corresponding rule
is derived. By checking the process model for compliance with these derived
criteria, we can identify the criteria not ful lled by the process model. This is
useful information to generate intelligible textual feedback in case incompliance
is detected. Based on the results of checking the structural criteria, the Struc-
tural Compliance Checker is able to provide detailed diagnosis that is helpful to
locate incompliance (cf. Fig. 3). For example, the feedback Fig. 3 indicates that
shipping insurance is optional to production in the process model. This detailed
diagnosis can further be applied to resolve incompliance.
By making assumptions on the veri cation setting (e.g., unique label as-
sumption) and exploiting the block-structure of process models the Structural
Compliance Checker identi es incompliance in an e cient manner.
SeaFlows Toolset 5
Fig. 3. The SeaFlows Structural Compliance Checker integrated into AristaFlow Pro-
cess Template Editor
The Structural Compliance Checker is implemented as Eclipse-plug-in for
AristaFlow Process Template Editor and thus, is smoothly integrated into the
process modeling environment. Therefore, compliance checks on the y during
process modeling can be carried out to support compliance by design.
2.3 Data-aware Compliance Checker
The Data-aware Compliance Checker is able to deal with data-aware compliance
rules and data conditions in process control ow. The challenge with data-aware
compliance checking is that the exploration of the data dimension during com-
pliance checking can lead to state explosion and thus, to intractable complexity.
To tackle this, we developed a process-meta-model-independent approach for
automatic context-sensitive (i.e., rule-speci c) abstraction (cf. Fig. 4 B). By an-
alyzing the data conditions contained in the compliance rule and in the process
model, it reduces the state space of the data dimension to be explored during
veri cation. The obtained abstract process model and abstract compliance rule
are given as input to the actual compliance checking procedure (cf. Fig. 4 A).
For compliance checking we used a model checker. In case of violation, the coun-
terexample obtained from the model checker is conretized to yield not only the
incompliant execution but also the its data conditions.
The Data-aware Compliance Checker rst performs automatic abstraction,
then transforms the abstract process model into a state space representation.
6 L.T. Ly, D. Knuplesch, S. Rinderle-Ma, K. Göser, M. Reichert, P. Dadam
B
abstract A
process
model process model automatic
automatic processing
compliance concretization
abstraction to compliance
checking for user
reduce complexity abstract data- report
data-aware feedback
compliance aware
rules compliance rules
Fig. 4. Abstraction and concretization as pre- and postprocessing steps to the actual
data-aware compliance checking
The latter is then passed to the model checker SAL [9], which carries out the ex-
ploration of the abstract process model. In case compliance violation is detected,
the Data-aware Compliance Checker retransforms the counterexample output of
the model checker and visualizes it as an execution trace and as process graph.
Similar to the Structural Compliance Checker, the Data-aware Compliance
Checker is directly integrated into the process modeling environment. 17.000
lines of code and the class hierarchy comprising about 70 interfaces and 210
classes indicate its complexity. Automatic abstraction is supported for domains
of numbers and for large domains of object references.
counterexample
as process log
original
process graph
counterexample as
process graph
visualization of the
counterexample’s steps
data-aware
compliance rules
Fig. 5. The Data-aware Compliance Checker visualizes the counterexample as execu-
tion trace and process graph
SeaFlows Toolset 7
3 Related Work
Three major challenges arise from compliance veri cation of process models:
compliance rule modeling, veri cation techniques, and feedback generation. The
concepts implemented in SeaFlows Toolset address all three issues. Existing ap-
proaches for modeling compliance rules range from rather informal annotations
of process models with compliance rules, over formal languages [10], to visual
patterns and languages [11, 12, 13]. With the compliance rule graphs, we opted
for a compositional graph-based modeling formalism that supports the typical
antecedent-consequence-structure of rules.
For compliance veri cation, model checking is often applied in literature [12,
13, 10]. As advantage we obtain an approach that is not speci c to a particu-
lar process meta-model or process modeling notation. One challenge of model
checking, however, is the generation of meaningful feedback from the report (e.g.,
counterexample) provided by the model checker. SeaFlows Toolset implements
two compliance checking approaches, one based on model checking and another
based on structural criteria, that complement each other.
Some approaches address the veri cation of data-aware compliance rules [11,
12]. However, the state explosion problem arising from exploration of the data
dimension is not addressed by these approaches. In SeaFlows Toolset we imple-
mented an abstraction approach that serves as preprocessing step to the actual
data-aware compliance checking to limit state explosion.
[7] addresses visualization of incompliance by querying the process model
for anti-patterns that are de ned for each compliance rule pattern. In our ap-
proach, structural criteria are automatically derived from the compliance rule
by the Structural Compliance Checker. Checking the structural criteria allows
for identifying precisely the structural reason for incompliance.
Similar to DECLARE [14], the declarative process management system,
SeaFlows enables to model graphical compliance rules. In DECLARE constraints
are mapped onto formula in temporal logic and then to nite automata in order
to execute constraint-based work ows. In contrast, SeaFlows compliance rule
graphs are used to verify process models.
SeaFlows Toolset can be further complemented by other process analysis
tools, such as the process mining framework ProM [15] to provide comprehensive
support of compliance checking a priori as well as a posteriori.
4 Summary and Outlook
SeaFlows Toolset featured in this tool demonstration extends process-aware in-
formation system by compliance checking functionality. It enables modeling com-
pliance rule as graphs independently from speci c process models by making
use of an activity repository. Process models can be enriched by compliance
rules for documentation purposes and for compliance veri cation. Two compli-
ance checkers, the Structural Compliance Checker and the Data-aware Compli-
8 L.T. Ly, D. Knuplesch, S. Rinderle-Ma, K. Göser, M. Reichert, P. Dadam
ance Checker, addressing speci c compliance veri cation scenarios (e.g., data-
awareness) complement each other and thus, ensure broad applicability.
In our future work, we will further extend SeaFlows Toolset to provide sup-
port for compliance checking during process execution (cf. the SeaFlows Rule
Graph Execution Engine in Fig. 1). In addition, SeaFlows Toolset will be ex-
tended by a visualization and explanation component to provide advanced user
feedback.
References
1. Sadiq, S., Governatori, G., Naimiri, K.: Modeling control objectives for business
process compliance. In: Proc. BPM '07. (2007) 149164
2. Bobrik, R., Reichert, M., Bauer, T.: View-based process visualization. In: Proc.
of the 5th Int'l Conf. on Business Process Management (BPM'07). Volume 4714
of LNCS. (2007) 8895
3. Ly, L.T., Rinderle-Ma, S., Dadam, P.: On enabling integrated process compliance
with semantic constraints in process management systems. Information Systems
Frontiers , accepted for publication.
4. Ly, L.T., Rinderle-Ma, S., Dadam, P.: Design and veri cation of instantiable com-
pliance rule graphs in process-aware information systems. In: The 22nd Int'l Conf.
on Advanced Information Systems Engineering (CAiSE'10). (2010) accepted for
publication.
5. 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
6. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property speci cations for
nite-state veri cation. In: Proc. ICSE'99. (1999) 411 420
7. Awad, A., Weske, M.: Visualization of compliance violation in business process
models. In: Proc. BPM Workshops. (2009)
8. Ly, L.T., Rinderle-Ma, S., Dadam, P.: Integration and veri cation of semantic con-
straints in adaptive process management systems. Data & Knowledge Engineering
64 (2007) 323
9. Bensalem, S., et al.: An overview of SAL. In: Proc. of the Fifth NASA Langley
Formal Methods Workshop, NASA Langley Research Center (2000) 187196
10. Ghose, A., Koliadis, G.: Auditing business process compliance. In: ICSOC '07.
Volume 4749 of LNCS., Springer (2007) 169180
11. Awad, A., Weidlich, M., Weske, M.: Speci cation, veri cation and explanation
of violation for data aware compliance rules. In: Proc. ICSOC/ServiceWave'09.
(2009) 500515
12. Liu, Y., Müller, S., Xu, K.: A static compliance-checking framework for business
process models. IBM Systems Journal 46(2) (2007) 335261
13. Förster, A., et al.: Veri cation of business process quality constraints based on
visual process patterns. In: Proc. 1st Joint IEEE/IFIP Symposium on Theoretical
Aspects of Sofware Engineering. (2007)
14. Pesic, M., Schonenberg, M., Sidorova, N., van der Aalst, W.: Constraint-based
work ow models: Change made easy. In: OTM 2007, Part I. Number 4803 in
LNCS, Springer-Verlag (2007) 7794
15. van der Aalst, W., et al.: ProM 4.0: Comprehensive support for real process anal-
ysis. In: Proc. ICATPN'07. Volume 4546 of LNCS., Springer (2007) 484494