トップエスイー修了制作

ビジネスプロセスの検証ツールの開発
株式会社日立製作所

村田大二郎

開発における問題点

手法・ツールの適用による解決

・要件定義段階での問題は、後になるほど修正が大変・ビジネスプロセスのデッドロックや詳細化関係
・ソースコードを自動生成する場合、検証された元情報が必要

・詳細化されるBPMNの検証のため、BPMNからCSPモデルへの変換規則を作成
・CSPを用いた検証ツールFDR2のコードをBPMNから生成するツールを開発
・CSPモデル実装のためのライブラリJCSPを利用
し、BPMNからJavaコードへの生成ツールを開発

ビジネスプロセスのFDR2による検証
ビジネスプロセスのデバッグ
設計者はFDR2のデバッグ結果に表示される名前と同じ名前の、ビジネスプロセス上の要素を見つけ、修正する

ビジネスプロセスエディタ

FDR2

入力BP依存Proc(GatewayIFBEnd) =ProcXOREnd(...)

並列処理

詳
細化

AND

入力BP非依存
並列処理

分岐OR

通信

設計者は並列処理を有する
BPMNダイアグラム（ビジネスプロセス）を編集

FDR2により検証されたBPMNからJavaソースコードを生成することで、デッドロック・ライブロックの検証されたプログラムを利用可能

BPMN: Business Process Modeling Notation
CSP: Communicating Sequential Processes
JCSP: Communicating Sequential Processes for JavaTM

生成ツール（今回開発）

ProcXOREnd(in1,in2, node, out) =( ((in1 -> SKIP) [](in2 -> SKIP)) ;(node -> out ->SKIP) ; inact ->SKIP ) [] (inact ->SKIP)（略）
Proc(Gate wayIFB End) =( ( sf.SF _from_ OrderP roduct Delive ry_to_ Gatewa yIFBEn d -> S KIP) [ ](sf.SF_fr om_Can celOrd er_to_ Gatewa yIFBEn d -> S KIP) ) ;(node.Gat ewayIF BEnd - > sf.S F_from _Gatew ayIFBE nd_to_ EventE ndLane LotSer ver >SKIP)
Proc(Even tEndLa neProd uctDis tribut er) =sf.SF_fro m_Rece ivePro ductDe livery Order_ to_Eve ntEndL anePro ductDi stribu ter >node.Even tEndLa neProd uctDis tribut er -> SKIP
Proc(Rece ivePro ductDe livery Order) =sf.SF_fro m_Send Produc tCheck Result _to_Re ceiveP roduct Delive ryOrde r ->node.Rece ivePro ductDe livery Order ->sf.SF_fro m_Rece ivePro ductDe livery Order_ to_Eve ntEndL anePro ductDi stribu ter > SKIP
Proc(Orde rProdu ctDeli very) =sf.SF_fro m_Gate wayIFB Start_ to_Ord erProd uctDel ivery ->node.Orde rProdu ctDeli very - >sf.SF_fro m_Orde rProdu ctDeli very_t o_Gate wayIFB End -> SKIP
ProcInact (P) = (P; in act -> SKIP) [](ina ct->SK IP)
EvInact(s ) = un ion(s, {inac t})
ProcAll = || x: Procna me @ [ EvInac t(Ev(x ))] Pr ocInac t(Proc (x))（略）-- assert ion
DF = (|~ | x:Ev ents @ x -> DF ) | ~| SKI P--deadloc kassert DF [F= P rocAll--liveloc kassert Pr ocAll :[ div ergenc e free ]生成ツールを用い、ビジネスプロセスからFDR2コードを自動生成

読込

FDR2コードを読み込みデッドロックを検証

JCSPによるプロト開発
public class ProcXOREnd implements CSProcess {...
入力BP非依存 public class ProcAll0 implements CSProcess {...
public ProcAll0() {...
= new ProcXOREnd(...); 入力BP依存
JCSPライブラリを m_proc[6]
...

呼び出す
Javaソースコードを自動生成

国立情報学研究所
トップエスイー～サイエンスによる知的のものづくり教育プログラム～
トップエスイー：サイエンスによる知的ものづくり教育プログラム
National Institute of Informatics文部科学省 振興調整費産学融合先端ソフトウェア技術者養成拠点の形成
文部科学省科学技術振興調整費
産学融合先端ソフトウェア技術者養成拠点の形成

トップエスイー修了制作

タイトル
所属

名前

開発における問題点

メールアドレス

手法・ツールの適用による解決

あああ

あああ

ヘッダ

ヘッダ

国立情報学研究所
トップエスイー～サイエンスによる知的のものづくり教育プログラム～
トップエスイー：サイエンスによる知的ものづくり教育プログラム
National Institute of Informatics
文部科学省 振興調整費産学融合先端ソフトウェア技術者養成拠点の形成
文部科学省科学技術振興調整費
産学融合先端ソフトウェア技術者養成拠点の形成

トップエスイー修了制作

タイトル
所属

名前

開発における問題点

メールアドレス

手法・ツールの提案による解決

あああ

あああ

ヘッダ

ヘッダ

国立情報学研究所
トップエスイー～サイエンスによる知的のものづくり教育プログラム～
トップエスイー：サイエンスによる知的ものづくり教育プログラム
National Institute of Informatics
文部科学省 振興調整費産学融合先端ソフトウェア技術者養成拠点の形成
文部科学省科学技術振興調整費
産学融合先端ソフトウェア技術者養成拠点の形成

トップエスイー修了制作（略）
Proc(GatewayIFBEnd) =( ( sf.SF_from_OrderProductDelivery_to_GatewayIFBEnd -> SKIP) [](sf.SF_from_CancelOrder_to_GatewayIFBEnd -> SKIP) ) ;(node.GatewayIFBEnd -> sf.SF_from_GatewayIFBEnd_to_EventEndLaneLotServer >SKIP)
Proc(EventEndLaneProductDistributer) =sf.SF_from_ReceiveProductDeliveryOrder_to_EventEndLaneProductDistributer >node.EventEndLaneProductDistributer -> SKIP
Proc(ReceiveProductDeliveryOrder) =sf.SF_from_SendProductCheckResult_to_ReceiveProductDeliveryOrder ->node.ReceiveProductDeliveryOrder ->sf.SF_from_ReceiveProductDeliveryOrder_to_EventEndLaneProductDistributer > SKIP
Proc(OrderProductDelivery) =sf.SF_from_GatewayIFBStart_to_OrderProductDelivery ->node.OrderProductDelivery ->sf.SF_from_OrderProductDelivery_to_GatewayIFBEnd -> SKIP
ProcInact(P) = (P; inact -> SKIP)[](inact->SKIP)
EvInact(s) = union(s, {inact})
ProcAll = || x:Procname @ [EvInact(Ev(x))] ProcInact(Proc(x))（略）-- assertion
DF = (|~| x:Events @ x -> DF ) |~| SKIP--deadlock
assert DF [F= ProcAll--livelock
assert ProcAll :[ divergence free ]国立情報学研究所
トップエスイー～サイエンスによる知的のものづくり教育プログラム～
トップエスイー：サイエンスによる知的ものづくり教育プログラム
National Institute of Informatics
文部科学省 振興調整費産学融合先端ソフトウェア技術者養成拠点の形成
文部科学省科学技術振興調整費
産学融合先端ソフトウェア技術者養成拠点の形成