2007 Fiscal Year Annual Research Report
電子社会における基盤ドメインの形式モデルの記述と検証
Project/Area Number |
07J54142
|
Research Institution | Japan Advanced Institute of Science and Technology |
Principal Investigator |
有本 泰仁 Japan Advanced Institute of Science and Technology, 情報科学研究科, 特別研究員(DC1)
|
Keywords | 形式手法 / ドメイン分析 / 形式ドメイン記述 |
Research Abstract |
この研究は電子社会における基盤ドメインのモデルの形式記述を行い、その記述の検証を行うことを目的としている.具体的には,(1)ドメイン上で満たされる性質を明らかにし,(2)それを基にドメインモデルの形式記述を行い,(3)その記述が(1)で抽出された性質を満たしているか形式検証を行う.つまり,(1)のドメインの性質の明確化は対象ドメイン上での暗黙知を明らかにし,(2)のドメインモデルの形式化は(1)で明らかになった性質の形式化,またドメインの振舞いの厳密な記述のために行われ,(3)の形式検証で,(2)で得られた記述の検証が可能となる.本研究は電子社会システム(社会システムのうちで情報システムとして実現されるもの)を形式していく上で,社会システムの性質(対象ドメイン上での暗黙知)の明確化及び社会システム(対象ドメイン)のモデルの厳密な記述(形式記述),そして,モデルの検証を行えるという点で重要な役割を担う.本研究で得られたドメインモデルは電子社会システムの形式仕様として利用することができるからである.また,ドメインモデルを再利用する際,変更が加えられたとしても,そのドメインが満たして欲しい性質を検証することでモデルの整合性が検証することができる. 現在までにドメインモデルの形式記述方法を簡略化した病院ドメインの例を基に,OTS/CafeOBJ法を用いてどのようにドメインの形式記述が行えるのかという実験を行った,この実験により,どのようにドメインの形式記述を行えば,記述の検証が効果的に行えるのかが明らかになった.また,内部統制ドメイン上での性質の分析を現在行っており,その分析と並行して,病院ドメインの記述から得られた知見を基に,内部統制ドメインの形式記述に取り掛かっている.
|
Research Products
(1 results)