記 号 実 行 を 用 いた テストデータ 自 動 生 成 の 試 行 評 価 株 式 会 社 デンソー 電 子 技 術 3 部 榎 本 秀 美 e-mail:hidemi_enomoto@denso.co.jp
目 次 1 / 19 1. 背 景 2. 単 体 テストの 問 題 点 3. 対 策 案 の 検 討 4. 評 価 内 容 5. 評 価 結 果 6. まとめ [ 参 考 ]CREST
デンソーの 紹 介 2 / 19 主 要 製 品
1. 背 景 3 / 19 自 動 車 系 組 込 みソフトウェアの 動 向 < 機 能 開 発 > 環 境 電 動 化 小 型 化 安 全 安 全 運 転 支 援 自 動 走 行 快 適 利 便 インフラ 連 携 市 場 の 要 求 安 全 安 心 の 保 障 機 能 安 全 規 格 の 準 拠 <プログラム 規 模 > プログラム 行 数 500 万 ~ 1000 万 行 100 万 行 5~10 倍 ( 参 考 ) 経 済 産 業 省 HP 2000 年 現 在 規 模 の 増 加 複 雑 化 製 品 の 早 期 市 場 投 入 新 興 市 場 での 低 価 格 車 需 要 短 期 開 発 コスト 削 減 機 能 安 全 準 拠 と 短 期 開 発 コスト 削 減 の 両 立 が 必 要
1. 背 景 4 / 19 機 能 安 全 準 拠 に 向 けたソフトウェア 開 発 の 取 組 み 機 能 安 全 規 格 : 機 能 部 品 が 故 障 したとしてもシステムの 安 全 性 を 確 保 することを 狙 いとして 定 められた 規 格 ソフトウェア 開 発 においては 安 全 性 確 保 のための 具 体 的 な 手 法 が 定 義 されている トレーサビリティ 管 理 要 件 定 義 要 求 の 検 証 欠 陥 注 入 詳 細 な 設 計 要 件 ( 安 全 設 計 ) 設 計 検 証 ( 制 御 フロー 解 析 など) アーキテクチャ 設 計 ユニット 設 計 結 合 テスト 単 体 テスト 負 荷 計 測 インターフェース 試 験 MC/DCカバレッジの 実 施 部 品 作 成 機 能 安 全 規 格 へ 対 応 と 効 率 化 を 推 進 している 今 回 は 単 体 テストに 対 する 取 組 み 内 容 を 報 告 する
2. 単 体 テストの 問 題 点 5 / 19 MC/DCカバレッジ100%を 達 成 するために 仕 様 ベーステストに 加 えて 実 装 ベーステストを 実 施 している 仕 様 書 ソース コード ( ) クロス コンパイラ 実 行 コード シミュレータ テスト 結 果 MC/DCカバレッジ 仕 様 ベーステスト 手 作 業 ソースコードに 対 する MC/DCカバレッジ100% 達 成 は 不 可 実 装 ベーステスト 手 作 業 テスト ケース 人 手 による テストデータの 作 成 + MC/DCカバレッジの テスト(テスト 数 が 多 い) 工 数 増 加 MC/DCカバレッジのテストが 追 加 されたことで 単 体 テストの 工 数 が 更 に 増 加 した
2. 単 体 テストの 問 題 点 6 / 19 実 装 ベーステストは 入 力 が 形 式 言 語 のためテストデータ 自 動 生 成 可 能 市 販 ツールの 導 入 を 開 始 している 仕 様 書 ソース コード ( ) C 言 語 クロス コンパイラ 仕 様 ベーステスト 手 作 業 実 行 コード シミュレータ テスト 結 果 MC/DCカバレッジ カバレッジ 未 達 の 場 合 実 装 ベーステスト テスト ケース 追 加 テスト 市 販 ツール 自 動 生 成 手 作 業 市 販 ツールでは MC/DCカバレッジ 未 達 のケースが 発 生 し 手 作 業 による 追 加 テストを 行 うため 効 率 化 の 妨 げとなっている ツールが 生 成 するテストデータの MC/DCカバレッジ 率 を 高 める 必 要 がある
3. 対 策 案 の 検 討 テストデータの 生 成 方 式 静 的 解 析 と 記 号 実 行 の2 種 類 が 存 在 説 明 静 的 解 析 ソースコードから 制 御 パスを 解 析 そのパスを 通 るテストデータを 生 成 メリット 市 販 ツールを 含 め 多 くのツールが 存 在 事 前 準 備 も 含 めた 機 能 を 持 ち 操 作 性 が 洗 練 されている デメリット 動 的 なメモリを 使 った 制 御 を 解 析 することが 困 難 7 / 19 記 号 実 行 ソースコードを 疑 似 的 に 実 行 変 数 間 の 関 係 を 制 約 として 記 述 制 約 ソルバで 解 を 得 てテストデータ を 生 成 動 的 なメモリを 使 った 制 御 を 解 析 可 能 研 究 段 階 で 操 作 性 が 行 き 届 いた 製 品 は 見 当 たらない ツールはオープンソースで 事 前 準 備 に 手 間 がかかる 記 号 実 行 は MC/DCカバレッジ 率 を 高 めることができるが 効 率 面 で 課 題 がある 合 理 的 にテストを 行 うには 静 的 解 析 と 記 号 実 行 を 組 合 わせる
3. 対 策 案 の 検 討 8 / 19 記 号 実 行 は 市 販 ツールよりテストデータ 生 成 能 力 は 高 いが 実 行 するのに 多 くの 手 間 がかかるため 使 用 する 範 囲 を 限 定 したい < 対 策 案 > テスト 対 象 1 市 販 ツールを 実 行 市 販 ツール ( 静 的 解 析 ) 記 号 実 行 の 対 象 を 絞 り 込 む MC/DC100% 未 満 MC/DC100% 2 記 号 実 行 ツールを 実 行 記 号 実 行 ツール MC/DC100% 市 販 ツールで カバレッジ 未 達 の 対 象 を 実 行 する 記 号 実 行 ツールの 作 業 量 を 減 らす 市 販 ツールで 出 来 ない を 解 決 する 市 販 ツールのMC/DCカバレッジ 未 達 部 分 を 記 号 実 行 で カバレッジ100%にできるか 確 認 する
4. 評 価 内 容 9 / 19 評 価 事 項 1 市 販 ツール 実 行 市 販 ツール MC/DC カバレッジ 未 達 カバレッジ 達 成 2 記 号 実 行 ツール 実 行 記 号 実 行 ツール MC/DC カバレッジ 達 成 評 価 事 項 確 認 項 目 記 号 実 行 の 対 象 を 絞 込 みできているか カバレッジ 未 達 の 数 未 達 パスの 条 件 市 販 ツールのカバレッジ 未 達 を 解 決 できているか カバレッジ 結 果 カバレッジ 未 達 の 原 因 対 象 製 品 で 用 いるソフトウェア (*) から 循 環 複 雑 度 (CCN)の 平 均 を 中 心 に 40 個 をランダムに 選 定 (*) 特 徴 : グローバル 変 数 の 参 照 が 多 い / 判 断 文 のネストや 構 成 する 条 件 が 多 い
4. 評 価 内 容 10 / 19 評 価 ツール 市 販 ツールは 現 在 使 用 しているツールとし 記 号 実 行 ツールはC 言 語 に 対 応 したツールを 選 定 市 販 ツール1 静 的 解 析 に 基 づくツール 組 込 み 系 テストベッドと 親 和 性 が 高 い 市 販 ツール2 静 的 解 析 にモンテカルロ 法 による 機 能 を 加 えたツール モデルベース 開 発 と 親 和 性 が 高 い 記 号 実 行 ツール Concolic tesiting 方 式 の CREST Concolic testing : 記 号 実 行 の 一 種 で 解 析 速 度 が 改 善 された 方 式 CREST: C 言 語 向 けのオープンツール 一 般 的 なCのライブラリが 使 用 可 能
[ 参 考 ]CREST 11 / 19 CRESTの 仕 組 み CRESTは 中 間 コードへの 変 換 と テストデータの 生 成 の 2つの 機 能 で 構 成 されている 変 数 名 変 数 名 テストデータを 生 成 する 変 数 中 間 コードへ 変 換 (crestc) CREST テストデータの 生 成 (run_crest) ソースコード ( 対 象 ) 中 間 言 語 コンパイラ 中 間 コード 記 号 実 行 (Concolic testing) テスト データ 解 析 実 行 できる 形 式 に 変 換 パスを 解 析 し テストデータを 生 成 テストドライバ
4. 評 価 内 容 12 / 19 評 価 環 境 MC/DCカバレッジを 比 較 評 価 するため シミュレータを 統 一 ソース コード クロス コンパイラ 実 行 コード シミュレータ テスト 結 果 MC/DCカバレッジ 実 行 環 境 : Windows OS 市 販 ツール1 市 販 ツール2 記 号 実 行 ツール (CREST) テスト データ テスト データ テスト データ 実 行 環 境 : Windows OS 上 にVagrantを 用 いて 構 築 したLINUX(ubuntu) 環 境 Vagrant: 開 発 環 境 の 構 築 と 共 有 を 容 易 とするツール コマンドを 実 行 Vagrant 仮 想 マシン 内 の 環 境 を 設 定 仮 想 マシンを 作 成 設 定 仮 想 マシン (LINUX) 記 号 実 行 ツール (CREST) 仮 想 化 ソフトウェア (VirtualBox) ( 参 考 )Vagrant: https://www.vagrantup.com/
5. 評 価 結 果 13 / 19 市 販 ツールの 実 行 結 果 <MC/DCカバレッジ 達 成 / 未 達 の 数 > 市 販 ツール1 市 販 ツール2 カバレッジ 達 成 (100%) 9 29 カバレッジ 未 達 (100% 未 満 ) 31 11 市 販 ツール1より 市 販 ツール2の 方 が 記 号 実 行 の 対 象 を 絞 り 込 める < 未 達 パスの 条 件 > 内 で 算 出 される 変 数 を 含 む 条 件 文 市 販 ツール2はモンテカルロ 法 により テストデータを 生 成 できるケースあり 変 数 同 士 を 比 較 する 条 件 文 ( 市 販 ツール1のみ) 条 件 が 多 い 判 断 文 ( 市 販 ツール2のみ) 対 象 :40 個 静 的 解 析 の 原 理 上 可 能 だが ツールの 仕 様 制 限 によりテストデータを 生 成 できない 市 販 ツール2でカバレッジ 未 達 の に 対 して 記 号 実 行 ツールを 実 行 する
5. 評 価 結 果 14 / 19 記 号 実 行 ツールの 実 行 結 果 <MC/DCカバレッジ 達 成 / 未 達 の 数 > 記 号 実 行 ツール カバレッジ 達 成 (100%) 7 カバレッジ 未 達 (100% 未 満 ) 4 <カバレッジ 未 達 の 原 因 > シミュレータ 解 析 画 面 実 行 : : MC/DCがOK 10 T/F if ( ( data1!= 1 ) 11 ( ( data1 == 1 ) MC/DCがNG 12 && ( data2 < data3 ) ) { [MC/DC t/f ] ( data1!= 1 ) [MC/DC t/ ] ( data1 == 1 ) [MC/DC t/f ] ( data2 < data3 ) 13 処 理 ; 14 } : : true 対 象 :11 個 true data1!= 1 記 号 実 行 を 用 いて MC/DCカバレッジ100%の テストデータを 生 成 できることを 確 認 した 到 達 不 可 のパス false true data1 == 1 false data2 < data3 false 可 読 性 向 上 のための 冗 長 なロジックが 原 因 カバレッジ 対 象 外
[ 参 考 ]MC/DCカバレッジ 結 果 MC/DCカバレッジ[%] No CCN 市 販 ツール1 市 販 ツール2 記 号 実 行 ツール 1 3 100 100-2 4 0 83 100 3 5 100 100-4 5 0 100-5 6 60 100-6 6 100 100-7 6 100 100-8 6 100 100-9 6 90 100-10 7 25 100-11 7 100 100-12 7 66 100-13 7 66 100-14 7 100 100-15 8 71 100-16 8 57 100 17 8 100 86 100 18 9 81 81 93 19 9 0 100-20 9 0 62 87 15 / 19 :カバレッジ 未 達 冗 長 なロジックが 原 因 MC/DCカバレッジ[%] No CCN 市 販 ツール1 市 販 ツール2 記 号 実 行 ツール 21 10 66 100-22 10 33 100-23 10 0 100-24 10 44 100-25 11 100 100-26 11 0 100-27 11 80 100-28 12 9 100-29 13 16 100-30 14 53 100-31 14 53 96 100 32 14 7 100-33 15 22 96 100 34 17 10 58 100 35 17 78 93 93 36 19 27 100-37 20 50 94 100 38 20 42 75 91 39 48 4 23 100 40 50 30 100 - ソフトウェアの 大 部 分 を 占 めるCCNが 小 さい は 市 販 ツールでもカバレッジを 達 成 CCNが 大 きい でも 記 号 実 行 ツールはカバレッジを 達 成 市 販 ツールと 記 号 実 行 ツールの 組 合 せで 合 理 的 にテストを 実 施 できる
6. まとめ 16 / 19 目 的 MC/DCカバレッジ100%のテストデータ 自 動 生 成 により 単 体 テスト( 実 装 ベーステスト)を 効 率 化 する 取 組 み 生 成 するテストデータのカバレッジ 率 を 高 めるために 記 号 実 行 ツールを 用 いたテストデータの 自 動 生 成 記 号 実 行 ツールを 用 いることで 可 達 パスに 対 する MC/DCカバレッジ100%のテストデータを 生 成 する 目 途 付 けができた 市 販 ツールとの 併 用 で 運 用 方 法 として 有 効 であることを 確 認 した 今 後 の 課 題 実 務 適 用 に 向 けた 追 加 評 価 と 運 用 方 法 の 検 討 記 号 実 行 ツールへの 置 換 えを 視 野 に 入 れた 追 加 評 価 開 発 現 場 で 容 易 に 使 える 方 法 の 検 討 と 環 境 整 備 ツールの 保 守 方 法 の 検 討
[ 参 考 ]CREST テストドライバ( 基 本 構 成 ) ヘッダファイルのインクルード テストデータを 生 成 する 変 数 の 指 定 ( 符 号 付 /なし char, short, long) テスト 対 象 の のコール ( 解 析 対 象 のソースコード) テストデータの 出 力 (printf) < 出 力 結 果 イメージ(テストデータ)> テストデータ( 入 力 変 数 ) 期 待 値 ( 出 力 変 数 ) In1 In2 Out1 1 2 3 4 : 0 145 0 1 0 1 126 255 1 255 152 0 : 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 17 / 19 #include <crest.h> /* CRESTのヘッダをインクルード */ #include <stdio.h> #include <stdlib.h> unsigned char In1; unsigned char In2; unsigned char Out1; int main( void ) { /* テストデータを 生 成 する 変 数 の 指 定 */ CREST_unsigned_char( In1 ); CREST_unsigned_char( In2 ); /* テスト 対 象 の ( 解 析 対 象 のソースコード) */ printf( %d %d t t, In1, In2 ); TestFunc(); /* テスト 対 象 の */ printf( %d n, Out1 ); return EXIT_SUCCESS; } /* テスト 対 象 の */ void TestFunc( void ) { : }
[ 参 考 ]CREST テストドライバの 工 夫 事 前 条 件 を 追 加 CRESTは 型 の 範 囲 でテストデータを 生 成 する 仕 様 上 取 り 得 る 値 でテストデータを 生 成 させる 仕 組 みを 追 加 < 出 力 結 果 イメージ(テストデータ)> テストデータ( 入 力 変 数 ) 期 待 値 ( 出 力 変 数 ) In1 In2 Out1 1 2 3 4 : 0 145 0 1 0 1 0 255 1 0 152 0 : : 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 : int main( void ) { /* テストデータを 生 成 する 変 数 の 指 定 */ CREST_unsigned_char( In1 ); /* 0 or 1 */ CREST_unsigned_char( In2 ); 18 / 19 /* テスト 対 象 の ( 解 析 対 象 のソースコード) */ if ( In1 <= 1 ) { printf( %d %d t t, In1, In2 ); TestFunc(); /* テスト 対 象 の */ printf( %d n, Out1 ); } return EXIT_SUCCESS; } /* テスト 対 象 の */ void TestFunc( void ) { : }
[ 参 考 ]CREST 19 / 19 テストデータ 生 成 時 の 解 析 方 法 の 選 択 CRESTには 幾 つかの 解 析 方 法 が 準 備 されており ソフトウェアに 合 わせて 選 ぶことができる -dfs (Bounded Depth First Search) : 主 にソルバの 性 能 を 高 める -random (Random Search) : 原 始 的 なヒューリスティック など ( 例 ) -dfs ではビット 演 算 を 解 析 できず MC/DCカバレッジ 未 達 となるが 他 の 解 析 方 法 を 用 いればカバレッジを 達 成 できる 1 2 data1 = (unsigned char)( ( data2 & 0x0000FF00 ) >> 8 ); if ( data1 == 0xE0 ) { 処 理 ; } テストドライバや 解 析 方 法 など 対 象 のソフトウェアに 合 った 使 用 方 法 を 見 つける 必 要 がある
参 考 文 献 謝 辞 20 / 19 Concolic testing K. Sen, D. Marinov, and G. Agha, CUTE: A Concolic Unit Testing Engine for C, ACM, vol.30, 2005 CREST CREST, Concolic test generation tool for C, http://jburnim.github.io/crest/ https://groups.google.com/forum/#!forum/crest-users (FAQ) J. Burnim and K. Sen, Heuristics for Scalable Dynamic Test Generation, Automated Software Engineering, 2008. ASE 2008. 23rd IEEEIACM International Conference on Moonzoo Kim, CREST Tutorial, http://swtv.kaist.ac.kr/courses/cs453-fall13/lec12-crest_tutorial.pdf 事 例 研 究 高 松 宏 樹, 佐 藤 晴 彦, 小 山 聡, 栗 原 正 仁, 動 的 記 号 実 行 によるメソッドの 複 雑 度 を 考 慮 したテストケース 自 動 生 成, 情 報 処 理 学 会 研 究 報 告, ソフトウェア 工 学 研 究 会 報 告, 2014(27) 植 月 啓 次, ソフトウェアの 実 装 情 報 に 基 づく 決 定 表 を 活 用 した 論 理 検 証 手 法, ソフトウェアシンポジウム2013, 12, 2013 岸 本 渉, 安 全 系 組 込 ソフトウェア 開 発 におけるユニットテストの 効 率 化, ソフトウェアシンポジウム2015, C-14-2, 2015 松 尾 谷 徹, 増 田 聡, 湯 本 剛, 植 月 啓 次, 津 田 和 彦, Concolic Testing を 活 用 した 実 装 ベースの 回 帰 テスト 人 手 によるテストケース 設 計 の 全 廃, ソフトウェアシンポジウム2015, C-14-2, 2015 謝 辞 : 本 取 組 において 社 内 の 研 修 などを 通 じ ご 指 導 ご 協 力 いただいた 方 々に 感 謝 いたします
21 / 19
[ 参 考 ] 記 号 実 行 22 / 19 1 2 3 4 5 6 7 8 9 10 11 12 13 int TestFunc( int x, int y, int z ) { int ans; if ( x == 0 ) { ans = 1; if ( y > 1 && z == 1 ) { ans = 2; } } else { ans = 0; } return ans; } 1 true true z == 1 x == 0 true 2 y > 1 false 3 false 4 false 入 力 変 数 をx, y, zの 時 それぞれに 与 えられる 値 をX, Y, Z( 記 号 )とする 制 約 式 は 以 下 となり X, Y, Z に 具 体 的 な 値 を 与 えてテストデータを 生 成 する 1 ( X = 0 ) ( Y > 1 ) ( Z = 1 ) 2 ( X = 0 ) ( Y > 1 ) ( Z!= 1 ) 3 ( X = 0 ) ( Y <= 1 ) 4 ( X!= 0 )