様々な論理推論エンジンを用いた組み合わせテストのテストケース自動生成

2012 年度 研究成果報告書

• 研究課題/領域番号: 22700032
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 神戸大学
• 研究代表者: 番原 睦則 神戸大学, 情報基盤センター, 准教授 (80290774)
• 研究期間 (年度): 2010 – 2012
• キーワード: 組合せテスト / SAT / 制約プログラミング / 解集合プログラミング

研究概要

組合せテストは,ソフトウェアの信頼性・安全性を高めるためのソフトウェア検証手法の 1つである.本研究では,組合せテストのテストケース生成の性能向上を目指し,SAT ソルバー,制約ソルバー,解集合ソルバーを用いたテストケース自動生成ツールに関する研究開発を行った.提案手法を実装した 3つのツールは,組合せデザイン・ハンドブック等に記載されているベンチマークに対して,様々な既存手法で得られた既知の最良値を更新することに成功した.

研究成果

• [雑誌論文] 位取り記数法に基づく整数有限領域上の制約充足問題のコンパクトかつ効率的なSAT符号化 (2013)
  • 著者名/発表者名: 丹生智也, 田村直之, 番原睦則
  • 雑誌名: コンピュータソフトウェア 巻: 30(1) ページ: 211-230
  • DOI: DOI:10.11309/jssst.30.1_211
  • 査読あり
• [雑誌論文] Scala上の制約プログラミング用ドメイン特化言語Coprisについて (2012)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 雑誌名: コンピュータソフトウェア 巻: 29(4) ページ: 114-129
  • DOI: DOI:10.11309/jssst.29.4_114
  • 査読あり
• [雑誌論文] SAT符号化を用いた釣合い型不完備ブロック計画の構成 (2012)
  • 著者名/発表者名: 松中春樹, 丹生智也, 番原睦則,田村直之
  • 雑誌名: 人工知能学会論文誌 巻: 27(2) ページ: 10-15
  • DOI: DOI:10.1527/tjsai.27.10
  • 査読あり
• [雑誌論文] A SAT-Based Method for Solving the Two-dimensional Strip Packing Problem (2010)
  • 著者名/発表者名: Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara and Hidetomo Nabeshima
  • 雑誌名: Fundamenta Informaticae 巻: 102(3-4) ページ: 467-487
  • DOI: DOI:10.3233/FI-2010-314
  • 査読あり
• [雑誌論文] SAT変換に基づく制約ソルバーとその性能評価 (2010)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 雑誌名: コンピュータソフトウェア 巻: 27(4) ページ: 183-196
  • DOI: DOI:10.11309/jssst.27.4_183
  • 査読あり
• [学会発表] Scarab:Scala上で実現された SAT型制約プログラミングシステムのための高速開発ツール (2013)
  • 著者名/発表者名: 宋剛秀,田村直之, 番原睦則
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013),日本ソフトウェア科学会
  • 発表場所: 福島県会津若松 東山温泉御宿東鳳 (福島県会津若松市東山町)
  • 年月日: 2013-03-05
• [学会発表] Generating Event-Sequence Test Cases by Constraint Programming and Answer Set Programming (2012)
  • 著者名/発表者名: Mutsunori Banbara, Naoyuki Tamura, Katsumi Inoue, and Hidetomo Nabeshima
  • 学会等名: The 2012 CRIL-NII Collaborative Meeting on Reasoning about Dynamic Constraint Networks
  • 発表場所: Universite d'Artois, Lens, France
  • 年月日: 2012-11-23
• [学会発表] SAT技術を用いた組合せテストケース生成 (2012)
  • 著者名/発表者名: 番原睦則
  • 学会等名: ERATOセミナー, JST ERATO湊離散構造処理系プロジェクト
  • 発表場所: 関西サテライトラボ(大阪府大阪市北区芝田)
  • 年月日: 2012-07-06
• [学会発表] Azucar:コンパクト順序符号化を用いたSAT型制約ソルバー (2012)
  • 著者名/発表者名: 丹生智也, 田村直之,番原睦則
  • 学会等名: 第14回プログラミングおよびプログラミング言語ワークショップ (PPL 2012), 日本ソフトウェア科学会
  • 発表場所: 和歌山県 南紀白浜 むさし (和歌山県西牟婁郡白浜町)
  • 年月日: 2012-03-08
• [備考] PBSugar: SAT技術を用いた擬似ブール制約ソルバー
  • URL: http://http://bach.istc.kobe-u.ac.jp/pb sugar/
• [備考] Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems
  • URL: http://http://kix.istc.kobe-u.ac.jp/~so h/scarab/
• [備考] Copris: Scala上の制約プログラミングシステム
  • URL: http://http://bach.istc.kobe-u.ac.jp/co pris/
• [備考] Sugar: SAT技術を用いた制約ソルバー
  • URL: http://http://bach.istc.kobe-u.ac.jp/su gar/
• [備考] Azucar: A SAT-based Constraint Solver based on Compact Order Encoding
  • URL: http://http://code.google.com/p/azucarsolver/