2008 Fiscal Year Annual Research Report
| Project/Area Number |
18300008
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
二木 厚吉 Japan Advanced Institute of Science and Technology, 情報科学研究科, 教授 (50251971)
|
|---|
| Keywords | ソフトウェア工学 / システム検証 / 安全性・信頼性 / 形式手法 / 問題モデル / 振舞仕様 / 証明スコア / 帰納法 |
|---|
| Research Abstract |
H18年度とH19年度に開発した種々の形式仕様と証明スコアの分析に基づき、帰納法と場合分けの方法を整理しつつ、(帰納法に基づく)推論と探索を融合した検証法を体系化し、「証明スコア作成ツール」を設計し一部開発した。ツールの設計と開発は、「人間と機械が各々の優れた能力を発揮しつつ協力して行う検証を支援する」という方針に従い、探索を支援する機能に焦点を絞って行った。すなわち、帰納法に基づく推論を用いる証明スコアの作成は人間が行い、探索を用いる検証をツール(システム、機械)が支援する、という方針を採用した。
具体的には、これまでの研究で得られた、(1)帰納法と場合分けの適用法、(2)推論と探索を融合した検証法、に関する以下のような知見に基づきツールの設計と開発を行った。[A]帰納法を用いた推論に基づく検証は、帰納スキーマの選択、帰納命題(帰納法で証明すべき命題)や補題の特定、などの検証すべき問題に関する深い理解を必要とするので、人間が証明スコアを作成しつつ対話的に行うのが適当である。[B]探索は、すべての可能な場合を網羅的に検査することにより、場合分けを自動化する。探索による網羅的な場合分けはツール化しシステムに支援させるのが適当である。[C]抽象化(abstraction)などにより、命題の検証を網羅的な場合分けの探索に帰着させるためには、一般的には帰納法による推論が必要である。この部分は人間が証明スコアを作成しつつ対話的に行うのが適当である。
|
