Comments
Description
Transcript
形式仕様に基づくテストケースの自動生成
情報処理学会第 77 回全国大会 3L-05 形式仕様に基づくテストケースの自動生成 池田 逸人 † 劉 少英 ‡ 法政大学情報科学部 † Email: [email protected] 法政大学情報科学部 ‡ Email: [email protected] Abstract Software testing is a time-consuming activity and automatic testing is a desirable solution to this problem. In this paper, we describe a software supporting tool for automatic test case generation from formal specifications written in the Structured Objectoriented Formal Language (SOFL). We discuss the algorithms for generating test cases from atomic predicates and their conjunctions that may involve various operations on data items of various data types such as set, sequence, and composite types. We describe the details of the software tool by presenting the three major functions implemented: (1) editing a SOFL specification, (2) generating test cases from the specification, and (3) managing test cases in files. 1. まえがき 現代社会においてソフトウェアは，交通システム，医 療機器，ATM 等の様々な分野で利用されている．これ らのソフトウェアは，プログラムのエラーやバグでシ ステムが停止することは合ってはならない．そこで Z 記法のような形式仕様記述言語を使って仕様を定義す ることで，厳密に仕様を定義してテストをすることが 出来る [1]．しかし，形式仕様は記述方法が難しく，書 くのに時間がかかるという問題点が存在する．そこで 形式工学手法である SOFL を使って，記述方法が難し いという問題を解決することが出来る [2]．しかし，ソ フトウェアテストに多くのコストと時間がかかるとい う問題点が残っている．この問題を解決するため本研 究では，SOFL 形式仕様からテストケースを自動生成 するツールを開発することで，テストに費やす時間を 削減することを試みる． 2. テストケース生成の概要 SOFL 形式仕様の process で定義された，入力変数の 値の生成を試みる．この入力変数の値がテストケース となる．process では，入力変数および出力変数の precondition と post-condition を定義する．これらの条件 は，述語論理によって定義される．次の図 1 は process の一例である． Automatic Testcase Generation Based on Formal Specification †「hayato ikeda・Faculty of Computer and Information Sciences Hosei University」 ‡「Shaoying Liu・Faculty of Computer and Information Sciences Hosei University」 図 1: SOFL 形式仕様の例 図 1 の process は，配列の先頭要素の値によって文 字列を出力する process である．入力変数が set of int 型の array で，出力変数が string 型の message であり， pre-condition と post-condition が定義されている． 2.1. 原子論理式でのテストケース生成 原子論理式でのテストケースは，オペレーターとオ ペランドと結果によって生成する．例えば，x>0 なら ば，x=2 のようなテストケースを簡単に生成すること ができる．しかし，次のような複数のオペレータを含 む論理式のテストケースの生成は困難である． card(union(a, b)) > 3 (1) (a, b は，set of int 型の入力変数とする) そこで，条件を逆ポーランド記法で記述して読み取 る．オペレータと対応するオペランドを 1 つの仮のオ ペランドとおいて，最終的にオペレーターを 1 つにす ることでテストケースは生成することができる． 2.1.1. オペレータを 1 つにする 条件を読み取るときに，オペランドはスタックにプッ シュする．オペレータを読み取ったとき，スタックか らオペレータに対応するオペランドをポップし，オペ ランドとオペレータの結果を 1 つの仮のオペランドと おいてスタックにプッシュする．最終的にオペレータ を 1 つにすることができる．例えば，この方法を (1) に 適用すると次のようになる． a b union card c union card c card c > > > [] [a b] [A] (2) (3) (4) > [B c] (5) (1) の論理式を逆ポーランド記法に変換した式が (2) であり，式の横にある [] はスタックの中身である．こ れらの式は，オペレータが最終的に 1 つになる様子を 表したものである．例えば，(3) で union を読み取った 場合，union はオペレータであるのでスタックにある 引数と union の結果を 1 つの仮のオペランド A と置い てスタックにプッシュする．その結果が (4) である． 1-355 Copyright 2015 Information Processing Society of Japan. All Rights Reserved. 情報処理学会第 77 回全国大会 2.1.2. オペレータによるテストケースの生成 オペレータを 1 つにしたら，論理式を満たす具体的 な値を求める．求めたものが仮のオペランドだった場 合は，元の式についても考える．先ほどの例で，オペ ランドを 1 つにした (5) の場合は論理式「B>3」につい て考える。オペレータは「>」であることから，上の論 理式を満たす値「B=4」を求めることができる． 「B」は 仮のオペランドであるので，元の式についても考える． B = card(A) = 4 能は「エディタ」， 「テストケース生成」， 「テストケー ス表示/保存」の 3 つである． 4. 実装 実装は C#で，統合開発環境として MicrosoftVisualStudio2013 を使用して行った．ライブラリとして． NET を利用している．画面は，WPF(Windows Presentation Foundation) を利用して開発した．ツールを 起動すると仕様を入力する画面が表示される (図 2)． (6) オペレータは「card」であることから，上の論理式を 満たす値「A={2,3,4,-5}」を求めることができる．同 様に「A」は仮のオペランドであるので，元の式につい ても考える． A = union(a, b) = {2, 3, 4, −5} (7) オペレータは「union」であることから，上の論理式 を満たす値「a={2,3},b={4,-5}」を求めることができ る．最終的に，論理式 (1) を満たす a,b を求めることが でき，これらの値がテストケースとなる． 2.2. 論理積によるテストケースの生成 「P1 and P2 ・ ・ ・ Pn」のような論理式に論理積 and を含むテストケースを求める手順を次に示す． (a) P1 を満たす入力変数を節「2．1」の方法によっ て生成する (b) (a) で求めた入力変数は，P2∼Pn に代入する (c) P2∼Pn に，(a),(b) を適用する このとき，手順 (b) によって，原子論理式 P が入力 変数を含まなくなる場合がある．その時は，原子論理 式 P が真であるかどうかを判断する．原子論理式 P が 真であれば次の原子論理式に手順 (a),(b) を適用し，偽 であれば生成は失敗である．P1∼Pn に方法を適用で きれば，テストケースの生成できたことになる．次は テストケース生成に成功した一例である． x > 0 and y > 0 and y > x (8) (8) の式の，原子論理式「x>0」から「x=1」を求める． そして，すべての x に 1 を代入すると「1>0 and y>0 and y>1」のようになる．さらに， 「y>0」から「y=2」 を求める．原子論理式「y>1」は「2>1」であるので真 である．よって，テストケースの生成に成功したといる． 生成に失敗した場合は，原子論理式に方法を適用す る順番を変えることで，上の例のように，テストケース が生成しやすくなる場合がある．それでもテストケー スを生成できない場合は，値を「nil」にする． 2.3. テスト条件からテストケースの生成方法 process のテストケースは，pre-condition と guardcondition を組み合わせたテスト条件によって生成され る．guard-condition とは，論理式が入力変数によって 構成された条件である． 3. 支援ツールの概要 今回開発するツールは，ウィンドウに SOFL 形式仕 様が書かれたテキストを読み込み，生成されたテスト ケースを別のウィンドウに表示する．ツールの主な機 図 2: ツールの仕様記述画面 仕様を直接記述またはテキストから読み込んで，メ ニューバーの Run ボタンを押すと，別ウインドウに， テストケースが表示される (図 3)．図 3 の画面左下の 「Save as xlxs file」ボタンを押すと，表示されたテスト ケースがエクセルファイルとして保存される． 図 3: テストケースの表示画面 5. 結論と課題 今回，SOFL 形式仕様からテストケース生成の方法 を考案し，実装した．オペレータから原子論理式を満 たす値を生成することに成功した．また，論理積 and と論理和 or を含む論理式からテストケースを生成でき るようになったことで，テスト条件からテストケース を生成できるようになった． しかし，問題点がいくつか存在する．1 つ目は，仕様 を逆ポーランド記法で書く必要があることである．逆 ポーランド記法に変換する構文解析器の実装は間に合 わなかった．2 つ目は，今回のツールに対するテスト不 足であることである．オペレータの数に制限がないた め完璧にテストをするのは難しい． 文 献 [1] Phill Stock and David Carrington, ”A Framework for Specification-Based Testing”, IEEE Transactions on Software Engineering, Vol. 22, No. 11, 1996. [2] Saoying Liu, ”Formal Engineering for Industrial Software Development Using the SOFL Method”, Springer, 2004. 1-356 Copyright 2015 Information Processing Society of Japan. All Rights Reserved.