研究課題
基盤研究(B)
ドメイン仕様や要求仕様などの問題モデルの検証技術の実用化を目指し、証明スコア法に基づく対話型検証法の最重要の技術課題である帰納法と場合分けに関し以下の研究開発を行う。(1) 多様な問題領域で有効な帰納法の開発 : 証明スコア法による検証法の基本的な推論スキーマは、再帰的に定義されたデータ型やプロセス型に関する数学的帰納法である。すでに多くの応用領域において帰納法による検証事例を蓄積しているが、それらにおける帰納法は個々の問題ごとに個別的になる傾向がある。これを改善し、実用的な検証技術を開発するために、蓄積した事例における帰納法の適用法を分析・体系化することで、より汎用的な帰納法を開発する。(2) 多様な問題領域で有効な場合分けの方法の開発 : 証明スコア法による検証の要点は、問題モデルの定義(形式仕様)に基づきすべての可能な場合を洗い出し、それらをもれ無く記述し、その各々について論理的なチェックを行うコードを確実に実行することで、検証を完成することである。このような場合分けに基づく証明スコア法が、多くの問題モデルに対して有効であることを事例研究で確認しているが、場合分けは個々の問題ごとに個別的で煩瑣になることが多い。これを改善し実用的な検証技術を開発するために、多様な問題領域で有効な汎用的な場合分けの方法を開発する。
すべて 2008 2007 2006 その他
すべて 雑誌論文 (4件) (うち査読あり 4件) 学会発表 (1件) 備考 (1件)
日本ソフトウェア科学会論文誌 25(2)
ページ: 1-13
1st VSTTE, LNCS 4171, Springer
ページ: 277-290
World Scientific Vol.17, No.6
ページ: 783-804
Elsevier 66(2)
ページ: 162-180
http://www.ldl.jaist.ac.jp/cafeobj
