電子社会における基盤ドメインの形式モデルの記述と検証
Project/Area Number |
07J54142
|
Research Category |
Grant-in-Aid for JSPS Fellows
|
Allocation Type | Single-year Grants |
Section | 国内 |
Research Field |
Software
|
Research Institution | Japan Advanced Institute of Science and Technology |
Principal Investigator |
有本 泰仁 Japan Advanced Institute of Science and Technology, 情報科学研究科, 特別研究員(DC1)
|
Project Period (FY) |
2007 – 2008
|
Project Status |
Completed (Fiscal Year 2008)
|
Budget Amount *help |
¥1,800,000 (Direct Cost: ¥1,800,000)
Fiscal Year 2008: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2007: ¥900,000 (Direct Cost: ¥900,000)
|
Keywords | 形式手法 / ドメイン工学 / ビジネスプロセスモデリング / 内部統制 / ドメイン分析 / 形式ドメイン記述 |
Research Abstract |
近年、相次ぐ有名企業のスキャンダルから内部統制の重要性が高まってきている。安心な電子社会の基盤となるドメインとして、ビジネスプロセスが考えられる。特に、ビジネスプロセスの中で内部統制としての統制活動がどのようにモデル化でき、それらの効力を科学的に検証できること、というのがより安心な電子社会を築くうえで重要になると考えられる。本研究では、Observational Transition System(OTS、ある種の状態遷移機械)でビジネスプロセスのモデリングを行い、代数仕様言語CafeOBJでビジネスプロセスモデルを記述、検証する方法を提案する。本研究では、(1)ビジネスプロセスをモデリングする際にプロセス中に現れるリスクと統制活動(コントロール)の形式記述方法、(2)ビジネスプロセスの安全性の形式検証法を提案することが成果である。モデリングのアプローチとしては、リスクパターンとコントロールパターンの発見を行い、モデリングパターンを確立する。リスクとコントロールのパターンを明らかにし、仕様の記述のパターンを作る。検証のアプローチは以下の戦略で行う。(i)リスクが起こらない(不正なアクションがなく、すべてのアクションは正しく行われる)ビジネスプロセスのOTSを記述する。(ii)リスクとコントロールを含んだビジネスプロセスのOTSを記述する。このOTSモデルでは、不正なアクションがあり、それによって不適切な状態へ到達可能である。コントロールはリスクを削減または予防するためのアクションである。(iii)(i)と(ii)で作成したOTSが等価であることを証明することによって、(ii)のビジネスプロセスはコントロールによってリスクのないビジネスプロセスと同じ振舞いになっていることが検証できる。
|
Report
(2 results)
Research Products
(2 results)