第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への変換（１）変換方針
 BPMNフローオブジェクト（節） 時間オートマトン（UPPAALでいう1システム）で表現 BPMN接続オブジェクト（枝） UPPAALシステム間の同期チャネル通信で表現

Activity

BPMN

UPPAALsyn!

Working clock >= mintime
syn !

syn?
clock := 0clock <= maxtime

Finished

BPMNからUPPAALへの変換（２）

BPMNの各要素に対応する時間オートマトンは、UPPAALのシステムテンプレートとして蓄積しておく 変換時にはパラメータを与えて利用

例：アクティビティの変換テンプレート
 Activity(前フロー、後フロー、最小実行時間、最大実行時間)

実験
1～10 days

Discussion Cycle

A2
Moderate
E-mailDiscussion

63

A1S1 1Announce
Issues forDiscussion

G12T147

Delay 6 days
from Announcement
5E-mailDiscussion
Deadline
Warning

A6A49G41514
Conference Callin Discussion Week?
Check Calendar
No 10for Conference
G38 G2Call
11A5Yes13
Moderate
12
Conference Call
T2Discussion
Wait until※BPMN 1.0 仕様書より抜粋/一部変更
Thursday
1 day

A3

Evaluate
Discussion
Progress

E116

実験

検証したい業務要件
 業務が停止しないこと（継続性）
 1週間以内で１サイクルが終了すること（リソース）
 議論が終了していない場合にのみ、締切の警告をすること（業務ルール）

BPMNからUPPAALへの変換（１）システム定義（抜粋）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への変換（２）業務要件の検証

検証式への変換と検証実行
 業務が停止しないこと
 A[] (not deadlock) or R1.EndOfProcess

 1週間以内で１サイクルが終了すること
 A[] E1.Finish imply ct <=7 議論が終了していない場合にのみ、締切の警告をだすこと
 A[] not O1.error

業務要件の検証

検証式への変換と検証実行OK  業務が停止しないこと
 A[] (not deadlock) or R1.EndOfProcess

NG  1週間以内で１サイクルが終了すること
 A[] E1.Finish imply ct <=7NG  議論が終了していない場合にのみ、締切の警告をだすこと
 A[] not O1.error

ビジネスプロセスのデバッグ
議論が6日以内に終わった場合でも締切の警告をしてしまう

1～10 days

議論が長引くと全体で7日以内に終わらない

A2
Moderate
E-mailDiscussion

63

A1
S1 1

Announce
Issues forDiscussionG12T1
47

Delay 6 days
from Announcement
5E-mailDiscussion
Deadline
Warning

A6A49G415

14
Conference Callin Discussion Week?
Check Calendar
No 10for Conference
G38 G2Call
11A5Yes
13Moderate
12
Conference Call
T2
Discussion
Wait until
Thursday
1 dayA3

Evaluate
Discussion
Progress

E1
16

ビジネスプロセスの修正
1～10 days

A2

締切警告前に議論が終了していないか確認する

6

Moderate
E-mailDiscussion

7日で一旦中断する

17
37 days

A1
S1

1

Announce
Issues forDiscussion

G1 42Yes

18

G5E-mailDiscussion
Deadline
Warning

T1
719
NoA49G620

15

Delay 6 daysfrom Announcement E-mailDiscussion Over?
5A3Check Calendar
for Conference
Call

Conference Callin Discussion Week?
10NoG2

814G3A511Yes

T212Wait untilThursday

Moderate
Conference CallDiscussion

A6G4

13

1day

Evaluate
Discussion
Progress

E116

業務要件の検証（再）

検証再実行 業務が停止しないこと
 A[] (not deadlock) or R1.EndOfProcess

 1週間以内で１サイクルが終了すること
 A[] E1.Finish imply ct <=7 議論が終了していない場合にのみ、締切の警告をだすこと
 A[] not O1.error

業務要件の検証（再）検証再実行NG  業務が停止しないこと
 A[] (not deadlock) or R1.EndOfProcessOK  1週間以内で１サイクルが終了すること
 A[] E1.Finish imply ct <=7OK  議論が終了していない場合にのみ、締切の警告をだすこと A[] not O1.error

ビジネスプロセスのデバッグ（再）1～10 days

A2

G4はA2からの両フローを待ちデッドロックしてしまう

6Moderate
E-mailDiscussion

173

7 daysA1
S1

1Announce
Issues forDiscussion

G1 42Yes

18

G5E-mailDiscussion
Deadline
Warning

T1
719
NoA4
9G620

15

Delay 6 days
from Announcement E-mailDiscussion Over?
5A3
Check Calendar
for Conference
CallConference Callin Discussion Week?
10NoG2814G3A511Yes

T212Wait untilThursday

Moderate
Conference Call
Discussion

A6G4131day

Evaluate
Discussion
Progress

E116

ビジネスプロセスの修正（再）1～10 days

A2Moderate
E-mailDiscussion

37 days

A1S1

1Announce
Issues forDiscussion

G1 4

26フローを併合

21

G717Yes18

G5E-mailDiscussion
Deadline
Warning

T1
719
NoA49G620

15

Delay 6 days
from Announcement E-mailDiscussion Over?
5A3
Check Calendar
for Conference
Call

Conference Callin Discussion Week?
10No

G2

814

G3

A511Yes

T212Wait until
ThursdayModerate
Conference Call
Discussion

A6G4131day

Evaluate
Discussion
Progress

E116

まとめ

UPPAALによるビジネスプロセス検証手法を提案
 BPMNをUPPAALモデル（時間オートマトン）に変換
 変換はテンプレートにより半自動化可能

 業務要件をUPPAAL検証式（TCTL）に変換



適用実験を行い手法の有効性を確認
 継続性、実行リソース（時間）、業務ルールに関する性質を検証、デバッグ今後の課題
変換テンプレートの拡充
 業務要件から検証式への変換方法
 UPPAAL上での反例から、BPMN上での不具合箇所の特定方法
