読者です 読者をやめる 読者になる 読者になる

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 ワークショップ 「意地悪漢字を使ってみよう! ~テスト設計ワークショップ~」 鈴木 三紀夫(リコーITソリューションズ)
情報交換会

前回書いた記事

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を適用する場面が出てくると思いますので、開発者と連携して取り組もうと思います。まずは、情報収集と活用できるところの検討から始めたいと思います。