Business Process Management (Part-2 Business Process Modelling[Chapter VI Properties Of Business Processes ] ) Sec C -- By Mathias Weske

Soundness

The first soundness criterion for business processes was developed by Wil van
der Aalst in the context of workflow nets; but this criterion is also applicable to
other process modelling notations. For this, the execution semantics of these
languages have to be taken into account. If formal proofs are required, then
process languages with a formal execution semantics, such as workflow nets
are needed.

Motivation of Soundness

In order to motivate the soundness criterion, a number of workflow nets with
errors are discussed. Figure 6.4 shows a workflow net with two transitions
which exhibit an exclusive or split behaviour and an and join behaviour.
The exclusive or split transition t1 puts a token either in the upper input
place of t2 or in the lower input place of t2, but not in both places. As a
consequence, the and join transition t2 can never be enabled, because not all
input places have tokens. Therefore, cases based on the workflow net shown
will suffer from deadlock—no case will ever terminate.

While in a deadlock the activities involved can never be executed, in a
livelock situation a set of activities are trapped in an infinite loop. Livelock
can be the consequence of different types of errors in process models. If a
condition to enter a loop is always evaluated to true, then the loop is never
left. This type of error cannot be detected on the basis of process models.
Not only can erroneous conditions in decision nodes lead to livelock, but
also erroneous process structures, as shown in Figure 6.5. This workflow net
suffers from the fact that the loop is entered by an and split transition and not
by an exclusive or split transition. Therefore, the loop is repeatedly iterated,
realizing a livelock situation.
In addition to the livelock, this workflow net also suffers from the fact that
each time the loop is iterated, one token is put in the output place. Therefore,
a token in the output place no longer indicates the completion of the process.
A workflow net that suffers from different problems is shown in Figure 6.6.
Depending on the decision made by the exclusive or split transition t1, either
a deadlock or an improper termination occurs. If t2 puts a token on p1, then the and join transition t3 cannot be enabled, since there will not be a token
at place p3. As a consequence, a deadlock situation will occur.
If, however, t1 puts a token in p2, then t2 can fire, putting a token in
the output condition o. At this point, there is still a token in p3, showing a
situation similar to that in the previous case: the process instance does not
terminate properly because the process runs even after a token is put in the
final place.6.3.2 Definition
Based on these observations, soundness in workflow nets is defined. The idea
of the soundness criterion is to make sure that all tasks can participate in
a process instance; each process instance eventually terminates, and when it
terminates there is exactly one token in the final place.
In order to formally specify sound workflow nets, the following definition
on the states of a workflow net is useful.
Definition 6.2 Let PN = (P, T, F) be a workflow net, i 2 P be its initial
place, o 2 P its final place, and M,M0 markings.
• i is the state in which there is exactly one token in place i 2 P and no
token in any other place of the workflow net
• o is the state in which there is exactly one token in place o 2 P and no
token in any other place of the workflow net
• M M0 if and only if M(p) M0(p), 8p 2 P
• M > M0 if and only if M M0 ^ 9p 2 P : M(p) > M0(p)

Using these definitions, the soundness criterion can be specified in a formal
way.Definition 6.3 A workflow system (PN, i) with a workflow net PN =
(P, T, F) is sound if and only if
• For every state M reachable from state i there exists a firing sequence
leading from M to o, i.e.,
8M(i ! M) =) (M ! o)
• State o is the only state reachable from state i with at least one token in
place o, i.e.,
8M(i ! M ^M o) =) (M = o)
• There are no dead transitions in the workflow net in state i, i.e.,
(8t 2 T) 9M,M0 : i ! M t! M0

Reachability analysis can be used to decide whether a given workflow net
is sound. The idea of reachability analysis is that the states and the state
changes of process instances are represented explicitly. Reachability graphs
are used to represent the different states that a process instance can take.
A reachability graph consists of nodes and labelled edges, where the nodes
correspond to states of the workflow net and the edges represent state transitions.
State transitions occur by firing transitions. Therefore, each state transition
is labelled with the transition that realized this state transition.
Definition 6.4 A directed graph G = (V,E, l) is called a reachability graph
of a workflow net PN if V corresponds to the set of reachable states of the
workflow net and E V × V corresponds to state transitions. The mapping
l : E 7! P(T) assigns to each edge a set of transitions, such that (M,M0) 2
E , M t! M0 for each t 2 l(E).
This definition is illustrated by the example shown in Figure 6.7. The workflow
net shown represents a business process for handling claims. The initial
place of that workflow net is called claim, and ready is the final place. The
initial state is (1, 0, 0), where the tuple contains the number of tokens at the
(claim, record, ready) places, in that order.
Note that the state transitions involving the under consideration and ready
places can be achieved by firing either the pay transition or the send letter
transition. Hence l((0, 1, 0), (0, 0, 1)) = {pay, send letter}.
A workflow net with a loop is shown in Figure 6.8. The exclusive or split
transition B is used to decide whether or not to iterate the loop. Figure 6.9
shows the corresponding reachability graph. In this case, the loop in the workflow
net is reflected by a loop in the reachability graph.