研究課題/領域番号 |
07J54142
|
研究種目 |
特別研究員奨励費
|
配分区分 | 補助金 |
応募区分 | 国内 |
研究分野 |
ソフトウエア
|
研究機関 | 北陸先端科学技術大学院大学 |
研究代表者 |
有本 泰仁 北陸先端科学技術大学院大学, 情報科学研究科, 特別研究員(DC1)
|
研究期間 (年度) |
2007 – 2008
|
研究課題ステータス |
完了 (2008年度)
|
配分額 *注記 |
1,800千円 (直接経費: 1,800千円)
2008年度: 900千円 (直接経費: 900千円)
2007年度: 900千円 (直接経費: 900千円)
|
キーワード | 形式手法 / ドメイン工学 / ビジネスプロセスモデリング / 内部統制 / ドメイン分析 / 形式ドメイン記述 |
研究概要 |
近年、相次ぐ有名企業のスキャンダルから内部統制の重要性が高まってきている。安心な電子社会の基盤となるドメインとして、ビジネスプロセスが考えられる。特に、ビジネスプロセスの中で内部統制としての統制活動がどのようにモデル化でき、それらの効力を科学的に検証できること、というのがより安心な電子社会を築くうえで重要になると考えられる。本研究では、Observational Transition System(OTS、ある種の状態遷移機械)でビジネスプロセスのモデリングを行い、代数仕様言語CafeOBJでビジネスプロセスモデルを記述、検証する方法を提案する。本研究では、(1)ビジネスプロセスをモデリングする際にプロセス中に現れるリスクと統制活動(コントロール)の形式記述方法、(2)ビジネスプロセスの安全性の形式検証法を提案することが成果である。モデリングのアプローチとしては、リスクパターンとコントロールパターンの発見を行い、モデリングパターンを確立する。リスクとコントロールのパターンを明らかにし、仕様の記述のパターンを作る。検証のアプローチは以下の戦略で行う。(i)リスクが起こらない(不正なアクションがなく、すべてのアクションは正しく行われる)ビジネスプロセスのOTSを記述する。(ii)リスクとコントロールを含んだビジネスプロセスのOTSを記述する。このOTSモデルでは、不正なアクションがあり、それによって不適切な状態へ到達可能である。コントロールはリスクを削減または予防するためのアクションである。(iii)(i)と(ii)で作成したOTSが等価であることを証明することによって、(ii)のビジネスプロセスはコントロールによってリスクのないビジネスプロセスと同じ振舞いになっていることが検証できる。
|