2007 Fiscal Year Annual Research Report
| Project/Area Number |
19500035
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
田原 康之 National Institute of Informatics, アーキテクチャ科学研究系, 特任准教授 (30390602)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
本位田 真一 国立情報学研究所, アーキテクチャ科学研究系, 教授 (70332153)
|
|---|
| Keywords | 計算機システム / 情報システム / ソフトウェア開発効率化・安定化 / ソフトウェア学 / ソフトウェア検証 |
|---|
| Research Abstract |
本研究の目的は、モテル検査手法による設計モテル検証フロセスにおいて、形式モテルの厳密さと、非形式的記述のあいまいさとのギャップを縮め、検証作業を容易にする技術を確立し、枝術を適用するための支援ツールを開発することである。
上記のギャップの重要な原因の1つが、意味論の有無である。形式モデルは、意味論によって数学的対象にマッピングされるため、厳密に扱えるのに対し、非形式的記述はそうではない。そこで、開発者が、容易に意味論を理解し、また必要に応じて意味論をカスタマイズすることにより、結果的に形式モデルの扱いを容易に可能とする。
平成19年度は、既存技術であるTemplate Semanticsをベースとした、形式モデルの意味論を参照・変更する枠組みの理論を確立し、さらに部分的に検証プロセスに適用するためのツールを開発・評価した。具体的には、開発者が非形式的記述による要求仕様と設計モデルに対し、形式モデルがそれらの意図を正確に反映するように、Template Parameterと呼ばれるデータを策定することにより、意味論を変更する方法を確立した。さらに、検証結果に対し、どの入力データを修正すべきかを特定し、意味論の修正が必要な場合に、適切にTemplate Parameterを修正する方法も確立した。また、上記枠組みを適用した検証プロセスを支援するツールのプロトタイプ第1版として、Template Semanticsに基づく枠組みに基づき、形式的振舞いモデルと性質記述から、モデル検査対象記述を自動生成するツールを開発し、ネットワーク家電の例題に適用してその有用性を評価した。
|
