The Test Cases Automatic Generation Tool BWDM


Go to English Ver.

最終更新日 平成29年2月28日

目次

BWDM image

研究背景

ソフトウェア開発おける上流工程において仕様書を作成する際に、自然言語の持つ曖昧さが問題となる。

自然言語の曖昧さ曖昧な仕様書を生み、
曖昧な仕様書は開発するシステムに対する曖昧な理解を呼び、
曖昧な理解を基に実装が行われることで仕様と実装間の齟齬が発生し、
最終的にソフトウェア内に不具合が含まれてしまう。

この問題を解決するために、形式手法(Formal Methods)が提案されている。
自然言語に代わり、数理論理学を基にした形式仕様記述言語(Formal Specification Language)を上流工程で用いることで、
厳密な仕様書を作成することが可能になる。
形式手法の1つにVDM(Vienna Development Method)、及びその形式仕様記述言語としてVDM-SLがある。

本研究では、形式手法VDMを用いたソフトウェア開発におけるソフトウェアテスト工程の作業効率化を目的として、
テストケース自動生成ツールBWDM(Boundary Value/Vienna Development Method)を開発した。
BWDMは、VDM-SLをオブジェクト指向拡張したVDM++により記述した仕様書に対し、
境界値分析を行い、テストケースを自動生成する。

入出力

input and output image

BWDMの入出力を以下に示す。

デシジョンテーブルファイルは、本研究室で西川、吉川らが開発したデシジョンテーブル生成支援ツールを用いて生成したものを用いる。
デシジョンテーブル生成支援ツールは、VDM++仕様ファイルを入力とし、出力としてデシジョンテーブルファイルをcsv形式で出力する。
生成するテストケースは、入力データとそれに対する期待出力データから構成する。

機能・対応構文

入力したVDM++仕様に対し構文解析を行い、データを抽出し、それを基に境界値分析を行い、テストケースを生成する。
境界値分析及びテストケース生成に対応する構文は、関数定義中の引数型とif式の条件式である。

制限

関数以外の定義には現在未対応である。
また、関数定義中の事前条件、事後条件等にも対応していない。
関数定義中の引数型については、整数型(int、nat、nat1)にのみ対応している。
関数定義の引数の個数は、2個にまで対応している。

今後の実装予定

future image

現在の境界値分析によるテストケース生成処理のみだと、プログラム中の全てのパスを網羅できない場合があることが判明している。
そのため新たに、それぞれの出力行に至るまでの条件式を満たす入力データ生成の処理を加える。

戻る