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 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.
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.
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.
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.
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.