| 研究概要 |
本研究の目的は,様々な論理推論エンジンを用いて,ソフトウェアの信頼性・安全性を高めるための現実的かつ効果的なテストケースを自動生成することである.本年度は,組合せテストケース生成問題のSAT符号化に関する研究を行った.
ソフトウェア/ハードウェアのテストは,製品を開発する過程において重要な役割を果たしている.しかし,たとえ小規模な製品であっても,網羅的テストはテストケースの増大を招き現実的に実行不可能である.組合せテストはソフトウェア/ハードウェアのテスト手法の一つである.この手法の特長は,欠陥の多くは少数のパラメータの組み合わせによって発生するという観測を元に,テストケースの増大を回避し,現実的かつ効果的なテストを行える点である.組合せテストケース生成問題は,組合せデザイン分野の被覆配列(Covering Array ; CA)を生成するCA問題に帰着できる.
本年度の研究では,CA問題に対して,新しいSAT符号化法を二つ提案した.一つは,順序符号化法をベースにしたものである.もう一つは,Hnich符号化法と順序符号化法を融合したものである.小中規模のCA問題に対する実行実験を行った結果,提案手法は様々な既存手法(群論等の数学的手法,貪欲法,局所探索法など)と比較して,ほぼ同等の結果を得ることができた.さらに,2009年に出版されたHandbook of Satisability中に記載されている未解決問題に対して,既知の最良値が最適値であることを証明することに成功した.加えて,いくつかの問題に対して,既知の下限を更新することにも成功した.
|
