Petri Nets-based Approaches for the Modelling and Verification
of Workflow Processes (Teza de Doctorat, coordonator: prof.dr.
Toader Jucan)
-----------------------------------
          
ABSTRACT
-----------------------------------
Starting with the late eighties, the industry began to focus 
on the idea of process in order to better organize and optimize 
the activity in large organizations.
The concept of a business process was defined in nineties by
Devenport and Short as a "set of logically related tasks performed 
to achieve a defined business outcome". A process is thus a conceptual 
way of organizing work and resources, defining "a specific ordering 
of work activities across time and place, with a beginning, an end, 
and clearly defined inputs and outputs". 
Business process management deals with the design, administration, 
configuration, enactment, and analysis of business processes.
In order to automatize business processes and support business process
management, a large number of software systems, called workflow man-
agement systems (WFMS's), has emerged in the past twenty years (e.g.
FLOWer, WebSphere, Staffware, MQSeries, etc). The main purpose of a
workflow management system is to support the definition, execution and
control of business processes.
A workflow process (or simply, workflow) is an abstraction of a business
process, which supports automated manipulation, such as modelling or enactment
by a workflow management system. An important characteristic of workflows 
is that they are case-based, where a case is defined as the subject
of operations in the process execution. A case is also called a workflow
instance. A workflow is structured into several perspectives:
- the process perspective specifies which tasks need to be executed and in
what order;
- the resource (or organization) perspective specifies the population in
which the workflow is executed (the resources) and the existing roles
(resource classes based on organisational or functional aspects);
- the data (information) perspective covers control data and production
data involved in a workflow;
- the task (function) perspective describes the elementary operations performed
by resources when they execute a task for a specific case;
- the operational (application) perspective describes the elementary actions/
operations performed by resources and applications in order to
create, read or modify control and production data.
Workflow management systems work with models of the workflow processes
(called workflow specifications), expressed in a certain modelling language.
There exist several workflow modelling languages which cover different perspectives
of a workflow. We can mention event-driven process chains, UML activity diagrams, 
flowcharts, BPEL, BPMN. These approaches do not have formal founded semantics 
and they do not address analysis issues. In order to reduce ambiguity and 
open possibilities for analysis, formal methods have been proposed for 
workflow specification: process algebra (\pi -calculus, CSP, CSS),
temporal logic, transactional logic, Petri nets.
Introduced by C. A. Petri, in 1964, Petri nets represent a well-known
formal method for modelling and verification of distributed systems, successfully
applied in different fields (manufacturing systems, real-time systems,
biological systems, hardware structures, telecommunications, protocols and
networks, programming languages, performance evaluation, etc). Due to
their formal semantics and their intuitive, graphical representation, Petri
nets proved to be one of the most convenient formalisms for modelling 
workflows. Throughout this thesis we will introduce several extensions of 
Petri nets in order to model and analyze workflows.
An important part of business process management is the analysis of
business processes, which aims to ensure the correctness and efficiency of
complex processes, before they are put into production. There exist several
types of analysis: validation is concerned with the differences between the
specified behaviour of the workflow process and its actual behaviour ; per-
formance analysis evaluates the ability of the workflow to meet requirements
with respect to throughput times in the execution of the tasks and to resource
utilization; verification is concerned with determining, in advance, whether a
workflow does not exhibit certain undesirable behaviours. Verification deals
with the logical correctness of workflow process definitions. Depending on
the workflow language used, there may be different properties, which have
to be satisfied. Usually, these properties concern the process perspective of
workflows.
A lot of research has been devoted to the verification problem and many 
analysis techniques have been developed for proving certain desirable 
properties of workflows. One of the required correctness criteria is the 
proper termination: this property implies that the workflow
is able to process completely any case and no garbage is left after the case
is completed. Another requirement is that any of the tasks involved in the
process must be able to execute at a certain time. These two conditions
form what is called the soundness property for workflows. Soundness has
been widely adopted in literature as the minimal logical criterion a workflow
should satisfy.
In what follows we present the issues addressed by this thesis in the area
of workflow modelling and verification.
One of the problems we approach is the modelling and verification of
the resource constrained workflows. In the past years a lot of research has
been devoted to workflow technology and workflow management systems,
most of this research focusing especially on the modelling of the process
perspective and (of) the data perspective of workflows. A well-known class
of Petri nest successfully used for modelling the process perspective is the
class of workflow nets. Despite their simple structure, workflow nets
have many interesting properties and sufficient expressive power in order to
capture the complex execution patterns which may appear in the process
perspective of workflows. Also, the soundness property was proved to be
decidable for workflow nets.
Although the existing resources in the organization represent a crucial
aspect in the execution of the workflow, less attention has been devoted to
the resource perspective. There exists a number of Petri net based approaches
for modelling resources in workflows: some approaches focus on the resource
perspective alone, abstracting from the process perspective; the
approaches from take into consideration the resource perspective
of the workflows but do not address the verification problem, focusing on
performance issues; the approach in [...] considers the verification problem for
resource constrained workflows, but the resource perspective is represented
in a simplistic manner. Also, in all the mentioned approaches, there is an
unclear mixture between the process and the resource perspective.
This thesis proposes a special class of Petri nets, Resource Workflow Nets,
for the modelling and verification of the workflows in which both the process
and the resource perspective are considered. We study the notion of soundness
for resource workflow nets, taking into consideration the influence of
resources over the execution of tasks.
Another issue this thesis addresses is the modelling and verification of
interorganizational workflows. In the past ten years, due to the development
of virtual enterprises, electronic commerce and internet technologies, many
existent business processes involve more than one organization. These workflows,
distributed over a number of different organizations, are referred to
as interorganizational workflows. An interorganizational workflow consists of
several processes belonging to different organizations, which must interact in
order to accomplish a common goal. There are several forms of interoperability
between processes (capacity sharing, chained execution, subcontracting,
case transfer, loosely coupled). The thesis focuses on the modelling and verification
of loosely coupled interorganizational workflows in which the number
of component processes may vary over time, due to the fact that certain
processes may interrupt abnormally their execution.
There is a large number of XML-based languages proposed for the specification
of interorganizational workflows (BPEL4WS, BPEL4Chor, WSCDL,
etc), but they lack a formal semantics and they are not suited for verification
purposes. In order to overcome this problem, several formal methods
have been proposed so far (abstract state machines, finite state automata, 
process algebra, Petri nets.
We will focus on Petri nets, as they have already been successfully used for
the modelling and verification of workflows inside an organization. The existing
approaches consider interorganizational workflows with a fixed structure
(i.e. the number of component workflows remains the same throughout the
execution of the interorganizational workflow). Also, in many of the existing
approaches, the component workflows and the interaction between them
are all described in the same Petri net, which makes the model difficult to
understand, modify and analyze.
In this thesis we propose dynamic interorganizational workflow nets (DIWFnets)
for modelling interorganizational workflows with dynamic structure: we
consider the case in which the component workflows interrupt abnormally
their execution and they are removed from the interorganizational workflow.
We define a notion of soundness for DIWF-nets, expressing the minimal
conditions an interorganizational workflow with dynamic structure should
satisfy. We prove that soundness is decidable for DIWF-nets.
Finally, we will propose a Petri net model for interorganizational workflows
in which the resource perspective of every component workflow involved
is represented explicitly. None of the existing formal approaches for the modelling
and analysis of interorganizational workflows takes into consideration
the influence of resources in the execution of the processes.
We propose resource interorganizational workflow nets (RIWF-nets) for
modelling resource constrained interorganizational workflows. In this case,
the structure of the interorganizational workflow is fixed (all of the component
workflows remain in the interorganizational workflow until they finish
their execution). Our model allows the representation of both the resource
perspective and the process perspective of the workflows involved and it permits
the sharing of resources across workflows. As in the case of RWF-nets
and DIWF-nets, we define and study a notion of soundness for RIWF-nets.
          
SPEAKER(S)
-----------------------------------
Asist.dr. Oana Otilia PRISECARU
Universitatea Alexandru Ioan Cuza, Facultatea de Informatica
Iasi
Romania
-----------------------------------