| Tweet | |
| 佐々木幸広, "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},
}
|