Verification of Problem Models with Proof Scores
Project/Area Number |
18300008
|
Research Category |
Grant-in-Aid for Scientific Research (B)
|
Allocation Type | Single-year Grants |
Section | 一般 |
Research Field |
Software
|
Research Institution | Japan Advanced Institute of Science and Technology |
Principal Investigator |
FUTATSUGI Kokichi Japan Advanced Institute of Science and Technology, 情報科学研究科, 教授 (50251971)
|
Co-Investigator(Kenkyū-buntansha) |
中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (40345658)
|
Co-Investigator(Renkei-kenkyūsha) |
NAKAMURA Masaki 金沢大学, 電子情報学系, 助教 (40345658)
|
Project Period (FY) |
2006 – 2009
|
Project Status |
Completed (Fiscal Year 2009)
|
Budget Amount *help |
¥18,890,000 (Direct Cost: ¥15,200,000、Indirect Cost: ¥3,690,000)
Fiscal Year 2009: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000)
Fiscal Year 2008: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000)
Fiscal Year 2007: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000)
Fiscal Year 2006: ¥2,900,000 (Direct Cost: ¥2,900,000)
|
Keywords | 仕様記述 / 仕様検証 / 形式手法 / 問題モデル / 証明スコア / 帰納法 / 場合分け / 仕様記述・仕様検証 / システム検証 / ソフトウェア工学 / 振舞仕様 / 安全性・信頼性 / 安全性 / 信頼性 |
Research Abstract |
「帰納法」と「場合分け」は、問題モデル(問題領域や応用領域におけるモデル)の証明スコアによる検証法の基本技術である。本研究では、多様な応用分野で有効な帰納法と場合分けについて以下の成果を得た。(1)帰納法をデータ型・プロセス型の帰納的な構造に基づき定式化した。(2)場合分けを構成子からの項の生成に基づき定式化した。(3)(1),(2)に基づき、汎用的な証明規則を定式化するとともに、推論と探索を融合した強力な検証法を開発した。
|
Report
(6 results)
Research Products
(66 results)