Page 30 -

1 Introduction 15

Fig. 1.8 Simplified architectural overview of the YAWL environment

theory and predicate logic, while the semantics has been defined in terms of a large
Colored Petri net (CPN), which can interpret YAWL specifications. This formal
foundation removes any ambiguity associated with the interpretation of complex
constructs and their interplay and also allows for the development of sophisticated
verification techniques that allow the detection of inherent flaws in an executable
process model before it is deployed (for a detailed treatment of verification in
YAWL see Chap. 20). While it is sometimes claimed that certain standards or oft-
used approaches have a formal foundation, the problem is usually that either (1) the
connection between the language and the formal theory remains unclear, or (2) the
formalization is not generally accepted, and certainly not by a standard body.
The importance of sophisticated flexibility support in BPM systems has long
been recognized. Because of the complexity of providing this support, it has taken
quite a long time for satisfactory solutions to become available. Flexibility require-
ments may take different forms. For example, exceptions may arise that were not
anticipated in advance, processes may be more easily captured by rules rather than
through an explicit representation of all possible execution paths, and processes may