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

佐々木, 幸広; 小林, 和貴; 岡野, 浩三 他

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2012, 111(481), 55-60

Number of Access:513（2025-09-04 16:35 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27416

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr111_481_055 pdf None 655 KB 114 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
SMT ソルバーとPDG 作成ツールを用 いたJava のテストケース自動導出手法の提案
Automatic derivation of test cases for Java using an SMT solver and a PDG generator
SMT　ソルバー　ト　PDG　サクセイ　ツール　ヲ　モチイタ　Java　ノ　テスト　ケース　ジドウ　ドウシュツ　シュホウ　ノ　テイアン
Creator
CreatorName
佐々木, 幸広 ; ササキ, ユキヒロ ; Sasaki, Yukihiro
NRID
1000050332317 1000050332317
CreatorName
小林, 和貴 ; コバヤシ, カズキ ; Kobayashi, Kazuki
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
CreatorName
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
Subject
SMT ソルバ
PDG
Daikon
テストケース
Java
SMT solver
test case
Abstract
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.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
111(481)
Page
55-60
Date of Issued
2012-03-06
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27416
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2002 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article