Soundness of Timed-Arc Workflow Nets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00080033" target="_blank" >RIV/00216224:14330/14:00080033 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007/978-3-319-07734-5_4" target="_blank" >http://link.springer.com/chapter/10.1007/978-3-319-07734-5_4</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-07734-5_4" target="_blank" >10.1007/978-3-319-07734-5_4</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Soundness of Timed-Arc Workflow Nets

Popis výsledku v původním jazyce

Analysis of workflow processes with quantitative aspects like timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and study the foundational problems of soundness and strong (time-bounded) soundness. We explore the decidability of these problems and show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable. For general timed-arc workflow nets soundness and strong soundness become undecidable, though we can design efficient verification algorithms for the subclass of bounded nets. Finally, we demonstrate the usability of our theory on the case studies of a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow. The implementation of the algorithms is freely available as a part of the model checker TAPAAL.

Název v anglickém jazyce

Soundness of Timed-Arc Workflow Nets

Popis výsledku anglicky

Analysis of workflow processes with quantitative aspects like timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and study the foundational problems of soundness and strong (time-bounded) soundness. We explore the decidability of these problems and show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable. For general timed-arc workflow nets soundness and strong soundness become undecidable, though we can design efficient verification algorithms for the subclass of bounded nets. Finally, we demonstrate the usability of our theory on the case studies of a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow. The implementation of the algorithms is freely available as a part of the model checker TAPAAL.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 35th International Conference on Application and Theory of {P}etri Nets and Concurrency ({ICATPN}'14)

ISBN

9783319077338

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

20

Strana od-do

51-70

Název nakladatele

Springer-Verlag

Místo vydání

Nizozemsko

Místo konání akce

Nizozemsko

Datum konání akce

1. 1. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—