Interval soundness of resource-constrained workflow nets : decidability and repair

E. Ramezani Taghiabadi, N. Sidorova, C. Stahl

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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.
Original languageEnglish
Title of host publicationFundamentals of Software Engineering (5th International Conference, FSEN 2013, Tehran, Iran, April 24-26, 2013, Revised Selected Papers)
EditorsF. Arbab, M. Sirjani
Place of PublicationBerlin
PublisherSpringer
Pages150-167
ISBN (Print)978-3-642-40212-8
DOIs
Publication statusPublished - 2013
Event5th International Conference on Fundamentals of Software Engineering (FSEN 2013), April 24-26, 2013, Tehran, Iran - Tehran, Iran, Islamic Republic of
Duration: 24 Apr 201326 Apr 2013

Publication series

NameLecture Notes in Computer Science
Volume8161
ISSN (Print)0302-9743

Conference

Conference5th International Conference on Fundamentals of Software Engineering (FSEN 2013), April 24-26, 2013, Tehran, Iran
Abbreviated titleFSEN 2013
Country/TerritoryIran, Islamic Republic of
CityTehran
Period24/04/1326/04/13

Fingerprint

Dive into the research topics of 'Interval soundness of resource-constrained workflow nets : decidability and repair'. Together they form a unique fingerprint.

Cite this