第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 UPPAAL syn! Working clock >= mintime syn ! syn? clock := 0 clock <= maxtime Finished BPMNからUPPAALへの変換（２） 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週間以内で１サイクルが終了すること（リソース） 議論が終了していない場合にのみ、締切の警告をす ること（業務ルール） 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[] NG 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週間以内で１サイクルが終了すること A[] E1.Finish imply ct <=7 議論が終了していない場合にのみ、締切の警告をだ すこと A[] not O1.error 業務要件の検証（再） NG 検証再実行 業務が停止しないこと A[] OK 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上での不具合箇 所の特定方法
© Copyright 2024 ExpyDoc
