(57)【要約】【課題】所望の網羅性と効率性を満たすテストケースを生成する。【解決手段】本発明のテストケース生成装置は、検査対象のシステムの状態と外部イベントの発生に応じた状態変化を表す第１遷移とを含む状態遷移系と、前記システムに対して発生し得る外部イベントと、前記システムの事前条件および事後条件とを関連づけた要求項目と、与えられた状態を、前記与えられた状態に対する前記事前条件および事後条件の真偽の組へ写像する状態写像関数を生成する状態写像生成手段と、前記状態遷移系を前記状態写像関数により縮約して剰余状態遷移系を生成する剰余状態遷移系生成手段と、前記剰余状態遷移系の各遷移を辿ることによって代表遷移パスを生成する代表遷移パス生成手段と、前記代表遷移パスを前記状態遷移系での遷移パスに復元する遷移パス変換手段と、前記遷移パスを前記テストケースとして出力する出力手段と、を備える。【選択図】図１
2010218152.tif 000002
【特許請求の範囲】
【請求項１】
検査対象のシステムのテストケース生成装置であって、
複数の内部変数の値の組によって表される前記システムの状態と、前記システムに対して発生する外部イベントに応じた状態変化を表す第１遷移とを含む状態遷移系を記憶する第１の記憶手段と、
前記システムに対して発生し得る外部イベント毎に、前記外部イベントが発生する前の前記システムの状態を定義した事前条件と、前記外部イベントの発生後の前記システムの状態を定義した事後条件とを記述した要求項目を記憶する第２の記憶手段と、
前記第２の記憶手段からｍ個（ｍは１以上の整数）の要求項目を選択し、前記ｍ個の要求項目から前記事前条件と前記事後条件とを抽出する条件抽出手段と、
与えられた状態を、前記与えられた状態に対する前記条件抽出手段により抽出したすべての事前条件および事後条件の真偽の組へ写像する状態写像関数を生成する状態写像生成手段と、
前記状態遷移系に含まれる前記複数の状態のそれぞれを、前記状態写像関数によりそれぞれ写像して複数の写像値を取得し、取得された複数の写像値に基づき、同じ写像値をもつ状態群を同じグループに分類することにより前記複数の状態をグループ化して、複数のグループを生成するグループ化手段と、
前記複数のグループのうちの２つのグループを指定し、一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの少なくとも１つの第１遷移が前記状態遷移系に存在するときは、前記一方のグループから前記他方のグループへの第２の遷移を設定し、前記グループの指定と第２の遷移の設定とを繰り返し、これにより複数の前記グループ間の第２遷移を表す剰余状態遷移系を生成する剰余状態遷移系生成手段と、
前記剰余状態遷移系の所定のグループから開始して、前記剰余状態遷移系における前記第２遷移を順次辿ることによって、前記第２遷移のシーケンスである代表遷移パスを生成する代表遷移パス生成手段と、
前記第２遷移が追跡された順番で前記代表遷移パスの前記第２遷移を順次選択し、前記順次選択された第２遷移のそれぞれについて、前記選択された第２遷移の遷移元グループにおける状態のうちの１つと同じ遷移元状態を有し、かつ前記選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に特定された第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を前記状態遷移系において特定し、前記順次選択された第２遷移に対して特定された各第１遷移のシーケンスを含むテストケースを生成する、遷移パス変換手段と、
を含むテストケース生成手段と、
前記テストケースを出力する出力手段と、
を備えたことを特徴とするテストケース生成装置。
【請求項２】
検査対象のシステムのテストケース生成装置であって、
複数の内部変数の値の組によって表される前記システムの状態と、前記システムに対して発生する外部イベントに応じた状態変化を表す第１遷移とを含む状態遷移系を記憶する第１の記憶手段と、
前記システムに対して発生し得る外部イベント毎に、前記外部イベントが発生する前の前記システムの状態を定義した事前条件と、前記外部イベントの発生後の前記システムの状態を定義した事後条件とを記述した要求項目を記憶し、前記事前条件および前記事後条件は、それぞれ１つの内部変数の条件を定めた１つ以上の原子述語の論理演算により形成されている、第２の記憶手段と、
前記第２の記憶手段からｍ個（ｍは１以上の整数）の要求項目を選択し、前記ｍ個の要求項目における前記事前条件と前記事後条件に含まれるすべての原子述語を抽出する原子述語抽出手段と、
各抽出された原子述語のうちｈ個（ｈは１以上の整数）の原子述語を選択し、与えられた状態を、前記与えられた状態に対する前記ｈ個の原子述語の真偽の組へ写像する状態写像関数を生成する状態写像生成手段と、
前記状態遷移系に含まれる前記複数の状態のそれぞれを、前記状態写像関数によりそれぞれ写像して複数の写像値を取得し、取得された複数の写像値に基づき、同じ写像値をもつ状態群を同じグループに分類することにより前記複数の状態をグループ化して、複数のグループを生成するグループ化手段と、
前記複数のグループのうちの２つのグループを指定し、一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの少なくとも１つの第１遷移が前記状態遷移系に存在するときは、前記一方のグループから前記他方のグループへの第２の遷移を設定し、前記グループの指定と第２の遷移の設定とを繰り返し、これにより複数の前記グループ間の第２遷移を表す剰余状態遷移系を生成する剰余状態遷移系生成手段と、
前記剰余状態遷移系の所定のグループから開始して、前記剰余状態遷移系における前記第２遷移を順次辿ることによって、前記第２遷移のシーケンスである代表遷移パスを生成する代表遷移パス生成手段と、
前記第２遷移が追跡された順番で前記代表遷移パスの前記第２遷移を順次選択し、前記順次選択された第２遷移のそれぞれについて、前記選択された第２遷移の遷移元グループにおける状態のうちの１つと同じ遷移元状態を有し、かつ前記選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に特定された第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を前記状態遷移系において特定し、前記順次選択された第２遷移に対して特定された各第１遷移のシーケンスを含むテストケースを生成する遷移パス変換手段と、
を含むテストケース生成手段と、
前記ｍ個の要求項目のそれぞれについて前記テストケースにおいて遷移元状態が前記事前条件を満たし遷移先状態が前記事後条件を満たす第１遷移が網羅されているか否かを評価し、前記ｍ個の要求項目のうち前記テストケースにより網羅されている要求項目の割合または個数を示す網羅度を計算する網羅性評価手段と、
前記網羅度が閾値を満たすときの前記テストケースを出力する出力手段と、を備え、
前記状態写像生成手段は、前記閾値を満たす前記網羅度が得られるように前記各抽出された原子述語を取捨選択して前記状態写像関数を生成する
ことを特徴とするテストケース生成装置。
【請求項３】
前記ｍ個の要求項目に含まれる前記事前条件および前記事後条件の集合において、前記各抽出された原子述語のそれぞれの出現頻度を計算する出現頻度解析手段をさらに備え、
前記状態写像生成手段は、前記網羅度が前記閾値を満たす前記状態遷移関数が生成されるまで、前記各抽出された原子述語から出現頻度の高い順に１つの原子述語を追加的に選択して前記状態遷移関数を生成することを繰り返す
ことを特徴とする請求項２に記載のテストケース生成装置。
【請求項４】
前記ｍ個の要求項目に含まれる前記事前条件および前記事後条件の集合において、前記各抽出された原子述語のそれぞれの出現頻度を計算する出現頻度解析手段をさらに備え、
前記状態写像生成手段は、前記各抽出された原子述語の全てを選択して前記状態写像関数を生成し、前記網羅度が前記閾値を満たしている間、前記原子述語の全てから、出現頻度の低い順に原子述語を１つ順番に除去しながら前記状態写像関数を生成することを繰り返す、
ことを特徴とする請求項２に記載のテストケース生成装置。
【請求項５】
コンピュータにおいて検査対象のシステムのテストケースを生成するテストケース生成方法であって、
読み出し手段が、複数の内部変数の値の組によって表される前記システムの状態と、前記システムに対して発生する外部イベントに応じた状態変化を表す第１遷移とを含む状態遷移系を記憶する第１の記憶手段から前記状態遷移系を読み出し、
条件抽出手段が、前記システムに対して発生し得る外部イベント毎に、前記外部イベントが発生する前の前記システムの状態を定義した事前条件と、前記外部イベントの発生後の前記システムの状態を定義した事後条件とを記述した要求項目を記憶する第２の記憶手段からｍ個（ｍは１以上の整数）の要求項目を選択し、前記ｍ個の要求項目から前記事前条件と前記事後条件とを抽出し、
状態写像生成手段が、与えられた状態を、前記与えられた状態に対する前記条件抽出手段により抽出したすべての事前条件および事後条件の真偽の組へ写像する状態写像関数を生成し、
グループ化手段が、前記状態遷移系に含まれる前記複数の状態のそれぞれを、前記状態写像関数によりそれぞれ写像して複数の写像値を取得し、取得された複数の写像値に基づき、同じ写像値をもつ状態群を同じグループに分類することにより前記複数の状態をグループ化して、複数のグループを生成し、
剰余状態遷移系生成手段が、前記複数のグループのうちの２つのグループを指定し、一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの少なくとも１つの第１遷移が前記状態遷移系に存在するときは、前記一方のグループから前記他方のグループへの第２の遷移を設定し、前記グループの指定と第２の遷移の設定とを繰り返し、これにより複数の前記グループ間の第２遷移を表す剰余状態遷移系を生成し、
代表遷移パス生成手段が、前記剰余状態遷移系の所定のグループから開始して、前記剰余状態遷移系における前記第２遷移を順次辿ることによって、前記第２遷移のシーケンスである代表遷移パスを生成し、
遷移パス変換手段が、前記第２遷移が追跡された順番で前記代表遷移パスの前記第２遷移を順次選択し、前記順次選択された第２遷移のそれぞれについて、前記選択された第２遷移の遷移元グループにおける状態のうちの１つと同じ遷移元状態を有し、かつ前記選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に特定された第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を前記状態遷移系において特定し、前記順次選択された第２遷移に対して特定された各第１遷移のシーケンスを含むテストケースを生成し、
出力手段が、前記テストケースを出力する、
ことを特徴とするテストケース生成方法。
【請求項６】
コンピュータにおいて検査対象のシステムのテストケースを生成するテストケース生成方法であって、
読み出し手段が、複数の内部変数の値の組によって表される前記システムの状態と、前記システムに対して発生する外部イベントに応じた状態変化を表す第１遷移とを含む状態遷移系を記憶する第１の記憶手段から前記状態遷移系を読み出し、
原子述語抽出手段が、前記システムに対して発生し得る外部イベント毎に、前記外部イベントが発生する前の前記システムの状態を定義した事前条件と、前記外部イベントの発生後の前記システムの状態を定義した事後条件とを記述した要求項目を記憶した、前記事前条件および前記事後条件は、それぞれ１つの内部変数の条件を定めた１つ以上の原子述語の論理演算により形成されている、第２の記憶手段からｍ個（ｍは１以上の整数）の要求項目を選択し、前記ｍ個の要求項目における前記事前条件と前記事後条件に含まれるすべての原子述語を抽出し、
状態写像生成手段が、各抽出された原子述語のうちｈ個（ｈは１以上の整数）の原子述語を選択し、与えられた状態を、前記与えられた状態に対する前記ｈ個の原子述語の真偽の組へ写像する状態写像関数を生成し、
グループ化手段が、前記状態遷移系に含まれる前記複数の状態のそれぞれを、前記状態写像関数によりそれぞれ写像して複数の写像値を取得し、取得された複数の写像値に基づき、同じ写像値をもつ状態群を同じグループに分類することにより前記複数の状態をグループ化して、複数のグループを生成し、
剰余状態遷移系生成手段が、前記複数のグループのうちの２つのグループを指定し、一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの少なくとも１つの第１遷移が前記状態遷移系に存在するときは、前記一方のグループから前記他方のグループへの第２の遷移を設定し、前記グループの指定と第２の遷移の設定とを繰り返し、これにより複数の前記グループ間の第２遷移を表す剰余状態遷移系を生成し、
代表遷移パス生成手段が、前記剰余状態遷移系の所定のグループから開始して、前記剰余状態遷移系における前記第２遷移を順次辿ることによって、前記第２遷移のシーケンスである代表遷移パスを生成し、
遷移パス変換手段が、前記第２遷移が追跡された順番で前記代表遷移パスの前記第２遷移を順次選択し、前記順次選択された第２遷移のそれぞれについて、前記選択された第２遷移の遷移元グループにおける状態のうちの１つと同じ遷移元状態を有し、かつ前記選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に特定された第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を前記状態遷移系において特定し、前記順次選択された第２遷移に対して特定された各第１遷移のシーケンスを含むテストケースを生成し、
網羅性評価手段が、前記ｍ個の要求項目のそれぞれについて前記テストケースにおいて遷移元状態が前記事前条件を満たし遷移先状態が前記事後条件を満たす第１遷移が網羅されているか否かを評価し、前記ｍ個の要求項目のうち前記テストケースにより網羅されている要求項目の割合または個数を示す網羅度を計算し、
出力手段が、前記網羅度が閾値を満たすときの前記テストケースを出力し、
前記状態写像生成手段は、前記閾値を満たす前記網羅度が得られるように前記各抽出された原子述語を取捨選択して前記状態写像関数を生成する
ことを特徴とするテストケース生成方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、テストケース生成装置およびテストケース生成方法に関し、たとえばソフトウェアを始めとするシステム開発のテスト工程の為に、システムの仕様からシステムのテストケースを自動的に生成する装置および方法に関する。
【背景技術】
【０００２】
ソフトウェアを始めとするシステム開発の検証段階において、開発対象システムを形式化したモデルから、システムを検証するテストケース(検証手順)を自動的に生成するMBT(モデルベーステスト)がある。MBTの一つとして、システムが取りえる状態と状態遷移を網羅した状態遷移系をベースに、状態遷移系からグラフ理論のアルゴリズムに従ってパスを生成する事により、テストケースを生成する手法が知られている。この手法により生成したテストケースを用いることで、システムに起こりえる状態遷移に対し網羅的なテストを行うことができる。
【先行技術文献】
【非特許文献】
【０００３】
【非特許文献１】Harold W. Thimbleby: "The directed Chinese Postman Problem", In Software - Practice and Experience (SPE), Volume 33, pp.1081-1096, 2003.
【非特許文献２】Harold Abelson and Gerald Jay Sussman with Julie Sussman: "Structure and Interpretation of Computer Programs", MIT Press, 1996.
【発明の概要】
【発明が解決しようとする課題】
【０００４】
ところが、状態遷移系は数多くの類似する状態遷移を含み、得られるテストケースは冗長であることが多い。例えば、下はオペレーティングシステムのタスク管理機能における例である。
・  場合1: 状態「タスク1が待ち状態」で、イベント「wakeup(タスク1)」が発生
・  場合2: 状態「タスク2が待ち状態」で、イベント「wakeup(タスク2)」が発生
【０００５】
相違点は対象となるタスクIDのみであり、場合によってはどちらか片方のみをテストすれば十分である。特に大規模なシステム開発では、全ての場合を網羅的に検証するのは不可能に近く、検証すべき事項に対する網羅性を確保したまま適度に間引いてテストするのが現実的である。
【０００６】
その一つの解として、本件出願人により２００８年４月２８日に出願された先願に係る特願2008-117173号では、以下のテストケース生成技術を提案している。すなわち、このテストケース生成技術では、状態遷移系の状態集合に関する写像(状態写像)関数を与え、状態写像関数で写した値の同一性により状態間の同値関係を定義する。これに基づいて状態遷移系を予め縮約し、縮約された状態遷移系（剰余状態遷移系）からテストケースを生成する。
【０００７】
より詳細には、このテストケース生成技術では、ユーザが指定した状態写像の値による同値関係で、状態遷移系の状態を同一視する。状態写像の値による同値関係とは、状態写像関数の出力結果（写像値）が等しい状態を同一視し、出力結果が異なる状態を同一視しない事である。そして、同一視された複数の状態を、一つの抽象状態（グループ）にまとめて状態遷移系を小さく縮約する事が可能である。抽象状態とは、同値関係で同一視された複数の状態を、一つの状態として認識した仮想的な状態である。更に、縮約された小さな状態遷移系の状態遷移を少なくとも一度は網羅するように、テストケースを生成する事が出来る。
【０００８】
図3および図4は、タスク管理機能における具体例である。図3では、各タスク状態(RUN, RDY, WAI)のタスクの個数を出力する状態写像関数を定義している。各タスク状態のタスクの個数が等しい時、タスクIDを区別しないで見た場合に同一の状態と見なせる。この状態写像関数で状態遷移系を縮約した例が図4に示される。状態遷移数が42から8にまで縮約されている。
【０００９】
前述の手法においては、状態写像関数が、出力されるテストケースの網羅性と効率性(トレードオフ関係)を大きく左右する。しかし、求める網羅性と効率性を満たすテストケースを生成可能にする状態写像関数の、リーズナブルな決定手段が無かった。
【００１０】
本願発明は、所望の網羅性と効率性を満たすテストケースを生成可能にする状態写像関数を決定するテストケース生成装置およびテストケース生成方法を提供する。
【課題を解決するための手段】
【００１１】
本発明の一態様としてのテストケース生成装置は、
複数の内部変数の値の組によって表される前記システムの状態と、前記システムに対して発生する外部イベントに応じた状態変化を表す第１遷移とを含む状態遷移系を記憶する第１の記憶手段と、
前記システムに対して発生し得る外部イベント毎に、前記外部イベントが発生する前の前記システムの状態を定義した事前条件と、前記外部イベントの発生後の前記システムの状態を定義した事後条件とを記述した要求項目を記憶する第２の記憶手段と、
前記第２の記憶手段からｍ個（ｍは１以上の整数）の要求項目を選択し、前記ｍ個の要求項目から前記事前条件と前記事後条件とを抽出する条件抽出手段と、
与えられた状態を、前記与えられた状態に対する前記条件抽出手段により抽出したすべての事前条件および事後条件の真偽の組へ写像する状態写像関数を生成する状態写像生成手段と、
前記状態遷移系に含まれる前記複数の状態のそれぞれを、前記状態写像関数によりそれぞれ写像して複数の写像値を取得し、取得された複数の写像値に基づき、同じ写像値をもつ状態群を同じグループに分類することにより前記複数の状態をグループ化して、複数のグループを生成するグループ化手段と、
前記複数のグループのうちの２つのグループを指定し、一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの少なくとも１つの第１遷移が前記状態遷移系に存在するときは、前記一方のグループから前記他方のグループへの第２の遷移を設定し、前記グループの指定と第２の遷移の設定とを繰り返し、これにより複数の前記グループ間の第２遷移を表す剰余状態遷移系を生成する剰余状態遷移系生成手段と、
前記剰余状態遷移系の所定のグループから開始して、前記剰余状態遷移系における前記第２遷移を順次辿ることによって、前記第２遷移のシーケンスである代表遷移パスを生成する代表遷移パス生成手段と、
前記第２遷移が追跡された順番で前記代表遷移パスの前記第２遷移を順次選択し、前記順次選択された第２遷移のそれぞれについて、前記選択された第２遷移の遷移元グループにおける状態のうちの１つと同じ遷移元状態を有し、かつ前記選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に特定された第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を特定し、前記順次選択された第２遷移に対して特定された各第１遷移のシーケンスと前記各第１遷移にそれぞれ対応する外部イベントとを含むテストケースを生成する、遷移パス変換手段と、
を含むテストケース生成手段と、
前記テストケースを出力する出力手段と、
を備えたことを特徴とする。
【００１２】
本発明の一態様としてのテストケース生成装置は、
複数の内部変数の値の組によって表される前記システムの状態と、前記システムに対して発生する外部イベントに応じた状態変化を表す第１遷移とを含む状態遷移系を記憶する第１の記憶手段と、
前記システムに対して発生し得る外部イベント毎に、前記外部イベントが発生する前の前記システムの状態を定義した事前条件と、前記外部イベントの発生後の前記システムの状態を定義した事後条件とを記述した要求項目を記憶し、前記事前条件および前記事後条件は、それぞれ１つの内部変数の条件を定めた１つ以上の原子述語の論理演算により形成されている、第２の記憶手段と、
前記第２の記憶手段からｍ個（ｍは１以上の整数）の要求項目を選択し、前記ｍ個の要求項目における前記事前条件と前記事後条件に含まれるすべての原子述語を抽出する原子述語抽出手段と、
各抽出された原子述語のうちｈ個（ｈは１以上の整数）の原子述語を選択し、与えられた状態を、前記与えられた状態に対する前記ｈ個の原子述語の真偽の組へ写像する状態写像関数を生成する状態写像生成手段と、
前記状態遷移系に含まれる前記複数の状態のそれぞれを、前記状態写像関数によりそれぞれ写像して複数の写像値を取得し、取得された複数の写像値に基づき、同じ写像値をもつ状態群を同じグループに分類することにより前記複数の状態をグループ化して、複数のグループを生成するグループ化手段と、
前記複数のグループのうちの２つのグループを指定し、一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの少なくとも１つの第１遷移が前記状態遷移系に存在するときは、前記一方のグループから前記他方のグループへの第２の遷移を設定し、前記グループの指定と第２の遷移の設定とを繰り返し、これにより複数の前記グループ間の第２遷移を表す剰余状態遷移系を生成する剰余状態遷移系生成手段と、
前記剰余状態遷移系の所定のグループから開始して、前記剰余状態遷移系における前記第２遷移を順次辿ることによって、前記第２遷移のシーケンスである代表遷移パスを生成する代表遷移パス生成手段と、
前記第２遷移が追跡された順番で前記代表遷移パスの前記第２遷移を順次選択し、前記順次選択された第２遷移のそれぞれについて、前記選択された第２遷移の遷移元グループにおける状態のうちの１つと同じ遷移元状態を有し、かつ前記選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に特定された第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を前記状態遷移系において特定し、前記順次選択された第２遷移に対して特定された各第１遷移のシーケンスを含むテストケースを生成する遷移パス変換手段と、
を含むテストケース生成手段と、
前記ｍ個の要求項目のそれぞれについて前記テストケースにおいて遷移元状態が前記事前条件を満たし遷移先状態が前記事後条件を満たす第１遷移が網羅されているか否かを評価し、前記ｍ個の要求項目のうち前記テストケースにより網羅されている要求項目の割合または個数を示す網羅度を計算する網羅性評価手段と、
前記網羅度が閾値を満たすときの前記テストケースを出力する出力手段と、を備え、
前記状態写像生成手段は、前記閾値を満たす前記網羅度が得られるように前記各抽出された原子述語を取捨選択して前記状態写像関数を生成する
ことを特徴とする。
【００１３】
本発明の一態様としてのテストケース生成方法は、
読み出し手段が、複数の内部変数の値の組によって表される前記システムの状態と、前記システムに対して発生する外部イベントに応じた状態変化を表す第１遷移とを含む状態遷移系を記憶する第１の記憶手段から前記状態遷移系を読み出し、
条件抽出手段が、前記システムに対して発生し得る外部イベント毎に、前記外部イベントが発生する前の前記システムの状態を定義した事前条件と、前記外部イベントの発生後の前記システムの状態を定義した事後条件とを記述した要求項目を記憶する第２の記憶手段からｍ個（ｍは１以上の整数）の要求項目を選択し、前記ｍ個の要求項目から前記事前条件と前記事後条件とを抽出し、
状態写像生成手段が、与えられた状態を、前記与えられた状態に対する前記条件抽出手段により抽出したすべての事前条件および事後条件の真偽の組へ写像する状態写像関数を生成し、
グループ化手段が、前記状態遷移系に含まれる前記複数の状態のそれぞれを、前記状態写像関数によりそれぞれ写像して複数の写像値を取得し、取得された複数の写像値に基づき、同じ写像値をもつ状態群を同じグループに分類することにより前記複数の状態をグループ化して、複数のグループを生成し、
剰余状態遷移系生成手段が、前記複数のグループのうちの２つのグループを指定し、一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの少なくとも１つの第１遷移が前記状態遷移系に存在するときは、前記一方のグループから前記他方のグループへの第２の遷移を設定し、前記グループの指定と第２の遷移の設定とを繰り返し、これにより複数の前記グループ間の第２遷移を表す剰余状態遷移系を生成し、
代表遷移パス生成手段が、前記剰余状態遷移系の所定のグループから開始して、前記剰余状態遷移系における前記第２遷移を順次辿ることによって、前記第２遷移のシーケンスである代表遷移パスを生成し、
遷移パス変換手段が、前記第２遷移が追跡された順番で前記代表遷移パスの前記第２遷移を順次選択し、前記順次選択された第２遷移のそれぞれについて、前記選択された第２遷移の遷移元グループにおける状態のうちの１つと同じ遷移元状態を有し、かつ前記選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に特定された第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を前記状態遷移系において特定し、前記順次選択された第２遷移に対して特定された各第１遷移のシーケンスを含むテストケースを生成し、
出力手段が、前記テストケースを出力する、
ことを特徴とする。
【００１４】
本発明の一態様としてのテストケース生成方法は、
読み出し手段が、複数の内部変数の値の組によって表される前記システムの状態と、前記システムに対して発生する外部イベントに応じた状態変化を表す第１遷移とを含む状態遷移系を記憶する第１の記憶手段から前記状態遷移系を読み出し、
原子述語抽出手段が、前記システムに対して発生し得る外部イベント毎に、前記外部イベントが発生する前の前記システムの状態を定義した事前条件と、前記外部イベントの発生後の前記システムの状態を定義した事後条件とを記述した要求項目を記憶した、前記事前条件および前記事後条件は、それぞれ１つの内部変数の条件を定めた１つ以上の原子述語の論理演算により形成されている、第２の記憶手段からｍ個（ｍは１以上の整数）の要求項目を選択し、前記ｍ個の要求項目における前記事前条件と前記事後条件に含まれるすべての原子述語を抽出し、
状態写像生成手段が、各抽出された原子述語のうちｈ個（ｈは１以上の整数）の原子述語を選択し、与えられた状態を、前記与えられた状態に対する前記ｈ個の原子述語の真偽の組へ写像する状態写像関数を生成し、
グループ化手段が、前記状態遷移系に含まれる前記複数の状態のそれぞれを、前記状態写像関数によりそれぞれ写像して複数の写像値を取得し、取得された複数の写像値に基づき、同じ写像値をもつ状態群を同じグループに分類することにより前記複数の状態をグループ化して、複数のグループを生成し、
剰余状態遷移系生成手段が、前記複数のグループのうちの２つのグループを指定し、一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの少なくとも１つの第１遷移が前記状態遷移系に存在するときは、前記一方のグループから前記他方のグループへの第２の遷移を設定し、前記グループの指定と第２の遷移の設定とを繰り返し、これにより複数の前記グループ間の第２遷移を表す剰余状態遷移系を生成し、
代表遷移パス生成手段が、前記剰余状態遷移系の所定のグループから開始して、前記剰余状態遷移系における前記第２遷移を順次辿ることによって、前記第２遷移のシーケンスである代表遷移パスを生成し、
遷移パス変換手段が、前記第２遷移が追跡された順番で前記代表遷移パスの前記第２遷移を順次選択し、前記順次選択された第２遷移のそれぞれについて、前記選択された第２遷移の遷移元グループにおける状態のうちの１つと同じ遷移元状態を有し、かつ前記選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に特定された第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を前記状態遷移系において特定し、前記順次選択された第２遷移に対して特定された各第１遷移のシーケンスを含むテストケースを生成し、
網羅性評価手段が、前記ｍ個の要求項目のそれぞれについて前記テストケースにおいて遷移元状態が前記事前条件を満たし遷移先状態が前記事後条件を満たす第１遷移が網羅されているか否かを評価し、前記ｍ個の要求項目のうち前記テストケースにより網羅されている要求項目の割合または個数を示す網羅度を計算し、
出力手段が、前記網羅度が閾値を満たすときの前記テストケースを出力し、
前記状態写像生成手段は、前記閾値を満たす前記網羅度が得られるように前記各抽出された原子述語を取捨選択して前記状態写像関数を生成する
ことを特徴とする。
【発明の効果】
【００１５】
本発明により、求める網羅性と効率性を満たすテストケースを、より確実且つ効率的に生成可能になり、結果的に、システム開発の信頼性向上と手戻り工数削減への寄与が期待される。
【図面の簡単な説明】
【００１６】
【図１】本発明の一実施形態としてのテストケース生成装置のブロック図。
【図２】図１のテストケース生成装置が備えるテストケース生成手段のブロック図。
【図３】状態遷移系の縮約1: 状態写像。
【図４】状態遷移系の縮約2: 縮約結果。
【図５】要求項目表の一例を示す図。
【図６】原子述語表の一例を示す図。
【図７】状態遷移系の一例を示す図。
【図８】単純化した状態遷移系の一例を示す図。
【図９】図８の状態遷移系から得られたテストケースを示す図。
【図１０】図８を縮約した状態遷移系を示す図。
【図１１】図１０の状態遷移系から得られたテストケースを示す図。
【図１２】形式的な要求項目表の一例を示す図。
【図１３】形式的な原子述語表の一例を示す図。
【図１４】状態表の一例を示す図。
【図１５】状態遷移表の一例を示す図。
【図１６】テストケースの一例を示す図。
【図１７】実施例１の全体の処理の流れを示すフローチャート。
【図１８】実施例１に係る縮約された状態遷移系（Ｓｔｅｐ３）を示す図。
【図１９】実施例２の全体の処理の流れを示すフローチャート。
【図２０】実施例２（Ｓｔｅｐ６）に係る縮約された状態遷移系。
【図２１】実施例２（Ｓｔｅｐ６）に係るテストケースを示す図。
【図２２】実施例２（Ｓｔｅｐ１１）に係る縮約された状態遷移系を示す図。
【図２３】実施例２（Ｓｔｅｐ１１）に係るテストケースを示す図。
【図２４】実施例３の全体の処理の流れを示すフローチャート。
【図２５】タスク制御モニタを説明する図。
【図２６】状態遷移系を示す図。
【図２７】剰余状態遷移系を示す図。
【図２８】状態同値関係定義手順を説明するフローチャート。
【図２９】剰余状態遷移系生成手順を説明するフローチャート。
【図３０】遷移パス変換手順を説明するフローチャート。
【図３１】図２６の状態遷移系に対応する状態表を表１として示す図。
【図３２】図２６の状態遷移系に対応する遷移表を表２として示す図。
【図３３】図２６の状態遷移系における遷移パスを表３として示す図。
【図３４】図２６の表１を同値分割した結果を表４（剰余状態遷移系に対応する状態表）として示す図。
【図３５】剰余状態遷移系に対応する遷移表を表５として示す図。
【図３６】図３５の遷移表を同値分割した結果を表６として示す図。
【図３７】剰余状態遷移系の代表遷移パスを表７として示す図。
【図３８】代表遷移パスを元に復元した、図２６の状態遷移上の遷移パスを表８として示す図。
【発明を実施するための形態】
【００１７】
図１は、本発明の一実施の形態としてのテストケース生成装置の構成を示すブロック図である。
【００１８】
＜テスト生成装置の入力＞
図１のテストケース生成装置は、検査対象のシステムの仕様の入力を受け付ける。仕様は要求項目表（要求項目データ）２０ａ、原子述語表２０ｂ、および状態遷移系２１を含む。テストケース生成装置は、入力された状態遷移系２１を記憶する第１の記憶手段と、入力された要求項目表２０ａおよび原子述語表２０ｂを記憶する第２の記憶手段と、各第１および第２の記憶手段からデータを読み出す読み出し手段を含む。
【００１９】
状態遷移系：
上記検査対象のシステムは、外部イベントの発生と共に内部処理が行われ、刻々と内部状態が変化する。状態遷移系は、検査対象のシステムがとり得る状態と、当該システムに対して発生する外部イベントに応じたシステムの状態変化を表す状態遷移（第１遷移）から構成される体系である（後述する図７参照）。システムの状態は、複数の内部変数の値の組により表される。
【００２０】
要求項目表：
外部イベント（簡単のため単にイベントと称することもある）に対して、イベント発生を受入れる為の内部状態に関する条件と、内部処理後の内部状態の変化に関する条件が規定されている。前者の条件は事前条件と呼ばれ、後者の条件は事後条件と呼ばれる。すなわち事前条件はイベント発生前にシステムに要求される状態の条件であり、事後条件はイベント発生後にシステムに要求される状態の条件である。事前条件および事後条件は状態述語として記述される。これらイベントと、事前条件と、事後条件との組は、要求項目と呼ぶ。要求項目はイベント毎に規定されている。これらを表形式にしたものが要求項目表である（後述する図５参照）。要求項目が、設計者が上記システムに要求する振舞いの条件であり、転じてシステム開発後に検証すべき事項になる。
【００２１】
原子述語表：
要求項目表における事前条件及び事後条件の状態述語を構成する原子述語の表である（後述する図６参照）。原子述語は１つの内部変数の値に関する条件を記述したものである。
【００２２】
＜テストケース生成装置の出力＞
テストケース：
図１のテストケース生成装置は、検査対象のシステムのテストケース２６を出力する。テストケース２６は、検査対象のシステムをテストする為の操作手順（イベントのシーケンス）と、その操作手順で検査対象のシステムをテストした結果の期待値（状態遷移のシーケンス）とを含むリストである。テストケース生成装置は、テストケース２６を出力する出力手段を含む。
【００２３】
＜題材説明: クルーズコントローラ＞
図１のテストケース生成装置の詳細を説明するに先立ち、本明細書で扱う題材を説明する。
【００２４】
本明細書では、クルーズコントローラ（あるいはクルーズコントロールシステム）を単純化したものを検査対象のシステムとし、これを題材にして、本発明の内容を説明する。クルーズコントロールシステムは、アクセルペダルを踏まなくても自動的に一定車速を保持する車両制御システムの一種である。
【００２５】
内部変数：
クルーズコントローラは、3つの内部変数
・  車速(変数名“vel”)
・  クルーズランプの点灯状態(変数名“cruise”)
・  セットランプの点灯状態(変数名“set”)
を持つ。
【００２６】
外部イベント：
クルーズコントローラは、4種類の外部イベントを受け付ける。外部イベントの発生と共に内部処理が行われ、刻々と内部変数の値が変化する。これによりクルーズコントローラの内部状態も変化する。
・  アクセル(イベント名”Accel”)
・  ブレーキ(イベント名”Brake”)
・  クルーズスイッチ(イベント名”Cruise”)
・  セットスイッチ(イベント名”Set”)
【００２７】
要求項目表と原子述語表：
図5はクルーズコントローラの要求項目表、図6はクルーズコントローラの原子述語表を示す。例えば、要求項目1はイベント「クルーズスイッチをONにする」のイベント処理に関する要求であり、事前条件が「P1 ∧ ¬P2∧ ¬P3」即ち「車速が40km/h以上で、クルーズランプとセットラップが共に消えている」であり、事後条件は「P2」即ち「クルーズランプが点灯している」である。クルーズコントローラは、内部状態がこの事前条件を満たすときに、このイベントを受入れ、イベント処理後にはこの事後条件を必ず満たす。
【００２８】
状態遷移系：
図7はクルーズコントローラの状態遷移系(状態数10、状態遷移数22)を示す。例えば状態4（すなわちs(4)）は、内部変数vel(車速)が40、cruise(クルーズランプ)がOFF、set(セットランプ)がOFFである状態である。状態遷移9は外部イベント「クルーズスイッチON」による内部処理に対応する遷移であり、状態4においてこの外部イベントが発生すると状態遷移9により状態5に至る。
【００２９】
＜簡単な具体例＞
状態写像関数の構成法例と、状態写像関数によるテストケース規模削減とについて、上記のクルーズコントローラを更に単純化した例で説明する。ここでは要求項目を図５の要求項目1だけに限定し（要求項目数ｍ＝１）、状態遷移系も図8のように単純化する。
【００３０】
図8の状態遷移系において、要求項目1の事前条件を満たす状態は、状態4・状態6の2つの状態である。要求項目1のテストとなる状態遷移は、これらの状態からイベント「クルーズスイッチON」に伴う状態遷移8と10である。いずれの状態遷移も状態5か状態7に至り、これらは共に要求項目1の事後条件を満たす。これら以外は、要求項目1のテストに無関係な状態遷移である。
【００３１】
この状態遷移系から、全ての状態遷移を少なくとも一度は網羅するようにテストケースを生成する。図9が、生成されたテストケース(16遷移)である。生成されたテストケースは上記の2つの状態遷移を含み、上記要求項目をすべて（本例では１つ）網羅する。しかし、このテストケースは、同じ事前条件および同じ事後条件をもつ状態遷移を２つ(状態遷移8、10)を含み、また、要求項目のテストに無関係な14つの状態遷移も含む。従って、生成されたテストケースは効率面で改善の余地がある。
【００３２】
そこで、本実施形態では、網羅性基準（要求項目のうち網羅すべき要求項目の割合または個数を定めた基準）を満たす効率的なテストケースを得るために、事前条件と事後条件の充足性（真偽）の組合せを出力する関数を、状態写像関数として構成する。例えば状態4は事前条件を満たし事後条件を満たさないので、状態4を状態写像関数により写像した結果（写像値）は、(OK, NG)である(左が事前条件の充足性（真偽）、右が事後条件の充足性（真偽）に対応する)。OKは真、NGは偽に対応する。一方、状態5は事後条件を満たし事前条件を満たさないので、状態5を状態写像関数により写像した結果（写像値）は、(NG, OK)である。
【００３３】
図10は、上記状態写像関数により図8の状態遷移系を縮約した結果を示す。先ほどの状態写像による同一視を、具体例で見てみる。例えば、状態6は、状態4と同様に、状態写像関数の出力結果は(OK, NG)であり、状態4と状態6は同一視される。一方、状態4と状態5は、状態写像の結果が異なるので、同一視されない。この同一視により、事前条件と事後条件の両方の充足性毎に一つの抽象状態に縮約される。例えば、事前条件を満たし、事後条件を満たさない状態は状態4と状態6であるが、これらはともに状態写像で(OK, NG)として一つの抽象状態に縮約され、同一視される。同様に、事前条件を満たさず、事後条件を満たす状態は状態5と状態7であるが、これらはともに状態写像で(NG, OK)として一つの抽象状態に縮約され、同一視される。また、事前条件および事後条件の両方とも満たさない状態0、1、2、3は、いずれも状態写像で(NG, NG)として一つの抽象状態に縮約され、同一視される。このような状態縮約により、上記テストに対応する状態遷移8、10も一つの遷移にまとめられる。
【００３４】
この縮約された状態遷移系から、従来通り全ての状態遷移を少なくとも一度は網羅するようにテストケースを生成する。図11が、生成されたテストケース(7遷移)を示す。状態縮約により、上記テストに対応する状態遷移8、10が一つにまとめられているので、結果的に網羅性基準を満たす範囲でテストケースの規模を縮小した、効率的なテストケースを生成できる。
【００３５】
以上が、予め定めた網羅性基準に対して、網羅性基準を満たしつつ効率的なテストケースを生成する為の状態写像関数の構成例と、テストケースサイズ削減効果の説明である。
【００３６】
＜状態写像関数の構成法＞
前節では要求項目を一つに限定して、状態写像関数の構成方法の具体例を挙げた。この方法は、複数の要求項目を網羅する一般の場合に拡張可能である。複数の要求項目を網羅する効率的なテストケースを生成する為には、全要求項目の事前条件と事後条件の充足性（真偽）の組合せを出力する状態写像関数を構成すれば十分である。これを“構成法1”（後述する実施例1に対応）と呼ぶ事にする。
【００３７】
例えば要求項目が二つの場合、状態写像は「(要求項目1の事前条件の充足性、要求項目1の事後条件の充足性、要求項目2の事前条件の充足性、要求項目2の事前条件の充足性)」となる。この状態写像で縮約された状態遷移系は、状態写像での値が(OK, *, *, *)である八つの抽象状態を含み、同時に状態写像での値が(*, *, OK, *)である八つの抽象状態も含む。「*」は、OK（真）とNG（偽）の両方を意味する。前者(OK, *, *, *)は要求項目1の事前条件を満たす状態からなり、後者(*, *, OK, *)は要求項目2の事前条件を満たす状態からなる。
【００３８】
従って、この縮約された状態遷移系から生成されたテストケースは、二つの要求項目に関して網羅性基準（ここではすべての要求項目を網羅することを定めているとする）を満たす。一方で、状態遷移系を縮約しているので、状態縮約しない場合に比べてテストケースサイズを削減する事が出来る。
【００３９】
しかしながら、構成法1は要求項目数の増大と共に、テストケースサイズが爆発する可能性がある。何故ならば、状態写像関数を構成する事前条件と事後条件が増加するに従い、縮約された状態遷移系の状態数が指数関数的に増大するからである。前節で例に挙げたとおり、一つの要求項目の事前条件と事後条件から状態写像関数を構成した場合、縮約された状態遷移系は多くとも4状態である。しかし、要求項目を二つにした場合、縮約された状態遷移系は最大16状態になる。
【００４０】
そこで、効率改善の為に、別の構成法(“構成法2”（後述する実施例2に対応）)も考えられる。この構成法では、最初に各要求項目に含まれる原子述語をすべて抽出し、各原子述語の出現頻度を計算し、最も頻出する原子述語のみから状態写像関数を構成する。この状態写像関数で状態遷移系を縮約し、テストケースの生成と評価を行う。もし、網羅性基準を満たさない場合、次に出現頻度が高い原子述語を状態写像関数へ追加し、テストケース生成と評価とを、再度行う。これを、求める網羅性基準を満たすまで繰り返し行う。これはいささか発見的な方法であるが、原子述語を追加するに従いテストケースの網羅度（テストケースにより網羅される要求項目の割合または個数）が少なくとも単調増加することにより、最終的に網羅性基準を満たす事が出来る。状態写像関数に原子述語を追加すると、テストケースの網羅度が単調増加するのは、原子述語を追加すると抽象状態がより詳細化されるからである。すなわち、縮約されて一つにまとめられていた状態遷移が、細分化されることで、より詳細なテストケースが得られる。故に、テストケースの網羅度は少なくとも単調増加になる。
【００４１】
更に、構成法2の考えを逆にした構成法3（後述する実施例3に対応）も考えられる。最初に各要求項目に出現するすべての原子述語から状態写像関数を構成する。この状態写像関数で状態遷移系を縮約し、テストケースの生成と評価を行う。もし、網羅性基準を満たす場合、最も出現頻度が低い原子述語を状態写像関数から除去し、テストケース生成と評価とを、求める網羅性基準が維持されている間繰り返す。これによっても最終的に網羅性基準を満たす、高い効率性を有するテストケースを生成できる。
【実施例１】
【００４２】
実施例1に関わる装置構成は、図１の内側の破線で囲まれた部分に相当する。外側の破線で囲まれた装置全体は、後述する実施例2および実施例3に関わる構成である。内側の破線で囲まれた部分の構成は、状態述語抽出手段（条件抽出手段）１と、直積手段２と、テストケース生成手段３と、状態遷移系２１を記憶する第１の記憶手段と、要求項目表２０ａおよび原子述語表２０ｂを記憶する第２の記憶手段と、テストケース２６を出力する出力手段と、を備える。以下実施例1について詳細に説明する。
【００４３】
1. 装置概要
検査対象のシステムがとり得る状態と状態遷移から構成される状態遷移系が予め用意され、また、該システムに対する外部イベントと期待される事前条件と事後条件との組合せとして形式的に表現されたシステムに対する幾つかの要求項目が準備されていることを前提とする。
【００４４】
上記幾つかの要求項目のうち、選択された要求項目の事前条件及び事後条件に記述される状態述語を直積することにより状態写像関数を構成する。
【００４５】
更に後述する実施例4の手法（本件出願人により２００８年４月２８日に出願された特願2008-117173号で提案されたテストケース生成装置および生成方法）を用いて、上記状態写像関数により上記状態遷移系２１を縮約し、縮約された状態遷移系（剰余状態遷移系）の全状態遷移を網羅するようにテストケース２６を生成する。
【００４６】
2. 装置の入出力
本装置の入力は、検査対象のシステムの仕様である。仕様は、要求項目表２０ａ、原子述語表２０ｂ、状態遷移系２１からなる。装置の出力は、テストケース２６である。
【００４７】
要求項目表と原子述語表：
要求項目表２０ａの各要求項目は図12のように、原子述語表２０ｂの各原子述語は図13のように、計算機が解釈可能に形式化されて記述される。これらは、プログラミング言語Scheme(非特許文献2)の関数として表現される。即ち、この関数は、状態を入力し、述語の充足性（真偽）を出力する関数である。なお図12の要求項目は図5と同一内容であり、図13の原子述語も図6と同一内容である。
【００４８】
状態遷移系：
状態遷移系２１は、図14に示す状態表と、図15に示す状態遷移表で表現される。初期状態は状態0である。状態表(図14)は各状態の識別子（SID:State ID）と内容（ステート）とを示している。状態遷移表(図15)は各遷移の識別子（TID:Transition ID）と遷移元の状態識別子（SID0）と遷移先の状態識別子（SID1）と遷移の内容（外部イベント）とを示している。
【００４９】
例えば、状態表の状態(SID)4は、内部変数vel(車速)が40、cruise(クルーズランプ)がOFF、set(セットランプ)がOFFである事を意味する。また、状態遷移表の状態遷移(TID)9は、外部イベント「CruiseOn」による内部処理に対応する遷移であり、状態4から状態5に至る。
【００５０】
テストケース：
図16は本装置が出力したテストケースの例である。テストケースは、初期状態から始まる15回の連続的な遷移により表される。
【００５１】
3. 処理の流れ
本装置による処理の流れを説明する。
【００５２】
3.1 装置全体
図17は本装置による全体の処理の流れを示すフローチャートである。
・  処理1: 状態述語抽出
＞  処理:要求項目表２０ａの事前条件及び事後条件として記述される状態述語を抽
出する。要求項目表２０ａのすべての要求項目を対象としてもよいし、選択した
幾つかの要求項目を対象としてもよい。たとえば図12の場合、２個の要求項目が
存在するため、１つの要求項目（ｍ＝１）または２つの要求項目（ｍ＝２）を対
象とすればよい。
＞  入力: 要求項目表２０ａ
＞  出力: 状態述語
＞  担当手段:「状態述語抽出手段１」
・  処理2:状態写像関数の構成
＞  処理: 抽出された形式的な状態述語（事前条件および事後条件）を直積して、状
態写像関数２２を構成する。
＞  入力: 状態述語（事前条件および事後条件）
＞  出力: 状態写像関数２２
＞  担当手段:「直積手段２」
・  処理3: テストケースの生成 (生成方法の詳細は後述する実施例4で説明する)
＞  処理: 状態写像関数２２により状態遷移系２１を縮約し、縮約された状態遷移系
（剰余状態遷移系）の全状態遷移を網羅するようなパスをテストケース２６とし
て生成する。
＞  入力: 状態遷移系２１、状態写像関数２２
＞  出力: テストケース２６
＞  担当手段:「テストケース生成手段３」
【００５３】
3.3 処理1
要求項目表２０ａの事前条件及び事後条件として記述される状態述語を抽出する。状態述語が原子述語でない場合は、状態述語定義の文字列を解析して、述語名を取得する。例えば、図12(要求項目表)の「(define (P1notP2notP3 s) (and (P1 s) (not (P2 s)) (not (P3 s))))」は状態述語の定義である。状態述語名は「P1notP2notP3」である。
【００５４】
3.3 処理2
処理1で抽出した状態述語から、各状態述語の充足性をリスト形式で出力する関数として、状態写像関数を構成する。
【００５５】
状態述語F1, F2,…,Fn(n個)を、処理1で抽出された状態述語とする。このとき、状態sに対して、リスト((F1 s), (F2 s), … , (Fn s))を出力する関数を、状態写像関数として定義する。この(F1 s)とは、状態sに述語F1を適用した結果、即ち述語F1の充足性（真偽）を表す。この状態写像関数は、「(define (stateFunc s) (list (F1 s) (F2 s) …(Fn s)))」と記述される。
【００５６】
4. 具体例
以下、「3. 処理の流れ」で説明した処理の具体例を示す。
Step1 (処理1: 状態述語抽出)
出力: 状態述語「P1notP2notP3」、「P2」、「P3」（ここではすべての要求項目表のすべての要求項目（ｍ＝２）を対象としている。）
Step2 (処理2: 状態写像関数を構成)
出力: 状態写像関数「(define (fun s) (list (P1notP2notP3 s) (P2 s) (P3 s)))」
Step3 (処理3: テストケース生成)
出力: テストケース(図16)
(中間データである、縮約された状態遷移系を図18に示す)
【実施例２】
【００５７】
実施例2に関わる装置構成は、図１の外側の破線で囲まれた部分（ただし要素７は除く）に相当する。本実施例2の構成は、実施例1の構成に対して要素４〜６、８を追加したものである。すなわち実施例2の構成は、状態述語抽出手段（条件抽出手段）１と、直積手段２と、テストケース生成手段３と、状態遷移系２１を記憶する第１の記憶手段と、要求項目表２０ａおよび原子述語表２０ｂを記憶する第２の記憶手段と、テストケース２６を出力する出力手段と、原子述語抽出手段４と、出現頻度分析手段５と、高頻度原子述語抽出手段６と、網羅性評価手段８とを備える。
【００５８】
1. 装置概要
実施例1をベースに、状態写像関数の構成方法を拡張する。
【００５９】
本実施例2における状態写像関数の構成方法では、各要求項目から抽出した状態述語の集合で最も頻出する原子述語から開始し、生成されるテストケースが、要求項目の網羅性基準を満たすまで、頻度の高い順に原子述語を追加(前記状態写像関数との直積)する操作を繰り返す。
【００６０】
2. 装置の入出力
実施例2の装置は、実施例1の装置の入出力と同じである。
【００６１】
3. 処理の流れ
本装置の処理の流れを説明する。図19が本装置の処理の流れを示すフローチャートである。実施例2は実施例1を拡張したものであり、実施例1との差分箇所はフローチャートの斜線ブロックとして示されている。以下、実施例1との差分を中心に説明する。
・  処理1a: 原子述語抽出
＞  処理: 状態述語表より原子述語を抽出する。
＞  入力: 状態述語表（状態述語抽出手段１で抽出された状態述語の集合）
＞  出力:原子述語リスト
＞  担当手段:「原子述語抽出手段４」
・  処理1b:原子述語の出現頻度分析
＞  処理: 処理1aで抽出された各原子述語に関して、状態述語集合全体における各原
子述語の出現頻度を分析する。
＞  入力: 原子述語リスト
＞  出力:原子述語の出現頻度順リスト
＞  担当手段:「出現頻度分析手段５」
・  処理1c:高頻度原子述語抽出 
＞  処理: 処理1bで得られた出現頻度順リストのトップ(最も頻出する原子述語)を取
り出す。
＞  入力:原子述語の出現頻度順リスト
＞  出力: (高頻度な)原子述語
＞  担当手段:「高頻度原子述語抽出手段６」
・  処理2’: 状態写像関数を構成
＞  処理: まだ状態写像関数が構成されていない場合、処理1cで取り出された原子述
語を状態写像関数とする。状態写像関数が既に構成されている場合は、既存の状
態写像関数に、処理1cで取り出された原子述語を直積して状態写像関数を構成す
る。直積は、実施例1と同様の方法で行う。
＞  入力: 原子述語、状態写像関数
＞  出力: 状態写像関数
＞  担当手段:「直積手段２」
・  処理4: 網羅性評価
＞  処理: 処理3で生成されたテストケースの、要求項目に対する網羅度（テストケ
ースにより網羅される要求項目の割合または個数）を評価する。具体的には、処
理1で選択された各要求項目に関して、要求項目の事前条件及び事後条件の状態
述語を形式化して得られた形式的状態述語を用いて、遷移元状態が事前条件を、
遷移先状態が事後条件を満たす状態遷移がテストケースに存在するかを検索す
る。存在する場合、その状態遷移が要求項目の検証に対応するテストケースの一
工程であるので、その要求項目は生成されたテストケースにより網羅されると評
価される。この処理を全要求項目に関して繰り返す事で、網羅性評価を行い、全
要求項目のうちテストケースにより網羅される要求項目の割合または個数である
網羅度を得る。
＞  入力:テストケース２６
＞  出力: テストケースの網羅度
＞  担当手段:「網羅性評価手段８」
【００６２】
4. 具体例
以下、「3. 処理の流れ」で説明した処理の具体例を示す。
Step1 (処理1:状態述語抽出)
出力: 状態述語「P1notP2notP3」、「P2」、「P3」
Step2 (処理1a:原子述語抽出)
出力: 原子述語リスト「P1, P2, P3」
Step3 (処理1b:原子述語の出現頻度分析)
出力: 原子述語の出現頻度順リスト「P2, P3, P1」(Step2で得られた原子述語リストに関して状態述語集合における各原子述語の出現頻度を計算し、各原子述語を出現頻度順に並べる。P2が最も頻出である。)
Step4 (処理1c:高頻度原子述語抽出)
出力: 原子述語「P2」(Step3で得られた出現頻度リストのトップ(最も頻出する原子述語)を取り出す。同時にStep3のリストから「P2」が削除される。)
Step5 (処理2’:状態写像関数を構成)
出力: 状態写像関数「P2」(現時点で状態写像関数が無いので、Step4の原子述語がそのまま状態写像関数となる。)
Step6 (処理3:テストケース生成)
出力: テストケース(図21)(テストケースサイズ7)
(中間データである、縮約された状態遷移系は図20(状態数2、状態遷移数4)に示される。)
Step7 (処理4:網羅性評価)
出力: 網羅度50%
※    要求項目1は状態遷移9で網羅されるが、要求項目2は網羅されない。
Step8 (条件分岐: 網羅性)
出力: No（上記網羅度は網羅性基準を満たさない。網羅性基準はここでは100%とする。）
Step9 (処理1c:高頻度原子述語抽出)
出力: 原子述語「P3」(原子述語の出現頻度順リストのトップ(次に最も頻出する原子述語)を取り出す。同時に原子述語の出現頻度順リストから「P3」が削除される。)
Step10 (処理2’:状態写像関数を構成)
出力: 状態写像関数「(define (stateFunc s) (list (P2 s) (P3 s)))」 (既に状態写像関数「P2」が存在するので、「P2」及び「P3」を直積する。)
Step11 (処理3:テストケース生成)
出力: テストケース(図23)(テストケースサイズ11)
(中間データである、縮約された状態遷移系は図22(状態数3、状態遷移数7)に示される。)
Step12 (処理7:網羅性評価)
出力: 網羅度100%
※    要求項目1は状態遷移9で、要求項目2は状態遷移12で網羅される。
Step13 (条件分岐: 網羅性)
出力: Yes 
Step14 (終了)
出力: Step12で得られたテストケース(網羅性基準を満たしたので処理を終了する。)
【実施例３】
【００６３】
実施例3に関わる装置構成は、図１の外側の破線で囲まれた部分（ただし要素６を除く）に相当する。本実施例3の構成は、実施例3の構成から要素６を除去して、要素７を追加したものである。すなわち実施例3の構成は、状態述語抽出手段（条件抽出手段）１と、直積手段２と、テストケース生成手段３と、状態遷移系２１を記憶する第１の記憶手段と、要求項目表２０ａおよび原子述語表２０ｂを記憶する第２の記憶手段と、テストケース２６を出力する出力手段と、原子述語抽出手段４と、出現頻度分析手段５と、低頻度原子述語抽出手段７と、網羅性評価手段８とを備える。実施例2で用いた要素と同じ名称の要素の動作は基本的に実施例2と同じであるが、直積手段２の処理が一部異なっている。
【００６４】
1. 装置概要
本実施例3における状態写像関数の構成方法では、要求項目の全原子述語を直積した状態写像関数から開始し(最大セット)、生成されるテストケースが要求項目を網羅している間、頻出頻度が低い原子述語を徐々に削除する操作を繰り返す。
【００６５】
すなわち、全原子述語を取捨選択して、網羅度が閾値を満たすように、選択したｈ（ｈは１以上の整数）個の原子述語を直積した状態写像関数を生成するという点において本実施例3と上述した実施例2とは共通するが、実施例2では出現頻度の高い順に原子述語を順次追加していくのに対し、本実施例では全原子述語から出現頻度の低い順に原子述語を削除していくという具体的な実現方法において実施例3と実施例2とは異なる。
【００６６】
2. 装置の入出力
実施例1の入出力と同様である。
【００６７】
3. 処理の流れ
本装置の処理の流れを説明する。図24が本装置の処理の流れを示すフローチャートである。実施例3は実施例2と大きく類似し、実施例2との差分箇所はフローチャートにおける斜線ブロックで示される。以下、実施例2との差分を中心に説明する。
・  処理1c:低頻度原子述語抽出 
＞  処理: 処理1bで得られた出現頻度リストから、最後尾(最も出現頻度が低い原子
述語)を削除する。
＞  入力:原子述語の出現頻度順リスト
＞  出力: 原子述語の出現頻度順リスト
＞  担当手段:「低頻度原子述語抽出手段７」
・  処理2’: 状態写像関数を構成
＞  処理:処理1aで出力された原子述語リスト（１回目の処理の場合）、または処理1
cで出力された出現頻度順リスト（２回目以降の処理の場合）を対象に、当該リ
スト内の原子述語を直積して状態写像関数を構成する。直積は、実施例1と同様
の方法で行う。
＞  入力: 原子述語リストまたは出現頻度順リスト
＞  出力: 状態写像関数
＞  担当手段:「直積手段２」
【００６８】
4. 具体例
「3. 処理の流れ」で説明した処理の具体例を示す。
Step1 (処理1:状態述語抽出)
出力: 状態述語「P1notP2notP3」、「P2」、「P3」
Step2 (処理1a:原子述語抽出)
出力: 原子述語リスト「P1, P2, P3」
Step3 (処理1b:原子述語の出現頻度分析)
出力: 原子述語の出現頻度順リスト「P2, P3, P1」((Step2で得られた原子述語リストに含まれる各原子述語について状態述語集合における出現頻度を計算し、各原子述語を出現頻度順に並べる。)
Step4 (処理2’:状態写像関数を構成)
出力: 状態写像関数「(define (fun s) (list (P1 s) (P2 s) (P3 s)))」
Step5 (処理3:テストケース生成)
出力: テストケース(図16)(テストケースサイズ15)
(中間データである、縮約された状態遷移系は図18(状態数4、状態遷移数10)に示される。)
Step6 (処理4:網羅性評価)
出力: 網羅性100%
※    要求項目1は状態遷移9で、要求項目2は状態遷移19、21で網羅される。
Step7 (条件分岐: 網羅性)
出力: Yes
Step8 (処理1c:低頻度原子述語抽出)
出力: 原子述語の出現頻度順リスト「P2, P3」(Step3で得られたリストの最後尾(最も出現頻度が低い原子述語)「P1」を削除する。)
Step9 (処理2’:状態写像を構成)
出力: 状態写像関数「(define (fun s) (list (P2 s) (P3 s)))」
Step10 (処理3:テストケース生成)
出力: テストケース(図23)(テストケースサイズ11)
(中間データである、縮約された状態遷移系は図22(状態数3、状態遷移数7)に示される。)
Step11 (処理4:網羅性評価)
出力: 網羅性100%
※    要求項目1は状態遷移9で、要求項目2は状態遷移12で網羅される。
Step12 (条件分岐: 網羅性)
出力: Yes
Step13 (処理1c:低頻度原子述語抽出)
出力: 原子述語の出現頻度順リスト「P2」(Step8で得られた出現頻度リストの最後尾(最も出現頻度が低い原子述語)「P3」を削除する。)
Step14 (処理2’:状態写像を構成)
出力: 状態写像関数「(define (fun s) (list (P2 s)))」
Step15 (処理3:テストケース生成)
出力: テストケース(図21)(テストケースサイズ7)
(中間データである、縮約された状態遷移系は図20(状態数2、状態遷移数4)に示される。)
Step16 (処理4:網羅性評価)
出力: 網羅性50%
※    要求項目1は状態遷移9で網羅されるが、要求項目2は網羅されない。
Step17 (条件分岐: 網羅性)
出力: No
Step18 (終了)
出力: Step10で得られたテストケース (処理を終了する。)
【００６９】
＜補足＞
上述した実施例3および実施例2の考えを実施例1に適用することも可能である。
【００７０】
実施例2の考えを適用する場合、各要求項目の状態述語（事前条件または事後条件）の出現頻度を計算し、最初に最も頻出する状態述語のみから状態写像関数を構成する。この状態写像関数で状態遷移系を縮約し、テストケースの生成と評価を行う。もし、網羅性基準を満たさない場合、次に出現頻度が高い状態述語（事前条件または事後条件）の状態写像関数への追加と、テストケース生成と評価とを、求める網羅性基準を満たすまで繰り返す。このように、状態写像関数を構成する状態述語（条件）を追加するに従いテストケースの網羅度が少なくとも単調増加して、最終的に網羅性基準を満たす事が出来る。
【００７１】
参考のため、状態写像関数に条件（原子述語）を追加すると、テストケースの網羅度が単調増加する理由にふれておく。それは、条件を追加すると抽象状態がより詳細化されるからである。例えば、要求項目1の事前条件と事後条件とのみで状態写像関数を構成した場合、抽象状態の一つとして(要求項目1の事前条件: OK, 要求項目1の事後条件: NG)がある。この状態写像関数に要求項目2の事前条件を追加したとする。すると、先ほどの抽象状態は(要求項目1の事前条件: OK, 要求項目1の事後条件: NG, 要求項目2の事前条件: OK)と(要求項目1の事前条件: OK, 要求項目1の事後条件: NG, 要求項目2の事前条件: NG)に詳細化される。これにより、縮約されて一つにまとめられていた状態遷移が、二つに細分化されることで、より詳細なテストケースが得られる。故に、テストケースの網羅度は少なくとも単調増加になる。
【００７２】
実施例3の考えを適用する場合、まず、各要求項目に出現するすべての状態述語（事前条件または事後条件）から状態写像関数を構成する。この状態写像関数で状態遷移系を縮約し、テストケースの生成と評価を行う。もし、網羅性基準を満たす場合、最も出現頻度が低い状態述語を状態写像関数から除去し、テストケース生成と評価とを行う。これを、求める網羅性基準が維持されなくなるまで繰り返す。これによっても最終的に網羅性基準を満たす、高い効率性を有するテストケースを生成できる。
【実施例４】
【００７３】
本実施例では図1のテストケース生成手段３の詳細を説明する。
【００７４】
図2は、図1のテストケース生成手段３の構成を示すブロック図である。
【００７５】
このテストケース生成手段３は、検査対象のシステムが取りうる複数の状態と状態間の遷移（第１遷移）とを表す状態遷移系２１と、状態の写像を定義した状態写像関数２２とを入力とし、上記検査対象のシステムのテストケース（遷移パス）２６を生成し、出力する。
【００７６】
このテストケースを用いることで、上記検査対象となるシステムが仕様を満たすかどうかを検証できる。より詳細には、実際に上記検査対象となるシステムにおいて上記テストケースの遷移（イベント）を発生させ、上記状態遷移系と同じ動作の発生を確認することによって、上記検査対象となるシステムが上記仕様を満たすかどうかを確認できる。
【００７７】
＜タスク制御モニタ＞
ここで複数のタスクが存在する情報システムで、タスクの実行状態を制御するモニタ機能を考える。図25に示すように、モニタ上の各タスクは、実行（RUN）状態と実行可能（RDY）状態とスリープ（WAI）状態の三つの状態を有する。
【００７８】
モニタは各タスクに、自発的なCPU譲り渡し（yield）操作と自発的なスリープ状態への遷移（sleep）操作とスリープ状態のタスクの実行可能状態への変更（wakeup）操作の三つのAPI（Application Programming Interface）関数を提供する。これらの関数は実行（RUN）状態のタスクにより呼び出される。
【００７９】
タスク数が三個の場合にタスク制御モニタがとり得る状態と状態間の遷移を表した状態遷移系を図26に示す。図26の状態遷移系は、図31に示す表1の状態と、図32に示す表2の遷移とで記述される有向グラフであり、初期状態は状態s0である。
【００８０】
より詳細に、表1は各状態の識別子（SID:State ID）と内容（ステート）を示しており、表2は各遷移の識別子（TID:Transition ID）と遷移元の状態識別子（SID0）と遷移先の状態識別子（SID1）と遷移の内容（イベント）を示している。ただし表1の写像結果は後述の状態同値関係定義部（グループ化手段）１１の処理で付加されるものであり、本装置への表1の入力時にはまだ存在しない。
【００８１】
＜テストケースの事例＞
この状態遷移系（図26、表1と表2）で記述されるタスク制御モニタの動作を確認するには、システムの初期状態から各タスクの遷移に対応するAPI関数を順番に呼び出して、遷移先の状態に対応したタスクの切り替えが起きることを確認すれば良い。たとえば、初期状態s0からタスク1が(sleep 1)を呼ぶとタスク2が実行中となり、次にタスク2が(sleep 2)を呼ぶとタスク2が実行中となり、次にタスク3が(yield 3)を呼ぶとタスク3が実行可能となり、という風な手順で動作を確認する。この確認手順は状態遷移系の上の状態s0から出発して状態s5へ至る遷移パスt0→t5→t18に対応する。
【００８２】
システムの動作確認を網羅的かつ最短の手順で実施するには、状態遷移系を有向グラフと見なすと、有向グラフの遷移を網羅する最短の遷移パスを計算して、最短の遷移列に対応する遷移に対応するイベントでシステムを動作させれば良い。
【００８３】
有向グラフの遷移を網羅する最短の遷移列の生成問題は中国人郵便配達夫問題（CPP: Chinese Postman Problem）としてグラフアルゴリズムの分野で公知であり、網羅を保証した遷移列を求める近似アルゴリズム（非特許文献１）が存在する。なお、この場合のアルゴリズムの近似性は、最小の遷移列に近い遷移列を生成するという意味である。
【００８４】
状態遷移系（図26：16状態、42遷移）の遷移を網羅する遷移列を近似アルゴリズム（非特許文献１）で求めた結果を図33の表3に記す。初期状態から始まるこれら4本の遷移列（遷移パス）に沿ってシステムを駆動すれば、50回の連続的な遷移で42個の遷移を網羅できる。このような遷移列をシステムのテストケースと呼ぶ。なお、この遷移列は必ず初期状態s0から開始するものとする。遷移列が1本でない理由は、状態s12が遷移先の存在しない状態であり、状態s12に入るとその後の遷移が続かなくなるからである。
【００８５】
＜テストケースのサイズの削減＞
ここでシステムの全ての遷移を網羅するテストは、一般にシステムの規模が大きくなるとテストケースのサイズが指数関数的に増大するため現実的でない。実行可能なテストとするため、一定のテスト基準を与えてテストケースのサイズを減らす必要が生ずる。たとえば、例題のタスク制御モニタは16の状態を有するが、これらの状態はタスク識別子の番号の並び替えにより一致する状態を含む。たとえば状態s0と状態s2はタスク識別子の順番を並び替えると一致するが、状態s0と状態s1はタスク識別子の順番を変えても一致しない状態であるなどの区別が考えられる。一定のテスト基準の例として「タスク識別子の番号を並び変えて一致する状態を等価な状態と見なし、等価でない状態間の遷移のみを動作確認する」などが考えられる。
【００８６】
このような一定のテスト基準を状態写像関数２２の形に表現して入力することで、指定したテスト基準を満たす効率的なテストケース（遷移パス）２６を自動的に生成する。
【００８７】
＜実施例1〜3の状態写像関数と、実施例4での状態写像関数との関係＞
実施例1〜3では、与えられた状態を、各状態述語あるいは各原子述語の充足性（真偽）の値の組へ写像する状態写像関数を示したが、本実施例4では説明の題材として、後述するようにRUN、RDY、WAIの各状態のタスク数へ写像する状態写像関数を用いることに注意されたい。このように状態写像関数の種類が異なっていてもテストケース生成手段の処理に本質的な違いはないため問題はない。
【００８８】
＜状態遷移系と剰余状態遷移系＞
ここで状態遷移系と剰余状態遷移系（縮約された状態遷移系）とについて説明する。
【００８９】
状態遷移系Fは、状態の有限集合S、遷移の有限集合T（⊆S×S）、初期状態s0の組み合わせにより定義する。剰余状態遷移系F/~は、状態遷移系Fと、Fの状態に関する同値関係”~”とを与えると定義できる。剰余状態遷移系F/~の状態は、状態遷移系Fの状態を同値関係”~”により同値分割（グループ化）した際の同値クラス（グループ）とする。剰余状態遷移系F/~の遷移は、状態sと状態s'の間に遷移が存在する場合に各状態を含む同値クラスの間にも遷移([s],[s'])が存在するとして同値クラスの間の遷移関係を定める。
状態遷移系：F = ＜S, T, s0＞
状態集合：S
遷移集合：T ⊆ S×S
初期状態：s0 ∈ S
剰余状態遷移系：F/~ = ＜S/~,T/~,[s0]＞
剰余状態：S/~ = { [s] | s ∈ S }
剰余遷移：T/~ = { ([s],[s’]) | (s,s’) ∈ T }
【００９０】
関係”〜”は上記の同値関係equivを意味し、同値クラス[s]は状態sを代表元とし同値関係の上で等価な状態を集めた集合とする。
同値クラス： [s] = { s’ ∈ S | equiv(s,s’) = true  }
【００９１】
なお、状態遷移系の各遷移t=(s,s’)∈Tにつき遷移tの前後の状態を参照する関数src(t)=sおよびdst(t)=s’と表記して以下で用いる。
遷移元の状態： dst: T → S
遷移先の状態： src: T → S
【００９２】
＜状態同値関係の定義＞
状態遷移系から剰余遷移系を計算するには状態間の同値関係を定義する必要がある。状態間の同値関係equiv(s,s’)は、同値関係の定義として反射律、対称律、推移律を満たす必要がある。なおＢは真または偽を表すブルーム値（真偽値）の集合を表す。s,s’が同値のとき、equiv(s,s)は真を返す。
同値関係 equiv: S×S → B
反射律：∀s∈S. equiv(s,s)
対称律：∀s∈S.∀s’∈S. equiv(s,s’) ⇒ equiv(s’,s)
推移律：∀s∈S.∀s’∈S. equiv(s,s’)∧equiv(s’,s’’) ⇒ equiv(s,s’’)
【００９３】
＜状態同値関係の構成＞
状態同値関係を構成するために、状態を抽象化する状態写像（写像map）関数２２を用意し、これをテストケース生成手段３に入力する。状態同値関係定義部（グループ化手段）１１は、状態写像関数２２と状態遷移系２１とから、剰余遷移系２４の生成に利用される状態同値関係２３（後述する図34の表4）を定義する。なお、関数equal?は写像mapの値域V上の等号関係とする。
状態写像 map: S → V
同値関係 equiv(s,s’) = equal?(map(s), map(s’))
【００９４】
図28は、状態間の同値関係を定義する手順を示すフローチャートである。この手順に従った処理は状態同値関係定義部（グループ化手段）１１により行われる。状態遷移系２１から２つの状態s1,s2を取り出し、これらを状態写像関数２２に与えてそれぞれ写像値を計算し（Ａ１１）、写像値が一致すれば（Ａ１２のＹＥＳ）s1,s2は同値であると判断し（Ａ１３）、一致しなければ（Ａ１２のＮＯ）s1,s2は同値でないと判断する（Ａ１４）。このように、状態同値関係定義部１１は、状態遷移系に含まれる各状態のそれぞれを状態写像関数２２で写像してそれぞれ写像値を取得し、取得した写像値に基づき、同じ写像値をもつ状態を１つのグループに分類することにより、各状態を複数のグループへグルーピングする。
【００９５】
例題：タスク制御モニタ
テスト基準から決まるタスク識別子の入れ替えで一致する状態を同一視する状態写像の事例を以下に示す。なお、この写像例は公知のプログラミング言語Scheme（非特許文献２）の書式で記述している。
写像例：
(define (len s) 
(map (lambda (v) (length (getval s v))) '(RUN RDY WAI)))
作用例：
s = ((RUN (1)) (RDY (2 3)) (WAI ())) のとき (len s) => (1 2 0)
s = ((RUN ()) (RDY ()) (WAI (1 2 3))) のとき (len s) => (0 0 3)
【００９６】
上記では、図31の表1の状態の内容（ステート）がプログラミング言語Scheme（非特許文献２）のリスト形式で変数sに格納されるとして、各タスクの状態を管理する変数（RUN、RDY、WAI）のリストの長さを返す関数を用いている。なお、関数getvalは変数の名前から対応する値を取得する関数とする。この関数を各状態へ適用した結果を図31の表1の一番右側の列（写像結果あるいは写像値）に示す。この写像による値が一致する状態を同値と見なして同値クラス（グループ）へ分割した結果を図34の表4に示す。同値クラスを代表する状態を状態識別子が最小の状態とすると、同値クラスの代表状態[SID]はs0、s1、s5、s12の4種類となる。
【００９７】
剰余状態遷移系の状態は、状態の同値クラス（以下、状態クラス）となり、剰余状態遷移系の遷移は状態クラス間の遷移となり、２つの状態クラスにそれぞれ含まれる状態間に状態遷移系２１において遷移関係が存在するとき、当該状態クラス間に遷移関係が存在するとする。
【００９８】
この剰余状態遷移系の生成アルゴリズムを以下に記す。またこのアルゴリズムに対応する処理の流れを図29のフローチャートに示す。このアルゴリズムは、剰余状態遷移系生成部１２により実行される。剰余状態遷移系生成部１２は、状態同値関係23（図34の表4）と、状態遷移系２１とを入力とし、下記のアルゴリズムに従い、剰余状態遷移系２４を生成する。
【００９９】
＜剰余状態遷移系の生成アルゴリズム＞
下記のアルゴリズムの記述において記号φは空集合の意味とし、記号←は右辺の左辺への代入を意味する。KEYSは写像の値域を取得する手順を意味し、“P(X)”はXのすべてのサブセットの集合（the set of all subsets of X）である、Xの累乗集合（power set）を意味する。
入力：状態遷移系F、同値関係equiv
出力：剰余状態遷移系F/~
変数：
SMAP: S → P(S)
TMAP: S×S → P(T)
REPL: S → S
ステップ１：状態の同値分割（図29のフローチャートの符号Ｂ１１）
事前：SMAPが空
事後：SMAPが状態の同値分割結果
SMAP ← φ
for each s ∈ S do
if ∃s' ∈ KEYS(SMAP). equiv(s,s') then
SMAP(s') ← SMAP(s')∪{s}
else
SMAP(s) ← {s}
end if
end do
ステップ２：代表状態の決定（図29のフローチャートの符号Ｂ１２）
事前：SMAPが状態の同値分割
事後：REPLが代表状態の検索表
REPL ← φ
for each s ∈KEYS(SMAP) do
for each s' ∈ SMAP(s) do
REPL(s') ← s
end do
end do
ステップ３：遷移の同値分割（図29のフローチャートの符号Ｂ１３）
事前：TMAPが空、REPLが代表状態の対応表
事後：TMAPが遷移の同値分割結果
for each t ∈ T do
key ← (REPL(src(t)),REPL(dst(t)))
if ∃t' ∈ KEYS(TMAP). key=t' do
TMAP(t') ← TMAP(t')∪{t}
else
TMAP(key) ← {t}
end if
end do
ステップ４：結果出力（図29のフローチャートの符号Ｂ１４）
状態分割SMAPからS/~、遷移分割TMAPからT/~を決め、
剰余遷移系F/~=＜S/~, T/~, [s0]＞を出力して停止
【０１００】
例題：タスク制御モニタ
状態同値関係定義部１１において状態の同値クラスへの分割が済めば各状態SIDに対して代表状態[SID]が定まる（図34の表4の一番左の列）。剰余遷移系の状態となる状態クラスは代表状態の識別子でラベルする。
【０１０１】
また剰余遷移系の遷移は、遷移表（図35の表5）に示すように各遷移の遷移元と遷移先の状態（SID0とSID1）の所属する状態クラスの代表状態（[SID0]と[SID1]）を求めて、代表状態の組が同じ遷移を同値クラスに分割する（図36の表6）。識別子TIDが最小の遷移を代表遷移[TID]として遷移クラスの識別に用いる。この例は遷移クラスがt0、t1、t4、t5、t6、t15、t17、t18の8個となる。
【０１０２】
図27は、得られた剰余状態遷移系（4状態、8遷移）２４を示す。これは図36の表6に相当するものである。この状態遷移系の状態および遷移は、元の状態遷移系の状態および遷移を含む。状態ステートや遷移イベントとしては、代表状態のステートや代表遷移のイベントを記している。
【０１０３】
図29のステップ1（Ｂ１１）終了時点のSMAPは以下の通りとなる。
SMAP(s0) = {s0,s2,s4,s10,s14,s15}
SMAP(s1) = {s1,s3,s6,s7,s9,s13}
SMAP(s5) = {s5,s8,s11}
SMAP(s12) = {s12}
【０１０４】
図29のステップ2（Ｂ１２）終了時点のREPLは以下の通りとなる。
REPL(s0) = s0
REPL(s1) = s1
REPL(s2) = s0
... 中略
REPL(s14) = s0
REPL(s15) = s0
【０１０５】
図29のステップ3（Ｂ１３）終了時点のTMAPは以下の通りとなる。
TMAP((s0,s0)) = {t1,t3,t8,t34,t39,t41}
TMAP((s0,s1)) = {t0,t2,t7,t33,t38,t40}
... 中略
TMAP((s5,s5)) = {t18,t28,t32}
【０１０６】
上記のSMAPの例でKEYSを例示するとKEYS(SMAP)={s0,s1,s5,s12}となる。
【０１０７】
このように、剰余状態遷移系生成部１２は複数のグループの中から２つのグループを指定する（すなわち２つの代表状態を組み合わせる）ことを順次行う。そして、指定した２つのグループ（すなわち２つの代表状態（２つのクラス））に対して、一方のグループから他方のグループへの遷移（第２遷移）を設定する。一方のグループに含まれる状態のうちの１つから他方のグループに含まれる状態のうちの１つへの遷移（第１遷移）が存在するとき。そしてこのような２つのグループの指定と第２遷移の設定とを繰り返し行う。これによりグループ間（代表状態間あるいはクラス間）の第２遷移を表す剰余状態遷移系を生成する。
【０１０８】
＜遷移パスの変換方法＞
代表遷移パス生成部１３は、剰余状態遷移系２４（図27）の遷移を網羅するパス２５（代表状態または代表遷移イベントで表現された代表遷移パス２５）を求める。これにはたとえば公知のアルゴリズム（非特許文献１）を用いることができる。ここでテストとして実行可能な遷移パスは初期状態s0から始まる連続な遷移パスである。連続な遷移パスとは遷移系列の中で、現在の遷移の遷移先の状態と、次の遷移の遷移元の状態とが一致することを意味する。剰余状態遷移系の上で連続な代表遷移パス２５をそのまま状態遷移系の上の遷移パスと見なすと、連続な遷移パスになるとは限らない。したがって、剰余状態遷移系２４を網羅する最短の代表遷移パス２５を生成した後、これが元の状態遷移系上で連続したパスにならないときは、この代表遷移パス２５を手がかりに連続な遷移パスに変換する必要がある。このパス変換の手順を以下に示す。またこの変換手順に対応する処理の流れを図30のフローチャートに示す。この処理は遷移パス変換部１４により行われる。なおこの処理は、元の状態遷移系上で代表遷移パス２５が連続したパスにならないと遷移パス変換部１４が判断したときのみ行うようにしてもよいし、代表遷移パス２５が元の状態遷移系上で連続したパスになるか否かの判断を行うことなく、常に行うようにすることも可能である。
遷移選択 SELECT: T/~ × S → P(T)
機能： 遷移クラス[t]の中で状態sを始点とする遷移を選択する。
詳細： SELECT([t],s) = { t’ ∈ [t] | src(t’) = s }
状態選択 SOURCE: T/~ → P(S)
機能： 遷移クラス[t]に含まれる遷移の始点を列挙する。
詳細： SOURCE([t]) = { src(t’) ∈ S | t’ ∈ [t] }
パス生成 SHORTP: S × P(S) → [T]
機能： 状態sから状態集合dstsへ至るパスの中で最短のパスを選択する
詳細： SHORTP(s,dsts) = DIJKSTRA(s,s’)
ただしDIJKSTRAは公知の最短パス計算手順（例：ダイクストラ法）とし
状態s’∈dstsはパス長|DIJKSTRA(s,s’')|が状態s''∈dstsの中で最小とする
【０１０９】
＜遷移パスの変換アルゴリズム＞
入力：開始状態s0、代表遷移列tin=([t0],[t1],...)
出力：遷移列tout=(t0’,t1’,...)
手順：
ステップ1：初期化（図30のフローチャートのＣ１１）
s ← 開始状態s0
todo ← 代表遷移列tin
tout ← 空列
ステップ2：遷移選択（図30のフローチャートのＣ１２、Ｃ１３）
next ← SELECT(todoの先頭, s)
if 集合nextが空 then
ステップ3：選択による連結不可（図30のフローチャートのＣ１５）
dsts ← SOURCE(todoの先頭)
path ← SHORTP(s,dsts)
s ← パスpathの最後の状態
tout ← tout + path
else
ステップ4：選択による連結可能（図30のフローチャートのＣ１４）
t ← 遷移集合nextから一つ遷移を選択
s ← dst(t)
todo ← todoの末尾
tout ← tout + t
end if
ステップ5：終了判定（図30のフローチャートのＣ１６）
if リストtodoが空 then
（ステップ6）へ
else
（ステップ2）へ
end if
ステップ6：結果出力
遷移パスtoutを出力して停止
【０１１０】
例題：タスク制御モニタ
剰余状態遷移系２４（図27）の遷移を網羅するパスを公知のアルゴリズム（非特許文献１）を用いて代表遷移パス生成部１３により求めると図37の表7に示す遷移系列（代表遷移パス２５）が得られる。この遷移系列は剰余状態遷移系２４（図27）の上では連結したパスとなるが、元の状態遷移系（図26）の上では連結したパスとなるとは限らない。その場合、そのままでは実行可能なテストケースとならない。
【０１１１】
たとえば図37の表7の二本目のパスの代表遷移に沿う遷移系列はt0→t6→t5→t15→t4→t1となるが、遷移先と遷移元の状態が連続的に繋がらない。たとえば状態s1と状態s6は状態クラスが一致するため、剰余状態遷移系（図27）上では同じ状態だが、元の状態遷移系（図26）上で異なる状態である。
【０１１２】
遷移パス変換部１４は、代表遷移パス２５が元の状態遷移系（図26）の上では連結したパスにならないときは、代表遷移パス２５を元に、遷移パス変換を行うことにより実行可能な遷移パス２６を得る。具体的には、遷移パス変換部１４は、代表遷移パス２５における遷移クラスの中から上手く遷移を選んで、元の状態遷移系上で状態の遷移が連続的となるようにパスを生成する。遷移の選択だけで状態の遷移を連続的となるパスを生成できない場合は、最短パスの計算アルゴリズムを利用してパスの状態を連続化する（ステップ3（図30のＣ１５））。すなわち、連続的となるパスの生成ができない対象遷移クラスについては、１つ前の遷移クラスに含まれる遷移の中から選択した遷移の遷移先状態を起点とし、対象遷移クラスの遷移先状態の状態クラスに含まれるいずれかの状態へのパスを生成し、生成したパスを採用する。
【０１１３】
ここで剰余状態遷移系のパスを入力として元の状態遷移系上で状態が連続に遷移するパスを計算する操作をパス変換（あるいはパス復元）と命名する。パス変換（パス復元）のアルゴリズムは上に図30を用いて記述した通りである。
【０１１４】
図37の表7の遷移パスと、初期状態s0とを入力として、パス変換（パス復元）アルゴリズムを適用した結果を図38の表8に記す。表8の遷移パスは初期状態を状態s0とし、表7の各遷移クラスにそれぞれ含まれる遷移の中から一度ずつ遷移を選択して得られる遷移パスであり、元の状態遷移系の上で状態が連続的に遷移する実行可能なパスとなる。図38の表8の遷移パスは、最初に設定したテスト基準「タスク識別子を区別しない範囲で全ての状態と状態間の遷移を網羅する」を満たす最小のテストケースとなる。
【０１１５】
このように遷移パス変換部１４は、代表遷移パス生成部１３で各第２遷移が辿られた順序で代表遷移パス２５の各遷移（第１遷移）を順次選択する。そして各選択された第２遷移のそれぞれに対し、遷移パス変換部は、選択された第２遷移の遷移元グループにおける状態の１つと同じ遷移元状態を有し、かつ、選択された第２遷移の遷移先グループにおける状態のうちの１つと同じ遷移先状態を有し、かつ、直前に見つかった第１遷移の遷移先状態と同じ遷移元状態を有する、第１遷移を特定する。第１遷移は、上述したように、元の状態遷移系に含まれる遷移である。遷移パス変換部１４は各特定された第１遷移の系列と、各第１遷移に対応するイベントとを含むテストーケース（遷移パス）を生成する。
【０１１６】
上述したように、順次選択された第２遷移のうちの１つに対して第１遷移が見つからなかったとき、遷移パス変換部１４は、当該１つの第２遷移の直前における第２遷移に対して特定された第２遷移の遷移先状態と同じ遷移元状態を有し、かつ当該１つの第２遷移の遷移先グループに含まれる状態のうちの１つと同じ遷移先状態を有する、第１遷移を選択する。これによって、遷移パス変換部１４は、元の状態遷移系において第１状態の遷移が連続するように遷移パスを生成する。
【０１１７】
なお、以上に説明したテストケース生成装置は、例えば、汎用のコンピュータ装置を基本ハードウェアとして用いることでも実現することが可能である。すなわち、テストケース生成装置における各要素１〜８（図１参照）、１１〜１４（図２参照）は、上記のコンピュータ装置に搭載されたプロセッサにプログラムを実行させることにより実現することができる。このとき、テストケース生成装置は、上記のプログラムをコンピュータ装置にあらかじめインストールすることで実現してもよいし、ＣＤ−ＲＯＭなどの記憶媒体に記憶して、あるいはネットワークを介して上記のプログラムを配布して、このプログラムをコンピュータ装置に適宜インストールすることで実現してもよい。
【符号の説明】
【０１１８】
１：状態述語抽出手段（条件抽出手段）
２：直積手段（状態写像生成手段）
３：テストケース生成手段
４：原子述語抽出手段
５：出現頻度分析手段
６：高頻度原子述語抽出手段
７：低頻度原子述語抽出手段
８：網羅性評価手段
１１：状態同値関係定義部（グループ化手段）
１２：剰余状態遷移系生成部
１３：代表遷移パス生成部
１４：遷移パス変換部
２１：状態遷移系
２２：状態写像関数
２３：状態同値関係
２４：剰余状態遷移系
２５：代表遷移パス
２６：遷移パス（テストケース）
【図１】
2010218152.tif 000003
【図２】
2010218152.tif 000004
【図３】
2010218152.tif 000005
【図４】
2010218152.tif 000006
【図５】
2010218152.tif 000007
【図６】
2010218152.tif 000008
【図７】
2010218152.tif 000009
【図８】
2010218152.tif 000010
【図９】
2010218152.tif 000011
【図１０】
2010218152.tif 000012
【図１１】
2010218152.tif 000013
【図１２】
2010218152.tif 000014
【図１３】
2010218152.tif 000015
【図１４】
2010218152.tif 000016
【図１５】
2010218152.tif 000017
【図１６】
2010218152.tif 000018
【図１７】
2010218152.tif 000019
【図１８】
2010218152.tif 000020
【図１９】
2010218152.tif 000021
【図２０】
2010218152.tif 000022
【図２１】
2010218152.tif 000023
【図２２】
2010218152.tif 000024
【図２３】
2010218152.tif 000025
【図２４】
2010218152.tif 000026
【図２５】
2010218152.tif 000027
【図２６】
2010218152.tif 000028
【図２７】
2010218152.tif 000029
【図２８】
2010218152.tif 000030
【図２９】
2010218152.tif 000031
【図３０】
2010218152.tif 000032
【図３１】
2010218152.tif 000033
【図３２】
2010218152.tif 000034
【図３３】
2010218152.tif 000035
【図３４】
2010218152.tif 000036
【図３５】
2010218152.tif 000037
【図３６】
2010218152.tif 000038
【図３７】
2010218152.tif 000039
【図３８】
2010218152.tif 000040