(57)【要約】【課題】本発明は、ソフトウェア設計書間の整合性検証を自動的に行い、手戻りによる修正コストを低減することが可能なソフトウェア設計検証装置ならびにそれに用いる検証プログラムおよび検証対象プログラムを提供することを目的とする。【解決手段】本発明によるソフトウェア設計検証装置は、シーケンス図１０８のデータに基づいて、当該シーケンス図１０８に含まれる検証対象オブジェクト以外の非検証対象オブジェクトの動作を実現する検証ソフトウェアを生成する検証ソフトウェア生成手段１０３と、状態遷移表１０９のデータに基づいて、検証対象オブジェクトの動作を実現する検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段１０４と、実行モジュール生成手段１０５にて生成された実行モジュールを実行し、シーケンス図１０８の内容と状態遷移表１０９の内容との整合性の検証を行う検証実行手段１０６とを備える。【選択図】図１
2012173834.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェア設計におけるシーケンス図と当該シーケンス図に基づいて作成された状態遷移表との整合性を検証するソフトウェア設計検証装置であって、
少なくとも１つ以上の前記シーケンス図のデータを格納するシーケンス図格納手段と、
前記シーケンス図に含まれた前記整合性が検証される検証対象オブジェクトが有する前記状態遷移表のデータを格納する状態遷移表格納手段と、
前記シーケンス図格納手段に格納された前記シーケンス図のデータに基づいて、当該シーケンス図に含まれる前記検証対象オブジェクト以外の非検証対象オブジェクトの動作を実現する検証ソフトウェアを生成する検証ソフトウェア生成手段と、
前記状態遷移表格納手段に格納された前記状態遷移表のデータに基づいて、前記検証対象オブジェクトの動作を実現する検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段と、
前記検証ソフトウェアと前記検証対象ソフトウェアとに対してビルドを行い、実行可能な実行モジュールを生成する実行モジュール生成手段と、
前記実行モジュール生成手段にて生成された前記実行モジュールを実行し、前記シーケンス図の内容と前記状態遷移表の内容との前記整合性の検証を行う検証実行手段と、
を備える、ソフトウェア設計検証装置。
【請求項２】
前記検証ソフトウェア生成手段は、
前記シーケンス図に含まれる前記検証対象オブジェクトを特定する検証対象オブジェクト特定手段と、
前記シーケンス図の内容を実行する前の前記検証対象オブジェクトの状態である、前記シーケンス図に含まれた初期状態を抽出する初期状態抽出手段と、
前記シーケンス図に含まれるメッセージ情報を抽出するメッセージ情報抽出手段と、
を備え、
前記検証対象オブジェクト特定手段にて特定された前記検証対象オブジェクト、前記初期状態抽出手段にて抽出された前記初期状態、および前記メッセージ情報抽出手段にて抽出された前記メッセージ情報によって前記検証ソフトウェアを作成することを特徴とする、請求項１に記載のソフトウェア設計検証装置。
【請求項３】
前記検証ソフトウェア生成手段は、
前記初期状態を前記検証ソフトウェアに設定する初期状態設定手段と、
前記非検証対象オブジェクトから前記検証対象オブジェクトに最初に送信されるシーケンス開始メッセージを前記検証ソフトウェアに設定するシーケンス開始メッセージ送信設定手段と、
前記整合性の検証の実行を前記検証ソフトウェアに設定する整合性検証手段と、
をさらに備えることを特徴とする、請求項２に記載のソフトウェア設計検証装置。
【請求項４】
前記検証ソフトウェア生成手段は、
前記検証対象オブジェクトから呼び出される第１のコール関数を前記検証ソフトウェアに設定する第１のコール関数設定手段をさらに備え、
前記第１のコール関数設定手段は、
前記検証対象オブジェクトの動作結果の保持する旨を前記検証ソフトウェアに設定する動作結果保持設定手段と、
前記非検証対象オブジェクトから前記検証対象オブジェクトに第１のメッセージを送信する旨を前記検証ソフトウェアに設定する第１のメッセージ送信設定手段と、
を備えることを特徴とする、請求項２または３に記載のソフトウェア設計検証装置。
【請求項５】
前記検証対象ソフトウェア生成手段は、
前記状態遷移表に含まれ、前記非検証対象オブジェクトから前記検証対象オブジェクトに入力されるメッセージである入力イベントを抽出する入力イベント抽出手段と、
前記状態遷移表に含まれ、前記検証対象オブジェクトの現在の状態を示す現在状態を抽出する現在状態抽出手段と、
前記入力イベントと前記現在状態とに基づく処理内容を抽出する処理内容抽出手段と、
前記処理内容に基づき、前記現在状態を変更した変更状態を抽出する変更状態抽出手段と、
前記処理内容に基づき、前記変更状態の抽出の際に、前記検証対象オブジェクトから前記非検証対象オブジェクトに送信される第２のメッセージを抽出する第２のメッセージ抽出手段と、
を備え、
前記入力イベント抽出手段にて抽出された前記入力イベント、前記現在状態抽出手段にて抽出された前記現在状態、前記処理内容抽出手段にて抽出された前記処理内容、前記変更状態抽出手段にて抽出された前記変更状態、および前記第２のメッセージ抽出手段にて抽出された前記第２のメッセージによって、前記検証対象ソフトウェアを生成することを特徴とする、請求項１に記載のソフトウェア設計検証装置。
【請求項６】
前記検証対象ソフトウェア生成手段は、
前記検証オブジェクトから呼び出される第２のコール関数を前記検証対象ソフトウェアに設定する第２のコール関数設定手段をさらに備え、
前記第２のコール関数設定手段は、前記現在状態を条件判定として前記検証対象ソフトウェアに設定する状態判定設定手段を含み、
前記状態判定設定手段は、
前記現在状態を前記変更状態に変更する旨を前記検証対象ソフトウェアに設定する状態変更設定手段と、
前記第２のメッセージを前記検証対象ソフトウェアに設定する第２のメッセージ送信設定手段と、
を備えることを特徴とする、請求項５に記載のソフトウェア設計検証装置。
【請求項７】
前記検証実行手段は、保持された前記検証対象オブジェクトの動作結果が前記メッセージ情報に含まれ、かつ、前記動作結果の保持順序が前記メッセージ情報の前記シーケンス図における処理順序と一致することによって、前記シーケンス図と前記状態遷移表との前記整合性があると判定することを特徴とする、請求項４に記載のソフトウェア設計検証装置。
【請求項８】
コンピュータに請求項１に記載のソフトウェア設計検証装置における前記検証ソフトウェアを実行させるためのプログラムであって、
（ａ）前記シーケンス図ごとにテスト関数を設定する手順と、
（ｂ）前記検証対象オブジェクトから呼び出される第１のコール関数を設定する手順と、
を備え、
前記手順（ａ）は、
（ｃ）前記検証対象オブジェクトの初期状態を設定する手順と、
（ｄ）前記非検証対象オブジェクトから前記検証対象オブジェクトに最初に送信されるシーケンス開始メッセージを設定する手順と、
（ｅ）前記整合性の検証を実行する手順と、
を含み、
前記手順（ｂ）は、
（ｆ）前記検証対象オブジェクトの動作結果を保持する手順と、
（ｇ）前記非検証対象オブジェクトから前記検証対象オブジェクトに第１のメッセージを送信する手順と、
を含み、上記手順（ａ）〜（ｇ）をコンピュータに実行させることを特徴とする、検証プログラム。
【請求項９】
前記初期状態は前記シーケンス図に含まれ、
前記シーケンス開始メッセージ、前記第２のコール関数、前記動作結果、および前記第１のメッセージは、前記シーケンス図に含まれるメッセージ情報に基づくメッセージ名が付されることを特徴とする、請求項８に記載の検証プログラム。
【請求項１０】
コンピュータに請求項１に記載のソフトウェア設計検証装置における前記検証対象ソフトウェアを実行させるためのプログラムであって、
（ｈ）前記検証オブジェクトから呼び出される第２のコール関数を設定する手順を含み、
前記手順（ｈ）は、
（ｉ）前記検証対象オブジェクトの現在の状態を示す現在状態を条件判定として処理を行う手順を含み、
前記手順（ｉ）は、
（ｊ）前記現在状態を変更する手順と、
（ｋ）前記検証対象オブジェクトから前記非検証対象オブジェクトに送信される第２のメッセージを送信する手順と、
をさらに含み、上記手順（ｈ）〜（ｋ）をコンピュータに実行させることを特徴とする、検証対象プログラム。
【請求項１１】
前記手順（ｈ）における前記第２のコール関数は、前記状態遷移表に含まれた前記非検証対象オブジェクトから前記検証対象オブジェクトに入力されるメッセージである入力イベントが付され、前記手順（ｉ）における前記現在状態は、前記状態遷移表に含まれる現在の状態が付され、前記手順（ｊ）における変更する状態は、前記状態遷移表に含まれる状態が付され、前記手順（ｋ）における前記第２のメッセージは、前記状態遷移表に含まれるメッセージ名が付されることを特徴とする、請求項１０に記載の検証対象プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェア（コンピュータプログラム）の開発、特に設計段階において作成するソフトウェア設計書間に対して、各ソフトウェア設計書間の内容に齟齬が存在しないことを検証する作業（以下、整合性検証とも称する）を行うソフトウェア設計検証装置ならびにそれに用いる検証プログラムおよび検証対象プログラムに関する。
【背景技術】
【０００２】
ソフトウェア開発では、様々な工程を経てソフトウェア設計書やソフトウェア仕様書、プログラム等の作業成果物が作成される。作業成果物は、入力となる作業成果物に対して所定の作業を経て別の作業成果物を出力することによって作成されている。一例を挙げると、シーケンス図を入力として状態遷移表を出力したり、ソフトウェア詳細設計書を入力としてプログラムを出力したりする。このような作業を行うにあたり、作業前後の作業成果物間（入力前の作業成果物と出力後の作業成果物との間）の整合性検証が必要となる。従来、整合性検証の多くは人手によるレビューや試験などによって行われており、多くのコストが必要となる。そのため、一部の整合性検証作業を自動化できるようなシステムが開発されている。
【０００３】
従来、仕様決定手段で作成した仕様決定表とソフトウェア情報から、業務システムで動作するソフトウェアをソフトウェア生成手段で自動生成するソフトウェア自動生成装置が開示されている（例えば、特許文献１参照）。
【０００４】
また、ソフトウェア本体とソフトウェアモジュールへの呼び出しシーケンスをチェックするシーケンスチェックモジュールを備え、シーケンスチェックモジュール生成器がインターフェースシーケンス定義よりシーケンスチェックモジュールを生成することにより、ソフトウェア本体からソフトウェアモジュールへの呼び出しシーケンスの正当性を確認することができるソフトウェア検証装置が開示されている（例えば、特許文献２参照）。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２００８−５９１３５号公報
【特許文献２】国際公開第２００８／５６４１９号
【発明の概要】
【発明が解決しようとする課題】
【０００６】
特許文献１のソフトウェア自動生成装置では、仕様決定表を入力して業務システムで動作するソフトウェアを出力している。仕様決定表と生成したソフトウェアとの整合性検証は試験工程で行われるが、試験工程で行われる試験は試験環境や試験に必要なソフトウェアや業務システムを準備する必要があり時間とコストがかかる。また、生成したソフトウェアに不具合が見つかると、仕様決定表における誤りの有無の確認が必要となり、不具合修正のための手戻りが大きくなるという問題がある。
【０００７】
また、特許文献２のソフトウェア検証装置では、インターフェースシーケンス定義とソフトウェア本体とソフトウェアモジュールとを入力としてソフトウェアモジュールの呼び出しシーケンスの正当性を確認している。インターフェースシーケンス定義とソフトウェアモジュールの呼び出しシーケンスとの整合性検証には、ソフトウェア本体とソフトウェアモジュールの開発の完了を待つ必要があり、特許文献１と同様に、不具合を発見するまでに時間がかかるため、不具合修正のための手戻りが大きくなるという問題がある。
【０００８】
このように、ソフトウェアの開発において、出力となる作業成果物（特許文献１では生成ソフトウェア、特許文献２ではソフトウェアモジュールの呼び出しシーケンス）が、入力となる作業成果物（特許文献１では仕様決定表、特許文献２ではインターフェースシーケンス定義）の内容を正しく反映しているか否かの整合性検証が必要となるが、その整合性確認検証を開始するまでに時間がかかり（整合性検証を実施するまでの準備に時間がかかり）、また、不具合が見つかったときの手戻りが大きくなり修正コストが大きくなるという問題がある。
【０００９】
本発明は、これらの問題を解決するためになされたものであり、整合性検証を自動的に行い、手戻りによる修正コストを低減することが可能なソフトウェア設計検証装置ならびにそれに用いる検証プログラムおよび検証対象プログラムを提供することを目的とする。
【課題を解決するための手段】
【００１０】
上記の課題を解決するために、本発明によるソフトウェア設計検証装置は、ソフトウェア設計におけるシーケンス図と当該シーケンス図に基づいて作成された状態遷移表との整合性を検証するソフトウェア設計検証装置であって、少なくとも１つ以上のシーケンス図のデータを格納するシーケンス図格納手段と、シーケンス図に含まれた整合性が検証される検証対象オブジェクトが有する状態遷移表のデータを格納する状態遷移表格納手段と、シーケンス図格納手段に格納されたシーケンス図のデータに基づいて、当該シーケンス図に含まれる検証対象オブジェクト以外の非検証対象オブジェクトの動作を実現する検証ソフトウェアを生成する検証ソフトウェア生成手段と、状態遷移表格納手段に格納された状態遷移表のデータに基づいて、検証対象オブジェクトの動作を実現する検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段と、検証ソフトウェアと検証対象ソフトウェアとに対してビルドを行い、実行可能な実行モジュールを生成する実行モジュール生成手段と、実行モジュール生成手段にて生成された実行モジュールを実行し、シーケンス図の内容と状態遷移表の内容との整合性の検証を行う検証実行手段とを備える。
【発明の効果】
【００１１】
本発明によると、少なくとも１つ以上のシーケンス図のデータを格納するシーケンス図格納手段と、シーケンス図に含まれた整合性が検証される検証対象オブジェクトが有する状態遷移表のデータを格納する状態遷移表格納手段と、シーケンス図格納手段に格納されたシーケンス図のデータに基づいて、当該シーケンス図に含まれる検証対象オブジェクト以外の非検証対象オブジェクトの動作を実現する検証ソフトウェアを生成する検証ソフトウェア生成手段と、状態遷移表格納手段に格納された状態遷移表のデータに基づいて、検証対象オブジェクトの動作を実現する検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段と、検証ソフトウェアと検証対象ソフトウェアとに対してビルドを行い、実行可能な実行モジュールを生成する実行モジュール生成手段と、実行モジュール生成手段にて生成された実行モジュールを実行し、シーケンス図の内容と状態遷移表の内容との整合性の検証を行う検証実行手段とを備えるため、整合性検証を自動的に行い、手戻りによる修正コストを低減することが可能となる。
【図面の簡単な説明】
【００１２】
【図１】本発明の実施形態によるソフトウェア設計検証装置の構成の一例を示すブロック図である。
【図２】本発明の実施形態によるソフトウェア設計検証装置の動作を示すフローチャートである。
【図３】本発明の実施形態によるシーケンス図の一例を示す図である。
【図４】本発明の実施形態による状態遷移表の一例を示す図である。
【図５】本発明の実施形態による検証ソフトウェア生成手段の動作を示すフローチャートである。
【図６】本発明の実施形態による検証ソフトウェア生成手段の動作を示すフローチャートである。
【図７】本発明の実施形態による検証ソフトウェア生成手段の動作を示すフローチャートである。
【図８】本発明の実施形態による検証ソフトウェア生成手段で作成される検証ソフトウェアの一例を示す図である。
【図９】本発明の実施形態による検証ソフトウェア生成手段で格納されるメッセージ情報の一例を示す図である。
【図１０】本発明の実施形態によるシーケンス図をＸＭＬ形式に変換した一例を示す図である。
【図１１】本発明の実施形態による検証対象ソフトウェア生成手段の動作を示すフローチャートである。
【図１２】本発明の実施形態による検証対象ソフトウェア生成手段で作成される検証対象ソフトウェアの一例を示す図である。
【図１３】本発明の実施形態による検証ソフトウェアおよび検証対象ソフトウェアに基づく検証実行手段における実行モジュールの動作を示す図である。
【発明を実施するための形態】
【００１３】
本発明の実施形態について、図面に基づいて以下に説明する。
【００１４】
まず、本実施形態によるソフトウェア設計検証装置１１０の構成について説明する。
【００１５】
図１は、本実施形態によるソフトウェア設計検証装置１１０の構成の一例を示すブロック図である。図１に示すように、本実施形態によるソフトウェア設計検証装置１１０は、少なくとも１つ以上のシーケンス図１０８のデータ（以下、単にシーケンス図１０８とも称する）を格納するシーケンス図格納手段１０１、状態遷移表１０９のデータ（以下、単に状態遷移表１０９とも称する）を格納する状態遷移表格納手段１０２、シーケンス図格納手段１０１に格納されたシーケンス図１０８に基づいて検証ソフトウェアを生成する検証ソフトウェア生成手段１０３、状態遷移表格納手段１０２に格納された状態遷移表１０９から検証対象ソフトウェアを生成する検証対象ソフトウェア生成手段１０４、生成した検証ソフトウェアと検証対象ソフトウェアとに対してビルドを行い実行可能な実行モジュールを生成する実行モジュール生成手段１０５、実行モジュール生成手段１０５にて生成された実行モジュールを実行し、シーケンス図１０８と状態遷移表１０９との整合性の検証を実行する検証実行手段１０６とを備え、ソフトウェア設計検証装置１１０は、検証実行手段１０６にて得られた検証結果を表示する検証結果提示手段１０７に接続される。
【００１６】
なお、本実施形態によるソフトウェア設計検証装置１１０は、プログラムによって図１のブロック図に従って機能化されたパーソナルコンピュータなどの情報端末によって構成され、図１のブロック図の機能が実行される。シーケンス図格納手段１０１および状態遷移表格納手段１０２は、磁気ディスク装置（図示せず）などの不揮発性の補助記憶装置で構成されており、シーケンス図１０８と状態遷移表１０９とがそれぞれに格納されている。また、検証ソフトウェア生成手段１０３、検証対象ソフトウェア生成手段１０４、実行モジュール生成手段１０５、および検証実行手段１０６は、通常は磁気ディスク装置（図示せず）などの不揮発性の補助記憶装置に格納されているが、ソフトウェア設計検証装置１１０の実行時には主メモリ（図示せず）に呼び出してＣＰＵによって実行される。また、検証結果提示手段１０７は、液晶モニタ（図示せず）などの外部ディスプレイ装置で構成されている。
【００１７】
次に、ソフトウェア設計装置１１０の動作の概要について説明する。
【００１８】
図２は、本実施形態によるソフトウェア設計検証装置１１０の動作を示すフローチャートである。図２に示すように、ソフトウェア設計検証装置１１０の実行を開始すると、検証ソフトウェア生成手段１０３は、シーケンス図格納手段１０１に格納されているシーケンス図１０８を読み出し（ステップＳ２０１）、読み出したシーケンス図１０８の内容に基づいて検証ソフトウェアを生成する（ステップＳ２０２）。一方、検証対象ソフトウェア生成手段１０４は、状態遷移表格納手段１０２に格納されている状態遷移表１０９を読み出し（ステップＳ２０３）、読み出した状態遷移表１０９の内容に基づいて検証対象ソフトウェアを生成する（ステップＳ２０４）。ステップＳ２０４の後、実行モジュール生成手段１０５は、ステップＳ２０２にて生成した検証ソフトウェアとステップＳ２０４にて生成した検証対象ソフトウェアとに対してビルドを行い、実行モジュールを生成する（ステップＳ２０５）。ステップＳ２０５の後、検証実行手段１０６は、ステップＳ２０５にて生成した実行モジュールを実行し（ステップＳ２０６）、実行結果に基づいてシーケンス図１０８と状態遷移表１０９との整合性検証を行う（ステップＳ２０７）。ステップＳ２０７にて整合性検証が終わると、検証の結果を検証結果提示手段１０７に表示する（ステップＳ２０８）。
【００１９】
なお、検証ソフトウェア生成手段１０３にて生成された検証ソフトウェア、検証対象ソフトウェア生成手段１０４にて生成された検証対象ソフトウェア、および実行モジュール生成手段１０５にて生成された実行モジュールは、それぞれ補助記憶装置（図示せず）に格納される。
【００２０】
次に、シーケンス図格納手段１０１に格納されるシーケンス図１０８について説明する。
【００２１】
図３は、本実施形態によるシーケンス図１０８の一例を示す図である。図３に示すように、シーケンス図１０８に含まれるオブジェクト３０１からオブジェクト３０３のうち、状態遷移表を持つオブジェクトを検証対象オブジェクト３０３とする。また、シーケンス図１０８には、シーケンスを開始する前の検証対象オブジェクト３０３の初期状態３０５が書き加えられている。シーケンス図格納手段１０１には、図３に示すようなシーケンス図１０８が少なくとも１つ以上格納されている。検証対象オブジェクト３０３は、上記の通り、状態遷移表を持つオブジェクトである。ソフトウェア設計検証装置１１０を実行する際には、シーケンス図１０８に含まれるオブジェクトのうちの１つのオブジェクトを検証対象オブジェクトとして設定し、設定した検証対象オブジェクトが持つ状態遷移表１０９とシーケンス図１０８の整合性検証を行う。なお、他の状態遷移表１０９の整合性検証を行う場合は、整合性検証を行う対象となる状態遷移表１０９を持つオブジェクトを検証対象オブジェクトとして設定してソフトウェア設計検証装置１１０を実行する。
【００２２】
次に、図３に示すシーケンス図１０８と検証ソフトウェア生成手段１０３にて生成される検証ソフトウェアとの関係について説明する。
【００２３】
検証ソフトウェア生成手段１０３は、図３に示すシーケンス図１０８を読み込み、読み込んだシーケンス図１０８に基づいて検証ソフトウェアを生成しており、シーケンス図１０８に含まれるオブジェクト３０１からオブジェクト３０３のうち、検証対象オブジェクト３０３を除いたオブジェクト３０１およびオブジェクト３０２（非検証対象オブジェクト）の動作を実現するソフトウェアを生成する（検証ソフトウェアの生成方法については後述する）。
【００２４】
次に、状態遷移表格納手段１０２に格納される状態遷移表１０９について説明する。
【００２５】
図４は、本実施形態による状態遷移表１０９の一例を示す図である。図４に示すように、状態遷移表１０９は、図３に示すシーケンス図１０８に含まれるオブジェクト３０１からオブジェクト３０３のうちの検証対象オブジェクト３０３の動作について記述されたものであり、検証対象オブジェクト３０３の現在の状態（現在状態）を示す現在状態記述行４０１と、検証対象オブジェクト３０３に入力されるメッセージを示すイベント名記述列４０２とからなる二次元の表形式で記述される。
【００２６】
現在状態記述行４０１に記述される各状態には、図３に示すシーケンス図１０８に含まれる検証対象オブジェクト３０３の初期状態３０５が記述される。また、イベント名記述列４０２に記述されるイベントは、図３に示すシーケンス図１０８に含まれ、検証対象オブジェクト３０３に入力されるメッセージが記述される。
【００２７】
処理内容４０３には、検証対象オブジェクト３０３の現在の状態と入力されるイベントとに基づいた処理内容が記述されている。例えば、検証対象オブジェクト３０３の現在の状態が“ｓｔａｔｅ１”の時に“ｍｅｓｓａｇｅ１１”が入力されると、検証対象オブジェクト３０３は処理内容４０３内のセル４０４の処理内容を実行する。セル４０４では、現在の状態を “ｓｔａｔｅ１”から“ｓｔａｔｅ２”に変更し、かつ、ｍｅｓｓａｇｅ１０１を出力するという処理内容が示されている。このセル４０４の処理内容は、図３に示すシーケンス図１０８において、オブジェクト３０１から検証対象オブジェクト３０３に対して“ｍｅｓｓａｇｅ１１”を送信した後、検証対象オブジェクト３０３からオブジェクト３０２に“ｍｅｓｓａｇｅ１０１”を送信する内容を示している。また、処理内容４０３の各セルにおける処理内容を区別することができるように、状態の変更を示すキーワードとして「Ｓ：」が、出力メッセージを示すキーワードとして「Ａ：」が記述されている。
【００２８】
また、検証対象オブジェクト３０３の現在の状態と入力されるイベントとの組合せが存在しないとき、あるいは、組合せが存在しても何も処理しない（処理内容の記述がない）場合は、処理内容４０３内のセル４０５のように空白で示される。また、状態遷移表格納手段１０２には、図４に示すような状態遷移表１０９が少なくとも１つ以上格納されている。
【００２９】
次に、図４に示す状態遷移表１０９と検証対象ソフトウェア生成手段１０４にて生成される検証対象ソフトウェアとの関係について説明する。
【００３０】
検証対象ソフトウェア生成手段１０４は、図４に示す状態遷移表１０９を読み込み、読み込んだ状態遷移表１０９に基づいて検証対象ソフトウェアを生成しており、図３に示すシーケンス図１０８に含まれる検証対象オブジェクト３０３の動作を実現するソフトウェアを生成している。
【００３１】
次に、シーケンス図１０８と状態遷移表１０９との整合性検証の考え方について説明する。
【００３２】
図３に示すシーケンス図１０８に基づいて作成された図４に示す状態遷移表１０９が、シーケンス図１０８の内容を正しく反映して作成されていれば、検証対象ソフトウェア生成手段１０４で生成される状態遷移表１０９の動作を実現する検証対象ソフトウェアを、検証ソフトウェア生成手段１０３で生成される検証対象オブジェクトを除いたオブジェクト（図３のオブジェクト３０１，３０２）の動作を実現する検証ソフトウェアで制御すると、検証対象ソフトウェアは、図３に示すシーケンス図１０８の検証対象オブジェクトの記述順序通りにかつ漏れなくメッセージ（図３の“ｍｅｓｓａｇｅ１０１”，“ｍｅｓｓａｇｅ１０２”）を出力する。つまり、検証対象ソフトウェアの動作結果が、シーケンス図１０８に含まれる検証対象オブジェクトが送信するメッセージの順序に一致しかつ漏れがないことを確認することができれば、シーケンス図１０８と状態遷移表１０９との整合性検証ができたといえる。
【００３３】
ソフトウェア設計検証装置１１０では、上記の考えを実現する検証ソフトウェアと検証対象ソフトウェアを生成し、生成した各ソフトウェアを動作させることによって整合性検証を行い、検証結果の判定を行う。以下では、検証ソフトウェア生成手段１０３の動作、および検証対象ソフトウェア生成手段１０４の動作についてそれぞれ詳細に説明する。
【００３４】
まず、検証ソフトウェア生成手段１０３の動作について説明する。
【００３５】
検証ソフトウェア生成手段１０３は、シーケンス図格納手段１０１から読み出した図３に示すシーケンス図１０８のデータに基づいて検証ソフトウェアを生成する。検証ソフトウェアの生成について、図５から図７に示すフローチャートと、図８に示す検証ソフトウェアとを用いて説明する。図５から図７は、本実施形態による検証ソフトウェア生成手段１０３の動作を示すフローチャートである。また、図８は、検証ソフトウェア生成手段１０３で作成される検証ソフトウェアの一例を示す図である。
【００３６】
なお、本実施形態による検証ソフトウェア生成手段１０３が生成する検証ソフトウェアは、シーケンス図格納手段１０１に格納されている全てのシーケンス図１０８の内容を含み、かつ、生成される検証ソフトウェアは１つのソフトウェアとする。また、図５に示すフローチャートは、図２に示すフローチャートのステップＳ２０１からステップＳ２０２までの処理を含んでいる。また、図５のフローチャートを実行する際には、予め作成されたシーケンス図１０８がシーケンス図格納手段１０１に格納されている。
【００３７】
図５に示すように、検証ソフトウェア生成手段１０３は、シーケンス図格納手段１０１に格納されている最初のシーケンス図１０８を読み出す（ステップＳ５０１）。ステップＳ５０１の後、ステップＳ５０１にて読み出したシーケンス図１０８に含まれる検証対象オブジェクトの名前を取得（検証対象オブジェクトの名前の取得方法については後述する）する（検証対象オブジェクト特定手段）（ステップＳ５０２）。
【００３８】
ステップＳ５０２の後、ステップＳ５０１で読み出したシーケンス図１０８に含まれる検証対象オブジェクト３０３に設定されている初期状態を読み出す（初期状態抽出手段）（ステップＳ５０３）。
【００３９】
ステップＳ５０３の後、ステップＳ５０１で読み出したシーケンス図１０８に含まれる全てのメッセージの情報（メッセージ情報）を読み出し（メッセージ情報抽出手段）、その出現順序と、各メッセージの送信オブジェクト名および受信オブジェクト名を格納（図９に格納の一例を示すが、詳細については後述）する（ステップＳ５０４）。ステップＳ５０４の後、シーケンス図格納手段１０１に格納されているシーケンス図１０８を全て読み出したか否かが判断され（ステップＳ５０５）、読み出していないシーケンス図１０８が存在する場合（ステップＳ５０５において“Ｎｏ”の場合）は、ステップＳ５０１に進み、新たなシーケンス図１０８を読み出して処理（ステップＳ５０１〜ステップＳ５０５の処理）を継続する。一方、ステップＳ５０５において、全てのシーケンス図１０８を読み出したと判断された場合（ステップＳ５０５において“Ｙｅｓ”の場合）は、図６に示すフローチャートのステップＳ６０１に進む。
【００４０】
このように、検証ソフトウェア生成手段１０３は、シーケンス図１０８に含まれる検証対象オブジェクトを特定する検証対象オブジェクト特定手段と、シーケンス図１０８の内容を実行する前の検証対象オブジェクトの状態である、シーケンス図１０８に含まれた初期状態を抽出する初期状態抽出手段と、シーケンス図１０８に含まれるメッセージ情報を抽出するメッセージ情報抽出手段とを備え、検証対象オブジェクト特定手段にて特定された検証対象オブジェクト、初期状態抽出手段にて抽出された初期状態、およびメッセージ情報抽出手段にて抽出されたメッセージ情報によって検証ソフトウェアを作成している。
【００４１】
ここで、図９に示すシーケンス図１０８に含まれるメッセージの情報の格納方法について、図３を用いて説明する。図９は、本実施形態による検証ソフトウェア生成手段１０３で格納されるメッセージ情報の一例を示す図である。
【００４２】
図９に示すように、検証ソフトウェア生成手段１０３は、図３に示すようなシーケンス図１０８を読み出すと、読み取ったシーケンス図名をシーケンス図名記述列９０１に出力する。また、オブジェクト３０１から検証対象オブジェクト３０３に対して送信するメッセージ“ｍｅｓｓａｇｅ１１”から、メッセージ名（ｍｅｓｓａｇｅ１１が該当）をメッセージ名記述列９０２に出力し、送信オブジェクト名（オブジェクト１が該当）を送信オブジェクト名記述列９０３に出力し、受信オブジェクト名（検証対象オブジェクトが該当）を受信オブジェクト名記述列９０４に出力する。以下、シーケンス図１０８から、“ｍｅｓｓｅｇｅ１１”の後に続く“ｍｅｓｓａｇｅ１０１”、“ｍｅｓｓａｇｅ１２”を取得し、メッセージ名記述列９０２、送信オブジェクト名記述列９０３、受信オブジェクト名記述列９０４にそれぞれ出力する。最初に読み出したシーケンス図１０８の出力を終えると、シーケンス図格納手段１０１に格納されている他のシーケンス図を読み出して上記と同様の動作を繰り返し、当該動作を全てのシーケンス図１０８を読み出すまで続ける。
【００４３】
図６では、シーケンス図格納手段１０１に格納されているシーケンス図１０８のそれぞれに対して１つのテスト関数を作成する動作を示している。
【００４４】
図６に示すように、図５のステップＳ５０５において全てのシーケンス図１０８が読み出されたと判断されると、検証ソフトウェアの内容がシーケンス図１０８の内容の影響を受けない固定部（図８の行番号０１〜０２）を出力する（ステップＳ６０１）。なお、図８の行番号０１は、検証ソフトウェア生成部１０３が生成する検証ソフトウェアのクラス名を示し、図８の行番号０２は、検証対象ソフトウェアが出力する（検証対象ソフトウェアから送信されてきた）メッセージを格納するリストの宣言と初期化命令（初期状態設定手段）を示している。また、本実施形態では、クラス名を“Ｔｅｓｔｃｏｄｅ”とし、リスト名を“ａｃｔｉｏｎＬｉｓｔ”としている。
【００４５】
ステップＳ６０１の後、テスト関数名（図８の行番号０３）を出力する（ステップＳ６０２）。なお、本実施形態では、シーケンス図格納手段１０１に格納されているシーケンス図１０８に含まれるシーケンス図のそれぞれに対して、１つのテスト関数を作成するものとする。従って、ステップＳ６０２にて書き込まれる（出力される）テスト関数名は、１つ目のシーケンス図では「ｔｅｓｔＳｅｑｕｅｎｃｅ１」とし、二つ目のシーケンス図では「ｔｅｓｔＳｅｑｕｅｎｃｅ２」など、シーケンス図１０８を読み出すごとに数字を１ずつ増やすこととする。
【００４６】
ステップＳ６０２の後、ステップＳ５０３で読み出した初期状態を設定する命令（図８の行番号０４）を出力する（ステップＳ６０３）。
【００４７】
ステップＳ６０３の後、図３に示す検証対象オブジェクト３０３に最初に入力するメッセージ（以下、トリガーメッセージ（シーケンス開始メッセージ）とも称する）の実行命令（図８の行番号０５）を出力する（シーケンス開始メッセージ送信設定手段）（ステップＳ６０４）。トリガーメッセージは、図９に格納されるメッセージのうち、受信オブジェクト名記述列９０４の最初に検証対象オブジェクト３０３が現れるメッセージ名が対応する。なお、本実施形態では、“ｍｅｓｓａｇｅ１１”がトリガーメッセージとなる。
【００４８】
ステップＳ６０４の後、検証対象オブジェクト３０３がシーケンス図１０８に記述された通りに実行したかを検証する検証命令（図８の行番号０６〜０９）を出力する（整合性検証設定手段）（ステップＳ６０５）。検証対象となるメッセージは、図９に格納されるメッセージのうち、送信オブジェクト名記述列９０３が検証対象オブジェクト３０３になっているときのメッセージ名が対応する。これを図９の上から順に、複数ある場合は複数のメッセージ名の検証命令を出力する。なお、本実施形態では、検証命令の例として、Ｊａｖａ（登録商標）言語やＣ言語などに標準で用意されている“ａｓｓｅｒｔ”を用いている。
【００４９】
ステップＳ６０５の後、他のシーケンスの検証を行う準備のために、格納した検証対象オブジェクトが出力するメッセージのリストの削除命令（図８の行番号１０〜１１）を出力する（ステップＳ６０６）。
【００５０】
ステップＳ６０６の後、シーケンス図格納手段１０１に格納されている全てのシーケンス図１０８を読み出したか否かが判断され（ステップＳ６０７）、読み出していないシーケンス図１０８が存在する場合（ステップＳ６０７において“Ｎｏ”の場合）はステップＳ６０２に進み、新たなシーケンス図１０８を読み出して処理（ステップＳ６０２〜ステップＳ６０７）を継続する。一方、全てのシーケンス図１０８が読み出されたと判断された場合（ステップＳ６０７において“Ｙｅｓ”の場合）は、図７に示すステップＳ７０１に進む。
【００５１】
このように、検証ソフトウェア生成手段１０３は、初期状態を検証ソフトウェアに設定する初期状態設定手段と、非検証対象オブジェクトから検証対象オブジェクトに最初に送信されるシーケンス開始メッセージを検証ソフトウェアに設定するシーケンス開始メッセージ送信設定手段と、整合性の検証の実行を検証ソフトウェアに設定する整合性検証設定手段とを備えている。
【００５２】
図７では、検証対象ソフトウェアが検証ソフトウェアにアクセスする関数を作成する動作について示している。
【００５３】
図７に示すように、図６のステップＳ６０７において全てのシーケンス図１０８が読み出されたと判断されると、図９に格納されているメッセージの一行目の内容を読み出す（ステップＳ７０１）。
【００５４】
ステップＳ７０１の後、ステップＳ７０１で読み出された行の送信オブジェクト名記述列９０３が検証対象オブジェクトであるか否かが判断される（ステップＳ７０２）。
【００５５】
ステップＳ７０２にて送信オブジェクト名が検証対象オブジェクトであると判断されると（ステップＳ７０２において“Ｙｅｓ”の場合）、ステップＳ７０１で読み出された行の受信オブジェクト名記述列９０４が検証対象オブジェクトであるか否かが判断される（ステップＳ７０３）。
【００５６】
ステップＳ７０３にて受信オブジェクト名が検証対象オブジェクト名でないと判断されると（ステップＳ７０３において“Ｎｏ”の場合）、ステップＳ７０１で読み出した行のメッセージ名記述列９０２に記述されるメッセージ名をメッセージリストに格納し（ステップＳ７０４）、ステップＳ７０５に進む。
【００５７】
ステップＳ７０２にて送信オブジェクト名が検証対象オブジェクトでないと判断された場合（ステップＳ７０２において“Ｎｏ”の場合）、あるいは、ステップＳ７０３にて受信オブジェクト名が検証対象オブジェクトであると判断された場合（ステップＳ７０３において“Ｙｅｓ”の場合）は、ステップＳ７０４にてメッセージリストに格納されたメッセージが存在するか否かが判断される（ステップＳ７０６）。
【００５８】
ステップＳ７０６にてメッセージリストにメッセージが存在すると判断された場合（ステップＳ７０６において“Ｙｅｓ”の場合）は、検証対象ソフトウェアが検証ソフトウェアにアクセスする関数名（第１のコール関数、第１のコール関数設定手段）と呼び出された関数名を保持する命令（動作結果保持設定手段）（図８の行番号１２〜１３）を出力し、さらに、ステップＳ７０４にて格納したメッセージ（第１のメッセージ）を検証対象ソフトウェアに送信する（第１のメッセージ送信設定手段）命令（図８の行番号１４〜１５）を出力し（ステップＳ７０７）、ステップＳ７１０に進む。一方、ステップＳ７０６にてメッセージリストにメッセージが存在しないと判断されるとステップＳ７０５に進む。
【００５９】
ステップＳ７０５では、図９に格納されている全てのメッセージを読み出したか否かが判断され、全てのメッセージを読み出していない場合（ステップＳ７０５で“Ｎｏ”の場合）は、読み出す行の位置を次の行に移動させて、ステップＳ７０１に進む。
【００６０】
一方、ステップＳ７０５において、図９に格納されるメッセージを全て読み出した場合（ステップＳ７０５において“Ｙｅｓ”の場合）は、ステップＳ７０８に進み、ステップＳ７０６と同様の判断がなされる。
【００６１】
ステップＳ７０８にてメッセージリストに格納したメッセージが存在すると判断された場合（ステップＳ７０８で“Ｙｅｓ”の場合）は、ステップＳ７０９に進む。
【００６２】
ステップＳ７０９では、ステップＳ７０７と同様の処理が実行され、ステップＳ７１０に進む。
【００６３】
一方、ステップＳ７０８において、メッセージリストに格納したメッセージが存在しないと判断された場合（ステップＳ７０８において“Ｎｏ”の場合）は、ステップＳ７１０に進む。
【００６４】
ステップＳ７１０では、検証ソフトウェア全体の終了処理（図８の行番号２０）を出力し、検証ソフトウェア生成手段１０３の動作を終了する。
【００６５】
このように、検証ソフトウェア生成手段１０３は、検証対象オブジェクトから呼び出される第１のコール関数を検証ソフトウェアに設定する第１のコール関数設定手段を備え、第１のコール関数設定手段は、検証対象オブジェクトの動作結果を保持する旨を検証ソフトウェアに設定する動作結果保持設定手段と、非検証対象オブジェクトから検証対象オブジェクトに第１のメッセージを送信する旨を検証ソフトウェアに設定する第１のメッセージ送信設定手段とを備えている。
【００６６】
次に、検証オブジェクトの名前の取得方法について説明する。検証対象オブジェクトの取得方法としては、シーケンス図１０８に含まれるオブジェクト３０１からオブジェクト３０３のうち、初期状態３０５を書き加えるオブジェクトを一つに限定するようにし、検証ソフトウェア生成手段１０３が検証ソフトウェアを生成する際に、初期状態３０５が書き加えられているオブジェクトを検証対象オブジェクト３０３として読み込む。その具体的な方法については、図１０に示すような、シーケンス図１０８をＸＭＬ（Ｅｘｔｅｎｓｉｂｌｅ  Ｍａｒｋｕｐ  Ｌａｎｇｕａｇｅ）に変換した一例を用いて説明する。なお、シーケンス図からＸＭＬへの変換は、図示しないＵＭＬ（Ｕｎｉｆｉｅｄ  Ｍｏｄｅｌｉｎｇ  Ｌａｎｇｕａｇｅ）エディタなどのソフトウェアで実現することができる。
【００６７】
図１０は、本実施形態によるシーケンス図１０８をＸＭＬ形式に変換した一例を示す図である。図１０に示すように、ＸＭＬにおいて、シーケンス図１０８に含まれるオブジェクト３０１からオブジェクト３０３は、タグ１００１からタグ１００３にそれぞれ記述され、初期状態３０５はタグ１００４に記述されている。また、初期状態３０５の内容はタグ１００５に記述されている。
【００６８】
検証ソフトウェア生成手段１０３は、検証対象オブジェクト３０３の名前を取得するために、初期状態３０５が記述されているタグ１００４の「ｃｏｖｅｒｅｄ」以下の“Ｌ００３”を読み取り、読み取った“Ｌ００３”が、タグ１００１からタグ１００３のどの「ｘｍｉ．ｉｄ」に設定されているかを読み取る。図１０では、“Ｌ００３”がタグ１００３に設定されているので、タグ１００３の「ｎａｍｅ」以下の“検証対象”を読み取り、読み取った“検証対象”を検証対象オブジェクトの名前として取得する。
【００６９】
次に、検証対象ソフトウェア生成手段１０４の動作について説明する。
【００７０】
検証対象ソフトウェア生成手段１０４は、図４に示す状態遷移表１０９を状態遷移表格納手段１０２から読み込み、読み込んだ状態遷移表１０９に基づいて検証対象ソフトウェアを生成する。検証対象ソフトウェア生成手段１０４の詳細な動作について、図１１に示すフローチャートと、図１２に示す検証対象ソフトウェアの一例に従い説明する。図１１は、本実施形態による検証対象ソフトウェア生成手段１０４の動作を示すフローチャートである。また、図１２は、検証対象ソフトウェア生成手段１０４で作成される検証対象ソフトウェアの一例を示す図である。
【００７１】
なお、本実施形態では、検証対象ソフトウェア生成手段１０４が生成する検証対象ソフトウェアは、状態遷移表格納手段１０２に格納される状態遷移表１０９の内容を含み、かつ１つのソフトウェアとする。また、図１１に示すフローチャートは、図２に示すフローチャートのステップＳ２０３からステップＳ２０４までの処理を含んでいる。また、図１１のフローチャートを実行する前には、予め作成された状態遷移表１０９が状態遷移表格納手段１０２に格納されている。
【００７２】
図１１に示すように、検証対象ソフトウェア生成手段１０４は、状態遷移表格納手段１０２に格納されている状態遷移表１０９を読み出す（ステップＳ１１０１）。すなわち、検証対象ソフトウェア生成手段１０４は、状態遷移表１０９に含まれ、非検証対象オブジェクトから検証対象オブジェクトに入力されるメッセージである入力イベントを抽出する入力イベント抽出手段と、状態遷移表１０９に含まれ、検証対象オブジェクトの現在の状態を示す現在状態を抽出する現在状態抽出手段と、入力イベントと現在状態とに基づく処理内容を抽出する処理内容抽出手段と、処理内容に基づき、現在状態を変更した変更状態を抽出する変更状態抽出手段と、処理内容に基づき、変更状態の抽出の際に、検証対象オブジェクトから非検証対象オブジェクトに送信される第２のメッセージを抽出する第２のメッセージ抽出手段とを備え、入力イベント抽出手段にて抽出された入力イベント、現在状態抽出手段にて抽出された現在状態、処理内容抽出手段にて抽出された処理内容、変更状態抽出手段にて抽出された変更状態、および第２のメッセージ抽出手段にて抽出された第２のメッセージによって、検証対象ソフトウェアを生成する。
【００７３】
ステップＳ１１０１の後、検証対象ソフトウェアの内容が状態遷移表１１０９の内容の影響を受けない固定部（図１２の行番号０１〜０５）を出力する（ステップＳ１１０２）。なお、図１２の行番号０１は、検証対象ソフトウェア生成部１０４が生成する検証対象ソフトウェアのクラス名であり、図１２の行番号０２は、検証対象ソフトウェアの現在状態を示す変数の宣言である。本実施形態では、クラス名を“Ｔｅｓｔｔａｒｇｅｔ”とし、状態変数名を“ｓｔａｔｅ”としている。
【００７４】
ステップＳ１１０２の後、図４に示すような状態遷移表１０９の一行目の内容を読み出す（ステップＳ１１０３）。
【００７５】
ステップＳ１１０３の後、ステップＳ１１０３にて読み出した行に記述されるイベント名記述列４０２を利用し、検証ソフトウェアが検証対象ソフトウェアにアクセスする関数（第２のコール関数）（図１２の行番号０６）を出力する（ステップＳ１１０４）。
【００７６】
ステップＳ１１０４の後、ステップＳ１１０３にて読み出した行の処理内容４０３のうち最左セル（図４のセル４０４）の内容を読み出す（ステップＳ１１０５）。
【００７７】
ステップＳ１１０５の後、ステップＳ１１０５にて読み出されたセルの内容が空であるか否かが判断され（ステップＳ１１０６）、空である場合（ステップＳ１１０６において“Ｙｅｓ”の場合）は、何も出力せずにステップＳ１１０７に進む。一方、空でない場合（ステップＳ１１０６において“Ｎｏ”の場合）は、ステップＳ１１０８に進む。
【００７８】
ステップＳ１１０８では、ステップＳ１１０５にて読み出されたセルの内容に基づき、検証対象ソフトウェアが実行する処理の内容を出力する。出力内容としては、検証対象ソフトウェアの現在の状態を条件判定文とする命令（図１２の行番号０７）を出力し（状態判定設定手段）、次に、読み出したセルの一行一行を確認し、行の先頭が「Ｓ：」である場合は、検証対象オブジェクトの現在の状態を変更する処理（図１２の行番号０８）を出力し（状態変更設定手段）、行の先頭が「Ａ：」である場合は、検証ソフトウェアへのメッセージ（第２のメッセージ）の送信命令（図１２の行番号０９）を出力し（第２のメッセージ送信設定手段）、最後に、条件判定文を閉じる処理（図１２の行番号１０）を出力する。出力した後、ステップＳ１１０７に進む。
【００７９】
ステップＳ１１０７では、ステップＳ１１０３にて読み出された行における全てのセルの内容を読み出したか、つまり、ステップＳ１１０５で読み出したセルの一つ右にセルが存在するか否かが判断され、読み出していないセルが存在する場合（ステップＳ１１０７において“Ｎｏ”の場合）は、読み出すセルの位置を一つ右に移動してステップＳ１１０５に進む。一方、全てのセルの内容を読み出した場合（ステップＳ１１０７において“Ｙｅｓ”の場合）は、検証ソフトウェアが検証対象ソフトウェアにアクセスする関数を閉じる処理（図１２の行番号１１）を出力してステップＳ１１０９に進む。
【００８０】
ステップＳ１１０９では、全ての行を読み出したか否かが判断され、全て読み出していない場合（ステップＳ１１０９において“Ｎｏ”の場合）は、読み出す行の位置を次の行に移動してステップＳ１１０３に進む。一方、全ての行を読み出した場合（ステップＳ１１０９において“Ｙｅｓ”の場合）は、検証対象ソフトウェア全体の終了処理（図１２の行番号２７）を出力し、検証対象ソフトウェア生成手段１０４の動作を終了する。
【００８１】
次に、図４に示すイベント名記述列４０２に記載されるイベントのうち、複数の処理内容４０３を持つイベントがあった場合の処理について、さらに詳しく説明する。説明の便宜上、検証対象ソフトウェア生成手段１０４は、図４のセル４０６までの処理を終了し、図１２の行番号２１までを出力しているものとする。また、このとき、検証対象ソフトウェア生成手段１０４は、図１１のステップＳ１１０８を終えているものとする。
【００８２】
ステップＳ１１０７では、セル４０７の処理が終了していないためステップＳ１１０５に進み、ステップＳ１１０５にてセル４０７の内容を読み出してステップＳ１１０６に進み、ステップＳ１１０６にてセル４０７は空でないためステップＳ１１０８に進む。
【００８３】
ステップＳ１１０８では、セル４０７の内容に基づいた出力を行うが、この時の条件判定文として既にセル４０６の内容に基づいた命令として“ｉｆ”が出力されているため、処理内容４０３を複数持つイベントにおける２つ目以降のセルに対する条件判定の命令文として“ｅｌｓｅ  ｉｆ” （図１２の行番号２２）を出力する。その後、前述の通り、検証対象オブジェクトの現在の状態を変更する処理（図１２の行番号２３）と検証ソフトウェアへのメッセージ送信命令（図１２の行番号２４）を出力し、最後に条件判定文を閉じる処理（図１２の行番号２５）を出力する。
【００８４】
このように、検証対象ソフトウェア生成手段１０４は、検証オブジェクトから呼び出される第２のコール関数を検証対象ソフトウェアに設定する第２のコール関数設定手段を備え、第２のコール関数設定手段は、現在状態を条件判定として検証対象ソフトウェアに設定する状態判定設定手段を含み、状態判定設定手段は、現在状態を変更状態に変更する旨を検証対象ソフトウェアに設定する状態変更設定手段と、第２のメッセージを検証対象ソフトウェアに設定する第２のメッセージ送信設定手段とを備えている。
【００８５】
次に、実行モジュール生成手段１０５の動作について説明する。
【００８６】
実行モジュール生成手段１０５は、検証ソフトウェア生成手段１０３にて生成された検証ソフトウェアと、検証対象ソフトウェア生成手段１０４にて生成された検証対象ソフトウェアとに対してビルドを行い、実行モジュールを生成する。
【００８７】
次に、実行モジュール生成手段１０５の構成について説明する。
【００８８】
実行モジュール生成手段１０５は、プログラミング言語で書かれたソフトウェアをコンピュータが直接に実行可能な機械語のプログラムに変換するソフトウェアであるコンパイラや、コンパイラによって変換された機械語のプログラムに対して必要なライブラリなどを付け加えて実行可能なモジュールを生成するソフトウェアであるリンカなどで構成されている。
【００８９】
次に、検証実行手段１０６の動作について説明する。
【００９０】
検証実行手段１０６では、実行モジュール生成手段１０５にて生成された実行モジュールの実行、および実行モジュールの動作結果からシーケンス図１０８と状態遷移表１０９との整合性検証と判定を行う。
【００９１】
検証実行手段１０６において、実行モジュール生成手段１０５にて生成された実行モジュールを実行すると、検証ソフトウェア生成手段１０３にて生成された検証ソフトウェア、および検証対象ソフトウェア生成装置１０４にて生成された検証対象ソフトウェアが動作を開始する。すなわち、シーケンス図格納手段１０１に格納されているシーケンス図１０８と状態遷移表格納手段１０２に格納されている状態遷移表１０９との整合性検証と判定を開始する。以下では、検証実行手段１０６にて行われるシーケンス図１０８と状態遷移表１０９との整合性検証および判定の方法を、検証ソフトウェアと検証対象ソフトウェアとの動作に基づいて図８，１２，１３を用いて説明する。
【００９２】
図１３は、本実施形態による検証ソフトウェアおよび検証対象ソフトウェアに基づく検証実行手段における実行モジュールの動作を示す図である。
【００９３】
図１３に示すように、まず、検証実行手段１０６で実行モジュールが実行されると、図８の行番号０３が呼び出される。そして、検証対象ソフトウェアに対して初期状態のセットが行われ（図８の行番号０４）、トリガーメッセージである“ｍｅｓｓａｇｅ１１”を検証対象ソフトウェアに対して送信する（図８の行番号０５）。
【００９４】
検証対象ソフトウェアが“ｍｅｓｓａｇｅ１１”を送信すると、図１２の行番号０６が呼び出され、現在状態を“ｓｔａｔｅ２”に変更した（図１２の行番号０８）後、検証ソフトウェアに対して“ｍｅｓｓａｇｅ１０１”を送信する（図１２の行番号０９）。
【００９５】
検証対象ソフトウェアが検証ソフトウェアに対して“ｍｅｓｓａｇｅ１０１”を送信すると、図８の行番号１２が呼び出され、“ｍｅｓｓａｇｅ１０１”が呼び出されたことを蓄積するため“ｍｅｓｓａｇｅ１０１”をａｃｔｉｏｎＬｉｓｔに格納した（図８の行番号１３）後、検証対象ソフトウェアに対して“ｍｅｓｓａｇｅ１２”を送信する（図８の行番号１４）。
【００９６】
検証ソフトウェアが検証対象ソフトウェアに対して“ｍｅｓｓａｇｅ１２”を送信すると、検証対象ソフトウェアでは図１２の行番号１２が呼び出され、現在状態を“ｓｔａｔｅ３”に変更した（図１２の行番号１４）後、検証ソフトウェアに対して“ｍｅｓｓａｇｅ１０２”を送信する（図１２の行番号１５）。
【００９７】
検証対象ソフトウェアが検証ソフトウェアに対して“ｍｅｓｓａｇｅ１０２”を送信すると、図８の行番号１６が呼び出され、“ｍｅｓｓａｇｅ１０２”が呼び出されたことを蓄積するために“ｍｅｓｓａｇｅ１０２”をａｃｔｉｏｎＬｉｓｔに格納した（図８の行番号１７）後、検証対象ソフトウェアに対し“ｍｅｓｓａｇｅ１３”を送信する（図８の行番号１８）。
【００９８】
検証ソフトウェアが検証対象ソフトウェアに対して“ｍｅｓｓａｇｅ１３”を送信すると、図１２の行番号１８が呼び出され、現在状態を“ｓｔａｔｅ４”に変更する（図１２の行番号２０）。この後、処理が検証ソフトウェアに戻り（図８の行番号０５）、続いて整合性検証を行う。
【００９９】
これまでの処理によって、検証対象ソフトウェアの動作を確認できるようにしたａｃｔｉｏｎＬｉｓｔの０番目には“ｍｅｓｓａｇｅ１０１”が蓄積され、１番目には“ｍｅｓｓａｇｅ１０２”が蓄積されている。検証ソフトウェアに処理が戻ってくると、１番目の検証（図８の行番号０７）を行い、続いて２番目の検証（図８の行番号０８）を行う。
【０１００】
次に、本実施形態における整合性検証の方法について説明する。
【０１０１】
本実施形態における整合性検証は、検証対象ソフトウェアの動作結果、つまりａｃｔｉｏｎＬｉｓｔに格納されるメッセージ名と、シーケンス図１０８に記述されるオブジェクトの文字列が一致するかを見て行う。具体的には、検証ソフトウェアに処理が戻って来たときには、ａｃｔｉｏｎＬｉｓｔの０番目に、検証対象ソフトウェアの動作結果として“ｍｅｓｓａｇｅ１０１”が蓄積されている。ａｃｔｉｏｎＬｉｓｔの０番目に蓄積された“ｍｅｓｓａｇｅ１０１”とシーケンス図１０８に記載される検証対象オブジェクト３０３から出力される最初のメッセージ“ｍｅｓｓａｇｅ１０１”とが一致するか否かの検証（図８の行番号０７）を行う。本実施形態では一致しているため整合性検証は成功となる。続いて、ａｃｔｉｏｎＬｉｓｔの１番目に蓄積している“ｍｅｓｓａｇｅ１０２”と、シーケンス図１１５に記載される検証対象オブジェクト３０３から出力される２番目のメッセージ“ｍｅｓｓａｇｅ１０２”とが一致するか否かの検証（図８の行番号０８）を行う。本実施形態では一致しているため整合性検証は成功となる。すなわち、検証実行手段１０６は、保持された検証対象オブジェクトの動作結果がメッセージ情報に含まれ、かつ、動作結果の保持順序がメッセージ情報のシーケンス図１０８における処理順序と一致することによって、シーケンス図１０８と状態遷移表１０９との整合性があると判定する。
【０１０２】
次に、本実施形態における判定方法について説明する。
【０１０３】
本実施形態における判定は、シーケンス図１０８の内容と状態遷移表１０９の内容との整合性が取れているか否か（整合性があるか否か）の判定を行うものであり、上記の検証において、全ての検証に成功した場合は、シーケンス図１０８と状態遷移表１０９との整合性が取れている（整合性がある）と判定する。一方、１つでも検証が失敗した場合は、シーケンス図１０８と状態遷移表１０９との整合性は取れていない（整合性がない）と判定する。
【０１０４】
このように、本実施形態におけるソフトウェア検証装置１１０を実行することによって全ての検証に成功したということは、状態遷移表１０９を持つ検証対象オブジェクトはシーケンス図１０８に記述した順序通りにかつ漏れなくメッセージを送信しているといえ、さらに、状態遷移表１０９はシーケンス図１０８の内容を反映できているといえるため、シーケンス図１０８と状態遷移表１０９との整合性が取れていることを確認することができる。
【０１０５】
次に、検証結果提示手段１０７について説明する。
【０１０６】
検証結果提示手段１０７は、検証実行手段１０６にて判定された結果を表示する。本実施形態では、整合性検証に“ａｓｓｅｒｔ”を用いているため、整合性検証の結果をコンピュータのコンソール画面に出力する。出力例としては、検証実行手段１０６による整合性検証の結果、失敗する検証が無ければ（全ての検証が成功すれば）何も表示しないが、失敗する検証が存在すれば、検証に失敗したソフトウェアの名前と行番号を表示する。
【０１０７】
以上のことから、本実施形態によるソフトウェア設計検証装置では、シーケンス図１０８に基づいて検証ソフトウェアを生成するとともに、状態遷移表１０９に基づいて検証対象ソフトウェアを生成し、生成した検証ソフトウェアと検証対象ソフトウェアを実行して整合性検証を行うことによって、シーケンス図１０８と状態遷移表１０９との整合性検証を自動で検証することが可能となる。また、全ての整合性検証に成功すれば、状態遷移表１０９はシーケンス図１０８の内容を満たしていることを自動で検証することができる。また、整合性検証を自動で行うことによって、手戻りによる修正コストを低減できることが可能である。
【０１０８】
なお、本実施形態による検証ソフトウェア生成手段１０３において、検証対象オブジェクト名の取得方法として、シーケンス図１０８に含まれるオブジェクト３０１からオブジェクト３０３のうち、初期状態３０５が書き加えられているオブジェクトを検証対象オブジェクト３０３として読み込むよう構成したが、これに限らず、ソフトウェア設計検証装置１１０を実行する際の引数として、キーボード（図示せず）などの入力装置を使用して指定するような構成でもあってもよく、他の方法として、例えば磁気ディスク装置（図示せず）などの不揮発性の補助記憶装置にテキストファイルを格納し、当該テキストファイルに検証対象オブジェクト名を記述しておき、ソフトウェア設計検証装置１１０がテキストファイルに記述された検証対象オブジェクト名を読み取るような構成としてもよい。上記２つの方法であれば、初期状態３０５を書き加えるオブジェクトを、シーケンス図１０８において１つのオブジェクトに限定する必要はなく、複数のオブジェクトに初期状態を設定することが可能になる。
【０１０９】
また、本実施形態による状態遷移表１０９の処理内容４０３には、状態の変化を示すキーワードとして「Ｓ：」を、出力メッセージを示すキーワードとして「Ａ：」を記述するようにしたが、これに限らず、例えば、一行目に状態の変化を記述し、二行目以降に出力メッセージを記述するよう記述箇所を固定するようにしてもよい。
【０１１０】
また、本実施形態では、検証結果提示手段１１２は外部ディスプレイ装置（図示せず）などに表示されるコンソール画面で構成されるとしたが、これに限らず、例えば、テキストファイルに結果を出力して磁気ディスク装置（図示せず）などの不揮発性の補助記憶装置に格納するよう構成してもよい。
【０１１１】
また、本実施形態では、テスト関数の作成にあたり、１つのシーケンス図１０８に対して１つの関数を作成するとしたが、これに限らず、全てのシーケンス図１０８の内容をまとめて１つのテスト関数に含めてもよい。
【０１１２】
また、本実施形態では、検証ソフトウェア生成手段１０３にて生成される検証ソフトウェア、および検証対象ソフトウェア生成手段１０４にて生成される検証対象ソフトウェアを１つのファイルで構成するとしたが、これに限らず、複数のファイルで構成するようにしてもよい。
【０１１３】
また、本実施形態では、状態遷移表１０９の処理内容４０３において、状態とイベントとの組合せが存在しない場合、あるいは、組み合わせが存在していても何も処理しない場合は空白が記述されるとしたが、これに限らず、例えば明示的に「−」や、処理しないことが明確になるような別の記号を記述してもよい。
【符号の説明】
【０１１４】
１０１  シーケンス図格納手段、１０２  状態遷移表格納手段、１０３  検証ソフトウェア生成手段、１０４  検証対象ソフトウェア生成手段、１０５  実行モジュール生成手段、１０６  検証実行手段、１０７  検証結果提示手段、１１０  ソフトウェア設計検証装置、３０１，３０２  オブジェクト、３０３  検証対象オブジェクト、３０５  初期状態、４０１  現在状態記述行、４０２  イベント名記述列、４０３  処理内容、４０４〜４０７  セル、９０１  シーケンス図名記述列、９０２  メッセージ名記述列、９０３  送信オブジェクト名記述列、９０４  受信オブジェクト記述列、１００１〜１００５  タグ、１３０１  検証ソフトウェア、１３０２  検証対象ソフトウェア。
【図１】
2012173834.tif 000003
【図２】
2012173834.tif 000004
【図３】
2012173834.tif 000005
【図４】
2012173834.tif 000006
【図５】
2012173834.tif 000007
【図６】
2012173834.tif 000008
【図７】
2012173834.tif 000009
【図８】
2012173834.tif 000010
【図９】
2012173834.tif 000011
【図１０】
2012173834.tif 000012
【図１１】
2012173834.tif 000013
【図１２】
2012173834.tif 000014
【図１３】
2012173834.tif 000015