We present a ̄exible framework that enables work ̄ow systems to adapt to changing conditions. The model is designed to reveal key aspects of the tasks involved in representing and enacting business processes. These fundamental characteristics are identi®ed as state, behaviour, distribution, coordination and enactment. By isolating such core concepts in a way that allows them to be varied, we open up the general process of task coordination and execution, allowing for extensions in a planned way. By suitable manipulation of each of these aspects, at the appropriate level, a work ̄ow system may be extensively modi®ed in a way that minimises the e€ect of such change upon other aspects of the system. Ó 2000 Published by Elsevier Science B.V. All rights reserved.

The goal of this paper is to demonstrate that process verification has matured to a level where it can be used in practice. Earlier techniques assumed simplified process models without the more advanced constructs available in today’s modelling languages (e.g., cancellation and OR-joins). This paper reports on new verification techniques that can be used to assess the correctness of real-life models. The proposed approach relies on using formal methods (i.e., mapping a business model to a reset net which is an extension of Petri nets, and performing state space analysis) to determine the correctness of business processes with cancellation and OR-joins. The paper also demonstrates how reduction rules can be used to improve the efficiency. We present these techniques in the context of the workflow language YAWL that provides direct support for 20 most frequently used patterns found today (including cancellation and OR-joins). But the results also apply to other languages with these features (e.g., BPMN, EPCs, UML activity diagrams, etc.). We have developed an editor that provides diagnostic information based on the techniques presented in this paper.

Workflow languages offer constructs for coordinating tasks. Among these constructs are various types of splits and joins. One type of join, which shows up in various incarnations, is the OR-join. Different approaches assign a different (often only intuitive) semantics to this type of join, though they do share the common theme that branches that cannot complete will not be waited for. Many systems and languages struggle with the semantics and implementation of the OR-join because its non-local semantics require a synchronization depending on the analysis of future execution paths. The presence of cancelation features, potentially unbounded behavior, and other OR-joins in a workflow further complicates the formal semantics of the OR-join. In this paper, the concept of the OR-join is examined in detail in the context of the workflow language YAWL, a powerful workflow language designed to support a collection of workflow patterns and inspired by Petri nets. The paper provides a suitable (non-local) semantics for an OR-join and gives a concrete algorithm with two optimization techniques to support the implementation. This approach exploits a link that is proposed between YAWL and reset nets, a variant of Petri nets with a special type of arc that can remove all tokens from a place when its transition fires. Through the behavior of reset arcs, the behavior of cancelation regions can be captured in a natural manner.

As the need for concepts such as cancellation and OR-joins occurs naturally in business scenarios, comprehensive support in a workflow language is desirable. However, there is a clear trade-off between the expressive power of a language (i.e., introducing complex constructs such as cancellation and OR-joins) and ease of verification. When a workflow contains a large number of tasks and involves complex control flow dependencies, verification can take too much time or it may even be impossible. There are a number of different approaches to deal with this complexity. Reducing the size of the workflow, while preserving its essential properties with respect to a particular analysis problem, is one such approach. In this paper, we present a set of reduction rules for workflows with cancellation regions and OR-joins and demonstrate how they can be used to improve the efficiency of verification. Our results are presented in the context of the YAWL workflow language.

PurposeThe purpose of this paper is to demonstrate that process verification has matured to a level where it can be used in practice. This paper reports on new verification techniques that can be used to assess the correctness of real‐life models.Design/methodology/approachThe proposed approach relies on using formal methods to determine the correctness of business processes with cancellation and OR‐joins. The paper also demonstrates how reduction rules can be used to improve the efficiency. These techniques are presented in the context of the workflow language yet another workflow language (YAWL) that provides direct support for 20 most frequently used patterns found today (including cancellation and OR‐joins). But the results also apply to other languages with these features (e.g. BPMN, EPCs, UML activity diagrams, etc.). An editor has been developed that provides diagnostic information based on the techniques presented in this paper.FindingsThe paper proposes four properties for business processes with cancellation and OR‐joins, namely: soundness, weak soundness, irreducible cancellation regions and immutable OR‐joins and develop new techniques to verify these properties. Reduction rules have been used as a means of improving the efficiency of the algorithm. The paper demonstrates the feasibility of this verification approach using a realistic and complex business process, the visa application process for general skilled migration to Australia, modelled as a YAWL workflow with cancellation regions and OR‐joins.Originality/valueBusiness processes sometimes require complex execution interdependencies to properly complete a process. For instance, it is possible that certain activities need to be cancelled mid‐way though the process. Some parallel activities may require complex “wait and see” style synchronisation depending on a given context. These types of business processes can be found in various domains, such as application integration, B2B commerce, web service composition and workflow systems. Even though cancellation and sophisticated join structures are present in many business processes, existing verification techniques are unable to deal with such processes. Hence, this paper plays an important role in making process verification a reality.

The application of reduction rules to any Petri net may assist in its analysis as its reduced version may be significantly smaller while still retaining the original net's essential properties. Reset nets extend Petri nets with the concept of a reset arc, allowing one to remove all tokens from a certain place. Such nets have a natural application in business process modelling where possible cancellation of activities need to be modelled explicitly and in workflow management where such process models with cancellation behaviours should be enacted correctly. As cancelling the entire workflow or even cancelling certain activities in a workflow has serious implications during execution (for instance, a workflow can deadlock because of cancellation), such workflows should be thoroughly tested before deployment. However, verification of large workflows with cancellation behaviour is time consuming and can become intractable due to the state space explosion problem. One way of speeding up verification of workflows based on reset nets is to apply reduction rules. Even though reduction rules exist for Petri nets and some of its subclasses and extensions, there are no documented reduction rules for reset nets. This paper systematically presents such reduction rules. Because we want to apply the results to the workflow domain, this paper focusses on reset workflow nets (RWF-nets), i.e. a subclass tailored to the modelling of workflows. The approach has been implemented in the context of the workflow system YAWL.

In business processes, knowledge-intensive tasks are ones in which the people performing such tasks are involved in a fair degree of uncertainty. These people are required to apply and bring together their experience, training, expertise and judgement. In particular, they are concerned about issues or problems that might arise and how these are best dealt with or avoided. Current workflow technology does not support such tasks, as it deals only with predictable and easily automated decision making. In particular, it fails to deliver the right information to the user at the right time based on the context of the process instance, thus not taking the opportunity to forewarn users of potential problems. Context-aware workflows are a way to overcome shortcomings of workflow management systems. This paper proposes an approach for the dynamic integration of knowledge and workflow processes by offering proper support for the realtime handling of the both the current context of a process and its execution path.

Reeection may be used as a way of opening up the general process of object reiication and management. Instead of having a situation where such activities are either totally closed or totally ad-hoc, we may provide a general policy framework for object management, one that allows particular policies in a controlled manner. By revealing the process or processes involved in making an object available to an application program, and by making those revelations in an modiiable and object-oriented way, distributed and possibly heterogeneous data and program resources, such as the so-called legacy systems, may be used by new applications in a transparent way. This paper discusses the R-OK (reeective object knowledge) model and how it may be used to such ends.

The Work∞ow Patterns provide a conceptual foundation for the control-∞ow, data and resource perspectives of process-aware information systems (PAIS). In this paper we present newYAWL, a reference language for PAIS based on the work∞ow patterns. newYAWL radically extends previous work undertaken on the YAWL language and provides a comprehensive formal description of how the complete set of work∞ow patterns can be realized and integrated in the context of an operational PAIS.

This paper presents the realisation, using a Service Oriented Architecture, of an approach for dynamic, flexible and extensible exception handling in workflows, based not on proprietary frameworks, but on accepted ideas of how people actually work. The resultant service implements a detailed taxonomy of workflow exception patterns to provide an extensible repertoire of self-contained exception-handling processes called exlets, which may be applied at the task, case or specification levels. When an exception occurs at runtime, an exlet is dynamically selected from the repertoire depending on the context of the exception and of the particular work instance. Both expected and unexpected exceptions are catered for in real time, so that 'manual handling' is avoided.

With the growing number of trading opportunities available online, software tools designed to act on behalf of human traders are increasingly being used to automate trading activities. The next logical step in this evolution is the automation of composite trading activities designed to fulfill complex user goals and requirements. In this paper, we describe a model for specifying composite trading activities involving concurrent and interrelated negotiations with multiple parties and heterogeneous protocols. The model supports the specification of several types of constraints, such as the number of required successful negotiations, the limit price for the items to be traded, and the temporal constraints imposed by all trading parties. In order to guide the execution of the trading activities, we describe a novel planning and execution model for composite trading activities which is designed to maximize the expected utility of the user.

This paper presents the realisation, using a Service Oriented Architecture, of an approach for dynamic, flexible and extensible excep- tion handling in workflows, based not on proprietary frameworks, but on accepted ideas of how people actually work. The approach utilises an established framework for workflow flexibility called worklets and a de- tailed taxonomy of workflow exception patterns to provide an extensible repertoire of self-contained exception-handling processes which may be applied at the task, case or specification levels, and from which a dynamic runtime selection is made depending on the context of the exception and the particular work instance. Both expected and unexpected exceptions are catered for in real time, so that `manual handling' of the exception is avoided.

When dealing with complex business processes (e.g., in the context of a workflow implementation or the configuration of some process-aware information system), it is important but sometimes difficult to determine whether a process contains any errors. The concepts such as cancellation and OR-joins occur naturally in business scenarios but the presence of these features in process models poses new challenges for verification. We take on the challenge of finding new verification techniques for workflows with cancellation regions and OR-joins. The proposed approach relies on reset nets and reachability analysis. We present these techniques in the context of workflow language YAWL that provides direct support for these features. We have extended the graphical editor of YAWL with these diagnostic features.

Negotiating with suppliers and with customers is a key part of supply chain management. However, with recent technological advances, the mechanisms available to carry out such activities have become increasingly sophisticated, and the environment in which these activities take place has become highly dynamic. As a consequence, the overall planning of these complex trades, and the coordination of the various production and scheduling activities, need to be carefully considered by the businesses involved in the supply chain management. In order to guide the overall planning, production, scheduling, and allocation of resources, especially designed strategies are increasingly used by the businesses. In this setting, it is crucial that the intended behaviour, and through that, the desired outcomes, of these strategies be precisely understood. Using an empirical analysis, this paper investigates two fundamental strategies in supply chain management: buy-to-build and build-to-order.

This paper presents the realisation, using a Service Oriented Architecture, of an approach for dynamic flexibility and evolution in workflows through the support of flexible work practices, based not on proprietary frameworks, but on accepted ideas of how people actually work. A set of principles have been derived from a sound theoretical base and applied to the development of worklets, an extensible repertoire of self-contained sub-processes aligned to each task, from which a dynamic runtime selection is made depending on the context of the particular work instance.

This paper presents the implementation, using a Service Oriented Architecture, of an approach for dynamic flexibility and evolution in workflows through the support of flexible work practices, based not on proprietary frameworks, but on accepted ideas of how people actually work. A set of principles have been derived from a sound theoretical base and applied to the development of worklets, an extensible repertoire of self-contained sub-processes that can be applied in a variety of situations depending on the context of the particular work instance.

When a workflow contains a large number of tasks and involves complex control flow dependencies, verification can take too much time or it may even be impossible. Reduction rules can be used to abstract from certain transitions and places in a large net and thus could cut down the size of the net used for verification. Petri nets have been proposed to model and analyse workflows and Petri nets reduction rules have been used for efficient verification of various properties of workflows, such as liveness and boundedness. Reset nets are Petri nets with reset arcs, which can remove tokens from places when a transition fires. The nature of reset arcs closely relates to the cancellation behaviour in workflows. As a result, reset nets have been proposed to formally represent workflows with cancellation behaviour, which is not easily modelled in ordinary Petri nets. Even though reduction rules exist for Petri nets, the nature of reset arcs could invalidate the transformation rules applicable to Petri nets. This motivated us to consider possible reduction rules for reset nets. In this paper, we propose a number of reduction rules for Reset Workflow Nets (RWF-nets) that are soundness preserving. These reduction rules are based on reduction rules available for Petri nets [19] and we present the necessary conditions under which these rules hold in the context of reset nets.

Workflow systems seek to provide an implementation vehicle for complex, recurring business processes. Notwithstanding this common objective, there are a variety of distinct features offered by commercial workflow management systems. These differences result in significant variations in the ability of distinct tools to represent and implement the plethora of requirements that may arise in contemporary business processes. Many of these requirements recur quite frequently during the requirements analysis activity for workflow systems and abstractions of these requirements serve as a useful means of identifying the key components of workflow languages. In this paper, we describe a series of workflow data patterns that aim to capture the various ways in which data is represented and utilised in workflows. By delineating these patterns in a form that is independent of specific workflow technologies and modelling languages, we are able to provide a comprehensive treatment of the workflow data perspective and we subsequently use these patterns as the basis for a detailed comparison of a number of commercially available workflow management systems, workflow standards and web-service composition languages.