2012 Fiscal Year Annual Research Report
| Project/Area Number |
24300010
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Section | 一般 |
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
細部 博史 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (60321577)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
中島 震 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60350211)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | ソフトウェア / デバッグ / 制約 |
|---|
| Research Abstract |
本研究はソフトウェアの自動デバッグ方式の構築を目的とし,特にプログラムの誤り特定手法の開発に重点を置く.そのためのアプローチとして制約の概念を採用する.具体的には,事後条件違反を生じる入力をモデル検査によって求め,入力,プログラム,事後条件から制約充足問題を構成した上で,違反の原因となった制約を特定し,プログラム中の対応する部分を誤り箇所の候補として提示する.本研究では効果的な誤り特定を行うために,特に柔らかい制約の考え方を採用する.またこの方法を応用して誤りの修正候補の提示も実現する.本研究ではこのような柔らかい制約を用いた自動デバッグ方式を構築し,C言語を対象とする自動デバッグツールを開発する.
初年度である平成24年度には,特に制約処理手法の高度化に関する研究を行った.従来の研究ではプログラムの誤り特定のために主に充足可能性判定の手法が使われていたのに対して,本研究では制約プログラミングの手法を採用していることが特徴である.充足可能性判定の手法でも算術的な式を論理式に変換することで扱うことができるが,一般に論理式による算術式の表現は単純ではなく,C言語で書かれたプログラムを変換すると問題が大きくなる.一方,制約プログラミングでは論理式による内部表現を用いることなく,算術式を含む問題を扱うことができる.しかし,C言語のプログラムには論理式が含まれることも多くあり,従来の制約プログラミングの手法は逆にそのような場合に適していない.本研究では制約プログラミングによって算術式と論理式の両方に適切に対処し,さらに柔らかい制約として処理することのできる手法を構築した.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究は順調に進展しているが,その成果を国際会議で発表する必要がある.
|
| Strategy for Future Research Activity |
研究目標であるソフトウェアの自動デバッグ方式の構築に向けて,プログラムの誤り特定手法の開発に重点を置きながら,C言語を対象とする自動デバッグツールの開発を継続する.
|
| Expenditure Plans for the Next FY Research Funding |
当該年度内に本研究に関する国際会議発表を行わなかったことと,本研究費による海外在住の研究協力者の招聘を行わなかったことにより直接経費次年度使用額が生じた.これらは次年度に行う予定である.
|
