Skip to Main content Skip to Navigation
Conference papers

Interval Soundness of Resource-Constrained Workflow Nets: Decidability and Repair

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Hal Ifip <>
Submitted on : Wednesday, April 26, 2017 - 3:22:08 PM
Last modification on : Wednesday, April 26, 2017 - 3:26:38 PM
Long-term archiving on: : Thursday, July 27, 2017 - 1:00:48 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Elham Ramezani, Natalia Sidorova, Christian Stahl. Interval Soundness of Resource-Constrained Workflow Nets: Decidability and Repair. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.150-167, ⟨10.1007/978-3-642-40213-5_10⟩. ⟨hal-01514666⟩



Record views


Files downloads