"ソフトウェア設計におけるシーケンス図と当該シーケンス図に基づいて作成された状態遷移表との整合性を検証するソフトウェア設計検証装置であって、少なくとも1つ以上の前記シーケンス図のデータを格納するシーケンス図格納手段と、前記シーケンス図に含まれた前記整合性が検証される検証対象オブジェクトが有する前記状態遷移表のデータを格納する状態遷移表格納手段と、前記シーケンス図格納手段に格納された前記シーケンス図のデータに基づいて、当該シーケンス図に含まれる前記検証対象オブジェクト以外の非検証対象オブジェクトの動作を実現する検証ソフトウェアを生成する検証ソフトウェア生成手段と、前記状態遷移表格納手段に格納された前記状態遷移表のデータに基づいて、前記検証対象オブジェクトの動作を実現する検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段と、前記検証ソフトウェアと前記検証対象ソフトウェアとに対してビルドを行い、実行可能な実行モジュールを生成する実行モジュール生成手段と、前記実行モジュール生成手段にて生成された前記実行モジュールを実行し、前記シーケンス図の内容と前記状態遷移表の内容との前記整合性の検証を行う検証実行手段と、を備える、ソフトウェア設計検証装置。前記検証ソフトウェア生成手段は、前記シーケンス図に含まれる前記検証対象オブジェクトを特定する検証対象オブジェクト特定手段と、前記シーケンス図の内容を実行する前の前記検証対象オブジェクトの状態である、前記シーケンス図に含まれた初期状態を抽出する初期状態抽出手段と、前記シーケンス図に含まれるメッセージ情報を抽出するメッセージ情報抽出手段と、を備え、前記検証対象オブジェクト特定手段にて特定された前記検証対象オブジェクト、前記初期状態抽出手段にて抽出された前記初期状態、および前記メッセージ情報抽出手段にて抽出された前記メッセージ情報によって前記検証ソフトウェアを作成することを特徴とする、請求項1に記載のソフトウェア設計検証装置。前記検証ソフトウェア生成手段は、前記初期状態を前記検証ソフトウェアに設定する初期状態設定手段と、前記非検証対象オブジェクトから前記検証対象オブジェクトに最初に送信されるシーケンス開始メッセージを前記検証ソフトウェアに設定するシーケンス開始メッセージ送信設定手段と、前記整合性の検証の実行を前記検証ソフトウェアに設定する整合性検証手段と、をさらに備えることを特徴とする、請求項2に記載のソフトウェア設計検証装置。前記検証ソフトウェア生成手段は、前記検証対象オブジェクトから呼び出される第1のコール関数を前記検証ソフトウェアに設定する第1のコール関数設定手段をさらに備え、前記第1のコール関数設定手段は、前記検証対象オブジェクトの動作結果の保持する旨を前記検証ソフトウェアに設定する動作結果保持設定手段と、前記非検証対象オブジェクトから前記検証対象オブジェクトに第1のメッセージを送信する旨を前記検証ソフトウェアに設定する第1のメッセージ送信設定手段と、を備えることを特徴とする、請求項2または3に記載のソフトウェア設計検証装置。前記検証対象ソフトウェア生成手段は、前記状態遷移表に含まれ、前記非検証対象オブジェクトから前記検証対象オブジェクトに入力されるメッセージである入力イベントを抽出する入力イベント抽出手段と、前記状態遷移表に含まれ、前記検証対象オブジェクトの現在の状態を示す現在状態を抽出する現在状態抽出手段と、前記入力イベントと前記現在状態とに基づく処理内容を抽出する処理内容抽出手段と、前記処理内容に基づき、前記現在状態を変更した変更状態を抽出する変更状態抽出手段と、前記処理内容に基づき、前記変更状態の抽出の際に、前記検証対象オブジェクトから前記非検証対象オブジェクトに送信される第2のメッセージを抽出する第2のメッセージ抽出手段と、を備え、前記入力イベント抽出手段にて抽出された前記入力イベント、前記現在状態抽出手段にて抽出された前記現在状態、前記処理内容抽出手段にて抽出された前記処理内容、前記変更状態抽出手段にて抽出された前記変更状態、および前記第2のメッセージ抽出手段にて抽出された前記第2のメッセージによって、前記検証対象ソフトウェアを生成することを特徴とする、請求項1に記載のソフトウェア設計検証装置。前記検証対象ソフトウェア生成手段は、前記検証オブジェクトから呼び出される第2のコール関数を前記検証対象ソフトウェアに設定する第2のコール関数設定手段をさらに備え、前記第2のコール関数設定手段は、前記現在状態を条件判定として前記検証対象ソフトウェアに設定する状態判定設定手段を含み、前記状態判定設定手段は、前記現在状態を前記変更状態に変更する旨を前記検証対象ソフトウェアに設定する状態変更設定手段と、前記第2のメッセージを前記検証対象ソフトウェアに設定する第2のメッセージ送信設定手段と、を備えることを特徴とする、請求項5に記載のソフトウェア設計検証装置。前記検証実行手段は、保持された前記検証対象オブジェクトの動作結果が前記メッセージ情報に含まれ、かつ、前記動作結果の保持順序が前記メッセージ情報の前記シーケンス図における処理順序と一致することによって、前記シーケンス図と前記状態遷移表との前記整合性があると判定することを特徴とする、請求項4に記載のソフトウェア設計検証装置。コンピュータに請求項1に記載のソフトウェア設計検証装置における前記検証ソフトウェアを実行させるためのプログラムであって、a前記シーケンス図ごとにテスト関数を設定する手順と、b前記検証対象オブジェクトから呼び出される第1のコール関数を設定する手順と、を備え、前記手順aは、c前記検証対象オブジェクトの初期状態を設定する手順と、d前記非検証対象オブジェクトから前記検証対象オブジェクトに最初に送信されるシーケンス開始メッセージを設定する手順と、e前記整合性の検証を実行する手順と、を含み、前記手順bは、f前記検証対象オブジェクトの動作結果を保持する手順と、g前記非検証対象オブジェクトから前記検証対象オブジェクトに第1のメッセージを送信する手順と、を含み、上記手順a~gをコンピュータに実行させることを特徴とする、検証プログラム。前記初期状態は前記シーケンス図に含まれ、前記シーケンス開始メッセージ、前記第2のコール関数、前記動作結果、および前記第1のメッセージは、前記シーケンス図に含まれるメッセージ情報に基づくメッセージ名が付されることを特徴とする、請求項8に記載の検証プログラム。コンピュータに請求項1に記載のソフトウェア設計検証装置における前記検証対象ソフトウェアを実行させるためのプログラムであって、h前記検証オブジェクトから呼び出される第2のコール関数を設定する手順を含み、前記手順hは、i前記検証対象オブジェクトの現在の状態を示す現在状態を条件判定として処理を行う手順を含み、前記手順iは、j前記現在状態を変更する手順と、k前記検証対象オブジェクトから前記非検証対象オブジェクトに送信される第2のメッセージを送信する手順と、をさらに含み、上記手順h~kをコンピュータに実行させることを特徴とする、検証対象プログラム。前記手順hにおける前記第2のコール関数は、前記状態遷移表に含まれた前記非検証対象オブジェクトから前記検証対象オブジェクトに入力されるメッセージである入力イベントが付され、前記手順iにおける前記現在状態は、前記状態遷移表に含まれる現在の状態が付され、前記手順jにおける変更する状態は、前記状態遷移表に含まれる状態が付され、前記手順kにおける前記第2のメッセージは、前記状態遷移表に含まれるメッセージ名が付されることを特徴とする、請求項10に記載の検証対象プログラム。特許文献1のソフトウェア自動生成装置では、仕様決定表を入力して業務システムで動作するソフトウェアを出力している。仕様決定表と生成したソフトウェアとの整合性検証は試験工程で行われるが、試験工程で行われる試験は試験環境や試験に必要なソフトウェアや業務システムを準備する必要があり時間とコストがかかる。また、生成したソフトウェアに不具合が見つかると、仕様決定表における誤りの有無の確認が必要となり、不具合修正のための手戻りが大きくなるという問題がある。また、特許文献2のソフトウェア検証装置では、インターフェースシーケンス定義とソフトウェア本体とソフトウェアモジュールとを入力としてソフトウェアモジュールの呼び出しシーケンスの正当性を確認している。インターフェースシーケンス定義とソフトウェアモジュールの呼び出しシーケンスとの整合性検証には、ソフトウェア本体とソフトウェアモジュールの開発の完了を待つ必要があり、特許文献1と同様に、不具合を発見するまでに時間がかかるため、不具合修正のための手戻りが大きくなるという問題がある。このように、ソフトウェアの開発において、出力となる作業成果物特許文献1では生成ソフトウェア、特許文献2ではソフトウェアモジュールの呼び出しシーケンスが、入力となる作業成果物特許文献1では仕様決定表、特許文献2ではインターフェースシーケンス定義の内容を正しく反映しているか否かの整合性検証が必要となるが、その整合性確認検証を開始するまでに時間がかかり整合性検証を実施するまでの準備に時間がかかり、また、不具合が見つかったときの手戻りが大きくなり修正コストが大きくなるという問題がある。本発明は、これらの問題を解決するためになされたものであり、整合性検証を自動的に行い、手戻りによる修正コストを低減することが可能なソフトウェア設計検証装置ならびにそれに用いる検証プログラムおよび検証対象プログラムを提供することを目的とする。上記の課題を解決するために、本発明によるソフトウェア設計検証装置は、ソフトウェア設計におけるシーケンス図と当該シーケンス図に基づいて作成された状態遷移表との整合性を検証するソフトウェア設計検証装置であって、少なくとも1つ以上のシーケンス図のデータを格納するシーケンス図格納手段と、シーケンス図に含まれた整合性が検証される検証対象オブジェクトが有する状態遷移表のデータを格納する状態遷移表格納手段と、シーケンス図格納手段に格納されたシーケンス図のデータに基づいて、当該シーケンス図に含まれる検証対象オブジェクト以外の非検証対象オブジェクトの動作を実現する検証ソフトウェアを生成する検証ソフトウェア生成手段と、状態遷移表格納手段に格納された状態遷移表のデータに基づいて、検証対象オブジェクトの動作を実現する検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段と、検証ソフトウェアと検証対象ソフトウェアとに対してビルドを行い、実行可能な実行モジュールを生成する実行モジュール生成手段と、実行モジュール生成手段にて生成された実行モジュールを実行し、シーケンス図の内容と状態遷移表の内容との整合性の検証を行う検証実行手段とを備える。本発明によると、少なくとも1つ以上のシーケンス図のデータを格納するシーケンス図格納手段と、シーケンス図に含まれた整合性が検証される検証対象オブジェクトが有する状態遷移表のデータを格納する状態遷移表格納手段と、シーケンス図格納手段に格納されたシーケンス図のデータに基づいて、当該シーケンス図に含まれる検証対象オブジェクト以外の非検証対象オブジェクトの動作を実現する検証ソフトウェアを生成する検証ソフトウェア生成手段と、状態遷移表格納手段に格納された状態遷移表のデータに基づいて、検証対象オブジェクトの動作を実現する検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段と、検証ソフトウェアと検証対象ソフトウェアとに対してビルドを行い、実行可能な実行モジュールを生成する実行モジュール生成手段と、実行モジュール生成手段にて生成された実行モジュールを実行し、シーケンス図の内容と状態遷移表の内容との整合性の検証を行う検証実行手段とを備えるため、整合性検証を自動的に行い、手戻りによる修正コストを低減することが可能となる。本発明の実施形態について、図面に基づいて以下に説明する。まず、本実施形態によるソフトウェア設計検証装置110の構成について説明する。図1は、本実施形態によるソフトウェア設計検証装置110の構成の一例を示すブロック図である。図1に示すように、本実施形態によるソフトウェア設計検証装置110は、少なくとも1つ以上のシーケンス図108のデータ以下、単にシーケンス図108とも称するを格納するシーケンス図格納手段101、状態遷移表109のデータ以下、単に状態遷移表109とも称するを格納する状態遷移表格納手段102、シーケンス図格納手段101に格納されたシーケンス図108に基づいて検証ソフトウェアを生成する検証ソフトウェア生成手段103、状態遷移表格納手段102に格納された状態遷移表109から検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段104、生成した検証ソフトウェアと検証対象ソフトウェアとに対してビルドを行い実行可能な実行モジュールを生成する実行モジュール生成手段105、実行モジュール生成手段105にて生成された実行モジュールを実行し、シーケンス図108と状態遷移表109との整合性の検証を実行する検証実行手段106とを備え、ソフトウェア設計検証装置110は、検証実行手段106にて得られた検証結果を表示する検証結果提示手段107に接続される。なお、本実施形態によるソフトウェア設計検証装置110は、プログラムによって図1のブロック図に従って機能化されたパーソナルコンピュータなどの情報端末によって構成され、図1のブロック図の機能が実行される。シーケンス図格納手段101および状態遷移表格納手段102は、磁気ディスク装置図示せずなどの不揮発性の補助記憶装置で構成されており、シーケンス図108と状態遷移表109とがそれぞれに格納されている。また、検証ソフトウェア生成手段103、検証対象ソフトウェア生成手段104、実行モジュール生成手段105、および検証実行手段106は、通常は磁気ディスク装置図示せずなどの不揮発性の補助記憶装置に格納されているが、ソフトウェア設計検証装置110の実行時には主メモリ図示せずに呼び出してCPUによって実行される。また、検証結果提示手段107は、液晶モニタ図示せずなどの外部ディスプレイ装置で構成されている。次に、ソフトウェア設計装置110の動作の概要について説明する。図2は、本実施形態によるソフトウェア設計検証装置110の動作を示すフローチャートである。図2に示すように、ソフトウェア設計検証装置110の実行を開始すると、検証ソフトウェア生成手段103は、シーケンス図格納手段101に格納されているシーケンス図108を読み出しステップS201、読み出したシーケンス図108の内容に基づいて検証ソフトウェアを生成するステップS202。一方、検証対象ソフトウェア生成手段104は、状態遷移表格納手段102に格納されている状態遷移表109を読み出しステップS203、読み出した状態遷移表109の内容に基づいて検証対象ソフトウェアを生成するステップS204。ステップS204の後、実行モジュール生成手段105は、ステップS202にて生成した検証ソフトウェアとステップS204にて生成した検証対象ソフトウェアとに対してビルドを行い、実行モジュールを生成するステップS205。ステップS205の後、検証実行手段106は、ステップS205にて生成した実行モジュールを実行しステップS206、実行結果に基づいてシーケンス図108と状態遷移表109との整合性検証を行うステップS207。ステップS207にて整合性検証が終わると、検証の結果を検証結果提示手段107に表示するステップS208。なお、検証ソフトウェア生成手段103にて生成された検証ソフトウェア、検証対象ソフトウェア生成手段104にて生成された検証対象ソフトウェア、および実行モジュール生成手段105にて生成された実行モジュールは、それぞれ補助記憶装置図示せずに格納される。次に、シーケンス図格納手段101に格納されるシーケンス図108について説明する。図3は、本実施形態によるシーケンス図108の一例を示す図である。図3に示すように、シーケンス図108に含まれるオブジェクト301からオブジェクト303のうち、状態遷移表を持つオブジェクトを検証対象オブジェクト303とする。また、シーケンス図108には、シーケンスを開始する前の検証対象オブジェクト303の初期状態305が書き加えられている。シーケンス図格納手段101には、図3に示すようなシーケンス図108が少なくとも1つ以上格納されている。検証対象オブジェクト303は、上記の通り、状態遷移表を持つオブジェクトである。ソフトウェア設計検証装置110を実行する際には、シーケンス図108に含まれるオブジェクトのうちの1つのオブジェクトを検証対象オブジェクトとして設定し、設定した検証対象オブジェクトが持つ状態遷移表109とシーケンス図108の整合性検証を行う。なお、他の状態遷移表109の整合性検証を行う場合は、整合性検証を行う対象となる状態遷移表109を持つオブジェクトを検証対象オブジェクトとして設定してソフトウェア設計検証装置110を実行する。次に、図3に示すシーケンス図108と検証ソフトウェア生成手段103にて生成される検証ソフトウェアとの関係について説明する。検証ソフトウェア生成手段103は、図3に示すシーケンス図108を読み込み、読み込んだシーケンス図108に基づいて検証ソフトウェアを生成しており、シーケンス図108に含まれるオブジェクト301からオブジェクト303のうち、検証対象オブジェクト303を除いたオブジェクト301およびオブジェクト302非検証対象オブジェクトの動作を実現するソフトウェアを生成する検証ソフトウェアの生成方法については後述する。次に、状態遷移表格納手段102に格納される状態遷移表109について説明する。図4は、本実施形態による状態遷移表109の一例を示す図である。図4に示すように、状態遷移表109は、図3に示すシーケンス図108に含まれるオブジェクト301からオブジェクト303のうちの検証対象オブジェクト303の動作について記述されたものであり、検証対象オブジェクト303の現在の状態現在状態を示す現在状態記述行401と、検証対象オブジェクト303に入力されるメッセージを示すイベント名記述列402とからなる二次元の表形式で記述される。現在状態記述行401に記述される各状態には、図3に示すシーケンス図108に含まれる検証対象オブジェクト303の初期状態305が記述される。また、イベント名記述列402に記述されるイベントは、図3に示すシーケンス図108に含まれ、検証対象オブジェクト303に入力されるメッセージが記述される。処理内容403には、検証対象オブジェクト303の現在の状態と入力されるイベントとに基づいた処理内容が記述されている。例えば、検証対象オブジェクト303の現在の状態がstate1の時にmessage11が入力されると、検証対象オブジェクト303は処理内容403内のセル404の処理内容を実行する。セル404では、現在の状態をstate1からstate2に変更し、かつ、message101を出力するという処理内容が示されている。このセル404の処理内容は、図3に示すシーケンス図108において、オブジェクト301から検証対象オブジェクト303に対してmessage11を送信した後、検証対象オブジェクト303からオブジェクト302にmessage101を送信する内容を示している。また、処理内容403の各セルにおける処理内容を区別することができるように、状態の変更を示すキーワードとしてS:が、出力メッセージを示すキーワードとしてA:が記述されている。また、検証対象オブジェクト303の現在の状態と入力されるイベントとの組合せが存在しないとき、あるいは、組合せが存在しても何も処理しない処理内容の記述がない場合は、処理内容403内のセル405のように空白で示される。また、状態遷移表格納手段102には、図4に示すような状態遷移表109が少なくとも1つ以上格納されている。次に、図4に示す状態遷移表109と検証対象ソフトウェア生成手段104にて生成される検証対象ソフトウェアとの関係について説明する。検証対象ソフトウェア生成手段104は、図4に示す状態遷移表109を読み込み、読み込んだ状態遷移表109に基づいて検証対象ソフトウェアを生成しており、図3に示すシーケンス図108に含まれる検証対象オブジェクト303の動作を実現するソフトウェアを生成している。次に、シーケンス図108と状態遷移表109との整合性検証の考え方について説明する。図3に示すシーケンス図108に基づいて作成された図4に示す状態遷移表109が、シーケンス図108の内容を正しく反映して作成されていれば、検証対象ソフトウェア生成手段104で生成される状態遷移表109の動作を実現する検証対象ソフトウェアを、検証ソフトウェア生成手段103で生成される検証対象オブジェクトを除いたオブジェクト図3のオブジェクト301,302の動作を実現する検証ソフトウェアで制御すると、検証対象ソフトウェアは、図3に示すシーケンス図108の検証対象オブジェクトの記述順序通りにかつ漏れなくメッセージ図3のmessage101,message102を出力する。つまり、検証対象ソフトウェアの動作結果が、シーケンス図108に含まれる検証対象オブジェクトが送信するメッセージの順序に一致しかつ漏れがないことを確認することができれば、シーケンス図108と状態遷移表109との整合性検証ができたといえる。ソフトウェア設計検証装置110では、上記の考えを実現する検証ソフトウェアと検証対象ソフトウェアを生成し、生成した各ソフトウェアを動作させることによって整合性検証を行い、検証結果の判定を行う。以下では、検証ソフトウェア生成手段103の動作、および検証対象ソフトウェア生成手段104の動作についてそれぞれ詳細に説明する。まず、検証ソフトウェア生成手段103の動作について説明する。検証ソフトウェア生成手段103は、シーケンス図格納手段101から読み出した図3に示すシーケンス図108のデータに基づいて検証ソフトウェアを生成する。検証ソフトウェアの生成について、図5から図7に示すフローチャートと、図8に示す検証ソフトウェアとを用いて説明する。図5から図7は、本実施形態による検証ソフトウェア生成手段103の動作を示すフローチャートである。また、図8は、検証ソフトウェア生成手段103で作成される検証ソフトウェアの一例を示す図である。なお、本実施形態による検証ソフトウェア生成手段103が生成する検証ソフトウェアは、シーケンス図格納手段101に格納されている全てのシーケンス図108の内容を含み、かつ、生成される検証ソフトウェアは1つのソフトウェアとする。また、図5に示すフローチャートは、図2に示すフローチャートのステップS201からステップS202までの処理を含んでいる。また、図5のフローチャートを実行する際には、予め作成されたシーケンス図108がシーケンス図格納手段101に格納されている。図5に示すように、検証ソフトウェア生成手段103は、シーケンス図格納手段101に格納されている最初のシーケンス図108を読み出すステップS501。ステップS501の後、ステップS501にて読み出したシーケンス図108に含まれる検証対象オブジェクトの名前を取得検証対象オブジェクトの名前の取得方法については後述するする検証対象オブジェクト特定手段ステップS502。ステップS502の後、ステップS501で読み出したシーケンス図108に含まれる検証対象オブジェクト303に設定されている初期状態を読み出す初期状態抽出手段ステップS503。ステップS503の後、ステップS501で読み出したシーケンス図108に含まれる全てのメッセージの情報メッセージ情報を読み出しメッセージ情報抽出手段、その出現順序と、各メッセージの送信オブジェクト名および受信オブジェクト名を格納図9に格納の一例を示すが、詳細については後述するステップS504。ステップS504の後、シーケンス図格納手段101に格納されているシーケンス図108を全て読み出したか否かが判断されステップS505、読み出していないシーケンス図108が存在する場合ステップS505においてNoの場合は、ステップS501に進み、新たなシーケンス図108を読み出して処理ステップS501~ステップS505の処理を継続する。一方、ステップS505において、全てのシーケンス図108を読み出したと判断された場合ステップS505においてYesの場合は、図6に示すフローチャートのステップS601に進む。このように、検証ソフトウェア生成手段103は、シーケンス図108に含まれる検証対象オブジェクトを特定する検証対象オブジェクト特定手段と、シーケンス図108の内容を実行する前の検証対象オブジェクトの状態である、シーケンス図108に含まれた初期状態を抽出する初期状態抽出手段と、シーケンス図108に含まれるメッセージ情報を抽出するメッセージ情報抽出手段とを備え、検証対象オブジェクト特定手段にて特定された検証対象オブジェクト、初期状態抽出手段にて抽出された初期状態、およびメッセージ情報抽出手段にて抽出されたメッセージ情報によって検証ソフトウェアを作成している。ここで、図9に示すシーケンス図108に含まれるメッセージの情報の格納方法について、図3を用いて説明する。図9は、本実施形態による検証ソフトウェア生成手段103で格納されるメッセージ情報の一例を示す図である。図9に示すように、検証ソフトウェア生成手段103は、図3に示すようなシーケンス図108を読み出すと、読み取ったシーケンス図名をシーケンス図名記述列901に出力する。また、オブジェクト301から検証対象オブジェクト303に対して送信するメッセージmessage11から、メッセージ名message11が該当をメッセージ名記述列902に出力し、送信オブジェクト名オブジェクト1が該当を送信オブジェクト名記述列903に出力し、受信オブジェクト名検証対象オブジェクトが該当を受信オブジェクト名記述列904に出力する。以下、シーケンス図108から、messege11の後に続くmessage101、message12を取得し、メッセージ名記述列902、送信オブジェクト名記述列903、受信オブジェクト名記述列904にそれぞれ出力する。最初に読み出したシーケンス図108の出力を終えると、シーケンス図格納手段101に格納されている他のシーケンス図を読み出して上記と同様の動作を繰り返し、当該動作を全てのシーケンス図108を読み出すまで続ける。図6では、シーケンス図格納手段101に格納されているシーケンス図108のそれぞれに対して1つのテスト関数を作成する動作を示している。図6に示すように、図5のステップS505において全てのシーケンス図108が読み出されたと判断されると、検証ソフトウェアの内容がシーケンス図108の内容の影響を受けない固定部図8の行番号01~02を出力するステップS601。なお、図8の行番号01は、検証ソフトウェア生成部103が生成する検証ソフトウェアのクラス名を示し、図8の行番号02は、検証対象ソフトウェアが出力する検証対象ソフトウェアから送信されてきたメッセージを格納するリストの宣言と初期化命令初期状態設定手段を示している。また、本実施形態では、クラス名をTestcodeとし、リスト名をactionListとしている。ステップS601の後、テスト関数名図8の行番号03を出力するステップS602。なお、本実施形態では、シーケンス図格納手段101に格納されているシーケンス図108に含まれるシーケンス図のそれぞれに対して、1つのテスト関数を作成するものとする。従って、ステップS602にて書き込まれる出力されるテスト関数名は、1つ目のシーケンス図ではtestSequence1とし、二つ目のシーケンス図ではtestSequence2など、シーケンス図108を読み出すごとに数字を1ずつ増やすこととする。ステップS602の後、ステップS503で読み出した初期状態を設定する命令図8の行番号04を出力するステップS603。ステップS603の後、図3に示す検証対象オブジェクト303に最初に入力するメッセージ以下、トリガーメッセージシーケンス開始メッセージとも称するの実行命令図8の行番号05を出力するシーケンス開始メッセージ送信設定手段ステップS604。トリガーメッセージは、図9に格納されるメッセージのうち、受信オブジェクト名記述列904の最初に検証対象オブジェクト303が現れるメッセージ名が対応する。なお、本実施形態では、message11がトリガーメッセージとなる。ステップS604の後、検証対象オブジェクト303がシーケンス図108に記述された通りに実行したかを検証する検証命令図8の行番号06~09を出力する整合性検証設定手段ステップS605。検証対象となるメッセージは、図9に格納されるメッセージのうち、送信オブジェクト名記述列903が検証対象オブジェクト303になっているときのメッセージ名が対応する。これを図9の上から順に、複数ある場合は複数のメッセージ名の検証命令を出力する。なお、本実施形態では、検証命令の例として、Java登録商標言語やC言語などに標準で用意されているassertを用いている。ステップS605の後、他のシーケンスの検証を行う準備のために、格納した検証対象オブジェクトが出力するメッセージのリストの削除命令図8の行番号10~11を出力するステップS606。ステップS606の後、シーケンス図格納手段101に格納されている全てのシーケンス図108を読み出したか否かが判断されステップS607、読み出していないシーケンス図108が存在する場合ステップS607においてNoの場合はステップS602に進み、新たなシーケンス図108を読み出して処理ステップS602~ステップS607を継続する。一方、全てのシーケンス図108が読み出されたと判断された場合ステップS607においてYesの場合は、図7に示すステップS701に進む。このように、検証ソフトウェア生成手段103は、初期状態を検証ソフトウェアに設定する初期状態設定手段と、非検証対象オブジェクトから検証対象オブジェクトに最初に送信されるシーケンス開始メッセージを検証ソフトウェアに設定するシーケンス開始メッセージ送信設定手段と、整合性の検証の実行を検証ソフトウェアに設定する整合性検証設定手段とを備えている。図7では、検証対象ソフトウェアが検証ソフトウェアにアクセスする関数を作成する動作について示している。図7に示すように、図6のステップS607において全てのシーケンス図108が読み出されたと判断されると、図9に格納されているメッセージの一行目の内容を読み出すステップS701。ステップS701の後、ステップS701で読み出された行の送信オブジェクト名記述列903が検証対象オブジェクトであるか否かが判断されるステップS702。ステップS702にて送信オブジェクト名が検証対象オブジェクトであると判断されるとステップS702においてYesの場合、ステップS701で読み出された行の受信オブジェクト名記述列904が検証対象オブジェクトであるか否かが判断されるステップS703。ステップS703にて受信オブジェクト名が検証対象オブジェクト名でないと判断されるとステップS703においてNoの場合、ステップS701で読み出した行のメッセージ名記述列902に記述されるメッセージ名をメッセージリストに格納しステップS704、ステップS705に進む。ステップS702にて送信オブジェクト名が検証対象オブジェクトでないと判断された場合ステップS702においてNoの場合、あるいは、ステップS703にて受信オブジェクト名が検証対象オブジェクトであると判断された場合ステップS703においてYesの場合は、ステップS704にてメッセージリストに格納されたメッセージが存在するか否かが判断されるステップS706。ステップS706にてメッセージリストにメッセージが存在すると判断された場合ステップS706においてYesの場合は、検証対象ソフトウェアが検証ソフトウェアにアクセスする関数名第1のコール関数、第1のコール関数設定手段と呼び出された関数名を保持する命令動作結果保持設定手段図8の行番号12~13を出力し、さらに、ステップS704にて格納したメッセージ第1のメッセージを検証対象ソフトウェアに送信する第1のメッセージ送信設定手段命令図8の行番号14~15を出力しステップS707、ステップS710に進む。一方、ステップS706にてメッセージリストにメッセージが存在しないと判断されるとステップS705に進む。ステップS705では、図9に格納されている全てのメッセージを読み出したか否かが判断され、全てのメッセージを読み出していない場合ステップS705でNoの場合は、読み出す行の位置を次の行に移動させて、ステップS701に進む。一方、ステップS705において、図9に格納されるメッセージを全て読み出した場合ステップS705においてYesの場合は、ステップS708に進み、ステップS706と同様の判断がなされる。ステップS708にてメッセージリストに格納したメッセージが存在すると判断された場合ステップS708でYesの場合は、ステップS709に進む。ステップS709では、ステップS707と同様の処理が実行され、ステップS710に進む。一方、ステップS708において、メッセージリストに格納したメッセージが存在しないと判断された場合ステップS708においてNoの場合は、ステップS710に進む。ステップS710では、検証ソフトウェア全体の終了処理図8の行番号20を出力し、検証ソフトウェア生成手段103の動作を終了する。このように、検証ソフトウェア生成手段103は、検証対象オブジェクトから呼び出される第1のコール関数を検証ソフトウェアに設定する第1のコール関数設定手段を備え、第1のコール関数設定手段は、検証対象オブジェクトの動作結果を保持する旨を検証ソフトウェアに設定する動作結果保持設定手段と、非検証対象オブジェクトから検証対象オブジェクトに第1のメッセージを送信する旨を検証ソフトウェアに設定する第1のメッセージ送信設定手段とを備えている。次に、検証オブジェクトの名前の取得方法について説明する。検証対象オブジェクトの取得方法としては、シーケンス図108に含まれるオブジェクト301からオブジェクト303のうち、初期状態305を書き加えるオブジェクトを一つに限定するようにし、検証ソフトウェア生成手段103が検証ソフトウェアを生成する際に、初期状態305が書き加えられているオブジェクトを検証対象オブジェクト303として読み込む。その具体的な方法については、図10に示すような、シーケンス図108をXMLExtensibleMarkupLanguageに変換した一例を用いて説明する。なお、シーケンス図からXMLへの変換は、図示しないUMLUnifiedModelingLanguageエディタなどのソフトウェアで実現することができる。図10は、本実施形態によるシーケンス図108をXML形式に変換した一例を示す図である。図10に示すように、XMLにおいて、シーケンス図108に含まれるオブジェクト301からオブジェクト303は、タグ1001からタグ1003にそれぞれ記述され、初期状態305はタグ1004に記述されている。また、初期状態305の内容はタグ1005に記述されている。検証ソフトウェア生成手段103は、検証対象オブジェクト303の名前を取得するために、初期状態305が記述されているタグ1004のcovered以下のL003を読み取り、読み取ったL003が、タグ1001からタグ1003のどのxmi.idに設定されているかを読み取る。図10では、L003がタグ1003に設定されているので、タグ1003のname以下の検証対象を読み取り、読み取った検証対象を検証対象オブジェクトの名前として取得する。次に、検証対象ソフトウェア生成手段104の動作について説明する。検証対象ソフトウェア生成手段104は、図4に示す状態遷移表109を状態遷移表格納手段102から読み込み、読み込んだ状態遷移表109に基づいて検証対象ソフトウェアを生成する。検証対象ソフトウェア生成手段104の詳細な動作について、図11に示すフローチャートと、図12に示す検証対象ソフトウェアの一例に従い説明する。図11は、本実施形態による検証対象ソフトウェア生成手段104の動作を示すフローチャートである。また、図12は、検証対象ソフトウェア生成手段104で作成される検証対象ソフトウェアの一例を示す図である。なお、本実施形態では、検証対象ソフトウェア生成手段104が生成する検証対象ソフトウェアは、状態遷移表格納手段102に格納される状態遷移表109の内容を含み、かつ1つのソフトウェアとする。また、図11に示すフローチャートは、図2に示すフローチャートのステップS203からステップS204までの処理を含んでいる。また、図11のフローチャートを実行する前には、予め作成された状態遷移表109が状態遷移表格納手段102に格納されている。図11に示すように、検証対象ソフトウェア生成手段104は、状態遷移表格納手段102に格納されている状態遷移表109を読み出すステップS1101。すなわち、検証対象ソフトウェア生成手段104は、状態遷移表109に含まれ、非検証対象オブジェクトから検証対象オブジェクトに入力されるメッセージである入力イベントを抽出する入力イベント抽出手段と、状態遷移表109に含まれ、検証対象オブジェクトの現在の状態を示す現在状態を抽出する現在状態抽出手段と、入力イベントと現在状態とに基づく処理内容を抽出する処理内容抽出手段と、処理内容に基づき、現在状態を変更した変更状態を抽出する変更状態抽出手段と、処理内容に基づき、変更状態の抽出の際に、検証対象オブジェクトから非検証対象オブジェクトに送信される第2のメッセージを抽出する第2のメッセージ抽出手段とを備え、入力イベント抽出手段にて抽出された入力イベント、現在状態抽出手段にて抽出された現在状態、処理内容抽出手段にて抽出された処理内容、変更状態抽出手段にて抽出された変更状態、および第2のメッセージ抽出手段にて抽出された第2のメッセージによって、検証対象ソフトウェアを生成する。ステップS1101の後、検証対象ソフトウェアの内容が状態遷移表1109の内容の影響を受けない固定部図12の行番号01~05を出力するステップS1102。なお、図12の行番号01は、検証対象ソフトウェア生成部104が生成する検証対象ソフトウェアのクラス名であり、図12の行番号02は、検証対象ソフトウェアの現在状態を示す変数の宣言である。本実施形態では、クラス名をTesttargetとし、状態変数名をstateとしている。ステップS1102の後、図4に示すような状態遷移表109の一行目の内容を読み出すステップS1103。ステップS1103の後、ステップS1103にて読み出した行に記述されるイベント名記述列402を利用し、検証ソフトウェアが検証対象ソフトウェアにアクセスする関数第2のコール関数図12の行番号06を出力するステップS1104。ステップS1104の後、ステップS1103にて読み出した行の処理内容403のうち最左セル図4のセル404の内容を読み出すステップS1105。ステップS1105の後、ステップS1105にて読み出されたセルの内容が空であるか否かが判断されステップS1106、空である場合ステップS1106においてYesの場合は、何も出力せずにステップS1107に進む。一方、空でない場合ステップS1106においてNoの場合は、ステップS1108に進む。ステップS1108では、ステップS1105にて読み出されたセルの内容に基づき、検証対象ソフトウェアが実行する処理の内容を出力する。出力内容としては、検証対象ソフトウェアの現在の状態を条件判定文とする命令図12の行番号07を出力し状態判定設定手段、次に、読み出したセルの一行一行を確認し、行の先頭がS:である場合は、検証対象オブジェクトの現在の状態を変更する処理図12の行番号08を出力し状態変更設定手段、行の先頭がA:である場合は、検証ソフトウェアへのメッセージ第2のメッセージの送信命令図12の行番号09を出力し第2のメッセージ送信設定手段、最後に、条件判定文を閉じる処理図12の行番号10を出力する。出力した後、ステップS1107に進む。ステップS1107では、ステップS1103にて読み出された行における全てのセルの内容を読み出したか、つまり、ステップS1105で読み出したセルの一つ右にセルが存在するか否かが判断され、読み出していないセルが存在する場合ステップS1107においてNoの場合は、読み出すセルの位置を一つ右に移動してステップS1105に進む。一方、全てのセルの内容を読み出した場合ステップS1107においてYesの場合は、検証ソフトウェアが検証対象ソフトウェアにアクセスする関数を閉じる処理図12の行番号11を出力してステップS1109に進む。ステップS1109では、全ての行を読み出したか否かが判断され、全て読み出していない場合ステップS1109においてNoの場合は、読み出す行の位置を次の行に移動してステップS1103に進む。一方、全ての行を読み出した場合ステップS1109においてYesの場合は、検証対象ソフトウェア全体の終了処理図12の行番号27を出力し、検証対象ソフトウェア生成手段104の動作を終了する。次に、図4に示すイベント名記述列402に記載されるイベントのうち、複数の処理内容403を持つイベントがあった場合の処理について、さらに詳しく説明する。説明の便宜上、検証対象ソフトウェア生成手段104は、図4のセル406までの処理を終了し、図12の行番号21までを出力しているものとする。また、このとき、検証対象ソフトウェア生成手段104は、図11のステップS1108を終えているものとする。ステップS1107では、セル407の処理が終了していないためステップS1105に進み、ステップS1105にてセル407の内容を読み出してステップS1106に進み、ステップS1106にてセル407は空でないためステップS1108に進む。ステップS1108では、セル407の内容に基づいた出力を行うが、この時の条件判定文として既にセル406の内容に基づいた命令としてifが出力されているため、処理内容403を複数持つイベントにおける2つ目以降のセルに対する条件判定の命令文としてelseif図12の行番号22を出力する。その後、前述の通り、検証対象オブジェクトの現在の状態を変更する処理図12の行番号23と検証ソフトウェアへのメッセージ送信命令図12の行番号24を出力し、最後に条件判定文を閉じる処理図12の行番号25を出力する。このように、検証対象ソフトウェア生成手段104は、検証オブジェクトから呼び出される第2のコール関数を検証対象ソフトウェアに設定する第2のコール関数設定手段を備え、第2のコール関数設定手段は、現在状態を条件判定として検証対象ソフトウェアに設定する状態判定設定手段を含み、状態判定設定手段は、現在状態を変更状態に変更する旨を検証対象ソフトウェアに設定する状態変更設定手段と、第2のメッセージを検証対象ソフトウェアに設定する第2のメッセージ送信設定手段とを備えている。次に、実行モジュール生成手段105の動作について説明する。実行モジュール生成手段105は、検証ソフトウェア生成手段103にて生成された検証ソフトウェアと、検証対象ソフトウェア生成手段104にて生成された検証対象ソフトウェアとに対してビルドを行い、実行モジュールを生成する。次に、実行モジュール生成手段105の構成について説明する。実行モジュール生成手段105は、プログラミング言語で書かれたソフトウェアをコンピュータが直接に実行可能な機械語のプログラムに変換するソフトウェアであるコンパイラや、コンパイラによって変換された機械語のプログラムに対して必要なライブラリなどを付け加えて実行可能なモジュールを生成するソフトウェアであるリンカなどで構成されている。次に、検証実行手段106の動作について説明する。検証実行手段106では、実行モジュール生成手段105にて生成された実行モジュールの実行、および実行モジュールの動作結果からシーケンス図108と状態遷移表109との整合性検証と判定を行う。検証実行手段106において、実行モジュール生成手段105にて生成された実行モジュールを実行すると、検証ソフトウェア生成手段103にて生成された検証ソフトウェア、および検証対象ソフトウェア生成装置104にて生成された検証対象ソフトウェアが動作を開始する。すなわち、シーケンス図格納手段101に格納されているシーケンス図108と状態遷移表格納手段102に格納されている状態遷移表109との整合性検証と判定を開始する。以下では、検証実行手段106にて行われるシーケンス図108と状態遷移表109との整合性検証および判定の方法を、検証ソフトウェアと検証対象ソフトウェアとの動作に基づいて図8,12,13を用いて説明する。図13は、本実施形態による検証ソフトウェアおよび検証対象ソフトウェアに基づく検証実行手段における実行モジュールの動作を示す図である。図13に示すように、まず、検証実行手段106で実行モジュールが実行されると、図8の行番号03が呼び出される。そして、検証対象ソフトウェアに対して初期状態のセットが行われ図8の行番号04、トリガーメッセージであるmessage11を検証対象ソフトウェアに対して送信する図8の行番号05。検証対象ソフトウェアがmessage11を送信すると、図12の行番号06が呼び出され、現在状態をstate2に変更した図12の行番号08後、検証ソフトウェアに対してmessage101を送信する図12の行番号09。検証対象ソフトウェアが検証ソフトウェアに対してmessage101を送信すると、図8の行番号12が呼び出され、message101が呼び出されたことを蓄積するためmessage101をactionListに格納した図8の行番号13後、検証対象ソフトウェアに対してmessage12を送信する図8の行番号14。検証ソフトウェアが検証対象ソフトウェアに対してmessage12を送信すると、検証対象ソフトウェアでは図12の行番号12が呼び出され、現在状態をstate3に変更した図12の行番号14後、検証ソフトウェアに対してmessage102を送信する図12の行番号15。検証対象ソフトウェアが検証ソフトウェアに対してmessage102を送信すると、図8の行番号16が呼び出され、message102が呼び出されたことを蓄積するためにmessage102をactionListに格納した図8の行番号17後、検証対象ソフトウェアに対しmessage13を送信する図8の行番号18。検証ソフトウェアが検証対象ソフトウェアに対してmessage13を送信すると、図12の行番号18が呼び出され、現在状態をstate4に変更する図12の行番号20。この後、処理が検証ソフトウェアに戻り図8の行番号05、続いて整合性検証を行う。これまでの処理によって、検証対象ソフトウェアの動作を確認できるようにしたactionListの0番目にはmessage101が蓄積され、1番目にはmessage102が蓄積されている。検証ソフトウェアに処理が戻ってくると、1番目の検証図8の行番号07を行い、続いて2番目の検証図8の行番号08を行う。次に、本実施形態における整合性検証の方法について説明する。本実施形態における整合性検証は、検証対象ソフトウェアの動作結果、つまりactionListに格納されるメッセージ名と、シーケンス図108に記述されるオブジェクトの文字列が一致するかを見て行う。具体的には、検証ソフトウェアに処理が戻って来たときには、actionListの0番目に、検証対象ソフトウェアの動作結果としてmessage101が蓄積されている。actionListの0番目に蓄積されたmessage101とシーケンス図108に記載される検証対象オブジェクト303から出力される最初のメッセージmessage101とが一致するか否かの検証図8の行番号07を行う。本実施形態では一致しているため整合性検証は成功となる。続いて、actionListの1番目に蓄積しているmessage102と、シーケンス図115に記載される検証対象オブジェクト303から出力される2番目のメッセージmessage102とが一致するか否かの検証図8の行番号08を行う。本実施形態では一致しているため整合性検証は成功となる。すなわち、検証実行手段106は、保持された検証対象オブジェクトの動作結果がメッセージ情報に含まれ、かつ、動作結果の保持順序がメッセージ情報のシーケンス図108における処理順序と一致することによって、シーケンス図108と状態遷移表109との整合性があると判定する。次に、本実施形態における判定方法について説明する。本実施形態における判定は、シーケンス図108の内容と状態遷移表109の内容との整合性が取れているか否か整合性があるか否かの判定を行うものであり、上記の検証において、全ての検証に成功した場合は、シーケンス図108と状態遷移表109との整合性が取れている整合性があると判定する。一方、1つでも検証が失敗した場合は、シーケンス図108と状態遷移表109との整合性は取れていない整合性がないと判定する。このように、本実施形態におけるソフトウェア検証装置110を実行することによって全ての検証に成功したということは、状態遷移表109を持つ検証対象オブジェクトはシーケンス図108に記述した順序通りにかつ漏れなくメッセージを送信しているといえ、さらに、状態遷移表109はシーケンス図108の内容を反映できているといえるため、シーケンス図108と状態遷移表109との整合性が取れていることを確認することができる。次に、検証結果提示手段107について説明する。検証結果提示手段107は、検証実行手段106にて判定された結果を表示する。本実施形態では、整合性検証にassertを用いているため、整合性検証の結果をコンピュータのコンソール画面に出力する。出力例としては、検証実行手段106による整合性検証の結果、失敗する検証が無ければ全ての検証が成功すれば何も表示しないが、失敗する検証が存在すれば、検証に失敗したソフトウェアの名前と行番号を表示する。以上のことから、本実施形態によるソフトウェア設計検証装置では、シーケンス図108に基づいて検証ソフトウェアを生成するとともに、状態遷移表109に基づいて検証対象ソフトウェアを生成し、生成した検証ソフトウェアと検証対象ソフトウェアを実行して整合性検証を行うことによって、シーケンス図108と状態遷移表109との整合性検証を自動で検証することが可能となる。また、全ての整合性検証に成功すれば、状態遷移表109はシーケンス図108の内容を満たしていることを自動で検証することができる。また、整合性検証を自動で行うことによって、手戻りによる修正コストを低減できることが可能である。なお、本実施形態による検証ソフトウェア生成手段103において、検証対象オブジェクト名の取得方法として、シーケンス図108に含まれるオブジェクト301からオブジェクト303のうち、初期状態305が書き加えられているオブジェクトを検証対象オブジェクト303として読み込むよう構成したが、これに限らず、ソフトウェア設計検証装置110を実行する際の引数として、キーボード図示せずなどの入力装置を使用して指定するような構成でもあってもよく、他の方法として、例えば磁気ディスク装置図示せずなどの不揮発性の補助記憶装置にテキストファイルを格納し、当該テキストファイルに検証対象オブジェクト名を記述しておき、ソフトウェア設計検証装置110がテキストファイルに記述された検証対象オブジェクト名を読み取るような構成としてもよい。上記2つの方法であれば、初期状態305を書き加えるオブジェクトを、シーケンス図108において1つのオブジェクトに限定する必要はなく、複数のオブジェクトに初期状態を設定することが可能になる。また、本実施形態による状態遷移表109の処理内容403には、状態の変化を示すキーワードとしてS:を、出力メッセージを示すキーワードとしてA:を記述するようにしたが、これに限らず、例えば、一行目に状態の変化を記述し、二行目以降に出力メッセージを記述するよう記述箇所を固定するようにしてもよい。また、本実施形態では、検証結果提示手段112は外部ディスプレイ装置図示せずなどに表示されるコンソール画面で構成されるとしたが、これに限らず、例えば、テキストファイルに結果を出力して磁気ディスク装置図示せずなどの不揮発性の補助記憶装置に格納するよう構成してもよい。また、本実施形態では、テスト関数の作成にあたり、1つのシーケンス図108に対して1つの関数を作成するとしたが、これに限らず、全てのシーケンス図108の内容をまとめて1つのテスト関数に含めてもよい。また、本実施形態では、検証ソフトウェア生成手段103にて生成される検証ソフトウェア、および検証対象ソフトウェア生成手段104にて生成される検証対象ソフトウェアを1つのファイルで構成するとしたが、これに限らず、複数のファイルで構成するようにしてもよい。また、本実施形態では、状態遷移表109の処理内容403において、状態とイベントとの組合せが存在しない場合、あるいは、組み合わせが存在していても何も処理しない場合は空白が記述されるとしたが、これに限らず、例えば明示的に-や、処理しないことが明確になるような別の記号を記述してもよい。"