Verification in YAWL
Verification is concerned with determining, in advance,
whether a process model exhibits certain desirable behaviours.
By performing this verification at design time, it is possible to
identify potential problems, and if so, the model can be modified
before it is used for execution. Although one would expect verification functionality to be present in any
business process modelling tool, workflow management system,
or business process management suite, this is not the case.
At best these systems do some basic
syntactical checks, but allow for the modelling of processes with deadlocks,
livelocks, and other anomalies. There are several academic
process verification tools. However, until recently, these tools
could not verify realistic processes because they assume highly simplified
models completely disconnected from real-life languages and systems.
Fortunately, a breakthrough has been realized
that makes process verification feasible in a practical setting. Sophisticated verification
techniques for process models with cancellation and OR-joins have been developed in the context of the workflow
language YAWL.
The YAWL editor supports two verification approaches:
- Verification using reset nets
- Verification using invariants
Verification approach using reset nets
There are established results related to the verification of workflows using Petri nets. We explore how these results can be used for YAWL workflows with cancellation and OR-joins. Reset nets form a natural foundation for workflow languages with explicit support for cancellation as the behaviour of reset arcs closely matches the behaviour of cancellation regions.
For verification purposes, the YAWL processes are divided into those with OR-joins and those without OR-joins. This distinction is necessary as a different verification technique is needed in each case. A process without OR-joins is mapped to a reset net and verification is performed on the resulting reset net. However, due to the non-local semantics of OR-joins, it is not possible to map a YAWL workflow with OR-joins to a reset net (without some approximation) and it is not possible to detect the soundness property for a YAWL net with OR-joins using verification techniques available for reset nets. Therefore, an alternative verification technique using the YAWL formal semantics is used. These algorithmic approaches have been derived using the state space analysis and the notions of coverability and reachability. Reduction rules have been used as a means of improving the
efficiency of the algorithm.
Four desirable properties for processes
with cancellation regions and OR-joins are proposed. These are
While soundness and weak soundness properties concentrate on the
correctness of the models, the other two properties;
irreducible cancellation regions and immutable
OR-joins, focus on detecting the existence of unnecessary
cancellation regions and OR-joins in the process models.
Verification menu
Verification functionality can be invoked from the "Analyse specification" menu item under the specification menu of the YAWL Editor.
Figure 1 shows the configuration menu for verification options.
Figure 1: Configuration menu in the YAWL Editor
Soundness property
There are certain desirable characteristics that every business process is expected
to exhibit. Firstly, it is important to know that a process, when
started, can always complete (Option to complete). Secondly, it
should not have any other tasks still running for that process
when the process ends (Proper completion). Thirdly, the process
should not contain tasks that will never be executed (No dead
transitions}). The combination of these three desirable properties
is known as the soundness property.
The two nets representing composite tasks Main assessment and Check basic requirements are nets without OR-joins. Thus,
reset analysis is used to detect the soundness property for these
nets. For nets with OR-joins and a finite reachability graph,
reachability analysis is carried out using the YAWL semantics.
Figure 2 shows a screenshot of the
YAWL editor with results of the soundness property check. The three
nets (Overview, Check basic requirements and
Perform main assessment, Allocate marks) are shown to satisfy the
soundness property and observation messages are provided to
indicate that these nets satisfy all three criteria.
Figure 2: Soundness property check
Weak soundness property
For certain processes with
OR-joins and cancellation regions having an infinite state
space, it is not possible to detect this soundness property,
i.e., although soundness is decidable for most models the soundness property is undecidable in the general case. Thus, a weaker
notion of soundness, known as the weak soundness
property is proposed instead. The weak soundness property relaxes
the option to complete criterion, to say that, is it possible to
complete a process in some cases, when started? (Weak
option to complete). Therefore, if a process model is sound, it
will also be weak sound, but not vice versa.
A net satisfies the weak
soundness property if and only if it has the weak option to
complete, proper completion and no dead transitions. The weak
soundness property check is performed using reset net
coverability analysis for nets with and without OR-joins. For
nets with OR-joins, only limited results are available.
Figure 3 shows a screenshot from
the editor with the results of the weak soundness property check
for all nets. We can see that all nets satisfy the weak soundness
property.
Figure 3: Weak soundness property check
Irreducible cancellation regions property
Reducible elements in a cancellation region represent elements that can
never be cancelled while that task is being executed (e.g.
conditions may never contain tokens). For example, if a model
contains truly alternative branches and one path contains a task
that covers some places and conditions from the other path within
its cancellation region, then those places and transitions are
superfluous as there will never be tokens to remove when the task
is executing. A process satisfies the irreducible
cancellation regions property if there are no reducible elements
in any of its cancellation regions.
An element within a cancellation region of a task is not necessary
if that element can never be marked when the task is being
executed. Such elements are called reducible because they can be
removed without changing the behaviour. To decide the irreducible
cancellation regions property of a net without OR-joins, analysis
on the corresponding reset net is performed.
The cancellation region for the Stop checks task includes the
Finalise basic requirements check task. As Finalise
basic requirements check is an AND-join task, it can never be
executed while the Stop checks task is being executed.
Therefore, it should not be in the cancellation region of the
Stop checks task. This is reported by the YAWL editor as shown in Figure 4.
Figure 4: Irreducible cancellation regions property check
Immutable or-join property
As the runtime analysis of OR-join tasks is
time-consuming and (computationally) expensive, it is desirable to determine at
design time whether a more appropriate join structure could be
found for a given model. A convertible OR-join task is an OR-join task for which it
is never possible to mark more than one input condition
(the task acts as an XOR-join) or when all the input
conditions are always marked (the task acts as an AND-join).
Such OR-joins should be replaced by XOR/AND-joins to better reflect their
role in the process and to improve the execution speed.
A process satisfies the immutable OR-joins property if
there are no convertible OR-joins in the net.
An immutable OR-join
is one that could not be replaced by either an XOR-join or an
AND-join. In Figure 5, the
split behaviour of the task Decide applicable categories has been changed from OR-split to AND-split for testing purposes.
As the net now contains an AND-split followed by an OR-join, the
OR-join should be more appropriately modelled as an AND-join.
Figure 5: Immutable OR-join property check
|
