2004 Fiscal Year Annual Research Report
| Project/Area Number |
15300007
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (40345658)
|
|---|
| Keywords | 問題モデル / システム検証 / システム安全性 / フォーマルメソッド / 振舞仕様 / 要求仕様 / CafeOBJ |
|---|
| Research Abstract |
認証プロトコルの安全性検証などの事例研究を通して得られた知見をもとに「適切な抽象度を持った振舞仕様の作成」「探索型と推論型の検証法の融合」に関して以下のようなアプローチで研究を遂行した.
1.適切な抽象度を持った振舞仕様の作成
A)OTS/CafeOBJ仕様による事例研究を通して得られた知見をもとに,昨年度から引き続き行われているbuilt-in基本データ型のライブラリの充実に加え,共通して用いられることが多いユーザ定義の抽象データ型についても分析し,その検証法と共に整理した.
B)OTS/CafeOBJ仕様による認証プロトコルの安全性検証は,仕様で用いられる各データ型について共通する部分が明確になってきており,検証においては状態遷移の回数に関する帰納法が有効であることがすでに分かっているため,その方法論はある程度確立できたと言える.本年度もこうして得られた方法論をもとに認証プロトコルの安全性検証を行った.
2.探索型と推論型の検証法の融合
A)昨年度から引き続き,OTS/CafeOBJ仕様からの各種モデル検査器への変換手法の研究を行った.特に同じ系統の代数型仕様言語であることからMaudeモデル検査器への変換手法について焦点をあてて研究を行った.
B)推論型検証法(OTS/CafeOBJ)における検証作業の自動化を充実させた.現在のところ探索型検証法(Maude, SMV)と推論型検証法(OTS/CafeOBJ)の見た目上の最も大きな違いは計算機による検証の自動化の部分である.完全自動な探索型検証法に対して推論型検証法は手作業に負う部分が大きいが,まだ自動化の余地が多く残されている.推論型検証法の自動化を充実させることにより探索型検証法と推論型検証法のより本質的な違いを明確にできる.
|
