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

WEBベース・ワークフローシステムのモデル化と検証

Author(s)平石, 邦彦CitationIssue Date

2008‑03‑03

TypePresentation

Text version

publisher

URL

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

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

WEBベース・ワークフローシステムのモデル化と検証
JAIST
平石 邦彦

目的• 電子社会における情報システムのモデル化と検証．
– 複数のサブシステムからなるWebベースのワークフロー
システムを対象．
– 商用の開発環境（日立Cosminexsus WorkCoordinator+ Business Logic Container)上で実際にシステムを作成．
– 同時進行でモデル作成．
– M2学生（山本 豊君）1名．約１０ヶ月．

VERITE 2008/3/3

2

モデル化の詳細度• 実際に稼動するシステムのミニチュア版．
• 論理的な設計仕様レベルのモデル化．
– ログイン・ログアウト，ユーザー認証プロセス．
– ユーザーの入力データ．
– 担当者の属性，組織構造の表現．
– サブシステムの連携，通信．

VERITE 2008/3/3

3

日立Cosminexsus• Cosminexus は，– インターネットやイントラネットなどのネットワークを使って，分散したシステムの情報を連携するためのアプリケーションサーバ．
– Web システム構築に必要な開発，実行，および管理環境を提供．
– Java やCORBA といった業界標準に準拠した開発環境と実行環境を提供することによって，既存システムのWeb対応から異種システムの統合までサポート．
(Cosminexus解説 3000-3-931-30より)

VERITE 2008/3/34

見積発注プロセス(WorkCoordinator Version 3 解説・手引・操作書 3000-3-447-30より)

VERITE 2008/3/3

5

ワークフローによる業務システムの統合(WorkCoordinator Version 3 解説・手引・操作書 3000-3-447-30より)

VERITE 2008/3/3

6

WorkCoordinator
Difiner

業務実行
クライアント

作業者DB

業務DB

WorkCoordinator
Server(WorkCoordinator Version 3 解説・手引・操作書 3000-3-447-30より)

VERITE 2008/3/3

7WorkCoordinator Definer

VERITE 2008/3/3

8

DB参照による実行制御(WorkCoordinator Version 3 解説・手引・操作書 3000-3-447-30より)

VERITE 2008/3/3

9Business Logic Container• ワークフローに対応するWeb 帳票アプリケーションの開発と実行を支援するプログラム．
• 開発支援プログラムでは，Web 帳票アプリケーションの構成要素となる情報を結合して，JSP 形式のWeb 帳票アプリケーションを生成（帳票ジェネレータ）．
• 実行支援プログラムでは，生成したWeb 帳票アプリケーションを実行するための，標準的な実行環境を提供．

VERITE 2008/3/310

BLC開発環境(Hitach Business Logic Container 解説・手引・操作書 3020-3-D63-10より)

VERITE 2008/3/3

11BLC実行環境
デプロイ(Hitach Business Logic Container 解説・手引・操作書 3020-3-D63-10より)

VERITE 2008/3/3

12BLC帳票の構成(Hitach Business Logic Container 解説・手引・操作書 3020-3-D63-10より)

VERITE 2008/3/3

13BLCコンソール(Hitach Business Logic Container 解説・手引・操作書 3020-3-D63-10より)

VERITE 2008/3/314

VERITE 2008/3/3

15

VERITE 2008/3/3

16

VERITE 2008/3/317

BLC画面遷移(Hitach Business Logic Container 解説・手引・操作書 3020-3-D63-10より)

VERITE 2008/3/318

モデル化• Coloured Petri netsを使用．
– データ型．
– DB参照（SQL)の表現．
– 階層的モデル．
– マクロ表現（テンプレート）．
– 並行動作．
– ツール（CPN TOOLS）の存在．

VERITE 2008/3/3

19

モデル化の手順
1.
2.
3.
4.

ワークフロー定義の分析：フロー定義データ・帳票データ・データベースに関する設計仕様の抽出．
定型的処理に対するテンプレート作成．
フロー定義データに対するモデル作成．
階層的モデルとして合成．

VERITE 2008/3/3

20

ワークフロー定義の分析

VERITE 2008/3/3

21

階層化

VERITE 2008/3/322

メインフローDB参照

VERITE 2008/3/323

ユーザー処理（テンプレート）

VERITE 2008/3/324

DB検索による担当者の動的割当

VERITE 2008/3/3

25

モデルの検証• シミュレーション• 状態空間生成– 単一フローに対して，87,390状態．計算に2,210sec.(PentiumD 3.0GHz, 4GBメモリ)．
– 複数フローの並行動作だと，状態数は指数関数的に増加．
– レポートの生成機能．
• CPN-ML関数の定義によるモデル検査．

VERITE 2008/3/326

検証例• 異常停止：Sinkノードに到達しないで終了．
• プロセスと帳票の不整合．

VERITE 2008/3/3

27

異常終了
fun IllegalEnd () : Node list
= PredAllNodes(fn n =>letval TokenInSink = Mark.Top'sink 1 nin(Terminal n)andalso(TokenInSink == empty)
end)

一般見積プロセスにおける帳票の不整合
fun snd_ms (x : PROCESSING) = 1`(#2 x);
fun IllegalFormAtIppanMitsumori () : Node list
= PredAllNodes(fn n =>letval Forms_ms = ext_ms snd_ms Mark'Ippan_mitsumori_sakusei'PROC 1 nin
cf("mitsumori(ippan)", Forms_ms) <> size(Forms_ms)
end);
VERITE 2008/3/3

28

実行結果

異常終了状態なし

プロセスと帳票の不整合状態あり（ユーザーの入力ミスが原因）

VERITE 2008/3/3

29

モデルのその他の利用法• システムの異常→実行ログの出力機能．
• モデル上で実行ログに基づいてシミュレーションを行うことで，障害の原因を特定．

VERITE 2008/3/330