2006 Fiscal Year Annual Research Report
| Project/Area Number |
18300008
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (40345658)
|
|---|
| Keywords | ソフトウェア工学 / システム検証 / 安全性・信頼性 / 形式手法 / 問題モデル / 振舞仕様 / 証明スコア / 帰納法 |
|---|
| Research Abstract |
証明スコア法における,(A)帰納法の適用法、(B)場合分けの方法、の二つの課題について、(1)データ型とプロセス型、(2)推論型検証と探索型検証、の2つの観点から、いままでに蓄積した事例を解析することを中心に研究を進め,提案している研究計画の妥当性を確認した.具体的には,以下を行った.
[A]事例の解析:(a)事例における「帰納法の適用法」を「データ型とプロセス型」ならびに「推論型検証と探索型検証」の観点から分析した.(b)事例における「場合分けの方法」を「データ型とプロセス型」ならびに「推論型検証と探索型検証」の観点から分析した.
[B]帰納法の適用法の定式化:[A]の事例の解析結果に基づき汎用的な帰納法の適用法を定式化した.
[C]場合分けの方法の定式化:[A]の事例の解析結果に基づき汎用的な場合分けの方法を定式化した.
[D]検証方法論の体系化:[B]と[C]の定式化にも基づき証明スコア法による検証方法論を体系化し,その正しさ(健全性)を証明した.
|
Research Products
(9 results)
