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

• 研究課題/領域番号: 22700032
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 神戸大学
• 研究代表者: 番原 睦則 神戸大学, 情報基盤センター, 准教授 (80290774)
• 研究期間 (年度): 2010 – 2012
• 研究課題ステータス: 完了 (2012年度)
• 配分額: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円); 2012年度: 650千円 (直接経費: 500千円、間接経費: 150千円); 2011年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2010年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
• キーワード: 組合せテスト / SAT / 制約プログラミング / 解集合プログラミング / SAT技術 / テストケース生成 / 被覆配列 / 制約充足問題 / 論理プログラミング

研究概要

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

研究成果

• [雑誌論文] 位取り記数法に基づく整数有限領域上の制約充足問題のコンパクトかつ効率的なSAT符号化 (2013)
  • 著者名/発表者名: 丹生智也, 田村直之, 番原睦則
  • 雑誌名: コンピュータ ソフトウェア 巻: 30 号: 1 ページ: 1_211-1_230
  • DOI: 10.11309/jssst.30.1_211
  • NAID: 130004549312
  • ISSN: 0289-6540
  • 査読あり
• [雑誌論文] Scala上の制約プログラミング用ドメイン特化言語Coprisについて (2012)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 雑誌名: コンピュータ ソフトウェア 巻: 29 号: 4 ページ: 4_114-4_129
  • DOI: 10.11309/jssst.29.4_114
  • NAID: 130004549288
  • ISSN: 0289-6540
  • 査読あり
• [雑誌論文] ＳＡＴ符号化を用いた釣合い型不完備ブロック計画の構成 (2012)
  • 著者名/発表者名: 松中春樹, 丹生智也, 番原睦則, 田村直之
  • 雑誌名: 人工知能学会論文誌 巻: 27 号: 2 ページ: 10-15
  • DOI: 10.1527/tjsai.27.10
  • NAID: 130001878739
  • ISSN: 1346-0714, 1346-8030
  • 査読あり
• [雑誌論文] Generating Event-Sequence Test Cases by Answer Set Programming with the Incidence Matrix (2012)
  • 著者名/発表者名: Mutsunori Banbara
  • 雑誌名: The 28th International Conference on Logic Programming (ICLP 2012) 巻: LIPIcs 17 ページ: 86-97
  • DOI: 10.4230/LIPIcs.ICLP.2012.86
  • 査読あり
• [雑誌論文] Azucar: A SAT-Based CSP Solver Using Compact Order Encoding (2012)
  • 著者名/発表者名: Tomoya Tanjo
  • 雑誌名: The 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012) 巻: LNCS 7317 ページ: 456-462
  • DOI: 10.1007/978-3-642-31612-8_37
  • ISBN: 9783642316111, 9783642316128
  • 査読あり
• [雑誌論文] 私のブックマーク:SATソルバー (2012)
  • 著者名/発表者名: 番原睦則, 田村直之, 井上克巳
  • 雑誌名: 人工知能学会誌 巻: (掲載決定)
• [雑誌論文] A Compact and Efficient SAT-Encoding of Finite Domain CSP (2011)
  • 著者名/発表者名: Tomoya Tanjo, Naoyuki Tamura, Mutsunori Banbara
  • 雑誌名: Proc.of the 14th Int'l Conf.on Theory and Applications of Satisfiability Testing (SAT 2011), LNCS 6695 ページ: 375-376
  • 査読あり
• [雑誌論文] Proposal of a compact and efficient SAT encoding using a numeral system of anybase (2011)
  • 著者名/発表者名: Tomoya Tanjo, Naoyuki Tamura, Mutsunori Banbara
  • 雑誌名: Proc.of the 1st Int'l Workshop on the Cross-Fertilization Between CSP and SAT (CSPSAT 2011)
  • 査読あり
• [雑誌論文] 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) 号: 3-4 ページ: 467-487
  • DOI: 10.3233/fi-2010-314
  • 査読あり
• [雑誌論文] SAT変換に基づく制約ソルバーとその性能評価 (2010)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 雑誌名: コンピュータ ソフトウェア 巻: 27 号: 4 ページ: 183-196
  • DOI: 10.11309/jssst.27.4_183
  • NAID: 130004549193
  • ISSN: 0289-6540
  • 査読あり
• [雑誌論文] Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers (2010)
  • 著者名/発表者名: M.Banbara, H.Matsunaka, N.Tamura, K.Inoue
  • 雑誌名: 17th Int'l Conf.on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-17) ページ: 112-126
  • 査読あり
• [学会発表] 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
• [学会発表] Azucar:コンパクト順序符号化を用いたSAT型制約ソルバー (2012)
  • 著者名/発表者名: 丹生智也, 田村直之, 番原睦則
  • 学会等名: 第14回プログラミングおよびプログラミング言語ワークショップ(PPL2012)
  • 発表場所: むさし(和歌山県)
  • 年月日: 2012-03-08
• [学会発表] 位収り記数法に基づく整数有限領域上の制約充足問題のコンパクトかつ効率的SAT符号化 (2011)
  • 著者名/発表者名: 丹生智也, 田村直之, 番原睦則
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター(沖縄県)
  • 年月日: 2011-09-27
• [学会発表] SAT型制約ソルバーSugarとScalaインターフェイスについて (2011)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター(沖縄県)
  • 年月日: 2011-09-27
• [学会発表] SAT符号化を用いた釣合い型不完備ブロック計画の構成 (2011)
  • 著者名/発表者名: 松中春樹, 丹生智也, 番原睦則, 田村直之
  • 学会等名: 2011年度人工知能学会全国大会(JSAI-2011)
  • 発表場所: アイーナいわて県民情報交流センター(岩手県)
  • 年月日: 2011-06-03
• [学会発表] 整数有限領域上の制約充足問題のコンパクトかつ効率的なSAT符号化 (2011)
  • 著者名/発表者名: 丹生智也, 田村直之, 番原睦則
  • 学会等名: 2011年度人工知能学会全国大会(JSAI-2011)
  • 発表場所: アイーナいわて県民情報交流センター(岩手県)
  • 年月日: 2011-06-03
• [学会発表] SAT型制約ソルバーSugarについて (2011)
  • 著者名/発表者名: 田村直之, 丹生智也, 番原睦則
  • 学会等名: 第81回人工知能学会人工知能基本問題研究会
  • 発表場所: 山梨大学(山梨県)(招待講演)
  • 年月日: 2011-01-31
• [学会発表] 整数有限領域上の線形制約充足問題のコンパクトかつ効率的なSAT符号化提案 (2011)
  • 著者名/発表者名: 丹生智也, 田村直之, 番原睦則
  • 学会等名: 第81回人工知能学会人工知能基本問題研究会
  • 発表場所: 山梨大学(山梨県)
  • 年月日: 2011-01-31
• [学会発表] SAT技術を用いた組合せテストケース生成 (2010)
  • 著者名/発表者名: 番原睦則, 松中春樹, 田村直之, 井上克巳
  • 学会等名: 日本ソフトウェア科学会第27回大会
  • 発表場所: 津田塾大学(東京都)
  • 年月日: 2010-09-13
• [学会発表] Towards a Compact and Efficient SAT-Encoding of Finite Linear CSP (2010)
  • 著者名/発表者名: T.Tanjo, N.Tamura, M.Banbara
  • 学会等名: 9th Int'l Workshop on Constraint Modelling and Reformulation (ModRef 2010)
  • 発表場所: St.Andrews (Scotland)
  • 年月日: 2010-09-06
• [学会発表] Solving Constraint Satisfaction Problems by a SAT Solver (2010)
  • 著者名/発表者名: N.Tamura, T.Tanjo, M.Banbara
  • 学会等名: Joint Workshop on Implementation of Constraint Logic Programming Systems and Logic-based Methods in Program-ming Environments (CICLOPS-WLPE 2010)
  • 発表場所: Edinburgh (Scotland)(招待講演)
  • 年月日: 2010-07-15
• [学会発表] Solving Constraint Satisfaction Problems with SAT Technology (2010)
  • 著者名/発表者名: N.Tamura, T.Tanjo, M.Banbara
  • 学会等名: 10th Int'l Symp.on Functional and Logic Programming (FLOPS 2010)
  • 発表場所: 東北大学(宮城県)(招待講演)
  • 年月日: 2010-04-19
• [学会発表] SAT符号化を用いたパッキング配列の構成
  • 著者名/発表者名: 則武治樹
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013)
  • 発表場所: 会津若松市 (福島県)
• [学会発表] Scarab: Scala上で実現されたSAT型制約プログラミングシステムのための高速開発ツール
  • 著者名/発表者名: 宋剛秀
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ (PPL 2013)
  • 発表場所: 会津若松市 (福島県)
• [学会発表] Generating Event-Sequence Test Cases by Constraint Programming and Answer Set Programming
  • 著者名/発表者名: Mutsunori Banbara
  • 学会等名: The 2012 CRIL-NII Collaborative Meeting on Reasoning about Dynamic Constraint Networks
  • 発表場所: University of Artois (Lens, France)
• [学会発表] Domain-Specific Language Copris for Constraint Programming in Scala
  • 著者名/発表者名: Naoyuki Tamura
  • 学会等名: The 2012 CRIL-NII Collaborative Meeting on Reasoning about Dynamic Constraint Networks
  • 発表場所: University of Artois (Lens, France)
• [学会発表] Towards Incremental SAT-based CSP Solving: Experimental Results for the Hamiltonian Cycle Problem
  • 著者名/発表者名: Takehide Soh
  • 学会等名: The 2012 CRIL-NII Collaborative Meeting on Reasoning about Dynamic Constraint Networks
  • 発表場所: University of Artois (Lens, France)
• [学会発表] カリキュラムベースのコース時間割問題の擬似ブール最適化問題への符号化
  • 著者名/発表者名: 鈴江美奈
  • 学会等名: 日本ソフトウェア科学会第29回大会
  • 発表場所: 法政大学 (東京都)
• [学会発表] SAT 技術を用いた組合せテストケース生成
  • 著者名/発表者名: 番原睦則
  • 学会等名: ERATO セミナー, JST ERATO 湊離散構造処理系プロジェクト
  • 発表場所: JST ERATO 湊離散構造処理系プロジェクト, 関西サテライトラボ (大阪府)
• [学会発表] 制約充足問題のSAT符号化を用いたパッキング配列の構成
  • 著者名/発表者名: 則武治樹
  • 学会等名: 第26回人工知能学会全国大会
  • 発表場所: 山口県教育会館 (山口県)
• [学会発表] ハミルトン閉路問題のSAT符号化に関する研究
  • 著者名/発表者名: 船越泰輔
  • 学会等名: 第26回人工知能学会全国大会
  • 発表場所: 山口県教育会館 (山口県)
• [備考] PBSugar: SAT技術を用いた擬似ブール制約ソルバー
• [備考] Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems
• [備考] Copris: Scala上の制約プログラミングシステム
• [備考] Sugar: SAT技術を用いた制約ソルバー
• [備考] Azucar: A SAT-based Constraint Solver based on Compact Order Encoding
  • URL: http://http://code.google.com/p/azucarsolver/