JAIST Repository
https://dspace.jaist.ac.jp/Title

Correctness Properties for Workflows with
Multiple Starts and/or Ends

Author(s)Takaki, O.; Takeuti, I.; Seino, T.; Izumi, N.;
Takahshi, K.

CitationIssue Date

2008‑03‑03

TypePresentation

Text version

publisher

URL

http://hdl.handle.net/10119/8288

RightsDescription

5th VERITE : JAIST/TRUST‑AIST/CVS joint workshop
on VERIfication TEchnologyでの発表資料, 開催：2008年3月3日, 開催場所：北陸先端科学技術大学院
大学・情報科学研究科棟 5F コラボレーションルーム
７, JAIST 21世紀COEシンポジウム 2008「検証進化可能電子社会」と共催

Japan Advanced Institute of Science and Technology

Correctness Properties for Workflows
with Multiple Starts and/or Ends

O.Takaki, I.Takeuti, T.Seino,N.Izumi, K.Takahshi
AIST• Contents of this talk– Motivation• Correctness of Workflows• Why do we consider multiple starts and/or ends?

– General Correctness of Workflows with Multiplestarts and/or Ends

Example of aworkflow

startMake a paper P

activity

Revise the paper

Select a conference
to submit the paper
Downloada registration form R
Fill out
the registration form

AND-joinAND-split

XOR-split
Do you need approval
to submit a paper?

yesnoExplain the contentof P to your boss

XOR-join

Submit the paper and the registration formend•Workflow (Nodes, Arcs):
a simple connected directed graph– Nodes = Starts U Ends U Activities
U XOR-splies U XOR-joins
U AND-splies U AND-joins– For each n∈Nodes there exists a path from astart to n.
– For each n∈Nodes there exists a path from n toan end.
– In this talk, we consider only acyclic workflows.

StartEndActivity

XOR-splitAND-spllit

XOR-join AND-join• Correctness of Workflow with one start andone end [Sadiq & Owlrowska 00]– Deadlock free
– Lack of synchronization free
企画書作成

企画書作成
50万円未満50万円以上50万円未満50万円以上

予算は？

企画準備

企画審査

企画準備

企画審査

f1

f2

f1

f2

R1
企画の実行

R1
企画の実行

• Verification of Correctness– Graph Reductions(Sadiq and Orlowska 1998, 2000)– WF-nets(van der Aalst 1997, 1998)– Grobal-Local Correctness(Kindler, Martens and Reisig 2000)– Woflan (Verbeek, Basten and van der Aalst 2001)– Improvement of Sadiq-Orlowska’s works(Lin, Zhao, Li and Chen 2002)– Standard Workflow Models (Kiepuszewski, ter
Hofstede and van der Aalst 2003)– EPCs (Dehnert and van der Aalst 2004～2006)

Why do we consider Multiple starts/ends?
WF1

WF2

WF3

Why do we consider Multiple starts/ends?
WF1

WF2

WF3

• Our purpose– Extend the concept of correctness over workflows
with one start and end to that over workflows withmultiple starts and/or end.
– Verification Algorithms of the extended crrectnessof given workflows.
– Imprement of the algorithms to develop design
assistant system of workflow.

• Our purpose– Extend the concept of correctness overworkflows with one start and end to that overworkflows with multiple starts and/or end.
– Verification Algorithms of the extended crrectnessof given workflows.
– Imprement of the algorithms to develop design
assistant system of workflow.

•General Correctness– We define ``general correctness’’, that is ageneralized version of correctness of workflow
to satisfies the following properties.
1. General correctness is a natural extension ofcorrectness, thar is, for a workflow with one
start, general correctness is the same asoriginal one.
2. General correctness is preserved by theoperation of connection and/or division ofworkflows.
3. General correctness assures the possibility for aworkflow to be completed to a correct workflow.

×

×•Conclusion– We extend the concept of correctness overworkflows with one start and end to that overworkflows with multiple starts and/or end.
1. General correctness is a natural extension ofcorrectness, thar is, for a workflow with onestart, general correctness is the same asoriginal one. (Theorem 0.13)
2. General correctness is preserved by theoperation of connection and/or division ofworkflows. (Theorem 0.15)
3. General correctness assures the possibility for aworkflow to be completed to a correct workflow.
(Corollary 0.18)