PowerPoint プレゼンテーション

Transcription

1 記 号 実 行 を 用 いた テストデータ 自 動 生 成 の 試 行 評 価 株 式 会 社 デンソー 電 子 技 術 3 部 榎 本 秀 美 [email protected]

2 目 次 1 / 背 景 2. 単 体 テストの 問 題 点 3. 対 策 案 の 検 討 4. 評 価 内 容 5. 評 価 結 果 6. まとめ [ 参 考 ]CREST

3 デンソーの 紹 介 2 / 19 主 要 製 品

4 1. 背 景 3 / 19 自 動 車 系 組 込 みソフトウェアの 動 向 < 機 能 開 発 > 環 境 電 動 化 小 型 化 安 全 安 全 運 転 支 援 自 動 走 行 快 適 利 便 インフラ 連 携 市 場 の 要 求 安 全 安 心 の 保 障 機 能 安 全 規 格 の 準 拠 <プログラム 規 模 > プログラム 行 数 500 万 ~ 1000 万 行 100 万 行 5~10 倍 ( 参 考 ) 経 済 産 業 省 HP 2000 年 現 在 規 模 の 増 加 複 雑 化 製 品 の 早 期 市 場 投 入 新 興 市 場 での 低 価 格 車 需 要 短 期 開 発 コスト 削 減 機 能 安 全 準 拠 と 短 期 開 発 コスト 削 減 の 両 立 が 必 要

5 1. 背 景 4 / 19 機 能 安 全 準 拠 に 向 けたソフトウェア 開 発 の 取 組 み 機 能 安 全 規 格 : 機 能 部 品 が 故 障 したとしてもシステムの 安 全 性 を 確 保 することを 狙 いとして 定 められた 規 格 ソフトウェア 開 発 においては 安 全 性 確 保 のための 具 体 的 な 手 法 が 定 義 されている トレーサビリティ 管 理 要 件 定 義 要 求 の 検 証 欠 陥 注 入 詳 細 な 設 計 要 件 ( 安 全 設 計 ) 設 計 検 証 ( 制 御 フロー 解 析 など) アーキテクチャ 設 計 ユニット 設 計 結 合 テスト 単 体 テスト 負 荷 計 測 インターフェース 試 験 MC/DCカバレッジの 実 施 部 品 作 成 機 能 安 全 規 格 へ 対 応 と 効 率 化 を 推 進 している 今 回 は 単 体 テストに 対 する 取 組 み 内 容 を 報 告 する

6 2. 単 体 テストの 問 題 点 5 / 19 MC/DCカバレッジ100%を 達 成 するために 仕 様 ベーステストに 加 えて 実 装 ベーステストを 実 施 している 仕 様 書 ソース コード ( ) クロス コンパイラ 実 行 コード シミュレータ テスト 結 果 MC/DCカバレッジ 仕 様 ベーステスト 手 作 業 ソースコードに 対 する MC/DCカバレッジ100% 達 成 は 不 可 実 装 ベーステスト 手 作 業 テスト ケース 人 手 による テストデータの 作 成 + MC/DCカバレッジの テスト(テスト 数 が 多 い) 工 数 増 加 MC/DCカバレッジのテストが 追 加 されたことで 単 体 テストの 工 数 が 更 に 増 加 した

7 2. 単 体 テストの 問 題 点 6 / 19 実 装 ベーステストは 入 力 が 形 式 言 語 のためテストデータ 自 動 生 成 可 能 市 販 ツールの 導 入 を 開 始 している 仕 様 書 ソース コード ( ) C 言 語 クロス コンパイラ 仕 様 ベーステスト 手 作 業 実 行 コード シミュレータ テスト 結 果 MC/DCカバレッジ カバレッジ 未 達 の 場 合 実 装 ベーステスト テスト ケース 追 加 テスト 市 販 ツール 自 動 生 成 手 作 業 市 販 ツールでは MC/DCカバレッジ 未 達 のケースが 発 生 し 手 作 業 による 追 加 テストを 行 うため 効 率 化 の 妨 げとなっている ツールが 生 成 するテストデータの MC/DCカバレッジ 率 を 高 める 必 要 がある

8 3. 対 策 案 の 検 討 テストデータの 生 成 方 式 静 的 解 析 と 記 号 実 行 の2 種 類 が 存 在 説 明 静 的 解 析 ソースコードから 制 御 パスを 解 析 そのパスを 通 るテストデータを 生 成 メリット 市 販 ツールを 含 め 多 くのツールが 存 在 事 前 準 備 も 含 めた 機 能 を 持 ち 操 作 性 が 洗 練 されている デメリット 動 的 なメモリを 使 った 制 御 を 解 析 することが 困 難 7 / 19 記 号 実 行 ソースコードを 疑 似 的 に 実 行 変 数 間 の 関 係 を 制 約 として 記 述 制 約 ソルバで 解 を 得 てテストデータ を 生 成 動 的 なメモリを 使 った 制 御 を 解 析 可 能 研 究 段 階 で 操 作 性 が 行 き 届 いた 製 品 は 見 当 たらない ツールはオープンソースで 事 前 準 備 に 手 間 がかかる 記 号 実 行 は MC/DCカバレッジ 率 を 高 めることができるが 効 率 面 で 課 題 がある 合 理 的 にテストを 行 うには 静 的 解 析 と 記 号 実 行 を 組 合 わせる

9 3. 対 策 案 の 検 討 8 / 19 記 号 実 行 は 市 販 ツールよりテストデータ 生 成 能 力 は 高 いが 実 行 するのに 多 くの 手 間 がかかるため 使 用 する 範 囲 を 限 定 したい < 対 策 案 > テスト 対 象 1 市 販 ツールを 実 行 市 販 ツール ( 静 的 解 析 ) 記 号 実 行 の 対 象 を 絞 り 込 む MC/DC100% 未 満 MC/DC100% 2 記 号 実 行 ツールを 実 行 記 号 実 行 ツール MC/DC100% 市 販 ツールで カバレッジ 未 達 の 対 象 を 実 行 する 記 号 実 行 ツールの 作 業 量 を 減 らす 市 販 ツールで 出 来 ない を 解 決 する 市 販 ツールのMC/DCカバレッジ 未 達 部 分 を 記 号 実 行 で カバレッジ100%にできるか 確 認 する

10 4. 評 価 内 容 9 / 19 評 価 事 項 1 市 販 ツール 実 行 市 販 ツール MC/DC カバレッジ 未 達 カバレッジ 達 成 2 記 号 実 行 ツール 実 行 記 号 実 行 ツール MC/DC カバレッジ 達 成 評 価 事 項 確 認 項 目 記 号 実 行 の 対 象 を 絞 込 みできているか カバレッジ 未 達 の 数 未 達 パスの 条 件 市 販 ツールのカバレッジ 未 達 を 解 決 できているか カバレッジ 結 果 カバレッジ 未 達 の 原 因 対 象 製 品 で 用 いるソフトウェア (*) から 循 環 複 雑 度 (CCN)の 平 均 を 中 心 に 40 個 をランダムに 選 定 (*) 特 徴 : グローバル 変 数 の 参 照 が 多 い / 判 断 文 のネストや 構 成 する 条 件 が 多 い

11 4. 評 価 内 容 10 / 19 評 価 ツール 市 販 ツールは 現 在 使 用 しているツールとし 記 号 実 行 ツールはC 言 語 に 対 応 したツールを 選 定 市 販 ツール1 静 的 解 析 に 基 づくツール 組 込 み 系 テストベッドと 親 和 性 が 高 い 市 販 ツール2 静 的 解 析 にモンテカルロ 法 による 機 能 を 加 えたツール モデルベース 開 発 と 親 和 性 が 高 い 記 号 実 行 ツール Concolic tesiting 方 式 の CREST Concolic testing : 記 号 実 行 の 一 種 で 解 析 速 度 が 改 善 された 方 式 CREST: C 言 語 向 けのオープンツール 一 般 的 なCのライブラリが 使 用 可 能

12 [ 参 考 ]CREST 11 / 19 CRESTの 仕 組 み CRESTは 中 間 コードへの 変 換 と テストデータの 生 成 の 2つの 機 能 で 構 成 されている 変 数 名 変 数 名 テストデータを 生 成 する 変 数 中 間 コードへ 変 換 (crestc) CREST テストデータの 生 成 (run_crest) ソースコード ( 対 象 ) 中 間 言 語 コンパイラ 中 間 コード 記 号 実 行 (Concolic testing) テスト データ 解 析 実 行 できる 形 式 に 変 換 パスを 解 析 し テストデータを 生 成 テストドライバ

13 4. 評 価 内 容 12 / 19 評 価 環 境 MC/DCカバレッジを 比 較 評 価 するため シミュレータを 統 一 ソース コード クロス コンパイラ 実 行 コード シミュレータ テスト 結 果 MC/DCカバレッジ 実 行 環 境 : Windows OS 市 販 ツール1 市 販 ツール2 記 号 実 行 ツール (CREST) テスト データ テスト データ テスト データ 実 行 環 境 : Windows OS 上 にVagrantを 用 いて 構 築 したLINUX(ubuntu) 環 境 Vagrant: 開 発 環 境 の 構 築 と 共 有 を 容 易 とするツール コマンドを 実 行 Vagrant 仮 想 マシン 内 の 環 境 を 設 定 仮 想 マシンを 作 成 設 定 仮 想 マシン (LINUX) 記 号 実 行 ツール (CREST) 仮 想 化 ソフトウェア (VirtualBox) ( 参 考 )Vagrant:

14 5. 評 価 結 果 13 / 19 市 販 ツールの 実 行 結 果 <MC/DCカバレッジ 達 成 / 未 達 の 数 > 市 販 ツール1 市 販 ツール2 カバレッジ 達 成 (100%) 9 29 カバレッジ 未 達 (100% 未 満 ) 市 販 ツール1より 市 販 ツール2の 方 が 記 号 実 行 の 対 象 を 絞 り 込 める < 未 達 パスの 条 件 > 内 で 算 出 される 変 数 を 含 む 条 件 文 市 販 ツール2はモンテカルロ 法 により テストデータを 生 成 できるケースあり 変 数 同 士 を 比 較 する 条 件 文 ( 市 販 ツール1のみ) 条 件 が 多 い 判 断 文 ( 市 販 ツール2のみ) 対 象 :40 個 静 的 解 析 の 原 理 上 可 能 だが ツールの 仕 様 制 限 によりテストデータを 生 成 できない 市 販 ツール2でカバレッジ 未 達 の に 対 して 記 号 実 行 ツールを 実 行 する

15 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 可 読 性 向 上 のための 冗 長 なロジックが 原 因 カバレッジ 対 象 外

16 [ 参 考 ]MC/DCカバレッジ 結 果 MC/DCカバレッジ[%] No CCN 市 販 ツール1 市 販 ツール2 記 号 実 行 ツール / 19 :カバレッジ 未 達 冗 長 なロジックが 原 因 MC/DCカバレッジ[%] No CCN 市 販 ツール1 市 販 ツール2 記 号 実 行 ツール ソフトウェアの 大 部 分 を 占 めるCCNが 小 さい は 市 販 ツールでもカバレッジを 達 成 CCNが 大 きい でも 記 号 実 行 ツールはカバレッジを 達 成 市 販 ツールと 記 号 実 行 ツールの 組 合 せで 合 理 的 にテストを 実 施 できる

17 6. まとめ 16 / 19 目 的 MC/DCカバレッジ100%のテストデータ 自 動 生 成 により 単 体 テスト( 実 装 ベーステスト)を 効 率 化 する 取 組 み 生 成 するテストデータのカバレッジ 率 を 高 めるために 記 号 実 行 ツールを 用 いたテストデータの 自 動 生 成 記 号 実 行 ツールを 用 いることで 可 達 パスに 対 する MC/DCカバレッジ100%のテストデータを 生 成 する 目 途 付 けができた 市 販 ツールとの 併 用 で 運 用 方 法 として 有 効 であることを 確 認 した 今 後 の 課 題 実 務 適 用 に 向 けた 追 加 評 価 と 運 用 方 法 の 検 討 記 号 実 行 ツールへの 置 換 えを 視 野 に 入 れた 追 加 評 価 開 発 現 場 で 容 易 に 使 える 方 法 の 検 討 と 環 境 整 備 ツールの 保 守 方 法 の 検 討

18 [ 参 考 ]CREST テストドライバ( 基 本 構 成 ) ヘッダファイルのインクルード テストデータを 生 成 する 変 数 の 指 定 ( 符 号 付 /なし char, short, long) テスト 対 象 の のコール ( 解 析 対 象 のソースコード) テストデータの 出 力 (printf) < 出 力 結 果 イメージ(テストデータ)> テストデータ( 入 力 変 数 ) 期 待 値 ( 出 力 変 数 ) In1 In2 Out : : / 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 ) { : }

19 [ 参 考 ]CREST テストドライバの 工 夫 事 前 条 件 を 追 加 CRESTは 型 の 範 囲 でテストデータを 生 成 する 仕 様 上 取 り 得 る 値 でテストデータを 生 成 させる 仕 組 みを 追 加 < 出 力 結 果 イメージ(テストデータ)> テストデータ( 入 力 変 数 ) 期 待 値 ( 出 力 変 数 ) In1 In2 Out : : : : 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 ) { : }

20 [ 参 考 ]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 ) { 処 理 ; } テストドライバや 解 析 方 法 など 対 象 のソフトウェアに 合 った 使 用 方 法 を 見 つける 必 要 がある

21 参 考 文 献 謝 辞 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, (FAQ) J. Burnim and K. Sen, Heuristics for Scalable Dynamic Test Generation, Automated Software Engineering, ASE rd IEEEIACM International Conference on Moonzoo Kim, CREST Tutorial, 事 例 研 究 高 松 宏 樹, 佐 藤 晴 彦, 小 山 聡, 栗 原 正 仁, 動 的 記 号 実 行 によるメソッドの 複 雑 度 を 考 慮 したテストケース 自 動 生 成, 情 報 処 理 学 会 研 究 報 告, ソフトウェア 工 学 研 究 会 報 告, 2014(27) 植 月 啓 次, ソフトウェアの 実 装 情 報 に 基 づく 決 定 表 を 活 用 した 論 理 検 証 手 法, ソフトウェアシンポジウム2013, 12, 2013 岸 本 渉, 安 全 系 組 込 ソフトウェア 開 発 におけるユニットテストの 効 率 化, ソフトウェアシンポジウム2015, C-14-2, 2015 松 尾 谷 徹, 増 田 聡, 湯 本 剛, 植 月 啓 次, 津 田 和 彦, Concolic Testing を 活 用 した 実 装 ベースの 回 帰 テスト 人 手 によるテストケース 設 計 の 全 廃, ソフトウェアシンポジウム2015, C-14-2, 2015 謝 辞 : 本 取 組 において 社 内 の 研 修 などを 通 じ ご 指 導 ご 協 力 いただいた 方 々に 感 謝 いたします

22 21 / 19

23 [ 参 考 ] 記 号 実 行 22 / 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 )