ソフトウェア・シンポジウム2017 in 宮崎

VDM++仕様を対象にしたテストケース自動生成ツール BWDM におけるif 式の構造認識に基づいたテストケース生成手法の提案
立山 博基
宮崎大学大学院工学研究科
tachiyama@earth.cs.miyazaki-u.ac.jp

要旨

片山 徹郎
宮崎大学工学教育研究部
kat@cs.miyazaki-u.ac.jp

様書上の表記を、仕様の作成者が本来意図していない意味で捉えてしまうことが起こる。実装者が、仕様書の本

ソフトウェア開発において、形式手法を用いることで、来の意図から外れた認識に基づいて実装を行った結果、仕様に曖昧さが含まれることを防ぐことができる。我々ソフトウェアにバグが混入されてしまう。

は、形式手法 VDM を用いたソフトウェア開発におけるこの問題を解決するための 1 つの手段として、形式テスト工程の効率化を目的として、テストケース自動生

手法 (Formal Methods)[3] が提案されている。形式手法

成ツール BWDM を試作した。既存の BWDM の問題点を用いた開発では、まず、数理論理学を基盤とした形式

として、VDM 仕様中の if 式からテストケース生成を行

仕様記述言語 (Formal Specification Language) により、う際に、ネストや else if などの if 式同士の構造を認識開発対象が持つ特性を仕様として記述する。数理論理学していない点が挙げられる。そのため、そのような構造を基にしているため、自然言語を用いた開発と異なり、の中にある戻り値に対するテストケース生成を行えな定理証明や機械的な検査を用いて、記述した内容が正しい。本稿では、この BWDM における、テストケース生いことを数学的に証明することが可能である。つまり、成処理の問題点を解決するために、if 式の構造認識に基自然言語の持つ曖昧さを排除した、厳密な仕様を作成すづいたテストケース生成手法の提案を行う。提案手法をることが可能となる。

VDM 仕様に適用した結果、従来の BWDM ではテストケース生成を行えなかった仕様中の戻り値に対する、テストケースの生成が可能になることを確認した。そのため、BWDM に提案手法を実装することで、テストケース生成処理の問題点を解決し、BWDM の有用性が向上すると言える。

一方で、自然言語もしくは形式手法を用いた設計のいずれにしても、実装を行った後は、作成したソフトウェアに対してテストを行う必要がある。テストを行うためには、テストケースの設計作業が必要であるが、人手によるテストケースの設計には手間と時間がかかる。そのため、テストケースの設計作業を効率よく行うことで、テスト工程を効率化できる。また、バグが潜みうる箇所に的を絞ったテストケースの設計を行うことも、テスト

1. はじめに実施の効率化のために重要である。
このような問題とソフトウェアテストの必要性を踏まソフトウェアは年々大規模化かつ高機能化を続け、そえ、形式仕様を基にしたテストケース自動生成ツールの結果、ソフトウェア上のバグが社会にもたらす影響もBWDM の試作を行った [4, 5, 6]。BWDM は、形式仕様記述言語 VDM++で記述した仕様とデシジョンテーブ
ルを入力とし、VDM++仕様を基に境界値分析を行い、テストケースを自動生成する。デシジョンテーブルとは、ソフトウェアの入力に対する出力を表形式でまとめたものである [7]。ソフトウェアに対してテストを行う際に、近年では甚大なものとなっている [1]。
ソフトウェアにバグが混入する原因の 1 つとして、上流工程のソフトウェア設計段階において、自然言語を一般的に用いていることが挙げられる。自然言語は元来、曖昧さを含んでいる [2]。そのため、プログラマが、仕13SEA

ソフトウェア・シンポジウム2017 in 宮崎

図 1. BWDM の構成

ソフトウェアの期待出力を確認する際に有用である。
既存の BWDM の問題点として、VDM++仕様中の if式からテストケース生成を行う際に、ネストや else if などの if 式同士の構造を認識していない点が挙げられる。
そのため、そのような構造の中にある戻り値に対するテストケース生成を行えない。
そこで本稿では、この問題の解決を目的として、if 式

図 2. BWDM の処理の流れの構造認識に基づいたテストケース生成手法を提案する。
具体的には、if 式の構造を認識し、条件式を生成し、それを基にテストケースを生成することによって、既存の• 期待出力データ生成部問題点の解決を目指す。

– デシジョンテーブル読み込み– 期待出力データ導出

2. テストケース自動生成ツール BWDM

– テストケース生成
本章では、既存のテストケース自動生成ツール BWDM

BWDM が持つ機能は、以下の通りである。の構成、機能、処理、入出力、及び、問題点について記す。

• VDM++仕様の構文解析及び情報の抽出

BWDM とは、Boundary Value と Vienna DevelopmentMethod の頭字語である。W は Value と Vienna の 2 つの V を意味する。

• 抽出した情報を基にした境界値分析• 境界値分析を行った結果を基にした入力データ生成

2.1. BWDM の構成・機能・処理• デシジョンテーブルを基にした入力データに対応す
る期待出力データの導出

図 1 に、BWDM の構成を示す。BWDM は入力データ生成部と期待出力データ生成部によって構成しており、• テストケースの出力 (入力データ＋期待出力データ)

それぞれの役割は以下の通りである。
図 2 に、BWDM の処理のフローチャートを示す。処理は以下の流れで行われる。

• 入力データ生成部– VDM++仕様読み込み

1. 指定された VDM++仕様ファイルを読み込む– 構文解析

2. VDM++仕様ファイルを構文解析する– データ抽出– 境界値分析

3. 関数定義中の引数型と if 式中の条件式に関する情報を抽出する– 入力データ生成

4. 抽出した情報に対して境界値分析を行う

14

SEA

ソフトウェア・シンポジウム2017 in 宮崎

1 class SampleClass
23 functions
4
5 sampleFunction : int*nat − > seq of char
6 sampleFunction(a, b) ==7 if(a <= 10) then
8if(-1 > a) then9“a <= 10 and -1 > a”
10else if(b > 0) then11“a <= 10 and !(-1 > a) and b > 0”
12else13“a <= 10 and !(-1 > a) and !(b > 0)”
14 else15
if(b <= -3) then16“!(a <= 10) and b <= -3”17else if(a < 20) then18“!(a <= 10) and !(b <= -3) and a < 20”
19else20“!(a <= 10) and !(b <= -3) and !(a < 20)”;
21
22 end SampleClass
図 3. 入力例：VDM++仕様

5. 境界値分析の結果から入力データを生成する
6. デシジョンテーブルを読み込む
図 4. 出力例：テストケース

7. 入力データとデシジョンテーブルから期待出力データを導出する

BWDM は現状、整数値の入力データ生成のみの対応

8. 入力データと期待出力データをテストケースとして併せて出力するであるため、以降の説明で登場する変数の型は全て整数型であるとする。また、テストケース生成処理は、関数構文解析は、Nick Battle 氏の開発した VDM 静的解

定義中の引数型と if 式のみを対象に行う。

析ツール VDMJ を用いて実現している [8]。境界値分析
は、抽出した引数型、if 式中の条件式のそれぞれに対し2.2. BWDM の入出力て行い、入力データを生成する。

BWDM は期待出力の導出を、入力データとデシジョBWDM の入出力に関して、VDM++仕様ファイルをンテーブルの照らし合わせによって行う。この際に使用

図 3 に、テストケースファイルを図 4 に、それぞれ示す。

するデシジョンテーブルは、本研究室で開発したデシジョ入出力に関係するファイルは以下である。

ンテーブル生成支援ツール [9] によって生成したもので• 入力ある。最終的に、テストケースを csv(comma-separatedvalues) 形式でファイルに書き出す。

– VDM++仕様ファイル (テキスト形式)

15SEAソフトウェア・シンポジウム2017 in 宮崎

1 class ProblemClass
23 functions
45 problemFunction : nat -> seq of char
6 problemFunction(a) ==7if(a mod 4 = 0) then
8if(a > 92) then9“a mod 4 = 0 and a > 92”
10else11“a mod 4 = 0 and !(a > 92)”
12else13“!(a mod 4 = 0)”;14
15 end ProblemClass

図 6. 図 5 から BWDM で生成したテストケース

図 5. 現状の課題：ネストした if 式

図 5 と図 6 に、現状、問題となる if 式、及び、その if式から生成したテストケースを示す。図 5 には、a mod– デシジョンテーブルファイル (csv 形式)

4 = 0 と a > 92 の整数値 a に関する 2 つの if 式がネストしており、戻り値は文字列である。文字列中には、その戻り値を返す際に a が満たすべき条件式を表している。

• 出力– テストケースファイル (csv 形式)

図 6 の期待出力データ中に戻り値 “a mod 4 = 0 anda > 92” に対するテストケースが存在しないことが確認できる。BWDM は境界値分析による入力データ生成処
理により、1 つ目の a mod 4 = 0 からは 3, 4, 5、2 つ目の a > 92 からは 92, 93 を入力データとして生成するが、それらの中には、“a mod 4 = 0 and a > 92” を出力する入力データは存在していない。戻り値 “a mod 4 =0 and a > 92” を出力するためには、a mod 4 = 0 anda > 92 を満たす入力データを生成する必要がある。

図 4 の入力データ中に存在する intM in, intM in −1, intM ax, intM ax + 1 などは、図 3 中の関数定義における引数型 (int) に対して境界値分析を行い、生成した入力データである。それぞれ、「引数型 int の最小値(Minimum)」、「引数型 int 型の最小値より 1 小さい値」、「引数型 int の最大値 (Maximum)」「引数型 int の最大値より 1 大きい値 (Maximum)」を表す。引数型の範囲外の値 (*Min-1, *Max+1) については、桁溢れにより、プログラムの動作が予測不可能であるため、期待出力デー
タは Undefined Action としている。

このような if 式による構造関係を認識し、その先の戻り値に対する入力データを生成できるように、BWDMを改良する必要がある。

2.3. BWDM の問題点
既存の BWDM は、構文解析により VDM++仕様中

3. if 式の構造認識に基づいたテストケース生成手法についての if 式の抽出を行っている。しかし、ネスト構造や elseif などの構造は無視している。それらの構造を持つ if 式が仕様中に存在する場合も、個々の if 式として抽出し、それら 1 つ 1 つに対して境界値分析を行い、入力データを生成している。そのため、複数の if 式が関わりあった構造の中にある戻り値に対する入力データの生成は行えない。

本章では、2.3 節で示した問題点を改良するための手法、及び、BWDM 上でその処理を行うための改良方法について述べる。

16

SEA

ソフトウェア・シンポジウム2017 in 宮崎

図 7. if 式へのインデックス付け及び満たすべき条件式の生成3.2. if 式の構造の認識及び満たすべき if 条件式の生成表 1. 図 5 における戻り値及びその際満たすべき条
件式と真偽値
戻り値

提案手法の例を、図 7 に示す。この例を基に、提案手条件式“a mod 4 = 0 and a > 92”

a mod 4 = 0,a > 92

“a mod 4 = 0 and !(a > 92)”

a mod 4 = 0,a <= 92“!(a mod 4 = 0)”法の説明を行う。手順は、if 式に対するインデックス付
けと条件式の生成の 2 つである。

1. if 式へのインデックス付け (図 7 中の手順 1.)
if 式の構造を認識するために、構文解析を行った後に、各 if 式へインデックスを付ける。インデックスにより、ネストや else if などの構造と、各戻り値に対する条件式を確認できるようにする。図 7 中には、if 条件式が 5 つ存在している。ネスト構造の中に存在している条件式 (図 7 中の condition0 −0, condition0 − 1, condition1 − 0) は、親の条件式(図 7 中の condition0, condition1) のインデックスの数字の後に、更にインデックスとして数字を割り振る。

a mod 4 != 0

3.1. 提案手法

if 式の各出力行へ至るためには、各出力行へ至る条件式を満たす入力データを生成すればよい。表 1 に、2.3節で用いた図 5 において、各出力行へ至るために満たす2. 条件式の生成 (図 7 中の手順 2.)べき条件式を示す。

各出力行へ至る入力データについて、if 条件式のイ

1 つ目と 2 つ目の出力においては、if 条件式がネストしているため、満たすべき if 条件式は and で繋がったものとなる。また、else 節の後にある出力は、記述してある if 条件式を否定した条件式を満たす必要がある。

ンデックスを辿りながら、入力データが満たすべき条件式を生成する。インデックスを辿る方法は複数の手法が考えられるが、今回は各戻り値から条件式を辿る。各戻り値ごとに、if 式のインデックスを利次節から、提案手法を実現するための具体的な処理の用して、その戻り値に至るために満たすべき条件式流れを述べる。

を導出する。

17SEAソフトウェア・シンポジウム2017 in 宮崎

して “a mod 4 = 0 and a > 92” を出力しているテストケースを確認できる。
よって、提案手法による処理を今後 BWDM に実装することで、if 式構造の中にある戻り値に対するテストケースを生成できる。

4. 考察
図 8. 図 5 に提案手法を適用して生成したテスト

4.1. 提案手法の有用性についてケース

本稿では、VDM++仕様を基にしたテストケース自動生成ツール BWDM において、if 式同士の構造の中にあ5 行目の output の出力に必要な条件式を具体例とすると、まず、4 行目の condition0 − 1 を満たす必要がある。更に、condition0 − 1 は else if の条件式であるため、2 行目の condition0 − 0 は否定する必要がある。そして、1 行目と 2 行目で if 式がネストしているため、1 行目の condition0 は満たす必要がある。

ンデックスに、更にインデックスを加える形とすることそのため、必要となる条件式は、condition0−1T rueで、ネストした if 式の構造を表現した。そして、付与しかつ condition0 − 0F alse かつ condition0T rue となたインデックスを基に、各出力行へ至るための条件式をる戻り値に対するテストケース生成を行えない問題を解決するために、if 式の構造認識に基づいたテストケース生成手法を提案した。
提案手法は、まず、VDM++仕様を構文解析した後に、関数定義中に登場する if 式にインデックス付けを行った。
この際、ネストの中にある if 式については、その親のイ生成した。最後に、生成した条件式を満たす入力データる。

を乱数によって生成した。
なお、ここでの condition∗T rue , condition∗F alse とは、今回提案した手法により、if 式同士の構造の中にある

a > 92 という if 条件式を例にすると、conditionT rue がa > 92、conditionF alse は、conditionT rue の a <= 92となる。

戻り値に対するテストケースを生成できることを確認できた。よって、既存の BWDM のテストケース生成処理に、今回提案したテストケース生成処理を追加で実装することで、if 式同士の構造の中にある戻り値に対するテ3.3. 生成した条件式を満たす入力データの生成ストケース生成を行えない問題を解決できる。

満たすべき条件式を生成した後に、その条件式を満た4.2. 関連研究

す整数値を生成する。乱数により整数値を生成し、整数値が条件式を満たせば、入力データとして採用する。

記号実行 (Symbolic Execution)[10] を用いることで、条件式を満たす整数が存在しない場合、入力データの今回の提案手法同様に、if 式が入れ子になった場合も全生成は不可能である。そのため、入力データ生成に時間ての戻り値に対してテストケース生成を行った事例とし制限を設け、一定時間が経過した場合は入力データ生成て、宮本らの研究 [11] と、高松らの研究 [12] がある。記号実行は、各戻り値に対する制約条件 (条件式) を導出処理を終了する。

する。
ソースコード中の表明 (Assersion) の動的な自動生成

3.4. 提案手法によるテストケース手法は広く研究されているが、その問題点として、最終
図 8 に、2.3 節の図 5 に対して、提案手法を適用する的に生成する表明は、手法中で対象プログラムの実行ことで生成できるテストケースを示す。提案手法によりデータを取得する際に用いられるテストケースに依存す新たに生成できるテストケース中に、期待出力データとるということが知られている。宮本らはこのテストケー

18

SEA

ソフトウェア・シンポジウム2017 in 宮崎

TOBIAS と BWDM は，どちらも VDM++を用いたソフトウェア開発のテスト段階を支援する．TOBIAS は，VDM++で記述された仕様そのもののテスト支援を行う．
これに対して，BWDM は VDM++で記述された仕様から実際に実装を行ったソフトウェアへのテストを支援する点で，異なっている．

ス依存問題を改善するために、記号実行などの手法を用いたテストケース生成手法を提案した。記号実行を用いて、対象ソースコード内の全ての戻り値に対して、その制約条件 (条件式) を導出し、その条件を満たす引数を生成している。
また、オブジェクト指向プログラミングにおけるソフトウェアテストを行うには、テスト対象のインスタ5. おわりにンス生成・状態の変更などの前準備のメソッド実行を、テストケース内で行う必要がある。そのようなテスト
ケース自動生成ツールの 1 つに Seeker[13] があり、高松

本稿では、VDM++を基にしたテストケース自動生成

らは Seeker の機能拡張を行った。Seeker では、記号実ツール BWDM における、if 式同士の構造の中にある戻行と具体的な値を組み合わせた動的記号実行 (Dynamicり値に対するテストケース生成を行えない問題を解決す

Symbolic Execution) を用いて、ソースコード中の条件式を基に、全ての戻り値に対する引数の組を生成している。

るために、if 式の構造認識に基づくテストケース生成手

本研究で提案する、if 式の構造認識に基づいたテストに、if 条件式にインデックスを付与し、そのインデック

ケース生成手法は、インデックスを用いて戻り値から条スを基に、各出力行へ至るための条件式を生成し最終的件式を導出するため、記号実行と比較して、探索空間をに、それらの条件式を満たす入力データを乱数によって削減できる。そのため、計算効率の面で、記号実行に比生成した。

法を提案した。
提案手法ではまず、VDM++仕様を構文解析した後べて優位性が有ると言える。

提案手法により、既存の BWDM では生成できなかっ

また、VDM 仕様を基にしたテストケースの自動生成た、if 式による構造の中にある戻り値に対するテストケー法に関する研究の 1 つに、馬場らの研究がある [14]。馬スの生成が可能なことを確認した。故に、既存の BWDM

場らの研究では、VDM 仕様記述からコーナーケースにのテストケース生成処理に、今回提案したテストケース対するテストを行うことを目的として、テストドライバ生成処理を追加で実装することで、if 式同士の構造の中の雛形の作成を行うツールを開発した。馬場らのツールにある戻り値に対するテストケース生成を行えない問題は、形式手法を用いたソフトウェア開発におけるプロセを解決できる。

ス中の、単体テストにおけるテストを支援する。

以上のことから、今回の提案手法に基づいて BWDM

馬場らのツールは、現状、VDM-SL 仕様内の操作定へ入力データ生成処理を実装することで、既存の BWDM義をテストケース作成の対象としている。そのため、の問題点を解決し、BWDM の更なる利便性の向上に繋

VDM++を対象に、関数定義からテストケースを作成する BWDM とは異なる。また、馬場らのツールから出力されるテストケースは、入力データとして記述内の条件式を表示するものである。これに対して、BWDM は条件式から生成した、具体的な数値の入力データを確認することが可能である。そのため、BWDM の出力を使ってそのままテストを実行できることが、BWDM の利点であるといえる。

がると言える。
以下に、BWDM の今後の課題を示す。

• デッドコードへの対応
戻り値に対する条件式を満たす整数が存在しない
場合、戻り値はデッドコードである。この場合、入力データ生成は行えないため、本研究では入力データ生成処理を一定時間で終了する。充足不能な条件

また，VDM++仕様記述をテストするためのテスト

式に対しては、入力データ生成処理を行わず、ユーケース自動生成ツールとして，TOBIAS[15] がある．TO-ザーにデッドコードを指摘する機能が必要である。

BIAS は，TOBIAS に入力されたテストパターンに従い，テストケースを自動生成する．テストパターンとは，テスト設計者が正規表現を用いて，出力するテストケースを定義したものである．

• 未対応の定義部や構文、演算子への対応
操作定義、型定義などの定義部へは現在未対応である。また、事前条件や事後条件、let 式など

19SEA

ソフトウェア・シンポジウム2017 in 宮崎の VDM++に存在する多くの構文にも、既存のPrototype of Test Cases Automatic Generation
Tool BWDM Based on Boundary Value Analysis
with VDM++, The 2017 International Conferenceon Artificial Life and Robotics(ICAROB 2017),
pp.275-278, 2017

BWDM は未対応である。これらの構文からテストケースを生成する手法を考案し、BWDM に実装することで、BWDM の有用性が更に向上すると考えている。
• 整数型以外への対応[7] SQuBOK 策定部会, ソフトウェア品質知識体系ガイド 第 2 版, オーム社, 2014

既存の BWDM は、整数型以外の、実数型や合成型には未対応である。構文解析の際に、整数型以外の[8] Nick Battle GitHub - nickbattle/vdmj, https://github.com/nickbattle/vdmj, 2017/3/8 アクセス型の情報を抽出し、境界値分析及び入力データ生成処理を実装することで、これらのテストケースの生[9] 西川拳太, 片山徹郎, VDM++を用いたデシジョンテーブル生成支援ツールについて, 平成 25 年度 電気関係学会 九州支部連合大会, p.381, 2013

成が可能になると考えている。

• 両辺が変数である if 条件式への対応
if 条件式中の両辺が変数である場合、既存の BWDMは境界値分析を行うことができないため、入力データ生成を行えない。このような if 条件式から境界値を抽出する処理を BWDM に実装することで、BWDM の適用範囲の更なる拡大を見込める。

[10] James C. King, Symbolic Execution and Program
Testing, Communications of The ACM Vol.19,
No.7, pp.385-394, DOI: 10.1145/360248.360252
1976[1] 失敗事例データベース, 失敗事例 – みずほファイ
ナンシャルグループ大規模システム障害, http://condezine.jp/article/detail/2364, 2017/3/8
アクセス[11] 宮 本 敬 三, 堀 直 哉, 岡 野 浩 三, 楠 本 真 二,
Daikon 生 成 表 明 改 善 の た め の テ ス ト ケ ー ス
自 動 生 成 手 法 と そ の 評 価 実 験,
コ ン ピュー
タ ソ フ ト ウェア, Vol.28, No.4, pp.306-317,
https://www.jstage.jst.go.jp/article/
jssst/28/4/28_4_4_306/_article/-char/ja/
2010[2] IPA 独立行政法人 情報処理推進機構, なぜ形式
手法か, http://sec.ipa.go.jp/users/seminar/
seminar_tokyo_20150912-02.pdf, 2017/3/8 アクセス[12] 高松宏樹, 佐藤晴彦, 小山聡, 栗原正仁, 動的記号実行によるメソッドの複雑度を考慮したテストケース
自動生成, 情報処理学会研究報告 Vol.2014-SE-185,
No.27, NAID: 110009803966 2014[3] 荒木啓二郎, 張漢明, プログラム仕様記述論, オーム社, 2002

[13] Suresh Thummalapenta, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, Zhendong Su, Synthesizing Method Sequences for High-Coverage Testing, SIGPLAN Notices Vol.46, No.10, pp.189-206,
DOI: 10.1145/2076021.2048083 2011

参考文献

[4] 立山博基, 片山徹郎, VDM++仕様を基にした境界値テストケース自動生成ツール BWDM の試作について, 平成 28 年度 電気・情報関係学会 九州支部連合大会, p.90, 2016[5] 立山博基, 片山徹郎, VDM++仕様に対する境界値分析を用いたテストケース自動生成, JaSST’16 九州,
p.32, 2016[14] 馬 場 勇 輔, 荒 木 啓 二 郎, 日 下 部 茂, 大 森 洋一, 形 式 仕 様 記 述 の プ ロ パ ティベ ー ス テ ス ト への活用, 情報処理学会 火の国シンポジウム予稿集, https://www.ipsj-kyushu.jp/page/ronbun/
hinokuni/1005/5C/5C-1.pdf, 2017/3/11 アクセス[6] Hiroki Tachiyama, Tetsuro Katayama, Yoshihiro
Kita, Hisaaki Yamaba, and Naonobu Okazaki,[15] Olivier Maury, Yves Ledru, Pierre Bountron and Lydie du Bousquet, Using TOBIAS

20SEA

ソフトウェア・シンポジウム2017 in 宮崎

for the automatic geneeration of VDM test
cases, Laboratoire Logiciels, Systemes Reseaux –IMAG, http://vasco.imag.fr/Tobias/Papers/
vdm02tobias.pdf, 2017/5/10 アクセス

21SEA