Interval Soundness of Resource-Constrained Workflow Nets: Decidability and Repair
Correctness of workflow design cannot be evaluated by checking the execution for one single instance of the workflow, because instances, even when being independent from the data perspective, depend on each other with respect to the resources they rely on
- PDF / 378,692 Bytes
- 18 Pages / 439.37 x 666.142 pts Page_size
- 9 Downloads / 178 Views
Abstract. Correctness of workflow design cannot be evaluated by checking the execution for one single instance of the workflow, because instances, even when being independent from the data perspective, depend on each other with respect to the resources they rely on for executing tasks. The resources are shared among the instances of the same workflow; moreover, other workflows can use the same resources. Therefore, we enrich the workflow model with the model of its environment that captures the resource perspective. This allows us to investigate the verification of workflows extended with resources in a more general setting than it was previously done. We focus on the soundness property, which means the ability to terminate properly from any reachable state of the system, for every instance of the system. We show the decision procedure for soundness and how to repair a workflow that is unsound from the resource perspective by synthesizing a controller such that the composition of the workflow and the controller is sound by design.
1
Introduction
A workflow consists of a set of coordinated tasks describing a flow of work for accomplishing some business process within an organization. The occurrence of those tasks may depend on resources, such as machines, manpower, and raw material. Often, several cases (i.e., instances) of a workflow coexist, and they may all concurrently access the resources. In that sense, the execution of a workflow is similar to executing several threads of a piece of software. Correctness of classical and resource-constrained workflows has been formalized in terms of the soundness property [1,14]. Soundness guarantees that given a finite number of cases and a number of resources of each type, every case has always the possibility to terminate. As we restrict ourselves to durable resources in this paper—that is, resources that can neither be created nor destroyed— soundness also ensures that the number of resources initially available remains invariant. The current notion of soundness for resource-constrained workflows assumes a workflow to be executed in isolation. However, workflows increasingly cross organizational boundaries and are usually intertwined. As a consequence, resources F. Arbab and M. Sirjani (Eds.): FSEN 2013, LNCS 8161, pp. 150–167, 2013. DOI: 10.1007/978-3-642-40213-5 10, c IFIP International Federation for Information Processing 2013
Interval Soundness of Resource-Constrained Workflow Nets
151
are no longer internal for a workflow but shared among different workflows. This, in fact, requires a different way of modeling workflows. To do so, we propose to enrich the workflow model with an environment capturing the resource perspective of the workflow. The environment is generic in the sense that it can be parameterized, thereby enabling the modeling of relevant instances of practical scenarios. More precisely, the environment allows for borrowing, lending, and permanently adding and removing of resources of each type up to an initially specified number. Moreover, it also creates the cases of th
Data Loading...
