SMT ソルバーとPDG 作成ツールを用 いたJava のテストケース自動導出手法の提案

佐々木, 幸広; ササキ, ユキヒロ; Sasaki, Yukihiro; 小林, 和貴; コバヤシ, カズキ; Kobayashi, Kazuki; 岡野, 浩三; オカノ, コウゾウ; Okano, Kozo; 楠本, 真二; クスモト, シンジ; Kusumoto, Shinji

このアイテムのアクセス数:95件（2022-10-03 05:30 集計）

このアイテムへのリンクには次のURLをご利用ください: https://hdl.handle.net/11094/27416

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	利用開始日	説明
itr111_481_055	pdf	655 KB	62	2014.04.11

論文情報

タイトル	SMT ソルバーとPDG 作成ツールを用いたJava のテストケース自動導出手法の提案
	Automatic derivation of test cases for Java using an SMT solver and a PDG generator
	SMT　ソルバー　ト　PDG　サクセイ　ツール　ヲ　モチイタ　Java　ノ　テスト　ケース　ジドウ　ドウシュツ　シュホウ　ノ　テイアン
著者	著者名佐々木, 幸広ササキ, ユキヒロ Sasaki, Yukihiro
	NRID 1000050332317 1000050332317 著者名小林, 和貴コバヤシ, カズキ Kobayashi, Kazuki
	NRID 1000070252632 1000070252632 著者名岡野, 浩三オカノ, コウゾウ Okano, Kozo
	NRID 1000030234438 1000030234438 著者名楠本, 真二クスモト, シンジ Kusumoto, Shinji
キーワード等	SMT ソルバ
	PDG
	Daikon
	テストケース
	Java
	SMT solver
	test case
抄録	Design by Contractに基づく表明の生成手法には静的生成手法と動的生成手法が存在する.動的生成手法では,テストケースを用いて引数やフィールド変数の値を変えながら対象メソッドを解析し,データを取得するため,比較的少ないコストで表明を生成できる.一方で,テストケースがどれだけの実行範囲をカバーしているかというテストケースの質が生成される表明の質に影響を与える.この問題に対し,インバリアントカバレッジという指標が存在する.本研究では対象メソッドのPDGからインバリアントカバレッジを満たす可能性のある実行パスを列挙しSMTソルバを用いてそのパスの実行可能性と具体的な引数値の導出を行う方法を提案する.また,複数の例題に適用し有効であることを確認した.
抄録	Assertions and Design by Contract play important roles for program understanding and program verification. In order to generate assertions, there are two kinds of methods, static analysis and dynamic analysis. Dynamic approach needs less CPU times, however suffers the test case depending problem in which the quality of assertions depends on the quality of test cases. Invariant coverage is one of indicator to specify the quality of test cases. In other words, the coverage of test cases affects the quality of generated assertions. The proposed method uses PDG of a target method to generate a candiate path set and uses an SMT solver to decide whether a candidate path is executable or not, as well as a concrete set of real parameters. We have implemented a tool and evaluated the usefulness of the proposed method through several programs.
出版者	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻	111
号	481
開始ページ	55
終了ページ	60
刊行年月	2012-03-06
言語	日本語
ハンドルURL	https://hdl.handle.net/11094/27416
ISSN	09135685
NCID	AN10013287
アクセス権	open access
権利情報	Copyright © 2002 IEICE
権利情報	本文データはCiNiiから複製したものである
出版タイプ	Version of Record
カテゴリ	学術雑誌論文 Journal Article

資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
DCMI資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス.111(481) p.55-p.60
DC.title	SMT ソルバーとPDG 作成ツールを用いたJava のテストケース自動導出手法の提案
	Automatic derivation of test cases for Java using an SMT solver and a PDG generator
	SMT　ソルバー　ト　PDG　サクセイ　ツール　ヲ　モチイタ　Java　ノ　テスト　ケース　ジドウ　ドウシュツ　シュホウ　ノ　テイアン
DC.creator	佐々木, 幸広
	ササキ, ユキヒロ
	Sasaki, Yukihiro
	小林, 和貴
	コバヤシ, カズキ
	Kobayashi, Kazuki
	岡野, 浩三
	オカノ, コウゾウ
	Okano, Kozo
	楠本, 真二
	クスモト, シンジ
	Kusumoto, Shinji
DC.publisher	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
DC.language' scheme='DCTERMS.RFC1766	日本語
DC.type' scheme='DCTERMS.DCMIType	text
DCTERMS.issued' scheme='DCTERMS.W3CDTF	2012-03-06
DC.subject	SMT ソルバ
	PDG
	Daikon
	テストケース
	Java
	SMT solver
	test case
DCTERMS.abstract	Design by Contractに基づく表明の生成手法には静的生成手法と動的生成手法が存在する.動的生成手法では,テストケースを用いて引数やフィールド変数の値を変えながら対象メソッドを解析し,データを取得するため,比較的少ないコストで表明を生成できる.一方で,テストケースがどれだけの実行範囲をカバーしているかというテストケースの質が生成される表明の質に影響を与える.この問題に対し,インバリアントカバレッジという指標が存在する.本研究では対象メソッドのPDGからインバリアントカバレッジを満たす可能性のある実行パスを列挙しSMTソルバを用いてそのパスの実行可能性と具体的な引数値の導出を行う方法を提案する.また,複数の例題に適用し有効であることを確認した.
DCTERMS.abstract	Assertions and Design by Contract play important roles for program understanding and program verification. In order to generate assertions, there are two kinds of methods, static analysis and dynamic analysis. Dynamic approach needs less CPU times, however suffers the test case depending problem in which the quality of assertions depends on the quality of test cases. Invariant coverage is one of indicator to specify the quality of test cases. In other words, the coverage of test cases affects the quality of generated assertions. The proposed method uses PDG of a target method to generate a candiate path set and uses an SMT solver to decide whether a candidate path is executable or not, as well as a concrete set of real parameters. We have implemented a tool and evaluated the usefulness of the proposed method through several programs.
DC.rights	Copyright © 2002 IEICE
DC.rights	本文データはCiNiiから複製したものである
DC.format	application/pdf
citation_title	SMT ソルバーとPDG 作成ツールを用いたJava のテストケース自動導出手法の提案
	Automatic derivation of test cases for Java using an SMT solver and a PDG generator
	SMT　ソルバー　ト　PDG　サクセイ　ツール　ヲ　モチイタ　Java　ノ　テスト　ケース　ジドウ　ドウシュツ　シュホウ　ノ　テイアン
citation_author	佐々木, 幸広
	ササキ, ユキヒロ
	Sasaki, Yukihiro
	小林, 和貴
	コバヤシ, カズキ
	Kobayashi, Kazuki
	岡野, 浩三
	オカノ, コウゾウ
	Okano, Kozo
	楠本, 真二
	クスモト, シンジ
	Kusumoto, Shinji
citation_publisher	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
citation_language	日本語
citation_date	2012-03-06
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	111
citation_issue	481
citation_firstpage	55
citation_lastpage	60
citation_issn	09135685
citation_public_url	https://hdl.handle.net/11094/27416

閲覧可能ファイル

論文情報

論文詳細を表示