2008 Fiscal Year Annual Research Report
| Project/Area Number |
19500035
|
|---|
| Research Institution | The University of Electro-Communications |
|---|
Principal Investigator |
田原 康之 The University of Electro-Communications, 大学院・情報システム学研究科, 准教授 (30390602)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
本位田 真一 国立情報学研究所, アーキテクチャ科学研究系, 教授 (70332153)
|
|---|
| Keywords | 計算機システム / 情報システム / ソフトウェア開発効率化・安定化 / ソフトウェア学 / ソフトウェア検証 |
|---|
| Research Abstract |
本研究の目的は、モデル検査手法による設計モデル検証プロセスにおいて、形式モデルの厳密さと、非形式的記述のあいまいさとのギャップを縮め、検証作業を容易にする技術を確立し、技術を適用するための支援ツールを開発することである。
上記のギャップの重要な原因の1つが、意味論の有無である。形式モデルは、意味論によって数学的対象にマッピングされるため、厳密に扱えるのに対し、非形式的記述はそうではない。そこで、開発者が、容易に意味論を理解し、また必要に応じて意味論をカスタマイズすることにより、結果的に形式モデルの扱いを容易に可能とする。
平成20年度は、平成19年度に確立した、形式モデルの意味論を参照・変更する枠組みを適用した検証プロセスに対し、実際の検証作業に適用する場合のノウハウを抽出・整理し、さらにノウハウを検証プロセスに適用するためのツールを開発・評価した。
具体的には、平成19年度に確立した検証プロセスを、実際の検証作業に適用するために必要な、詳細なノウハウを抽出し、検証プロセスに沿って整理することにより、開発者がノウハウを容易に利用可能とした。たとえば、ネットワーク家電の制御ソフトウェアにおける、タイムアウト処理の厳密な振舞いの定義について、単純なモデルから始めて、検証・修正の繰り返しを行い、より正確な定義に近づける、といったノウハウを確立した。また、検証プロセスを支援するツールのプロトタイプ第2版として、意味論、形式モデル、および非形式的記述の記述・デバッグ支援ツールを構築した。さらに、ツールをネットワーク家電の例題に適用し、その有用性を評価した。
|
