Information Technology Reference
In-Depth Information
constraints, which include a non-deterministic future, as e.g. formalizing a quality con-
straint or a part of it which must not hold for all control flows in a business process, but
for at least one control flow.
Our goal in this paper is to overcome the expressiveness limitations concerning the
branching logic, by allowing to formalize non-deterministic user-defined quality con-
straints, and to make this formalization intuitively understandable for business process
users. For this reason, we have investigated the formalization approaches, which are
based on UML Activity Diagrams [3], since these diagrams are a widely used standard
and are familiar to business process users. One of these approaches is developed in [2].
It models business processes as UML 2.0 Activity Diagrams, and quality constraints as
business process patterns using the Process Pattern Specification Language (PPSL) [4],
which is a light weight extension of UML Activity Diagrams. Both business processes
and business process patterns are then written in a formal way by transforming UML
2.0 Activity Diagrams into labeled transition systems, and translating business pro-
cess patterns into LTL-formulas [5]. This enables the automated verification of quality
constraints on business processes by using a model checker to verify LTL formulas on
labeled transition systems. However, the Linear Temporal Logic (LTL) does not support
the non-deterministic future. To support this kind of future, we replace LTL by the Com-
putation Tree Logic (CTL) [6]. To achieve that, we extend PPSL to a new visual model-
ing language, Extended Process Pattern Specification Language (EPPSL), which has a
formally defined semantics given by a translation into CTL-formulas. EPPSL is a heavy
weight extension of UML Activity Diagrams. In other words, EPPSL uses the elements
of UML Activity Diagrams, which semantics can serve to model quality constraints. It
also defines new classes of elements to cover the semantics of quality constraints which
are not defined by UML Activity Diagrams. We also provide a pattern-based translation
for EPPSL models into CTL-formulas. In the following section, we give an overview
of the related work. In Section 3, we provide a scenario for verifying business process
quality constraints. In Section 4, we describe the modeling elements of EPPSL and how
to use them for composing EPPSL models. In Section 5, we explain how to translate
EPPSL models into CTL-formulas. In Section 6, we provide a conclusion and outlook
for our approach.
2
Related Work
Modeling and formalizing business process constraints in order to verify their correct-
ness are considered in several approaches. For example, PPSL is introduced in [4] and
translated in [2] into LTL formulas. In [7], the graphical Business Property Specifica-
tion Language is used to capture business process compliance rules, which are trans-
lated into LTL. In [8], DecSerFlow is mapped on LTL. DECLARE is defined in [9] and
[10]. DECLARE models are also translated into LTL. BPMN-Q is developed in [11]
to model requested compliance rules on business processes as queries. These queries
are translated in [12] into PLTL [13][14] formulas. BPMN is used in [15] to check the
semantic correctness of business process models by mapping them to Petri nets. In [16],
the Object Constraint Language [17] expressions are used to refer to an integrated meta-
model for different process models. In [18], process-independent compliance rules are
