研究課題/領域番号 |
18300008
|
研究種目 |
基盤研究(B)
|
配分区分 | 補助金 |
応募区分 | 一般 |
研究分野 |
ソフトウエア
|
研究機関 | 北陸先端科学技術大学院大学 |
研究代表者 |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
研究分担者 |
中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (40345658)
|
連携研究者 |
中村 正樹 金沢大学, 電子情報学系, 助教 (40345658)
|
研究期間 (年度) |
2006 – 2009
|
研究課題ステータス |
完了 (2009年度)
|
配分額 *注記 |
18,890千円 (直接経費: 15,200千円、間接経費: 3,690千円)
2009年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円)
2008年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円)
2007年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円)
2006年度: 2,900千円 (直接経費: 2,900千円)
|
キーワード | 仕様記述 / 仕様検証 / 形式手法 / 問題モデル / 証明スコア / 帰納法 / 場合分け / 仕様記述・仕様検証 / システム検証 / ソフトウェア工学 / 振舞仕様 / 安全性・信頼性 / 安全性 / 信頼性 |
研究概要 |
「帰納法」と「場合分け」は、問題モデル(問題領域や応用領域におけるモデル)の証明スコアによる検証法の基本技術である。本研究では、多様な応用分野で有効な帰納法と場合分けについて以下の成果を得た。(1)帰納法をデータ型・プロセス型の帰納的な構造に基づき定式化した。(2)場合分けを構成子からの項の生成に基づき定式化した。(3)(1),(2)に基づき、汎用的な証明規則を定式化するとともに、推論と探索を融合した強力な検証法を開発した。
|