Page 198 -

6 Declarative Workflow 189
6.2.6 Verification of Constraint Models

Verification techniques can be used for detection of possible errors in models. The
verification capabilities of YAWL will be described in Chap. 20. Just like for proce-
dural languages having formal semantics, constraint-based model expressed in LTL
allow for various kinds of analysis.
Certain combinations of constraints can cause errors in constraint models that
lead to undesirable effects at execution-time. We distinguish two types of constraint
model errors: dead tasks and conflicts.
A task in a constraint model is dead if none of the traces satisfying the model
contains this task, that is, the task cannot be executed in any instance of the model
without violating the specified (mandatory) constraints.

Definition 8 (Dead task). Let cm 2 U cm be a constraint model. Task t 2 T is dead
in model cm, if and only if 2 T W t 2 .
cm
Example 5 (Dead task). Figure 6.11a shows a ConDec model where tasks pickup
and bill are dead. This error is caused by the combination of the two precedence
constraints. While one precedence constraint specifies that task bill cannot be exe-
cuted before task pickup, the other precedence constraint specifies that task pickup
cannot be executed before task bill. Therefore, it will never be possible to execute
tasks pickup and bill in any instance of the model shown in Fig. 6.11a.

Dead tasks can easily be detected by analyzing the automaton generated for the
mandatory formula of a ConDec model. A task is dead if none of the transitions
in the automaton allow the execution of this task. Figure 6.11b shows the automa-
ton generated for the model in Fig. 6.11a. Indeed, this automaton does not contain
transitions that allow for the execution of tasks pickup and bill.
A constraint model contains a conflict if there are no traces that can satisfy the
model, that is, instances of the model can never become satisfied.

Definition 9 (Conflict). Model cm 2 U cm has a conflict if and only if T D ∅.
cm
Example 6 (Conflict). Figure 6.12a shows a ConDec model containing a conflict.
In addition to the constraints described in Example 5, there now is an additional

<> delivery (! bill) W pickup
!bill & !pickup
1..* & !delivery !bill & !pickup
delivery
precedence delivery
pickup bill
precedence S0 S5
(! pickup) W bill (b) Automaton for the model
(a) a ConDec model

Fig. 6.11 Tasks pickup and bill are dead