Abstract
In this thesis we focus on improving current modeling and verification techniques
for complex business processes. The objective of the thesis is to consider
several aspects of real-life business processes and give specific solutions to cope
with their complexity.
In particular, we address verification of a proper termination property for
workflows, called generalized soundness. We give a new decision procedure for
generalized soundness that improves the original decision procedure. The new
decision procedure reports on the decidability status of generalized soundness
and returns a counterexample in case the workflow net is not generalized sound.
We report on experimental results obtained with the prototype implementation
we made and describe how to verify large workflows compositionally, using
reduction rules.
Next, we concentrate on modeling and verification of adaptive workflows
— workflows that are able to change their structure at runtime, for instance
when some exceptional events occur. In order to model the exception handling
properly and allow structural changes of the system in a modular way, we introduce
a new class of nets, called adaptive workflow nets. Adaptive workflow
nets are a special type of Nets in Nets and they allow for creation, deletion and
transformation of net tokens at runtime and for two types of synchronizations:
synchronization on proper termination and synchronization on exception. We
define some behavioral properties of adaptive workflow nets: soundness and
circumspectness and employ an abstraction to reduce the verification of these
properties to the verification of behavioral properties of a finite state abstraction.
Further, we study how formal methods can help in understanding and designing
business processes. We investigate this for the extended event-driven
process chains (eEPCs), a popular industrial business process language used in
the ARIS Toolset. Several semantics have been proposed for EPCs. However,
most of them concentrated solely on the control flow. We argue that other aspects
of business processes must also be taken into account in order to analyze
eEPCs and propose a semantics that takes data and time information from
eEPCs into account. Moreover, we provide a translation of eEPCs to Timed
Colored Petri nets in order to facilitate verification of eEPCs.
Finally, we discuss modeling issues for business processes whose behavior
may depend on the previous behavior of the process, history which is recorded
by workflow management systems as a log. To increase the precision of models
with respect to modeling choices depending on the process history, we introduce
history-dependent guards. The obtained business processes are called historydependent
processes.We introduce a logic, called LogLogics for the specification
of guards based on a log of a current running process and give an evaluation
algorithm for such guards. Moreover, we show how these guards can be used in
practice and define LogLogics patterns for properties that occur most commonly
in practice.
Original language | English |
---|---|
Qualification | Doctor of Philosophy |
Awarding Institution |
|
Supervisors/Advisors |
|
Award date | 11 Dec 2007 |
Place of Publication | Eindhoven |
Publisher | |
Print ISBNs | 978-90-386-1166-2 |
DOIs | |
Publication status | Published - 2007 |