Soundness Theorem
Reachability analysis based on reachability graphs is a simple method to characterize
the cases that comply with a given workflow net. However, reachability
analysis only works well for small examples. The reachability graphs of
real world business processes involving dozens of activities suffer from state
explosion, which renders reachability graph analysis inappropriate in these
settings.
Besides manually creating a reachability graph and checking for the
three properties of workflow nets that collectively define soundness, there
are computer-supported ways to determine soundness. The first class of approaches
creates the reachability graph automatically and checks the soundness
property. Due to the state explosion problem, this approach suffers from
exponential run time behaviour. As a result, the creation of the reachability
graph might not be feasible for real-world applications.
But there are other options that take advantage of the rich set of tools
that have been developed by the Petri net community. In the reminder of this
section, one of these approaches is discussed. It is based on a theorem that boundedness.
The general idea is deriving a Petri net from the workflow net to be checked
for soundness, as sketched in Figure 6.10: By adding a transition t to a
workflow net PN, and linking the final place o to t and t to the initial place
i, a Petri net PN0 is created.
We can show that PN0 is live and bounded if and only if PN is sound. As
a consequence, existing techniques to analyze liveness and boundedness for
Petri nets can be used to check a workflow net for the soundness property.
For an important subclass of Petri nets, there are efficient analysis techniques
for liveness and boundedness. This renders the check for soundness of
workflow nets an efficient task, even for large workflow nets, which can be
found in real-world scenarios.
Theorem 6.1 A Workflow net PN = (P, T, F) is sound if and only if
(PN0, i), such that PN0 = (P0, T0, F0), P0 = P, T0 = T [ {t }, and
F0 = F [ {(o, t ), (t , i)}, is live and bounded.
To prove this theorem, we first show that if PN0 is live and bounded, then PN
is a sound workflow net. Then, it is shown that from the soundness property
of the workflow net, liveness and boundedness properties of the Petri net PN0
follow. The proof is illustrated in Figure 6.10.
Since PN0 is live, for each transition there is a firing sequence starting
in the initial state i that activates it. This is especially true for the added
transition t . Since o is the only input place of t , we can conclude that there
is a state M reachable from i with at least one token in o, i.e., M o.
When t fires, a token is put on the initial place i. Again, there is a firing
sequence that leads to a state in which there is a token in o. Since PN0 is
bounded, M = o, because otherwise tokens would aggregate in a place of the
Petri net.
Now we show that if PN is sound, PN0 is bounded. This is shown by
contradiction. Assume that PN is sound, but that PN0 is unbounded. Since
PN is sound and (by assumption) PN0 is unbounded, there exist states M,M0
such that i ! M ! M0 and M0 M, allowing the aggregation of tokens in
a place of PN0.
Since PN is a sound workflow net, there exists a firing sequence such
that i ! M ! o. Applying the same firing sequence to state M0 leads to
a state M00 > o. This means that in M00 there is a token in o; but there is
at least one additional token in the net! This is a violation of the soundness
property of PN and shows the contradiction.
Finally, we have to show that if PN is sound then PN0 is live. Soundness
implies that each transition can participate in a firing sequence leading from
the initial state i to the final state o. By firing t , the initial state i can be
reached, so that liveness of PN0 follows. For arbitrary Petri nets, liveness and boundedness are still complex to
compute, so that exponential run time behaviour can be expected. However, for an important subclass of Petri nets, liveness and boundedness can be
computed in polynomial time. This subclass is free choice nets. Free choice
nets have the property that the sets of input places of two transitions are
either disjoint or identical.
Saturday, March 20, 2010
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.
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.
Business Process Management (Part-2 Business Process Modelling[Chapter VI Properties Of Business Processes ] ) Sec B -- By Mathias Weske
Structural Soundness
In this section, the structure of business process models is investigated, and
an initial soundness criterion is introduced. While the considerations in this
section hold for process models represented in any of the process orchestration
languages introduced above, this section uses Petri nets, in most cases,
workflow nets, to represent these structural errors. The reasons are not only of
historical nature—workflow nets were the first approach for which soundness
was investigated—but also practical: the formal foundation of workflow nets
allows to formally specify and reason about soundness properties.
The type of structural error discussed in this section can be characterized
by dangling transitions or places, i.e., transitions without input places or output
places. Petri net with dangling places and transitions.
Notice that this Petri net is not a workflow net, since there are multiple places
without incoming edges and not all nodes, for instance, t5, are on a path from
i to o.
When a token enters the Petri net in place i, transition t1 is enabled. Note
that there is no way that t4 can ever be enabled. When t2 fires, t5 and t3
are enabled. When t3 terminates, the output place o is reached, signalling
the completion of the case. However, at this point in time, t5 could still be
running! As a consequence, the token at the output place o does not signal the
completion of the case. These types of errors are ruled out by the definition
of workflow nets.
This example motivates the development of correctness criteria for process
models to prevent the modelling errors discussed. The simplest correctness criterion uses the structure of business process models. It is inspired by the
definition of workflow nets and takes advantage of the definition of workflow
nets.
Definition 6.1 A process model is structurally sound if the following conditions
hold:
• There is exactly one initial node, which is the only node without any
incoming edges.
• There is exactly one final node, which is the only node without any outgoing
edges.
• Each node in the process model is on a path from the initial node to the
final node.
Structural soundness also goes well with the definition of business process
models, which states that business process models consist of related activities.
Structural soundness makes this relationship concrete by defining that each
activity is embedded in the context of the process and that no activities are
independent of other activities of the same business process.
Many business process languages enforce structural soundness, for instance,
event-driven process chains and business process diagrams expressed
in the Business Process Modeling Notation. However, the process designer has
the freedom to use these process languages to design process models that are
structurally sound.
In this section, the structure of business process models is investigated, and
an initial soundness criterion is introduced. While the considerations in this
section hold for process models represented in any of the process orchestration
languages introduced above, this section uses Petri nets, in most cases,
workflow nets, to represent these structural errors. The reasons are not only of
historical nature—workflow nets were the first approach for which soundness
was investigated—but also practical: the formal foundation of workflow nets
allows to formally specify and reason about soundness properties.
The type of structural error discussed in this section can be characterized
by dangling transitions or places, i.e., transitions without input places or output
places. Petri net with dangling places and transitions.
Notice that this Petri net is not a workflow net, since there are multiple places
without incoming edges and not all nodes, for instance, t5, are on a path from
i to o.
When a token enters the Petri net in place i, transition t1 is enabled. Note
that there is no way that t4 can ever be enabled. When t2 fires, t5 and t3
are enabled. When t3 terminates, the output place o is reached, signalling
the completion of the case. However, at this point in time, t5 could still be
running! As a consequence, the token at the output place o does not signal the
completion of the case. These types of errors are ruled out by the definition
of workflow nets.
This example motivates the development of correctness criteria for process
models to prevent the modelling errors discussed. The simplest correctness criterion uses the structure of business process models. It is inspired by the
definition of workflow nets and takes advantage of the definition of workflow
nets.
Definition 6.1 A process model is structurally sound if the following conditions
hold:
• There is exactly one initial node, which is the only node without any
incoming edges.
• There is exactly one final node, which is the only node without any outgoing
edges.
• Each node in the process model is on a path from the initial node to the
final node.
Structural soundness also goes well with the definition of business process
models, which states that business process models consist of related activities.
Structural soundness makes this relationship concrete by defining that each
activity is embedded in the context of the process and that no activities are
independent of other activities of the same business process.
Many business process languages enforce structural soundness, for instance,
event-driven process chains and business process diagrams expressed
in the Business Process Modeling Notation. However, the process designer has
the freedom to use these process languages to design process models that are
structurally sound.
Business Process Management (Part-2 Business Process Modelling[Chapter VI Properties Of Business Processes ] ) Sec A -- By Mathias Weske
Data Dependencies
Application data are an integral part of business processes. Data can be created,
modified, and deleted during the execution of business processes. Since
business processes consist of a set of activities that are related, these activities
operate on an integrated set of application data.
Data in business process models has two aspects, both of which need to
be covered:
• Data that activity instances manipulate by invoking applications or services.
• Data dependencies between process activities.
The former issue is dealt with in the operations subdomain. In service-oriented
systems architectures, for instance, the parameters of service invocations are
specified, so that data can be communicated correctly with software systems
at run time.
At the process level, data dependencies between process activities is typically
described by data flow. An example of data flow in a business process in
the financial sector is given. A credit approval business process contains activities
to enter a credit request, to assess the risks of granting the credit, and
to inform the customer about the decision made by the financial institution.
The activities of this process model operate on case data, in particular,
the credit request. The credit request can be represented by a record data
type with fields for the name and address of the credit requester, the amount
requested, and other information, such as the risk related to granting the
credit.
There are data dependencies between the activities mentioned. The Collect
Credit Info activity is the first activity performed. Only when this data
is available, can the risk be assessed in the Assess Risk activity, the final
decision be made(Decide), and the requestor be notified (Notify). Therefore,
the ordering of the activities in the business process is strongly related to the
data dependencies of the activities.
The process model is illustrated , using a graph-based process
language that explicitly represents input and output parameters of activities and data dependencies. Observe that the actual data transfer can be performed
by passing references to data objects or values of data objects, as
described the context of workflow data patterns.
This diagram shows that data dependencies have implications on the ordering
of activities in the process: the Assess Risk activity can be started only
when the credit information is available. Since this data object is provided as
output parameter CreditInfo of the Collect Credit Info activity, this activity
needs to complete before the risk can be assessed, implying an ordering
between these activities.
This example shows that data dependencies between process activities are
reflected by data flow. A data flow edge between an output parameter of one
activity and an input parameter of another activity represents the fact that
the latter activity requires a data value that the former generates. In the
example, the Collect Credit Request activity generates an output parameter
CreditInfo that the Assess Risk activity requires for its start.
If, as assumed so far, output parameter values are only available when the
respective activity terminates, there is a direct implication of data flow on
control flow. This property is known as control flow follows data flow, and it
is explained as follows.
Control flow needs to follow data flow, since otherwise the process instance
would come to halt. This observation is illustrated in an example
where a data dependency from the Assess Risk activity to the
Decide activity is shown, while the control flow constraint exists, for some
reason, in the opposite direction.
As a result, neither of these activities can be started, because control flow
defines that Assess Risk can only start after Decide has completed, and Decide
can only start after Assess Risk has generated the risk factor data value.
Because the risk factor value is only available when the activity terminates,
both activities are stuck in a permanent waiting condition, and a deadlock
situation has occurred. The process model results from a
modelling mistake, and the control flow follows data flow rule can be used to
detect these kinds of modelling mistakes.
These considerations hold only if it is assumed that an activity instance
requires its input parameters at the start. If this constraint is relaxed and
input parameters can be consumed after an activity instance has started,
then in a process with a data flow A ! B, B can actually start before A
terminates. At some point—when the input values are required—B needs to
wait for A to deliver the required data.
This assumption can also be relaxed at the producer side of data. If we
allow activities to generate data while they are running, then the generated
data can be taken by the follow-up activity, so that activities can execute
concurrently, realizing a data value stream between them.
While most workflow management systems assume that input data is available
up front and that only on completion, does an activity instance write
output data values, some approaches, for instance, the BPMN, relax this assumption.
The use of data dependencies for process enactment control will be discussed
in more detail in the context of case handling , where
data dependencies—and not the proce
Application data are an integral part of business processes. Data can be created,
modified, and deleted during the execution of business processes. Since
business processes consist of a set of activities that are related, these activities
operate on an integrated set of application data.
Data in business process models has two aspects, both of which need to
be covered:
• Data that activity instances manipulate by invoking applications or services.
• Data dependencies between process activities.
The former issue is dealt with in the operations subdomain. In service-oriented
systems architectures, for instance, the parameters of service invocations are
specified, so that data can be communicated correctly with software systems
at run time.
At the process level, data dependencies between process activities is typically
described by data flow. An example of data flow in a business process in
the financial sector is given. A credit approval business process contains activities
to enter a credit request, to assess the risks of granting the credit, and
to inform the customer about the decision made by the financial institution.
The activities of this process model operate on case data, in particular,
the credit request. The credit request can be represented by a record data
type with fields for the name and address of the credit requester, the amount
requested, and other information, such as the risk related to granting the
credit.
There are data dependencies between the activities mentioned. The Collect
Credit Info activity is the first activity performed. Only when this data
is available, can the risk be assessed in the Assess Risk activity, the final
decision be made(Decide), and the requestor be notified (Notify). Therefore,
the ordering of the activities in the business process is strongly related to the
data dependencies of the activities.
The process model is illustrated , using a graph-based process
language that explicitly represents input and output parameters of activities and data dependencies. Observe that the actual data transfer can be performed
by passing references to data objects or values of data objects, as
described the context of workflow data patterns.
This diagram shows that data dependencies have implications on the ordering
of activities in the process: the Assess Risk activity can be started only
when the credit information is available. Since this data object is provided as
output parameter CreditInfo of the Collect Credit Info activity, this activity
needs to complete before the risk can be assessed, implying an ordering
between these activities.
This example shows that data dependencies between process activities are
reflected by data flow. A data flow edge between an output parameter of one
activity and an input parameter of another activity represents the fact that
the latter activity requires a data value that the former generates. In the
example, the Collect Credit Request activity generates an output parameter
CreditInfo that the Assess Risk activity requires for its start.
If, as assumed so far, output parameter values are only available when the
respective activity terminates, there is a direct implication of data flow on
control flow. This property is known as control flow follows data flow, and it
is explained as follows.
Control flow needs to follow data flow, since otherwise the process instance
would come to halt. This observation is illustrated in an example
where a data dependency from the Assess Risk activity to the
Decide activity is shown, while the control flow constraint exists, for some
reason, in the opposite direction.
As a result, neither of these activities can be started, because control flow
defines that Assess Risk can only start after Decide has completed, and Decide
can only start after Assess Risk has generated the risk factor data value.
Because the risk factor value is only available when the activity terminates,
both activities are stuck in a permanent waiting condition, and a deadlock
situation has occurred. The process model results from a
modelling mistake, and the control flow follows data flow rule can be used to
detect these kinds of modelling mistakes.
These considerations hold only if it is assumed that an activity instance
requires its input parameters at the start. If this constraint is relaxed and
input parameters can be consumed after an activity instance has started,
then in a process with a data flow A ! B, B can actually start before A
terminates. At some point—when the input values are required—B needs to
wait for A to deliver the required data.
This assumption can also be relaxed at the producer side of data. If we
allow activities to generate data while they are running, then the generated
data can be taken by the follow-up activity, so that activities can execute
concurrently, realizing a data value stream between them.
While most workflow management systems assume that input data is available
up front and that only on completion, does an activity instance write
output data values, some approaches, for instance, the BPMN, relax this assumption.
The use of data dependencies for process enactment control will be discussed
in more detail in the context of case handling , where
data dependencies—and not the proce
Subscribe to:
Posts (Atom)
