講演名 2002/2/25
記号実行法による仕様要素の抽出
森本 紘史, 佐藤 匡正,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 記号実行法は、仕様違反検出に対する有力な机上確認法(Static analysis)の技法であるが、繰り返し構造をもつ複雑な処理においては、パス数の増大などによって記号実行の結果の複雑化を招く。このため明快性に欠け、仕様との対応を示すことが難しかった。ここでは、繰り返し構造を関数化することによって仕様の部分化、要素化を図り、仕様との対応をとる方法を試みた。本論文では、繰り返しの関数化結果の分析および提案した記号実行法を適用した事例について考察を行う。
抄録(英) Symbolic execution is an effective technique of static analysis for detecting errors against the specification. It would , however ,lead to complicated results with so many numbers of paths through symbolic execution for programs with iterations. This would become blur the correspondence between the program and the specification to identify the errors. This paper proposes an approach of dividing a program into elements to detect the correspondence; modularizing a program through the transformation of an iteration structure into a function. It is discussed the methods and the results and the analysis function transformations, along with examples applied of them.
キーワード(和) 記号実行法 / 繰り返しの関数化 / 機能仕様 / サイクロマティック数
キーワード(英) Symbolic Execution / Functionalized loop / Functional Specification / Cyclomatic Number
資料番号 SS2001-46
発行日

研究会情報
研究会 SS
開催期間 2002/2/25(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Software Science (SS)
本文の言語 JPN
タイトル(和) 記号実行法による仕様要素の抽出
サブタイトル(和)
タイトル(英) Symbolic Execution for Abstraction of Functional Specification
サブタイトル(和)
キーワード(1)(和/英) 記号実行法 / Symbolic Execution
キーワード(2)(和/英) 繰り返しの関数化 / Functionalized loop
キーワード(3)(和/英) 機能仕様 / Functional Specification
キーワード(4)(和/英) サイクロマティック数 / Cyclomatic Number
第 1 著者 氏名(和/英) 森本 紘史 / Hiroshi MORIMOTO
第 1 著者 所属(和/英) 島根大学大学院総合理工学研究科
Interdisciplinary Graduates School of Science and Engineering, Shimane University
第 2 著者 氏名(和/英) 佐藤 匡正 / Tadamasa SATOU
第 2 著者 所属(和/英) 島根大学大学総合理工学部
Faculty of Science and Engineering, Shimane University
発表年月日 2002/2/25
資料番号 SS2001-46
巻番号(vol) vol.101
号番号(no) 673
ページ範囲 pp.-
ページ数 5
発行日