スライド発表 - トップエスイー

第3回 教育シンポジウム 2009/3/19
トップエスイー修了制作
モデル検査を用いた
ビジネスプロセスの検証
綿引 健二
テーマ

モデル検査技法を用いたビジネスプロセスの検証
ビジネスプロセス
業務要件
モデル
検査
ビジネスプロセスと
業務要件の間の
整合性を形式的に検証
業務は滞らず継続すること
○○日以内に終了できること
必ず入金後に発送すること
・・・・
アジェンダ





背景と目的
手法
実験
まとめ
今後の課題
背景と目的

背景
 ビジネスプロセス検証の必要性
 上流工程における重要な成果物
 SOAとBPM
 レビューによる検証の限界
 すべてのプロセス状態を把握することは困難
 モデル検査技法
 システムの状態空間を網羅的に探索して性質を検証

ビジネスプロセスと業務要件の整合性をモデル検
査技法を用いて形式的に検証する手法を提案
アプローチ
ビジネスプロセス
業務要件
整合?

業務は滞らず継続すること
○○日以内に終了できること
必ず入金後に発送すること
・・・・
基本方針
 ビジネスプロセスはBPMNで記述
 モデル検査ツールとして“UPPAAL”を利用
 時間制約の扱いに優れるため
手法
ビジネスプロセス(BPMN)
業務要件
整合?
業務は滞らず継続すること
○○日以内に終了できること
必ず入金後に発送すること
・・・・
手法
ビジネスプロセス(BPMN)
業務要件
整合?
UPPAALモデル(時間オートマトン)
業務は滞らず継続すること
○○日以内に終了できること
必ず入金後に発送すること
・・・・
検証式(TCTL)
A[] not deadlock
A[] A1.finish imply ・・・
手法
ビジネスプロセス(BPMN)
業務要件
整合?
UPPAALモデル(時間オートマトン)
業務は滞らず継続すること
○○日以内に終了できること
必ず入金後に発送すること
・・・・
検証式(TCTL)
UPPAAL
による
検証
A[] not deadlock
A[] A1.finish imply ・・・
手法
ビジネスプロセス(BPMN)
業務要件
整合?
UPPAALモデル(時間オートマトン)
業務は滞らず継続すること
○○日以内に終了できること
必ず入金後に発送すること
・・・・
検証式(TCTL)
UPPAAL
による
検証
NG
A[] not deadlock
A[] A1.finish imply ・・・
BPMNからUPPAALへの変換(1)

変換方針
 BPMNフローオブジェクト(節)
 時間オートマトン(UPPAALでいう1システム)で表現
 BPMN接続オブジェクト(枝)
 UPPAALシステム間の同期チャネル通信で表現
Activity
BPMN
UPPAAL
syn!
Working clock >= mintime
syn !
syn?
clock := 0
clock <= maxtime
Finished
BPMNからUPPAALへの変換(2)

BPMNの各要素に対応する時間オートマトンは、UPPAAL
のシステムテンプレートとして蓄積しておく


変換時にはパラメータを与えて利用
例:アクティビティの変換テンプレート

Activity(前フロー、後フロー、最小実行時間、最大実行時間)
実験
1~10 days
Discussion Cycle
A2
Moderate
E-mail
Discussion
6
3
A1
S1
1
Announce
Issues for
Discussion
G1
2
T1
4
7
Delay 6 days
from Announcement
E-mail
Discussion
Deadline
Warning
A6
A4
9
G4
15
5
14
A3
Conference Call
in Discussion Week?
Check Calendar
No 10
for Conference
8 G2
Call
11
A5
Yes
Moderate
12
Conference Call
T2
Discussion
Wait until
※BPMN 1.0 仕様書より抜粋/一部変更
Thursday
G3
13
1 day
Evaluate
Discussion
Progress
E1
16
実験

検証したい業務要件
 業務が停止しないこと(継続性)
 1週間以内で1サイクルが終了すること(リソース)
 議論が終了していない場合にのみ、締切の警告をす
ること(業務ルール)
BPMNからUPPAALへの変換(1)

システム定義(抜粋)
S1 = StartEvent(1);
E1 = EndEvent(16);
A1 = Activity(1, 2, 0, 0);
(中略)
A6 = Activity(15, 16, 0, 0);
テンプレートにパラメータを
与えてシステムを定義
G1 = AND(2, g1next, 3);
(中略)
T1 = TimerDelay(6, 4, 7);
T2 = TimerAt(isThursday, 11, 12);
R1 = Root();
C1 = Calendar();
O1 = DiscussionObserver();
追加作成したシステムと
検証のためのオブザーバ
system R1, C1, S1, E1, A1, A2, A3, A4, A5, A6, G1, G2, G3, G4, T1, T2, O1;
BPMNからUPPAALへの変換(2)
業務要件の検証

検証式への変換と検証実行
 業務が停止しないこと
 A[]
(not deadlock) or R1.EndOfProcess
 1週間以内で1サイクルが終了すること
 A[]
E1.Finish imply ct <=7
 議論が終了していない場合にのみ、締切の警告をだ
すこと
 A[]
not O1.error
業務要件の検証

OK
検証式への変換と検証実行
 業務が停止しないこと
 A[]
NG
 1週間以内で1サイクルが終了すること
 A[]
NG
(not deadlock) or R1.EndOfProcess
E1.Finish imply ct <=7
 議論が終了していない場合にのみ、締切の警告をだ
すこと
 A[]
not O1.error
ビジネスプロセスのデバッグ
議論が6日以内に
終わった場合でも
締切の警告をしてしまう
1~10 days
議論が長引くと
全体で7日以内に
終わらない
A2
Moderate
E-mail
Discussion
6
3
A1
S1
1
Announce
Issues for
Discussion
G1
2
T1
4
7
Delay 6 days
from Announcement
E-mail
Discussion
Deadline
Warning
A6
A4
9
G4
15
5
14
A3
Conference Call
in Discussion Week?
Check Calendar
No 10
for Conference
8 G2
Call
11
A5
Yes
Moderate
12
Conference Call
T2
Discussion
Wait until
Thursday
G3
13
1 day
Evaluate
Discussion
Progress
E1
16
ビジネスプロセスの修正
1~10 days
A2
締切警告前に
議論が終了していないか
確認する
6
Moderate
E-mail
Discussion
7日で一旦中断する
17
3
7 days
18
Yes
A1
S1
1
Announce
Issues for
Discussion
G1 4
2
T1
7
19
G5
No
E-mail
Discussion
Deadline
Warning
A4
9
G6
20
15
Delay 6 days
from Announcement E-mail
Discussion Over?
5
A3
Check Calendar
for Conference
Call
Conference Call
in Discussion Week?
10
No
G2
8
14
G3
A5
11
Yes
T2
12
Wait until
Thursday
Moderate
Conference Call
Discussion
A6
G4
13
1day
Evaluate
Discussion
Progress
E1
16
業務要件の検証(再)

検証再実行
 業務が停止しないこと
 A[]
(not deadlock) or R1.EndOfProcess
 1週間以内で1サイクルが終了すること
 A[]
E1.Finish imply ct <=7
 議論が終了していない場合にのみ、締切の警告をだ
すこと
 A[]
not O1.error
業務要件の検証(再)

NG
検証再実行
 業務が停止しないこと
 A[]
OK
 1週間以内で1サイクルが終了すること
 A[]
OK
(not deadlock) or R1.EndOfProcess
E1.Finish imply ct <=7
 議論が終了していない場合にのみ、締切の警告をだ
すこと
 A[]
not O1.error
ビジネスプロセスのデバッグ(再)
1~10 days
A2
G4は
A2からの両フローを待ち
デッドロックしてしまう
6
Moderate
E-mail
Discussion
17
3
7 days
18
Yes
A1
S1
1
Announce
Issues for
Discussion
G1 4
2
T1
7
19
G5
No
E-mail
Discussion
Deadline
Warning
A4
9
G6
20
15
Delay 6 days
from Announcement E-mail
Discussion Over?
5
A3
Check Calendar
for Conference
Call
Conference Call
in Discussion Week?
10
No
G2
8
14
G3
A5
11
Yes
T2
12
Wait until
Thursday
Moderate
Conference Call
Discussion
A6
G4
13
1day
Evaluate
Discussion
Progress
E1
16
ビジネスプロセスの修正(再)
1~10 days
A2
Moderate
E-mail
Discussion
3
7 days
6
フローを併合
21
G7
17
Yes
A1
S1
1
Announce
Issues for
Discussion
G1 4
2
18
T1
7
19
G5
No
E-mail
Discussion
Deadline
Warning
A4
9
G6
20
15
Delay 6 days
from Announcement E-mail
Discussion Over?
5
A3
Check Calendar
for Conference
Call
Conference Call
in Discussion Week?
10
No
G2
8
14
G3
A5
11
Yes
T2
12
Wait until
Thursday
Moderate
Conference Call
Discussion
A6
G4
13
1day
Evaluate
Discussion
Progress
E1
16
まとめ

UPPAALによるビジネスプロセス検証手法を提案
 BPMNをUPPAALモデル(時間オートマトン)に変換
 変換はテンプレートにより半自動化可能
 業務要件をUPPAAL検証式(TCTL)に変換

適用実験を行い手法の有効性を確認
 継続性、実行リソース(時間)、業務ルールに関する
性質を検証、デバッグ
今後の課題



変換テンプレートの拡充
業務要件から検証式への変換方法
UPPAAL上での反例から、BPMN上での不具合箇
所の特定方法