MasaoApril's Library.

Software Testingなネタを書いてみた。

JaSST15東海(2)「特別講演：はじめてのコンコリックテスト ～基本原理から知るホワイトボックステストの新技術とその応用～」

JaSST Tokai Conference Concolic test

　11/6(金)に開催されたソフトウェアテストシンポジウム2015東海(JaSST'15 Tokai)に参加しました。私が聴講したセッションは下記です。

セッション1 基調講演：「テストから観た実体のモデリングと実装構造の評価 ～検証指向設計の実現に向けて～」 松尾谷 徹(デバッグ工学研究所)
セッション 4-1 特別講演：「はじめてのコンコリックテスト ～基本原理から知るホワイトボックステストの新技術とその応用～」 植月 啓次(フェリカネットワークス)
セッション 4-2 事例発表：「安全系組込ソフトウェア開発におけるユニットテストの効率化」 岸本 渉(デンソー)
セッション 4-3 ワークショップ 「意地悪漢字を使ってみよう！ ～テスト設計ワークショップ～」 鈴木 三紀夫(リコーＩＴソリューションズ)
情報交換会

前回書いた記事

masaoapril.hatenablog.com

　今回は、セッション 4-1 特別講演：「はじめてのコンコリックテスト ～基本原理から知るホワイトボックステストの新技術とその応用～」です。

セッション 4-1 特別講演：「はじめてのコンコリックテスト ～基本原理から知るホワイトボックステストの新技術とその応用～」 植月 啓次(フェリカネットワークス)

(1)シンボリック実行(Symbolic execution)

  • プログラム解析後、実行パスの抽出と実行パスを実行するための入力データを特定する技術。
  • 入力データ：シンボリック(Symbolic)として扱う。
  • 静的テストに分類される。

(2)SAT(充足可能性問題)

  • 論理式の変数True/Falseの組み合わせで、結果がTrueかFalseかを判定する問題。
  • 論理式をコンピュータで解くアルゴリズムを利用。
  • SATソルバで解く。

(3)動的実行

　実行結果の値を入力してSATソルバで解かせる。

(4)Concolic = Concrete + Symbolic

　"Concolic test"は、具体的な値(Conclete Value)を使った動的実行とシンボリック実行(Symbolic execution)を組み合わせたもの。

流れは以下。

  1. 入力する変数を指定する。
  2. 入力する変数に任意の初期値を指定
  3. 実行の過程で出てきた数値を次のテストに入れて、SATソルバに解かせる
(5)Concolic testを現場適用するときの障壁
  • パス数が爆発
    10回のループが2つ並んだら→100回。
  • ソルバの制約
    • 種類によって得意不得意。
    • 浮動小数やポインタは苦手。
  • オラクル問題
    入力は求められるが、期待結果は求められない。
(6)ツール
  • PathCrawler
    • C
    • Web上で試行できる。
  • CUTE
    • C/Java
    • 更新が滞っている。
  • CREST C
  • KLEE LLVM
  • Microsoft Pex
  • SPF(Symbolic Path Finder)
  • DART(非公開)
(7)実例

　Fuzzテストで応用されている。MictosoftのSAGEというツールの事例が有名とのこと。

(8)課題
  • パス数の爆発
    • 処理能力Upで改善。
    • 部分適用で工夫する。
  • ソルバの制約
    • ソルバの進化で改善。
    • SMTソルバ。
  • オラクル問題
(9)デモ

所感

　Concolic Testは、1～2年前から時折耳にしていますが、概要は分からない状態でした。近い将来、concolic testを適用する場面が出てくると思いますので、開発者と連携して取り組もうと思います。まずは、情報収集と活用できるところの検討から始めたいと思います。