(57)【要約】【課題】並行する状態を考慮したテストケースを生成することを目的とする。【解決手段】取得部１１０がそれぞれが状態遷移する２つのサブ状態を含む状態遷移モデル１５０を取得し、時相論理式（組合せ）生成部１２１が一方のサブ状態に含まれる複数の第１状態と、他方のサブ状態に含まれる複数の第２状態とから、第１状態と第２状態との組合せを複数生成し、状態遷移経路生成部１２３が、組合せ毎に、状態遷移経路１２３１を生成し、テストケース生成部１２５が組合せ毎に生成された状態遷移経路１２３１に基づいて、テストケース１６０を生成する。【選択図】図１
2015225422.tif 000002
【特許請求の範囲】
【請求項１】
対象物の状態遷移を検証するためのテストケースを生成するテストケース生成装置において、
前記対象物の状態遷移を表す状態遷移図であって、それぞれが状態遷移する２つの部分状態遷移図であって一方の部分状態遷移図には複数の状態が複数の第１状態として含まれ、他方の部分状態遷移図には複数の状態が複数の第２状態として含まれる２つの部分状態遷移図を含む状態遷移図を取得する取得部と、
前記取得部により取得された前記状態遷移図を取得し、前記一方の部分状態遷移図に含まれる前記複数の第１状態と、前記他方の部分状態遷移図に含まれる前記複数の第２状態とから、第１状態と第２状態との組を複数生成する組生成部と、
前記組生成部により生成された前記複数の組の組毎に、前記一方の部分状態遷移図における状態遷移の開始から前記組の前記第１状態までの状態遷移の経路を第１経路として取得するとともに、前記他方の部分状態遷移図における状態遷移の開始から前記組の前記第２状態までの状態遷移の経路を第２経路として取得し、取得した前記第１経路と前記第２経路とを結合し、結合した前記第１経路と前記第２経路とを状態遷移経路として生成する経路生成部と、
前記複数の組の組毎の前記状態遷移経路に基づいて、前記テストケースを生成するテストケース生成部と
を備えることを特徴とするテストケース生成装置。
【請求項２】
前記組生成部は、
前記一方の部分状態遷移図に含まれる前記複数の第１状態と、前記他方の部分状態遷移図に含まれる複数の第２状態とから、前記第１状態と前記第２状態との組合せを前記組として複数生成することを特徴とする請求項１に記載のテストケース生成装置。
【請求項３】
前記組生成部は、さらに、
前記組に含まれる前記第１状態と前記第２状態とが将来同時に起こる可能性があることを示す組合せ時相論理式を生成し、
前記経路生成部は、
前記組生成部により生成された前記組合せ時相論理式に基づいて、前記状態遷移経路を取得することを特徴とする請求項２に記載のテストケース生成装置。
【請求項４】
前記テストケース生成部は、
前記複数の組の組毎の前記状態遷移経路からなる状態遷移経路群から、所定の条件に従って状態遷移経路を削除し、削除後の前記状態遷移経路群を前記テストケースとすることを特徴とする請求項１または２に記載のテストケース生成装置。
【請求項５】
前記テストケース生成部は、
前記状態遷移経路群のうち処理の対象となる対象状態遷移経路が前記状態遷移経路群の前記対象状態遷移経路以外の状態遷移経路に含まれるか否かを処理装置により判定し、前記対象状態遷移経路以外の状態遷移経路に含まれると判定した場合に、前記対象状態遷移経路を前記状態遷移経路群から削除することを特徴とする請求項４に記載のテストケース生成装置。
【請求項６】
前記取得部は、
前記複数の第１状態の各第１状態間を接続する第１状態遷移が含まれる前記一方の部分状態遷移図と、前記複数の第２状態間を接続する第２状態遷移が含まれる前記他方の部分状態遷移図とを含む前記状態遷移図を取得し、
さらに、前記取得部により取得された前記状態遷移図を取得し、前記一方の部分状態遷移図に含まれる前記第１状態遷移と、前記他方の部分状態遷移図に含まれる前記第２状態遷移との順列を複数生成し、生成した前記複数の順列の順列毎に、前記第１状態遷移の後に前記第２状態遷移が起きることを意味する順列時相論理式を生成する順列生成部を備え、
前記経路生成部は、
前記順列生成部により生成された前記順列時相論理式に基づいて、前記複数の順列の順列毎に、前記順列時相論理式を満たす状態遷移の経路を順列時状態遷移経路として生成し、
前記テストケース生成部は、
前記複数の順列の順列毎の前記順列時状態遷移経路に基づいて、前記テストケースを生成することを特徴とする請求項１〜５のいずれかに記載のテストケース生成装置。
【請求項７】
さらに、前記取得部により取得された前記状態遷移図を取得し、取得した前記状態遷移図を前記組生成部と前記順列生成部とのいずれに入力するかを判定し、判定結果に基づいて前記組生成部と前記順列生成部とのいずれに入力するかを切り替える切替部を備えることを特徴とする請求項６に記載のテストケース生成装置。
【請求項８】
対象物の状態遷移を検証するためのテストケースを生成するテストケース生成装置のテストケース生成方法において、
取得部が、前記対象物の状態遷移を表す状態遷移図であって、それぞれが状態遷移する２つの部分状態遷移図であって一方の部分状態遷移図には複数の状態が複数の第１状態として含まれ、他方の部分状態遷移図には複数の状態が複数の第２状態として含まれる２つの部分状態遷移図を含む状態遷移図を取得し、
組生成部が、前記取得部により取得された前記状態遷移図を取得し、前記一方の部分状態遷移図に含まれる前記複数の第１状態と、前記他方の部分状態遷移図に含まれる複数の第２状態とから、第１状態と第２状態との組を複数生成し、
経路生成部が、前記組生成部により生成された前記複数の組の組毎に、前記一方の部分状態遷移図における状態遷移の開始から前記組の前記第１状態までの状態遷移の経路を第１経路として取得するとともに、前記他方の部分状態遷移図における状態遷移の開始から前記組の前記第２状態までの状態遷移の経路を第２経路として取得し、取得した前記第１経路と前記第２経路とを結合し、結合した前記第１経路と前記第２経路とを状態遷移経路として生成し、
テストケース生成部が、前記複数の組の組毎の前記状態遷移経路に基づいて、前記テストケースを生成することを特徴とするテストケース生成方法。
【請求項９】
対象物の状態遷移を検証するためのテストケースを生成するテストケース生成装置のプログラムにおいて、
前記対象物の状態遷移を表す状態遷移図であって、それぞれが状態遷移する２つの部分状態遷移図であって一方の部分状態遷移図には複数の状態が複数の第１状態として含まれ、他方の部分状態遷移図には複数の状態が複数の第２状態として含まれる２つの部分状態遷移図を含む状態遷移図を取得する取得処理と、
前記取得処理により取得された前記状態遷移図を取得し、前記一方の部分状態遷移図に含まれる前記複数の第１状態と、前記他方の部分状態遷移図に含まれる複数の第２状態とから、第１状態と第２状態との組を複数生成する組生成処理と、
前記組生成処理により生成された前記複数の組の組毎に、前記一方の部分状態遷移図における状態遷移の開始から前記組の前記第１状態までの状態遷移の経路を第１経路として取得するとともに、前記他方の部分状態遷移図における状態遷移の開始から前記組の前記第２状態までの状態遷移の経路を第２経路として取得し、取得した前記第１経路と前記第２経路とを結合し、結合した前記第１経路と前記第２経路とを状態遷移経路として生成する経路生成処理と、
前記複数の組の組毎の前記状態遷移経路に基づいて、前記テストケースを生成するテストケース生成処理とをコンピュータに実行させるプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、テストケース生成装置、テストケース生成方法及びプログラムに関する。
【背景技術】
【０００２】
ソフトウェア開発の試験（主に組み合わせ試験）においては、仕様や設計で定めた状態遷移モデルが実現されているかを確認することが有効である。
【０００３】
状態遷移モデルとは、状態遷移を表した１つ以上の図または表を表す。状態遷移モデルは、状態と状態遷移イベント、イベント受信後の状態の組み合わせで表される。試験の仕様は、状態遷移モデルをもとに１つ以上の「状態遷移イベント、イベント受信後の状態」なるテストケースとして表現される。
【０００４】
従来技術として、状態遷移図を入力として、そこに含まれる状態や状態遷移を網羅する複数のテストケース（テストスイート）を自動生成する技術が開示されている（例えば、特許文献１参照）。この技術は、並行な状態遷移モデルを入力として、所望の網羅性を保証する効率的なテストケースを生成するものであり、特定遷移の遷移禁止を指定することで、テストに必要な遷移のみでテストケースを自動生成する。
【０００５】
また、並行な状態遷移モデルから生成するテストケースサイズを小さくする技術が開示されている（例えば、特許文献２参照）。この技術は、並行な状態遷移モデルに対して発生するイベントの順序等を時相論理式（組合せ）で制限し、テストケースを自動生成するものである。
【０００６】
また、非特許文献１では、ＵＭＬ（Ｕｎｉｆｉｅｄ  Ｍｏｄｅｌｉｎｇ  Ｌａｎｇｕａｇｅ）のステートマシン図を、モデル検査ツール（例えば、ＳＰＩＮなど）の入力言語であるＰＲＯＭＥＬＡへ自動的に変換する規則を提供している。
【先行技術文献】
【特許文献】
【０００７】
【特許文献１】特開平０７−２５３９０５号公報
【特許文献２】特開２０１１−０６５５７６号公報
【非特許文献】
【０００８】
【非特許文献１】ＵＭＬモデルの振舞いのモデル検査における表現方法について  ＮＥＣ  八鍬、野田（情報科学技術フォーラム講演論文集９）
【発明の概要】
【発明が解決しようとする課題】
【０００９】
既存技術では、状態遷移図を入力として、状態や状態遷移を網羅する複数のテストケース（テストスイート）を自動生成することが可能である。しかし、並行する状態や状態遷移の組み合わせを考慮したテストケース生成は実現していない。既存技術では、複数の状態遷移図（または表）を含む状態遷移モデルを入力可能だが、状態遷移図個別にテストケースを生成するものである。このため、並行する状態や状態遷移の組み合わせを考慮したテストケース生成は実現していない。
【００１０】
特許文献１では、並行な状態遷移モデルが入力でき、遷移網羅のテストケースを生成するが、並行な状態遷移モデルを考慮した組み合わせを保証していない。
【００１１】
特許文献２では、並行な状態遷移モデルが入力できるが、時相論理式（組合せ）の自動生成、「二並行状態組合せ」と「二状態遷移順列」を網羅したテストケースの自動生成、重複したテストケースの自動削除ができない。
【００１２】
本発明は、このような課題を解決するためになされたもので、並行な状態遷移モデルを入力として、二並行なサブ状態の全２状態の組合せである「二並行状態組み合わせ」と二並行なサブ状態の全２遷移の順列である「二状態遷移順列」を網羅したテストケース生成可能なテストケース生成装置を提供することを目的とする。
【課題を解決するための手段】
【００１３】
本発明に係るテストケース生成装置は、対象物の状態遷移を検証するためのテストケースを生成するテストケース生成装置において、
前記対象物の状態遷移を表す状態遷移図であって、それぞれが状態遷移する２つの部分状態遷移図であって一方の部分状態遷移図には複数の状態が複数の第１状態として含まれ、他方の部分状態遷移図には複数の状態が複数の第２状態として含まれる２つの部分状態遷移図を含む状態遷移図を取得する取得部と、
前記取得部により取得された前記状態遷移図を取得し、前記一方の部分状態遷移図に含まれる前記複数の第１状態と、前記他方の部分状態遷移図に含まれる複数の第２状態とから、第１状態と第２状態との組を複数生成する組生成部と、
前記組生成部により生成された前記複数の組の組毎に、前記一方の部分状態遷移図における状態遷移の開始から前記組の前記第１状態までの状態遷移の経路を第１経路として取得するとともに、前記他方の部分状態遷移図における状態遷移の開始から前記組の前記第２状態までの状態遷移の経路を第２経路として取得し、取得した前記第１経路と前記第２経路とを結合し、結合した前記第１経路と前記第２経路とを状態遷移経路として生成する経路生成部と、
前記複数の組の組毎の前記状態遷移経路に基づいて、前記テストケースを生成するテストケース生成部と
を備えることを特徴とする。
【発明の効果】
【００１４】
本実施の形態に係るテストケース生成装置によれば、組生成部が一方の部分状態遷移図に含まれる複数の第１状態と、他方の部分状態遷移図に含まれる複数の第２状態とから、第１状態と第２状態との組を複数生成し、経路生成部が、組毎に、一方の部分状態遷移図における状態遷移の開始から第１状態までの状態遷移の経路を第１経路として取得するとともに、他方の部分状態遷移図における状態遷移の開始から第２状態までの状態遷移の経路を第２経路として取得し、取得した第１経路と第２経路とを結合して状態遷移経路を生成し、テストケース生成部が組毎に生成された状態遷移経路に基づいて、テストケースを生成するので、並行する状態を考慮したテストケースを生成することができるという効果を奏する。
【図面の簡単な説明】
【００１５】
【図１】実施の形態１に係るテストケース生成装置のブロック構成の一例を示す図である。
【図２】実施の形態１に係るテストケース生成装置のハードウェア構成の一例を示す図である。
【図３】実施の形態１に係るテストケース生成装置におけるテストケース生成方法（処理、工程）の動作の一例を示すフローチャートである。
【図４】実施の形態１に係るテストケース生成処理の入力となる状態遷移モデルの一例を示す図である。
【図５】実施の形態１に係る時相論理式（組合せ）生成部により抽出された状態の組合せを示す状態組合せ図である。
【図６】実施の形態１に係る時相論理式（組合せ）生成部１２１により生成された時相論理式（組合せ）群の一例を示す図である。
【図７】実施の形態１に係る状態遷移経路生成部により生成された状態遷移経路郡の一例を示す図である。
【図８】実施の形態１におけるＵＭＬのステートマシン図からモデル検査ツール（ＳＰＩＮ）の入力言語ＰＲＯＭＥＬＡへの変換方法を示す図である。
【図９】実施の形態１におけるステートマシン図からＰＲＯＭＥＬＡへの変換例を示す図である。
【図１０】実施の形態１に係るテストケース生成部によるテストケース生成処理の一例を示すフローチャートである。
【図１１】実施の形態１に係るテストケース生成処理により生成されたテストケースの一例を示す図である。
【図１２】実施の形態２に係るテストケース生成装置のブロック構成の一例を示す図である。
【図１３】実施の形態２に係るテストケース生成装置におけるテストケース生成方法（処理、工程）の動作の一例を示すフローチャートである。
【図１４】実施の形態２に係るテストケース生成処理の入力となる状態遷移モデルの一例を示す図である。
【図１５】実施の形態２に係る時相論理式（順列）生成部により抽出された状態遷移の順列例を示す図（状態遷移順列図）である。
【図１６】実施の形態２に係る時相論理式（順列）生成部により生成された時相論理式（順列）群の一例を示す図である。
【図１７】実施の形態３に係るテストケース生成装置のブロック構成の一例を示す図である。
【図１８】実施の形態３に係るテストケース生成装置におけるテストケース生成方法（処理、工程）の動作の一例を示すフローチャートである。
【発明を実施するための形態】
【００１６】
実施の形態１．
図１は、本実施の形態に係るテストケース生成装置１００のブロック構成の一例を示す図である。図１を用いて、本実施の形態に係るテストケース生成装置１００のブロック構成について説明する。
【００１７】
テストケース生成装置１００は、複数の並行なサブ状態を含む状態遷移モデル１５０に対し、二並行状態の組合せを網羅するテストケース１６０を自動生成する装置である。
【００１８】
図１に示すように、テストケース生成装置１００は、取得部１１０と、テストケース生成処理部１２０と、表示部１３０とを有する。
【００１９】
取得部１１０は、状態遷移モデル１５０を取得する状態遷移モデル取得部１１１を有する。
状態遷移モデル１５０の構成については後で説明する。
【００２０】
テストケース生成処理部１２０は、二並行状態組合せ網羅時相論理式（組合せ）生成部（以下、時相論理式（組合せ）生成部１２１とする）と、時相論理式（組合せ）記憶部１２２と、状態遷移経路生成部１２３と、状態遷移経路記憶部１２４と、テストケース生成部１２５とを有する。
【００２１】
表示部１３０は、テストケース生成部１２５により生成されたテストケース１６０を表示するテストケース表示部１３１を有する。
テストケース１６０の構成については後で説明する。
【００２２】
時相論理式（組合せ）生成部１２１は、状態遷移モデル１５０に含まれる異なる２つの並行なサブ状態から、それぞれ１つの状態を取り出した二並行状態の全組合せについて、「いつか指定した二並行状態が同時におきる」を意味する二並行状態組合せ網羅時相論理式（以下、時相論理式（組合せ）１２１１と呼ぶ）を生成する。時相論理式（組合せ）１２１１は二並行状態の全組合せにおいて生成する。
例えば、サブ状態Ａが２状態、サブ状態Ｂが３状態保有している場合、６つの時相論理式（組合せ）１２１１が生成される。
時相論理式（組合せ）生成部１２１による時相論理式（組合せ）１２１１の生成については、後で説明する。
【００２３】
時相論理式（組合せ）記憶部１２２は、時相論理式（組合せ）生成部１２１で生成した「いつか指定した二並行状態が同時におきる」を意味する時相論理式（組合せ）１２１１を記憶する。
【００２４】
状態遷移経路生成部１２３は、取得された状態遷移モデル１５０を基に、時相論理式（組合せ）記憶部から取り出した時相論理式（組合せ）１２１１を満たす状態遷移経路１２３１を生成する。
【００２５】
状態遷移経路記憶部１２４は、状態遷移経路生成部１２３により生成された状態遷移経路１２３１を記憶する。
【００２６】
テストケース生成部１２５は、状態遷移経路記憶部１２４から取り出した複数の状態遷移経路１２３１から、他の状態遷移経路１２３１に包含されている冗長な状態遷移経路１２３１を削除する正規化を実行し、テストケース１６０を生成する。
【００２７】
図２は、本実施の形態に係るテストケース生成装置１００のハードウェア構成の一例を示す図である。
図２を用いて、テストケース生成装置１００のハードウェア構成例について説明する。
【００２８】
テストケース生成装置１００はコンピュータであり、テストケース生成装置１００の各要素をプログラムで実現することができる。
テストケース生成装置１００のハードウェア構成としては、バスに、演算装置９０１、外部記憶装置９０２、主記憶装置９０３、通信装置９０４、入出力装置９０５が接続されている。
【００２９】
演算装置９０１は、プログラムを実行するＣＰＵ（Ｃｅｎｔｒａｌ・Ｐｒｏｃｅｓｓｉｎｇ・Ｕｎｉｔ）である。
外部記憶装置９０２は、例えばＲＯＭ（Ｒｅａｄ・Ｏｎｌｙ・Ｍｅｍｏｒｙ）やフラッシュメモリ、ハードディスク装置である。
主記憶装置９０３は、ＲＡＭ（Ｒａｎｄｏｍ・Ａｃｃｅｓｓ・Ｍｅｍｏｒｙ）である。
通信装置９０４は、例えば通信ボード等であり、ＬＡＮ（Ｌｏｃａｌ・Ａｒｅａ・Ｎｅｔｗｏｒｋ）等に接続されている。通信装置９０４は、ＬＡＮに限らず、ＩＰ−ＶＰＮ（Ｉｎｔｅｒｎｅｔ・Ｐｒｏｔｏｃｏｌ・Ｖｉｒｔｕａｌ・Ｐｒｉｖａｔｅ・Ｎｅｔｗｏｒｋ）、広域ＬＡＮ、ＡＴＭ（Ａｓｙｎｃｈｒｏｎｏｕｓ・Ｔｒａｎｓｆｅｒ・Ｍｏｄｅ）ネットワークといったＷＡＮ（Ｗｉｄｅ・Ａｒｅａ・Ｎｅｔｗｏｒｋ）、あるいは、インターネットに接続されていても構わない。ＬＡＮ、ＷＡＮ、インターネットは、ネットワークの一例である。
入出力装置９０５は、例えばマウス、キーボード、ディスプレイ装置等である。マウスの代わりに、タッチパネル、タッチパッド、トラックボール、ペンタブレット、あるいは、その他のポインティングデバイスが用いられてもよい。ディスプレイ装置は、ＬＣＤ（Ｌｉｑｕｉｄ・Ｃｒｙｓｔａｌ・Ｄｉｓｐｌａｙ）、ＣＲＴ（Ｃａｔｈｏｄｅ・Ｒａｙ・Ｔｕｂｅ）、あるいは、その他の表示装置でもよい。
【００３０】
プログラムは、通常は外部記憶装置９０２に記憶されており、主記憶装置９０３にロードされた状態で、順次演算装置９０１に読み込まれ、実行される。
プログラムは、ブロック構成図に示す「〜部」として説明している機能を実現するプログラムである。
プログラムプロダクト（コンピュータプログラムプロダクト）は、ブロック構成図に示す「〜部」の機能を実現するプログラムが記録された記憶媒体、記憶装置などから構成される。プログラムプロダクトは、外観に関わらず、コンピュータ読み取り可能なプログラムをロードしているものである。
【００３１】
更に、外部記憶装置９０２にはオペレーティングシステム（ＯＳ）も記憶されており、ＯＳの少なくとも一部が主記憶装置９０３にロードされ、演算装置９０１はＯＳを実行しながら、ブロック構成図に示す「〜部」の機能を実現するプログラムを実行する。
また、アプリケーションプログラムも外部記憶装置９０２に記憶されており、主記憶装置９０３にロードされた状態で、順次演算装置９０１により実行される。
また、「〜テーブル」等の情報も外部記憶装置９０２に記憶されている。
【００３２】
また、「〜の判断」、「〜の判定」、「〜の抽出」、「〜の検知」、「〜の設定」、「〜の登録」、「〜の選択」、「〜の生成」、「〜の入力」、「〜の取得」、「〜の出力」等の処理の結果を示す情報やデータや信号値や変数値が主記憶装置９０３に記憶されている。
また、テストケース生成装置１００が受信したデータが主記憶装置９０３に記憶される。
また、暗号鍵・復号鍵や乱数値やパラメータが、主記憶装置９０３に記憶されてもよい。
【００３３】
なお、図２の構成は、あくまでもテストケース生成装置１００のハードウェア構成の一例を示すものであり、テストケース生成装置１００のハードウェア構成は図２に記載の構成に限らず、他の構成であってもよい。
【００３４】
図３は、本実施の形態に係るテストケース生成装置１００におけるテストケース生成方法（処理、工程）の動作の一例を示すフローチャートである。
図３を用いて、本実施の形態に係るテストケース生成装置１００におけるテストケース生成方法（処理、工程）の動作について説明する。
【００３５】
テストケース生成処理は、状態遷移モデル取得処理（工程、ステップ）と、二並行状態組合せ網羅時相論理式（組合せ）生成処理（工程、ステップ）（以下、時相論理式（組合せ）生成処理とも呼ぶ）と、状態遷移経路生成処理（工程、ステップ）と、テストケース生成処理（工程、ステップ）と、テストケース表示処理（工程、ステップ）とから構成される。
【００３６】
＜状態遷移モデル取得処理（工程）（取得処理（工程））：Ｓ１０１＞
Ｓ１０１の状態遷移モデル取得処理において、状態遷移モデル取得部１１１は、状態遷移モデル１５０を取得する。
【００３７】
＜時相論理式（組合せ）生成処理（工程）（組生成処理（工程））：Ｓ１０２＞
Ｓ１０２の時相論理式（組合せ）生成処理において、時相論理式（組合せ）生成部１２１は、入力された状態遷移モデル１５０における異なる２つの並行なサブ状態から、それぞれ１つの状態を取り出し、「指定した二並行状態がいつか同時におきる」を意味する時相論理式（組合せ）１２１１を生成する。時相論理式（組合せ）生成部１２１は、取得された状態遷移モデル１５０において、取り出し得る異なる２つのサブ状態に属する２つの並行状態の全ての組合せについて、時相論理式（組合せ）１２１１を生成する。時相論理式（組合せ）１２１１は二並行状態のすべての組合せにおいて生成されるため、例えば、サブ状態Ａが２状態、サブ状態Ｂが３状態保有している場合、６つの時相論理式（組合せ）１２１１が生成される。
【００３８】
＜状態遷移経路生成処理（工程）（経路生成処理（工程））：Ｓ１０３＞
Ｓ１０３の状態遷移経路生成処理において、状態遷移経路生成部１２３は、入力された状態遷移モデル１５０を基に、１つの時相論理式（組合せ）１２１１（二並行状態組合せ網羅時相論理式）を満たす状態遷移経路１２３１を生成する。状態遷移経路生成部１２３は、例えば、「モデル検査ツール」（非特許文献１参照）等を利用して、時相論理式（組合せ）１２１１を満たす状態遷移経路１２３１を生成する。
【００３９】
＜テストケース生成処理（工程）：Ｓ１０４＞
Ｓ１０４のテストケース生成処理において、テストケース生成部１２５は、他の状態遷移経路１２３１に包含されている冗長な状態遷移経路１２３１を削除する正規化を実行し、テストケース１６０を生成する。
【００４０】
＜テストケース表示処理（工程）：Ｓ１０５＞
Ｓ１０５のテストケース表示処理において、テストケース表示部１３１は、テストケース生成部１２５により生成されたテストケース１６０を表示装置などに表示する。
【００４１】
図４は、本実施の形態に係るテストケース生成処理の入力となる状態遷移モデル１５０の一例を示す図である。
図４に示す状態遷移モデル１５０の一例を用いて、テストケース生成処理の動作の一例について説明する。
【００４２】
状態遷移モデル１５０のサブ状態は、ＵＭＬのステートマシン図（状態遷移図）で記述する。
状態遷移モデル１５０は、並行に動作する２つのサブ状態を有する。２つのサブ状態を図４に示すステートマシン図Ａ，Ｂで表す。２つのサブ状態（ステートマシン図Ａ，Ｂ）は、入れ子状態ではないものとする。ステートマシン図Ａをサブ状態Ａ、ステートマシン図Ｂをサブ状態Ｂと呼ぶ場合がある。
サブ状態Ａ，Ｂ（ステートマシン図Ａ，Ｂ）のそれぞれは、初期状態を１つ、初期状態以外の状態を少なくとも１つ、状態遷移を少なくとも１つ持つ。遷移に対しては遷移イベントを１つ持つ。
【００４３】
状態遷移モデル１５０は、テストの対象となる対象物の状態遷移を表す状態遷移図の一例である。また、サブ状態Ａ，Ｂ（ステートマシン図Ａ，Ｂ）は、それぞれが状態遷移する２つの部分状態遷移図の一例である。
【００４４】
ステートマシン図Ａは、初期状態「Ａ１」から開始する。状態「Ａ１」においてイベント「ｅ１」により状態「Ａ２」へ、イベント「ｅ４」により状態「Ａ３」へ遷移する。状態「Ａ２」においてイベント「ｅ２」により状態「Ａ３」へ遷移する。状態「Ａ３」においてイベント「ｅ３」により状態「Ａ１」へ遷移する。例えば、状態Ａ１，Ａ２，Ａ３は、一方の部分状態遷移図の一例であるサブ状態Ａに含まれる複数の第１状態の一例である。状態Ｂ１，Ｂ２，Ｂ３は、他方の部分状態遷移図の一例であるサブ状態Ｂに含まれる複数の第２状態の一例である。また、イベントｅ１〜ｅ３は、複数の第１状態の各第１状態間を接続する第１状態遷移の一例であり、イベントｅ５〜ｅ７は複数の第２状態間を接続する第２状態遷移の一例である。
【００４５】
ステートマシン図Ｂは初期状態「Ｂ１」から開始する。状態「Ｂ１」においてイベント「ｅ５」により状態「Ｂ２」へ遷移する。状態「Ｂ２」においてイベント「ｅ６」により状態「Ｂ３」へ遷移する。状態「Ｂ３」においてイベント「ｅ７」により状態「Ｂ１」へ遷移する。
【００４６】
図３のＳ１０１において、状態遷移モデル取得部１１１は、図４に示す２つのサブ状態Ａ，Ｂ（ステートマシン図Ａ，Ｂ）を有する状態遷移モデル１５０を取得する。
【００４７】
次に、図３のＳ１０２における時相論理式（組合せ）生成部１２１による時相論理式（組合せ）生成処理について、具体例を用いて説明する。
まず、時相論理式（組合せ）生成部１２１は、異なる２つのサブ状態Ａ，Ｂから取り出し得る異なる二並行状態の全組合せを抽出し、時相論理式（組合せ）１２１１を生成する。
具体的には、例えば、ステートマシン図Ａの状態「Ａ１」、「Ａ２」、「Ａ３」とステートマシン図Ｂの状態「Ｂ１」、「Ｂ２」、「Ｂ３」に対して、各ステートマシン図から１つ取り出して組み合わせた全組合せを抽出する。
【００４８】
図５は、本実施の形態に係る時相論理式（組合せ）生成部１２１により抽出された状態の組合せを示す状態組合せ図である。
図５の状態組合せ図において、「ｓｔａｔｅＡ」列はステートマシン図Ａが取りうる状態、「ｓｔａｔｅＢ」列はステートマシン図Ｂが取りうる状態を意味する。状態組合せ図の各行は、番号に対応付けられた状態組合せを意味する。図５の状態組合せ図では、９つの抽出された状態組合せを示している。
時相論理式（組合せ）生成部１２１は、サブ状態Ａに含まれる複数の第１状態と、サブ状態Ｂに含まれる複数の第２状態とから、第１状態と第２状態との組（組合せ）を複数生成する組生成部の一例である。
【００４９】
次に、時相論理式（組合せ）生成部１２１は、状態組合せ図を用いて、時相論理式（組合せ）１２１１を生成する。
時相論理式（組合せ）生成部１２１は、時相論理式（組合せ）１２１１を生成するために、二並行状態組合せ網羅時相論理式（組合せ）テンプレート（以下、時相論理式（組合せ）テンプレートと呼ぶ）を用いる。
時相論理式（組合せ）テンプレートは、「いつか指定した二並行状態が同時に起きる」を意味する時相論理式（組合せ）で、演算子や利用する変数名は固定とし、二並行状態の組合せの部分を可変としているものである。
時相論理式（組合せ）テンプレートは、予めテストケース生成装置１００の記憶装置に設定されるものである。
【００５０】
具体的には、時相論理式（組合せ）テンプレートは、「＜＞（ｓｔａｔｅ＿ｖａｒ＿Ａ＝＝ｓｔａｔｅ＿ｎａｍｅ＿Ａ）＆＆（ｓｔａｔｅ＿ｖａｒ＿Ｂ＝＝ｓａｔｅ＿ｎａｍｅ＿Ｂ）」である。（ｓｔａｔｅ＿ｖａｒ＿Ａ＝＝ｓｔａｔｅ＿ｎａｍｅ＿Ａ）が真、かつ、（ｓｔａｔｅ＿ｖａｒ＿Ｂ＝＝ｓａｔｅ＿ｎａｍｅ＿Ｂ）が真の場合、真となる論理式である。演算子「＜＞」は、将来のいずれかの時点で論理式が真になることを示す演算子である。
【００５１】
本実施の形態では、状態遷移経路生成部１２３が、時相論理式（組合せ）生成部１２１により生成された時相論理式（組合せ）１２１１に対して、最短の状態遷移経路１２３１を生成する。このとき、状態遷移経路生成部１２３は、モデル検査ツールを用いて、時相論理式（組合せ）１２１１から最短の状態遷移経路１２３１を生成する。
「ｓｔａｔｅ＿ｖａｒ＿Ａ」、「ｓｔａｔｅ＿ｖａｒ＿Ｂ」は、このモデル検査ツールにおいて、ステートマシン図Ａ、ステートマシン図Ｂの状態を格納する変数とする。
時相論理式（組合せ）生成部１２１は、時相論理式（組合せ）テンプレートの「ｓｔａｔｅ＿ｎａｍｅ＿Ａ」に、図５の「ｓｔａｔｅＡ」列に設定されている値を、「ｓａｔｅ＿ｎａｍｅ＿Ｂ」に図５の「ｓｔａｔｅＢ」列に設定されている値を当てはめることで、二並行状態の組合せ毎に二並行状態組合せ網羅時相論理式（組合せ）を生成する。
【００５２】
図６は、本実施の形態に係る時相論理式（組合せ）生成部１２１により生成された時相論理式（組合せ）群の一例を示す図である。
時相論理式（組合せ）生成部１２１は、上述したように、図５の状態組合せ図の各状態組合せを時相論理式（組合せ）テンプレートに当てはめ、時相論理式（組合せ）１２１１を生成する。
時相論理式（組合せ）１２１１は、第１状態と第２状態とが将来同時に起こる可能性があることを示す組合せ時相論理式の一例である。
【００５３】
具体的には、図５の１行目において、「ｓｔａｔｅＡ」列は「Ａ１」、「ｓｔａｔｅＢ」列は「Ｂ１」のため、二並行状態組合せ網羅の時相論理式（組合せ）テンプレート「＜＞（ｓｔａｔｅ＿ｖａｒ＿Ａ＝＝ｓｔａｔｅ＿ｎａｍｅ＿Ａ）＆＆（ｓｔａｔｅ＿ｖａｒ＿Ｂ＝＝ｓａｔｅ＿ｎａｍｅ＿Ｂ）」の「ｓｔａｔｅ＿ｎａｍｅ＿Ａ」に「Ａ１」を、「ｓｔａｔｅ＿ｎａｍｅ＿Ｂ」に「Ｂ１」を当てはめる。このように、時相論理式（組合せ）生成部１２１の時相論理式（組合せ）生成処理により、時相論理式（組合せ）１２１１（二並行状態組合せ網羅時相論理式）「＜＞（ｓｔａｔｅ＿ｖａｒ＿Ａ＝＝Ａ１）＆＆（ｓｔａｔｅ＿ｖａｒ＿Ｂ＝＝Ｂ１）」が得られる。時相論理式（組合せ）生成部１２１は、図５の状態組合せ図の全状態組合せについて上記処理を実行し、図６に示すように９つの時相論理式（組合せ）１２１１を生成する。図６に示す９つの時相論理式（組合せ）１２１１を時相論理式（組合せ）群と呼ぶ場合がある。
【００５４】
状態遷移モデル１５０が３つ以上のステートマシン図を有しており、状態遷移モデル取得部１１１に３つ以上のステートマシン図が入力された場合は、ステートマシン図群から取り出した２つのステートマシン図の全組合せに対して、時相論理式（組合せ）生成処理を適用する。例えば、入力された状態遷移モデル１５０がステートマシン図Ａ、ステートマシン図Ｂ、ステートマシン図Ｃであった場合、ステートマシン図Ａとステートマシン図Ｂ、ステートマシン図Ａとステートマシン図Ｃ、ステートマシン図Ｂとステートマシン図Ｃの組合せ（組の一例）に対して、時相論理式（組合せ）生成処理を適用する。
【００５５】
時相論理式（組合せ）記憶部１２２は、時相論理式（組合せ）生成部１２１により生成された時相論理式（組合せ）１２１１（時相論理式（組合せ）群）を記憶装置に記憶する。
【００５６】
次に、図３のＳ１０３における状態遷移経路生成部１２３による状態遷移経路生成処理について、具体例を用いて説明する。
状態遷移経路生成部１２３は、時相論理式（組合せ）記憶部１２２に記憶されている時相論理式（組合せ）群から、時相論理式（組合せ）１２１１を１つ取り出す。状態遷移経路生成部１２３は、状態遷移モデル１５０に基づいて、取り出した時相論理式（組合せ）１２１１を満たす最短（遷移数が最小）の状態遷移経路１２３１を生成し、状態遷移経路記憶部１２４に記憶する。状態遷移経路生成部１２３は、時相論理式（組合せ）群に含まれるすべての時相論理式（組合せ）１２１１に対して、状態遷移経路生成処理を実行する。
状態遷移経路生成部１２３は、例えば、モデル検査ツール（例えば、ＳＰＩＮモデルチェッカー）を用いて、時相論理式（組合せ）１２２１から最短の状態遷移経路１２３１を生成する。
【００５７】
例えば、状態遷移経路生成部１２３は、時相論理式（組合せ）１２２１毎に、サブ状態Ａにおける状態遷移の開始から第１状態までの状態遷移の経路を第１経路として取得するとともに、サブ状態Ｂにおける状態遷移の開始から第２状態までの状態遷移の経路を第２経路として取得する（図７参照）。状態遷移経路生成部１２３は、取得した第１経路と第２経路とを結合し、結合した第１経路と第２経路とを状態遷移経路として生成する経路生成部の一例である。
【００５８】
図７は、本実施の形態に係る状態遷移経路生成部１２３により生成された状態遷移経路群の一例を示す図である。
図７に示すように、状態遷移経路群には、９つの状態遷移経路１２３１が含まれる。９つの状態遷移経路１２３１は、図６の時相論理式（組合せ）群に含まれる９つの時相論理式（組合せ）１２１１のそれぞれに対応する状態遷移経路１２３１である。図７に示す９つの状態遷移経路１２３１を状態遷移経路群と呼ぶ場合がある。
【００５９】
図７に示すように、状態遷移経路１２３１の保存形式は、「遷移元の状態」、「遷移したイベント」、「遷移先の状態」を１つの遷移単位として、複数の遷移単位分設定することができる。例えば、状態遷移経路群は、表形式で保存される。なお、必ずしも表形式でなくてもよく、「遷移元の状態」、「遷移したイベント」、「遷移先の状態」が複数遷移分表現できれば、任意の形式でよい。
【００６０】
ここで、状態遷移モデル取得部１１１によるステートマシン図からＰＲＯＭＥＬＡへの変換方法について説明する。
図８は、本実施の形態におけるＵＭＬのステートマシン図からモデル検査ツール（ＳＰＩＮ）の入力言語ＰＲＯＭＥＬＡへの変換方法を示す図である。
図９は、本実施の形態におけるステートマシン図からＰＲＯＭＥＬＡへの変換の具体例を示す図である。
【００６１】
状態遷移モデル取得部１１１は、入力された状態遷移モデル１５０を、状態遷移経路生成部１２３が入力可能な形式へ変換する。本実施の形態では、状態遷移モデル１５０としてＵＭＬのステートマシン図、状態遷移経路生成部１２３としてモデル検査ツールＳＰＩＮを用いるものとする。
【００６２】
以下に、ＵＭＬのステートマシン図から、モデル検査ツールＳＰＩＮの入力言語であるＰＲＯＭＥＬＡへの変換方法について、図８を用いて説明する。
図８に示すように、１つの並行動作単位を示す「Ｐｒｏｃｔｙｐｅ」の名前にステートマシン図名を、「ｇｏｔｏ」文による移動の印となるラベルには状態名を記述する。遷移イベントの取得は繰り返し文を示す「ｄｏ」文の分岐として記述する。「ｃｈａｎｎｅｌ」は遷移イベントを受信する受信路を、「遷移イベント用一時変数」は遷移イベントを格納する一時変数を示す。遷移の評価は選択を示す「ｉｆ」文の分岐として記述する。「遷移イベント用一時変数＝＝遷移イベント」は遷移する遷移イベントを、「ｇｏｔｏ  遷移先状態名ラベル」は遷移先の状態を示す。
図９を用いて、ステートマシン図からＰＲＯＭＥＬＡへの変換方法の具体例について説明する。ステートマシン図名「Ｓｔａｔｅ＿ｍａｃｈｉｎｅ＿Ｂ」から「Ｐｒｏｃｔｙｐｅ  Ｓｔａｔｅ＿ｍａｃｈｉｎｅ＿Ｂ（）」（１行目）へ変換している。状態名「Ｂ１」、「Ｂ２」からラベル「Ｂ１」（２行目）、ラベル「Ｂ２」（１１行目）へ変換している。状態「Ｂ１」から状態「Ｂ２」の遷移から３行目〜９行目へ変換している。状態「Ｂ２」から状態「Ｂ１」の遷移から１２行目〜１６行目へ変換している。
【００６３】
図１０は、本実施の形態に係るテストケース生成部１２５によるテストケース生成処理の一例を示すフローチャートである。
図１１は、本実施の形態に係るテストケース生成処理により生成されたテストケース１６０の一例を示す図である。
【００６４】
図１０及び図１１を用いて、図３のＳ１０４におけるテストケース生成部１２５によるテストケース生成処理について、具体例を用いて説明する。
テストケース生成部１２５は、状態遷移経路記憶部１２４から状態遷移経路群（状態遷移経路１２３１の全て）を取り出す。テストケース生成部１２５は、処理対象の状態遷移経路について、他の状態遷移経路１２３１に包含されている冗長な状態遷移経路１２３１を削除する正規化を実行する。テストケース生成部１２５は、正規化の結果、残った状態遷移経路１２３１から構成される状態遷移経路群を、テストケース１６０として生成する。この正規化手順について図１０に示す。また、正規化手順により状態遷移経路記憶部１２４に記憶されている状態遷移経路１２３１を正規化した結果（テストケース１６０）を図１１に示す。
【００６５】
Ｓ２０１において、テストケース生成部１２５は、状態遷移経路記憶部１２４から全ての状態遷移経路１２３１を取り出し、時相論理式（組合せ）１２１１と対応する状態遷移経路１２３１とを対応付けた検証対象表に格納する。この検証対象表は、例えば、図７に示す状態遷移経路群と同様の構成である。
Ｓ２０２において、テストケース生成部１２５は、検証対象表の全ての状態遷移経路１２３１に対して処理を実施したかを処理装置により判定する。
Ｓ２０２においてＹｅｓの場合、処理を終了する。
Ｓ２０２においてＮｏの場合、Ｓ２０３に進む。
【００６６】
Ｓ２０３において、テストケース生成部１２５は、検証対象表から処理の対象となる状態遷移経路（以下、処理対象状態遷移経路とする）を選択する。
Ｓ２０４において、テストケース生成部１２５は、処理対象状態遷移経路が、現在の検証対象表の他の状態遷移経路に「遷移元状態」、「遷移先状態」が全て含まれているかを処理装置により判定する。
【００６７】
例えば、処理対象状態遷移経路が番号１に対応する状態遷移経路１２３１の場合、処理対象状態遷移経路は「遷移元の状態：Ａ１」−「遷移先の状態：−」，「遷移元の状態：Ｂ１」−「遷移先の状態：−」である。これは、番号２に対応する状態遷移経路１２３１「遷移元の状態：Ａ１」−「遷移先の状態：−」、「遷移元の状態：Ｂ１」−「遷移先の状態：Ｂ２」に含まれる。よって、テストケース生成部１２５は、番号１に対応する状態遷移経路１２３１は、他の状態遷移経路１２３１に含まれると判定する。
【００６８】
また、処理対象状態遷移経路が番号２に対応する状態遷移経路１２３１の場合、処理対象状態遷移経路は「遷移元の状態：Ａ１」−「遷移先の状態：−」、「遷移元の状態：Ｂ１」−「遷移先の状態：Ｂ２」である。これは、番号３に対応する状態遷移経路１２３１「遷移元の状態：Ａ１」−「遷移先の状態：−」、「遷移元の状態：Ｂ１」−「遷移先の状態：Ｂ２」、「遷移元の状態：Ｂ２」−「遷移先の状態：Ｂ３」に含まれる。よって、テストケース生成部１２５は、番号２に対応する状態遷移経路１２３１は、他の状態遷移経路１２３１に含まれると判定する。
【００６９】
このような処理を実行することにより、番号１〜５に対応する状態遷移経路１２３１を処理対象状態遷移経路とした場合は、すべて他の状態遷移経路１２３１に含まれると判定され、検証対象表から削除されることになる。
【００７０】
ここで、処置対象状態遷移経路が他の状態遷移経路１２３１に含まれないと判定される場合について説明する。
番号６の状態遷移経路１２３１が処理対象状態遷移経路の場合、上述したように、番号１〜５に対応する状態遷移経路１２３１は既に検証対象表から削除されていることになる。
この状態で、処理対象状態遷移経路である番号６に対応する状態遷移経路１２３１は、「遷移元の状態：Ａ１」−「遷移先の状態：Ａ２」、「遷移元の状態：Ｂ１」−「遷移先の状態：Ｂ２」、「遷移元の状態：Ｂ２」−「遷移先の状態：Ｂ３」であるため、他のどの状態遷移経路１２３１にも含まれない判定される。
よって、番号６の状態遷移経路１２３１が処理対象状態遷移経路の場合は、Ｓ２０４においてＮｏとなる。
【００７１】
Ｓ２０４においてＹｅｓの場合、Ｓ２０５に進む。
Ｓ２０４においてＮｏの場合、Ｓ２０２に戻り、次の処理対象状態遷移経路について処理を繰り返す。
【００７２】
Ｓ２０５において、テストケース生成部１２５は、現在の検証対象表から処理対象状態遷移経路のレコードを削除する。
以上で、テストケース生成部１２５によるテストケース生成処理の説明を終わる。
【００７３】
図１１は、テストケース生成部１２５によるテストケース生成処理の結果、生成されたテストケース１６０である。
ここで、テストケース１６０は、番号６の状態遷移経路と番号９の状態遷移経路とがテストケースとなる。図１１に示すテストケース１６０は、経路が重複せず、かつ、二並行状態組合せを網羅するテストケースとなる。
【００７４】
以上のように、テストケース生成部１２５は、状態遷移経路群のうち処理の対象となる処理対象状態遷移経路（対象状態遷移経路の一例）が、状態遷移経路群の処理対象状態遷移経路以外の状態遷移経路に含まれることを「所定の条件」として、処理対象状態遷移経路を状態遷移経路群から削除する。
【００７５】
「状態組み合わせ網羅」からテストケースを生成すると順列は膨大になり、正しいテストケース導出には、イベントの順序関係等による起きえない遷移の除外など、人手によるミス混入の可能性がある。
しかし、本実施の形態に係るテストケース生成装置１００によれば、経路が重複せず、かつ、二並行状態組合せを網羅するテストケースを自動的に生成することができるので、ミスが防止でき、二並行状態組合せを考慮するとともにサイズの小さいテストケースを生成することができる。
【００７６】
実施の形態２．
本実施の形態では、主に、実施の形態１と異なる点について説明する。
本実施の形態において、実施の形態１で説明した構成部と同様の機能を有する構成部については同一の符号を付し、その説明を省略する場合がある。
【００７７】
実施の形態１では、異なる２つの並行なサブ状態からそれぞれ１つの「状態」を取出した「二並行状態のすべての組合せ」について、「いつか指定した二並行状態が同時におきる」を満たす状態遷移経路１２３１をテストケース１６０として生成していた。
本実施の形態では、異なる２つの並行なサブ状態からそれぞれ１つの「状態遷移」を取出した「２つの状態遷移の順列」について、「状態遷移１が起きた直後に状態遷移２がおきる」を満たす状態遷移経路１２３１をテストケース１６０として生成する場合について説明する。
【００７８】
図１２は、本実施の形態に係るテストケース生成装置１０１のブロック構成の一例を示す図である。
テストケース生成装置１０１は、複数の並行なサブ状態を含む状態遷移モデル１５０について、二並行状態遷移の順列を網羅するテストケース１６０を自動生成する装置である。
図１２において、テストケース生成装置１０１は、時相論理式（組合せ）生成部１２１に代わって、時相論理式（順列）生成部１２１ａを有する。また、時相論理式（組合せ）記憶部１２２に代わって、時相論理式（順列）記憶部１２２ａを有する。時相論理式（順列）記憶部１２２ａは、時相論理式（順列）生成部１２１ａにより生成された時相論理式（順列）１２１１ａを記憶する。
【００７９】
次に、動作について説明する。
図１３は、本実施の形態に係るテストケース生成装置１０１におけるテストケース生成方法（処理、工程）の動作の一例を示すフローチャートである。図１３を用いて、実施の形態２におけるテストケース生成処理のフローの一例について説明する。
【００８０】
図１３において、Ｓ３０１，Ｓ３０３〜Ｓ３０５の処理は、実施の形態１で説明したＳ１０１，Ｓ１０３〜Ｓ１０５の処理と同様である。本実施の形態におけるテストケース生成処理は、実施の形態１で説明した図３の＜時相論理式（組合せ）生成処理（工程）：Ｓ１０２＞を、＜時相論理式（順列）生成処理（工程）：Ｓ３０２＞に代えた処理である。
【００８１】
Ｓ３０２において、時相論理式（順列）生成部１２１ａは、異なる２つの並行なサブ状態からそれぞれ１つの状態を取出した二並行状態の全組合せについて、「いつか指定した二並行状態が同時におきる」を意味する時相論理式（組合せ）を生成する。時相論理式（組合せ）は二並行状態の全組合せにおいて生成する。例えば、サブ状態Ａが２状態、サブ状態Ｂが３状態保有している場合、６個の時相論理式（組合せ）が生成される。この処理は、図３のＳ１０２の時相論理式（組合せ）生成処理と同様である。
【００８２】
時相論理式（順列）生成部１２１ａは、時相論理式（順列）生成処理において、入力された状態遷移モデル１５０ａが有する異なる２つの並行なサブ状態からそれぞれ１つの状態遷移を取出し、「状態遷移１が起きた直後に状態遷移２が起きる」を意味する時相論理式（順列）を生成する。
時相論理式（順列）生成部１２１ａは、入力された状態遷移モデル１５０ａにおいて、取り出し得る異なる２つのサブ状態に属する２つの並行状態の全ての組合せについて時相論理式（順列）を生成する。
【００８３】
図１４は、本実施の形態に係るテストケース生成処理の入力となる状態遷移モデル１５０ａの一例を示す図である。
状態遷移モデル１５０ａのサブ状態Ａ，Ｂは、実施の形態１と同様にＵＭＬのステートマシン図Ａ，Ｂで記述する。サブ状態は状態遷移を開始する状態である初期状態を１つ、初期状態以外の状態を少なくとも１つ、状態遷移を複数持つ。遷移に対しては遷移イベントを１つ持つ。サブ状態Ａ，Ｂは、入れ子状態でなく、並行に動作する２つのステートマシン図Ａ，Ｂとする。
【００８４】
入力となる状態遷移モデル１５０ａのステートマシン図Ａは、初期状態「Ａ１」から開始する。状態「Ａ１」においてイベント「ｅ１」により状態「Ａ２」へ、イベント「ｅ４」により状態「Ａ３」へ遷移する。状態「Ａ２」においてイベント「ｅ２」により状態「Ａ３」へ遷移する。状態「Ａ３」においてイベント「ｅ３」により状態「Ａ１」へ遷移する。
状態遷移モデル１５０ａのステートマシン図Ｂは、初期状態「Ｂ１」から開始する。状態「Ｂ１」においてイベント「ｅ５」により状態「Ｂ２」へ遷移する。状態「Ｂ２」においてイベント「ｅ６」により状態「Ｂ１」へ遷移する。
遷移イベントに付随しているカッコ内の値は、直後に遷移した状態遷移を識別する状態遷移識別子である。
【００８５】
時相論理式（順列）生成部１２１ａは、異なる２つのサブ状態から取り出し得る異なる二並行状態遷移の全順列を抽出し、時相論理式（順列）１２１１ａを生成する。
具体的には、時相論理式（順列）生成部１２１ａは、ステートマシン図Ａの状態「Ａ１」、「Ａ２」、「Ａ３」とステートマシン図Ｂの状態「Ｂ１」、「Ｂ２」に対して、各ステートマシン図から１つ取り出した状態遷移の順列の全てを抽出する。
【００８６】
図１５は、本実施の形態に係る時相論理式（順列）生成部１２１ａにより抽出された状態遷移の順列例を示す図（状態遷移順列図）である。
図１５において、「先に遷移する遷移の値」列はステートマシン図Ａが取りうる状態遷移を、「後に遷移する遷移の値」列はステートマシン図Ｂが取りうる状態遷移を意味する。各行は状態遷移の順列（状態遷移順列）を意味する。図１５の状態遷移順列図では、１６つの抽出された状態遷移順列を示している。
時相論理式（順列）生成部１２１ａは、状態遷移モデル１５０ａを取得し、サブ状態Ａに含まれる第１状態遷移（ｅ１（Ｘ１）〜ｅ４（Ｘ４））と、サブ状態Ｂに含まれる前記第２状態遷移（ｅ５（Ｘ５）〜ｅ６（Ｘ６））との順列を複数生成する（図１５参照）。そして、時相論理式（順列）生成部１２１ａは、生成した複数の順列の順列毎に「状態遷移１が起きた直後に状態遷移２が起きる」（第１状態遷移の直後に第２状態遷移が起きる）ことを意味する時相論理式（順列）１２１１ａ（順列時相論理式）を生成する順列生成部の一例である。
【００８７】
次に、図１３のＳ３０２における時相論理式（順列）生成部１２１ａによる時相論理式（順列）生成処理について、具体例を用いて説明する。
時相論理式（順列）生成部１２１ａは、時相論理式（順列）１２１１ａ（二並行状態遷移順列網羅時相論理式）を生成するために、時相論理式（順列）テンプレート（二並行状態遷移順列網羅時相論理式テンプレート）を用いる。
【００８８】
時相論理式（順列）テンプレートは、「状態遷移１が起きた直後に状態遷移２が起きる」を意味する時相論理式（順列）で、演算子や利用する変数名は固定とし、二並行状態遷移の部分を可変としているものである。
時相論理式（順列）テンプレートも時相論理式（組合せ）テンプレートと同様に、予めテストケース生成装置１０１の記憶装置に設定されている。
【００８９】
具体的には、時相論理式（順列）テンプレートは、「（（ｔｒａｎｓ２＿ｖａｒ！＝ｔｒａｎｓ２）Ｕ（（ｔｒａｎｓ１＿ｖａｒ＝＝ｔｒａｎｓ１）＆＆（ｔｒａｎｓ２＿ｖａｒ！＝ｔｒａｎｓ２）））＆＆＜＞（ｔｒａｎｓ２＿ｖａｒ＝＝ｔｒａｎｓ２）」である。
【００９０】
「ｔｒａｎｓ１＿ｖａｒ」、「ｔｒａｎｓ２＿ｖａｒ」は、状態遷移経路生成部１２３で用いられるモデル検査ツールにおいて、ステートマシン図Ａ、ステートマシン図Ｂの状態遷移の値を格納する変数である。
「（（ｔｒａｎｓ２＿ｖａｒ！＝ｔｒａｎｓ２）Ｕ（（ｔｒａｎｓ１＿ｖａｒ＝＝ｔｒａｎｓ１）＆＆（ｔｒａｎｓ２＿ｖａｒ！＝ｔｒａｎｓ２）））＆＆＜＞（ｔｒａｎｓ２＿ｖａｒ＝＝ｔｒａｎｓ２）」の「ｔｒａｎｓ１」に図１５の「先に遷移する遷移の値」列に設定されている値を、「ｔｒａｎｓ２」に図１５の「後に遷移する遷移の値」列に設定されている値を当てはめることで、二並行状態遷移の順列毎に時相論理式（順列）（二並行状態遷移順列網羅時相論理式）の生成を可能とする。
【００９１】
時相論理式（順列）生成の具体例を示す。図１５の１行目において、「先に遷移する遷移の値」列は「Ｘ１」、「後に遷移する遷移の値」列は「Ｙ１」のため、時相論理式（順列）テンプレート「（（ｔｒａｎｓ２＿ｖａｒ！＝ｔｒａｎｓ２）Ｕ（（ｔｒａｎｓ１＿ｖａｒ＝＝ｔｒａｎｓ１）＆＆（ｔｒａｎｓ２＿ｖａｒ！＝ｔｒａｎｓ２）））＆＆＜＞（ｔｒａｎｓ２＿ｖａｒ＝＝ｔｒａｎｓ２）」の「ｔｒａｎｓ１」に「Ｘ１」を、「ｔｒａｎｓ２」に「Ｙ１」を当てはめる。これにより、時相論理式（順列）「（（ｔｒａｎｓ２＿ｖａｒ！＝Ｙ１）Ｕ（（ｔｒａｎｓ１＿ｖａｒ＝＝Ｘ１）＆＆（ｔｒａｎｓ２＿ｖａｒ！＝Ｙ１）））＆＆＜＞（ｔｒａｎｓ２＿ｖａｒ＝＝Ｙ１）」が得られる。図１５の各行（各状態遷移の順列）に対し、生成した時相論理式（順列）を図１６に示す。
【００９２】
図１６は、本実施の形態に係る時相論理式（順列）生成部１２１ａにより生成された時相論理式（順列）群の一例を示す図である。図１６に示す１６つの時相論理式（順列）１２１１ａを時相論理式（順列）群と呼ぶ場合がある。
【００９３】
状態遷移モデル１５０ａが３つ以上のステートマシン図を有しており、状態遷移モデル取得部１１１に３つ以上のステートマシン図に入力された場合は、ステートマシン図群から取り出した２つのサブ状態の組合せに対して、時相論理式（順列）生成処理を適用する。例えば、入力された状態遷移モデル１５０ａがステートマシン図Ａ、ステートマシン図Ｂ、ステートマシン図Ｃであった場合、ステートマシン図Ａとステートマシン図Ｂ、ステートマシン図Ａとステートマシン図Ｃ、ステートマシン図Ｂとステートマシン図Ｃの組合せに対して、時相論理式（順列）生成処理を適用する。
【００９４】
Ｓ３０２において、時相論理式（順列）生成部１２１ａが時相論理式（順列）群を生成すると、実施の形と同様に、Ｓ３０３において状態遷移経路生成処理を実行する。すなわち、状態遷移経路生成部１２３は、モデル検査ツールを利用して、時相論理式（順列）１２１１ａを満たす最短の状態遷移経路１２３１を生成する。状態遷移経路生成部１２３は、時相論理式（順列）生成部１２１ａにより生成された時相論理式（順列）１２１１ａに基づいて、時相論理式（順列）１２１１ａ毎に、時相論理式（順列）１２１１ａを満たす状態遷移の経路を状態遷移経路１２３１として生成する。このように、時相論理式（順列）１２１１ａ毎に生成される時相論理式（順列）１２１１ａを満たす状態遷移経路１２３１は順列時状態遷移経路の一例である。
【００９５】
そして、Ｓ３０４のテストケース生成処理において、テストケース生成部１２５は、生成された状態遷移経路１２３１のそれぞれについて、他の状態遷移経路１２３１に包含されている冗長な状態遷移経路１２３１を削除する正規化を実行し、テストケース１６０を生成する。このように、テストケース生成部１２５は、時相論理式（順列）１２１１ａ毎の状態遷移経路１２３１（順列時状態遷移経路）に基づいて、テストケース１６０を生成する。
Ｓ３０５のテストケース表示処理において、テストケース表示部１３１は、テストケース生成部１２５により生成されたテストケース１６０を表示装置などに表示する。
【００９６】
以上のように、本実施の形態に係るテストケース生成装置は、異なる２つの並行なサブ状態からそれぞれ１つの状態を取出した二並行状態のすべての組合せについて、「いつか指定した二並行状態が同時におきる」を意味する時相論理式を生成する二並行状態組合せ網羅時相論理式生成部に代えて、異なる２つの並行なサブ状態からそれぞれ１つの状態遷移を取出した２つの状態遷移の順列について、「状態遷移１が起きた直後に状態遷移２が起きる」を意味する時相論理式（順列）を生成する二状態遷移順列網羅時相論理式生成部を備える。
【００９７】
以上のように、本実施の形態に係るテストケース生成装置では、時相論理式（順列）生成部１２１ａを備えているので、二状態遷移順列網羅のテストケース生成が可能となる。
【００９８】
実施の形態３．
本実施の形態では、主に、実施の形態１，２と異なる点について説明する。
本実施の形態において、実施の形態１，２で説明した構成部と同様の機能を有する構成部については同一の符号を付し、その説明を省略する場合がある。
【００９９】
図１７は、本実施の形態に係るテストケース生成装置１０２のブロック構成の一例を示す図である。図１７を用いて、本実施の形態におけるテストケース生成装置１０２について説明する。
【０１００】
図１７に示すように、テストケース生成装置１０２は、時相論理式（組合せ）１２１１を生成して記憶する構成（時相論理式（組合せ）生成部１２１、時相論理式（組合せ）記憶部１２２）と、時相論理式（順列）１２１１ａを生成して記憶する構成（時相論理式（順列）生成部１２１ａ、時相論理式（順列）記憶部１２２ａ）とを備え、さらに、生成時相論理式切替部１２６を備える。
【０１０１】
実施の形態１では二並行状態組合せ網羅のテストケースを生成する形態について説明し、実施の形態２では二状態遷移順列網羅のテストケースを生成する形態について説明した。しかし、本実施の形態では、どちらのテストケースを生成するか選択することができる構成について説明する。
【０１０２】
図１８は、本実施の形態に係るテストケース生成装置１０２におけるテストケース生成方法（処理、工程）の動作の一例を示すフローチャートである。図１８を用いて、本実施の形態におけるテストケース生成処理のフローの一例について説明する。
【０１０３】
図１８において、Ｓ４０１，Ｓ４０３〜Ｓ４０５の処理は、実施の形態１で説明したＳ１０１，Ｓ１０３〜Ｓ１０５の処理と同様である。また、＜時相論理式（組合せ）生成処理（工程）：Ｓ４０２ｂ＞は実施の形態１で説明したＳ１０２と同様であり、＜時相論理式（順列）生成処理（工程）：Ｓ４０２ｃ＞は実施の形態２で説明したＳ３０２と同様である。
本実施の形態に係るテストケース生成処理では、Ｓ４０１の次に、Ｓ４０２ａの生成時相論理式切替処理を備える。
【０１０４】
Ｓ４０２ａにおいて、生成時相論理式切替部１２６は、＜時相論理式（組合せ）生成処理（工程）：Ｓ４０２ｂ＞を実行するか、＜時相論理式（順列）生成処理（工程）：Ｓ４０２ｃ＞を実行するかを切り替えることができる。例えば、生成時相論理式切替部１２６は、Ｓ４０１で状態遷移モデルが入力されると、時相論理式（組合せ）生成処理を実行するか時相論理式（順列）生成処理を実行するかを利用者に選択させる選択画面を表示装置などに表示してもよい。そして、生成時相論理式切替部１２６は、選択画面から入力された選択結果に基づいて、時相論理式（組合せ）生成処理（Ｓ４０２ｂ）あるいは時相論理式（順列）生成処理（Ｓ４０２ｃ）を実行するものとしてもよい。
【０１０５】
あるいは、生成時相論理式切替部１２６は、入力された状態遷移モデルの状態遷移の数を計数し、状態遷移の数が閾値以下の場合は時相論理式（順列）生成処理（Ｓ４０２ｃ）を実行し、状態遷移の数が閾値より多い場合は時相論理式（組合せ）生成処理（Ｓ４０２ｂ）を実行するとしてもよい。
【０１０６】
このように、生成時相論理式切替部１２６は、入力された状態遷移モデル１５０ａを時相論理式（組合せ）生成部１２１と時相論理式（順列）生成部１２１ａとのいずれに入力するかを判定し、判定結果に基づいて時相論理式（組合せ）生成部１２１と時相論理式（順列）生成部１２１ａとのいずれに入力するかを切り替える切替部の一例である。
【０１０７】
以上のように、本実施の形態に係るテストケース生成装置１０２は、異なる２つの並行なサブ状態からそれぞれ１つの状態を取出した二並行状態のすべての組合せについて、「いつか指定した二並行状態が同時におきる」を意味する時相論理式（組合せ）を生成する二並行状態組合せ網羅時相論理式生成部と、異なる２つの並行なサブ状態からそれぞれ１つの状態遷移を取出した２つの状態遷移の順列について、「状態遷移１が起きた直後に状態遷移２が起きる」を意味する時相論理式（順列）を生成する二状態遷移順列網羅時相論理式生成部と、生成する時相論理式を切り替える生成時相論理式切替部とを備えているので、きめ細かくテストケースを生成することができる。
【０１０８】
以上に説明したように、実施の形態１〜３に係るテストケース生成装置によれば、並行であるサブ状態を含んだ状態モデルを入力として、「いつか指定した二並行状態が同時に起きる」を意味する時相論理式（組合せ）を自動生成し、「二並行状態組み合わせ」を網羅したテストケースが生成可能となる。
【０１０９】
さらに、並行であるサブ状態を含んだ状態モデルを入力として、「状態遷移１が起きた直後に状態遷移２が起きる」を意味する時相論理式（順列）を自動生成し、「二並行状態遷移順列」を網羅したテストケースが生成可能となる。
【０１１０】
また、テストケース生成時に「二並行状態組み合わせ」または「二並行状態遷移順列」の選択が可能である。
【０１１１】
なお、テストケース生成装置の機能ブロックの構成は、上記の実施の形態１〜３において説明したブロック構成に限られない。他の機能ブロック構成でも構わない。
例えば、図１において、テストケース生成装置は、状態遷移モデル取得部、時相論理式（組合せ）生成部、時相論理式（組合せ）記憶部、状態遷移経路生成部、状態遷移経路記憶部、テストケース生成部、テストケース表示部を備えている。しかし、このようなブロック構成に限らず、例えば、時相論理式（組合せ）生成部、時相論理式（組合せ）記憶部、状態遷移経路生成部、状態遷移経路記憶部をひとつの機能ブロックとしてもよい。あるいは、テストケース生成部、テストケース表示部をひとつの機能ブロックとしてもよい。
【０１１２】
機能ブロックは、矛盾しない範囲であれば必要に応じて種々の変更が可能であり、上記のブロック構成は任意である。つまり、実施の形態１〜３で説明した機能ブロックを、矛盾しない範囲で、テストケース生成装置にどのように分散して配置しても構わない。
【０１１３】
また、実施の形態１〜３では、テストケース生成装置を１つの装置として説明したが、複数の装置から構成されたシステムでもよい。例えば、「〜記憶部」はまとめて１つのデータベースサーバとし、「〜記憶部」以外の機能を有するテストケース生成装置とデータベースサーバとはネットワークで接続され、実施の形態１〜３で説明したテストケース生成装置の機能を有するテストケース生成システムを構成してもよい。実施の形態１〜３で説明した機能ブロックを、矛盾しない範囲で、テストケース生成システムにどのように分散して配置しても構わない。
【０１１４】
以上、本発明の実施の形態について説明したが、これらの実施の形態のうち、２つ以上を組み合わせて実施しても構わない。あるいは、これらの実施の形態のうち、１つを部分的に実施しても構わない。あるいは、これらの実施の形態のうち、２つ以上を部分的に組み合わせて実施しても構わない。
なお、以上の実施の形態は、本質的に好ましい例示であって、本発明、その適用物や用途の範囲を制限することを意図するものではなく、矛盾しない範囲であれば必要に応じて種々の変更が可能である。
【符号の説明】
【０１１５】
１００１０１，１０２  テストケース生成装置、１１０  取得部、１１１  状態遷移モデル取得部、１２０  テストケース生成処理部、１２１  時相論理式（組合せ）生成部、１２１ａ  時相論理式（順列）生成部、１２２  時相論理式（組合せ）記憶部、１２２ａ  時相論理式（順列）記憶部、１２３  状態遷移経路生成部、１２４  状態遷移経路記憶部、１２５  テストケース生成部、１２６  生成時相論理式切替部、１３０  表示部、１３１  テストケース表示部、１５０，１５０ａ  状態遷移モデル、１６０  テストケース、９０１  演算装置、９０２  外部記憶装置、９０３  主記憶装置、９０４  通信装置、９０５  入出力装置、１２１１  時相論理式（組合せ）、１２１１ａ  時相論理式（順列）、１２３１  状態遷移経路。
【図１】
2015225422.tif 000003
【図２】
2015225422.tif 000004
【図３】
2015225422.tif 000005
【図４】
2015225422.tif 000006
【図５】
2015225422.tif 000007
【図６】
2015225422.tif 000008
【図７】
2015225422.tif 000009
【図８】
2015225422.tif 000010
【図９】
2015225422.tif 000011
【図１０】
2015225422.tif 000012
【図１１】
2015225422.tif 000013
【図１２】
2015225422.tif 000014
【図１３】
2015225422.tif 000015
【図１４】
2015225422.tif 000016
【図１５】
2015225422.tif 000017
【図１６】
2015225422.tif 000018
【図１７】
2015225422.tif 000019
【図１８】
2015225422.tif 000020