2008 Fiscal Year Self-evaluation Report
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)
|
|---|
| Project Period (FY) |
2006 – 2009
|
| Keywords | 仕様記述 / 仕様検証 / システム検証 / 安全性 / 信頼性 / 形式手法 / 問題モデル |
|---|
| Research Abstract |
ドメイン仕様や要求仕様などの問題モデルの検証技術の実用化を目指し、証明スコア法に基づく対話型検証法の最重要の技術課題である帰納法と場合分けに関し以下の研究開発を行う。
(1) 多様な問題領域で有効な帰納法の開発 : 証明スコア法による検証法の基本的な推論スキーマは、再帰的に定義されたデータ型やプロセス型に関する数学的帰納法である。すでに多くの応用領域において帰納法による検証事例を蓄積しているが、それらにおける帰納法は個々の問題ごとに個別的になる傾向がある。これを改善し、実用的な検証技術を開発するために、蓄積した事例における帰納法の適用法を分析・体系化することで、より汎用的な帰納法を開発する。
(2) 多様な問題領域で有効な場合分けの方法の開発 : 証明スコア法による検証の要点は、問題モデルの定義(形式仕様)に基づきすべての可能な場合を洗い出し、それらをもれ無く記述し、その各々について論理的なチェックを行うコードを確実に実行することで、検証を完成することである。このような場合分けに基づく証明スコア法が、多くの問題モデルに対して有効であることを事例研究で確認しているが、場合分けは個々の問題ごとに個別的で煩瑣になることが多い。これを改善し実用的な検証技術を開発するために、多様な問題領域で有効な汎用的な場合分けの方法を開発する。
|
Research Products
(6 results)
