2005 Fiscal Year Annual Research Report
| Project/Area Number |
15300007
|
|---|
| Research Institution | Japan Advanced Institute Science and Technology |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (40345658)
|
|---|
| Keywords | 問題モデル / システム検証 / システム安全性 / フォーマルメソッド / 振舞仕様 / 要求仕様 / CafeOBJ |
|---|
| Research Abstract |
最終年度である本年度は、2年間を通じてその有効性が明らかとなったOTS/CafeOBJ方法論の有効性を高めるために、「適切な抽象度を持った振舞仕様の作成」と「探索型と推論型の検証法の融合」の二つのテーマについて以下のような研究を行い、本研究の成果を取りまとめた。
1.適切な抽象度を持った振舞仕様の作成:
OTS/CafeOBJ方法論では,問題領域で観測可能なデータ型をCafeOBJ言語における抽象データ型として定義し,それに基づきシステムの振舞を観測されるデータ値の変化としてモデル化する。これまでの研究からデータ型の部分は比較的汎用的に利用でき,観測値の変化を定義する部分は問題領域に依存することが多いことが分かっている。これらの成果に基づき、基本データ型については汎用型として、OTSモデルに基づく状態型については問題領域への依存型として、検証事例を整理し、適切な抽象度を持った振舞仕様を作成するガイドラインを示した。
2.探索型と推論型の検証法の融合:
これまでの研究結果から,OTS/CafeOBJ方法論では,モデル検査器を用いた自動検証・反例発見と推論型検証を適切に使い分けることが特に有効であるとの知見が得られた。これに基づき、モデル検査器と推論型検証の適切な使い分けを支援する、Maude言語のモデル検査器への変換システム開発し、いくつかの例題についてその有効性を確認した。
|
