Interval Soundness of Resource-Constrained Workflow Nets: Decidability and Repair - Fundamentals of Software Engineering
Conference Papers Year : 2013

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.
Fichier principal
Vignette du fichier
978-3-642-40213-5_10_Chapter.pdf (473.88 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01514666 , version 1 (26-04-2017)

Licence

Identifiers

Cite

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⟩
133 View
89 Download

Altmetric

Share

More