佐々木幸広, "Java の実行パスからパス実行可能性判定式への変換と SMTソルバによる求解," , 2012年2月.
ID 196
分類 学位論文
タグ assertion Invariant coverage SMT solver PDG Daikon
表題 (title) Java の実行パスからパス実行可能性判定式への変換と SMTソルバによる求解
表題 (英文) Conversion of Paths in Java into Their Execution Decision Expressions and Their Resolution by Smt Solver
著者名 (author) 佐々木幸広
英文著者名 (author) Yukihiro Sasaki
キー (key) Yukihiro Sasaki
刊行月 (month) 2
出版年 (year) 2012
刊行形式 (howpublished)
URL
付加情報 (note)
注釈 (annote)
内容梗概 (abstract) Design by Contract に基づく表明の記述はソースコードの仕様理解の補助やプログラム
の検証に役立つ.しかし,ソースコードのサイズの増加に伴い,表明の記述量も増大する.そのため,表明の自動生成手法が注目されている.
表明の自動生成手法には静的生成手法と動的生成手法が存在する.表明の静的生成手法では,プログラムを静的に解析することで,表明を導出する.しかし,表明生成にかかる時間が長い点が問題となる.表明の動的生成手法では,テストケースを用いて引数やフィールド変数の値を変えながら対象メソッドを解析し,データを取得する.それにより,比較的少ないコストで表明を生成できる.代表的な表明の動的生成ツールにDaikon などがある.
一方で,表明の動的導出手法はテストケースにの質が生成表明に影響を与えるという問題がある.ここでテストケースとの質とは,テストケースがどれだけの実行範囲をカバーしているかを表す.この問題に対し,インバリアントカバレッジという指標が存在する.インバリアントカバレッジとはテストケースがどれだけプログラムの返り値にデータ依存関係を持つ命令文を実行するかを表す指標である.著者が所属する研究グループではインバリアントカバレッジの値が高いテストケースを静的解析器ESC/Java2 の反例出力を用いて導出する手法を提案してきた.
しかし,既存研究では導出したテストケース制約が本来求めるべき制約より狭いという課題点があった.これは既存研究では反例情報に基づいたテストケース制約の導出を行っているため起こる問題である.
提案手法ではSMT ソルバを用いてこの課題を解決する.まず,対象メソッドのPDG からインバリアントカバレッジを満たす実行パスを列挙する.その実行パスをSMT ソルバの文法に変換し,求解する.その解を用いて,そのパスの実行可能性と具体的な引数値を導出する.提案手法を複数のJava プログラムに対して適用し,評価実験を行った.その結果,提案手法が有用であることを確認した.
論文電子ファイル document.pdf (application/pdf) [一般閲覧可]
BiBTeXエントリ
@misc{id196,
         title = {Java の実行パスからパス実行可能性判定式への変換と SMTソルバによる求解},
        author = {佐々木幸広},
         month = {2},
          year = {2012},
}