(57)【要約】【課題】ソフトウェアの検査において、検査したい部分とそうでない部分との間でメッセージ送受信がある場合、必要となる外部環境を自動的に生成することでソフトウェアの検査を効果的に支援する情報処理システムを提供する。【解決手段】外部環境生成手段１１０により、検査対象のソフトウェアの記述を元に検査対象の状態遷移を網羅するような外部環境を自動的に生成し、メッセージの送受信の動作に必要な通信相手を提供する。また、外部環境編集手段１３０により、自動的に生成された外部環境を雛形として利用者が外部環境を記述することを可能とする。【選択図】図９
2009123159.tif 000002
【特許請求の範囲】
【請求項１】
動作検査対象のソフトウェアの処理で送受信されるメッセージの情報を入力し、前記情報にもとづいて、前記動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を生成する検査対象入力手段と、
前記検査対象入力手段が生成した状態遷移情報にもとづいて、前記動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、生成した前記状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力する外部環境生成手段とを備え、
前記検査対象入力手段は、生成した状態遷移情報を前記動作検査手段に出力する
ことを特徴とする情報処理システム。
【請求項２】
動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を入力する検査対象入力手段と、
前記検査対象入力手段に入力された状態遷移情報にもとづいて、前記動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、生成した前記状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力する外部環境生成手段とを備え、
前記検査対象入力手段は、入力された状態遷移情報を前記動作検査手段に出力する
ことを特徴とする情報処理システム。
【請求項３】
動作検査手段に状態遷移情報にもとづいてソフトウェアの動作を検査させるために、外部環境生成手段が生成した状態遷移情報を記憶する外部環境保存手段と、
利用者の要求に応じて、前記外部環境保存手段に記憶されている状態遷移情報を変更する外部環境編集手段とを備えた
請求項１または請求項２記載の情報処理システム。
【請求項４】
外部環境生成手段は、動作検査対象のソフトウェアの状態遷移情報にもとづいて、前記動作検査対象のソフトウェアによってメッセージが送信されることを当該メッセージを受信することとし、前記動作検査対象のソフトウェアによってメッセージが受信されることを当該メッセージを送信することとした通信相手の状態遷移情報を生成する
請求項１から請求項３のうちいずれか１項記載の情報処理システム。
【請求項５】
動作検査対象のソフトウェアの動作を検査し、前記動作検査対象のソフトウェアにデッドロックが発生するか否かを検出する動作検査手段を備え、
前記動作検査手段は、前記動作検査対象のソフトウェアにデッドロックが発生することを検出した場合に、前記デッドロックが発生する原因を示す情報を外部環境生成手段に送信し、
前記外部環境生成手段は、前記動作検査手段から送信された情報にもとづいて、生成した状態遷移情報を変更する
請求項１から請求項４のうちいずれか１項記載の情報処理システム。
【請求項６】
動作検査手段は、デッドロックが発生する原因を示す情報として、前記デッドロックが発生するときの動作検査対象のソフトウェアの処理の状態と、メッセージを送信または受信しようとしている通信相手と、前記メッセージとを示す情報を外部環境生成手段に送信し、
前記外部環境生成手段は、前記動作検査手段から受信した前記情報にもとづいて、前記動作検査対象のソフトウェアによって送信されようとしているメッセージを当該メッセージを受信することとし、前記動作検査対象のソフトウェアによってメッセージが受信されようとしていることを当該メッセージを送信することとして、デッドロックが発生するときの動作検査対象のソフトウェアの処理の状態に応じて、前記通信相手の状態遷移情報を変更する
請求項５記載の情報処理システム。
【請求項７】
動作検査対象のソフトウェアの処理で送受信されるメッセージの情報を入力し、
前記情報にもとづいて、前記動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を生成し、
生成した状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力し、
生成した前記状態遷移情報にもとづいて、前記動作検査対象のソフトウェアの処理で送受信されるメッセージを送受信する通信相手の状態の遷移を示す状態遷移情報を生成し、
生成した前記状態遷移情報を前記動作検査手段に出力する
ことを特徴とする情報処理方法。
【請求項８】
動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を入力し、
入力された状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力し、
入力された状態遷移情報にもとづいて、前記動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、
生成した前記状態遷移情報を前記動作検査手段に出力する
ことを特徴とする情報処理方法。
【請求項９】
動作検査手段に状態遷移情報にもとづいてソフトウェアの動作を検査させるために、通信相手の状態遷移情報を外部環境保存手段に記憶させ、
利用者の要求に応じて、前記外部環境保存手段に記憶されている状態遷移情報を変更する
請求項７または請求項８記載の情報処理方法。
【請求項１０】
コンピュータに、
動作検査対象のソフトウェアの処理で送受信されるメッセージの情報を入力し、前記情報にもとづいて、前記動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を生成する検査対象入力処理と、
前記検査対象入力処理で生成された状態遷移情報にもとづいて、前記動作検査対象のソフトウェアの処理で送受信されるメッセージを送受信する通信相手の状態の遷移を示す状態遷移情報を生成し、生成した前記状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力する外部環境生成処理とを実行させ、
前記検査対象入力処理で、生成させた状態遷移情報を前記動作検査手段に出力する処理を実行させる
ための情報処理プログラム。
【請求項１１】
コンピュータに、
動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を入力する検査対象入力処理と、
前記検査対象入力処理で入力された状態遷移情報にもとづいて、前記動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、生成した前記状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力する外部環境生成処理とを実行させ、
前記検査対象入力処理で、入力された状態遷移情報を前記動作検査手段に出力する処理を実行させる
ための情報処理プログラム。
【請求項１２】
コンピュータに、
動作検査手段に状態遷移情報にもとづいてソフトウェアの動作を検査させるために、外部環境生成処理で生成された状態遷移情報を外部環境保存手段に記憶させる記憶処理と、
利用者の要求に応じて、前記外部環境保存手段に記憶されている状態遷移情報を変更する外部環境編集処理とを実行させる
請求項１１または請求項１２記載の情報処理プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェア検査のための情報処理システム、情報処理方法、および情報処理プログラムに関し、特にメッセージの送受信に着目したソフトウェア検査のための情報処理システム、情報処理方法、および情報処理プログラムに関する。
【背景技術】
【０００２】
ソフトウェアの動作を検査するシステムとして、モデル検査システムがある。モデル検査とは、検査対象となるソフトウェアの振る舞いを状態遷移としてモデル化し、スレッドやプロセスの動作タイミングなどの考えられる可能性をすべて調べて、どのような場合にもソフトウェアが期待通りに動作することを確認する手法である。動作タイミングによって発生する問題は通常のテストでは発見しづらいが、モデル検査を利用することで発見できるようになる。
【０００３】
モデル検査システムの一例として、非特許文献１にＳＰＩＮ（Ｓｉｍｐｌｅ  Ｐｒｏｍｅｌａ  Ｉｎｔｅｒｐｒｅｔｅｒ）というツールが記載されている。
【０００４】
モデル検査システムは、利用者から検査対象となるソフトウェアの記述および検査項目を受け取り、検査対象となるソフトウェアがどのような場合にも検査項目を満たすかどうかを調べる。検査対象となるソフトウェアは状態遷移図、検査用の専用プログラミング言語、もしくは汎用のプログラミング言語で記述される。検査対象となるソフトウェアがプログラミング言語で記述される場合も、モデル検査システムの内部において状態遷移に変換され、処理される。検査項目にはＬＴＬ（Ｌｉｎｅａｒ  Ｔｅｍｐｏｒａｌ  Ｌｏｇｉｃ）やＣＴＬ（Ｃｏｍｐｕｔａｔｉｏｎ  Ｔｒｅｅ  Ｌｏｇｉｃ）などの時相論理式が用いられる。
【０００５】
ここで、入力される検査対象のソフトウェアの記述においては、検査したい部分だけではなく、検査したい部分に関連するモジュールや人間の動作も記述されている必要がある。なぜならば、モデル検査システムは受け取ったソフトウェアの記述に従ってすべての実行可能な動作を調べるが、検査したい部分とそうでない部分との間でメッセージ送受信がある場合、検査したい部分だけではそのようなメッセージ送受信は実行不可能となってしまうためである。このような、検査したい部分に関連するモジュールや人間の動作を記述した情報を外部環境と呼ぶ。
【０００６】
特許文献１には、ソフトウェアの動作を検証するシミュレーション装置が記載されている。
【０００７】
特許文献２には、スタブまたはドライバを生成し、生成したスタブまたはドライバを用いて、ソフトウェアの動作を検証するシステムが記載されている。
【０００８】
特許文献３には、予め用意されたドライバを用いてソフトウェアの動作を検証した後、テスト項目を変更または追加した場合に、テスト項目に応じたドライバを生成し、生成したドライバを用いて、ソフトウェアの動作を検証するシステムが記載されている。
【０００９】
【特許文献１】特開平１０−３１２３１４号公報  （第３−４頁、図１）
【特許文献２】特開２００２−３６６３８７号公報  （第６−１７頁、図１）
【特許文献３】特開平１０−１１６２０９号公報    （第２−４頁、図１）
【非特許文献１】ホルツマン・ジー・ジェイ（Ｈｏｌｚｍａｎｎ  Ｇ．Ｊ．）著、「ザ  エスピーアイエヌ  モデルチェッカー：プライマアンドリファレンスマニュアル（Ｔｈｅ  ＳＰＩＮ  Ｍｏｄｅｌ  Ｃｈｅｃｋｅｒ：Ｐｒｉｍｅｒ  ａｎｄ  Ｒｅｆｅｒｅｎｃｅ  Ｍａｎｕａｌ）」、（米国）、アディソンウェスレィプロフェッショナル（Ａｄｄｉｓｏｎ  Ｗｅｓｌｅｙ  Ｐｒｏｆｅｓｓｉｏｎａｌ）、２００３年９月、ｐ．２４５−２４７
【発明の開示】
【発明が解決しようとする課題】
【００１０】
外部環境に相当するモジュールは実際には複雑な振る舞いを持ち、一部の振る舞いは検査結果にも影響を与える。その一方で、外部環境は直接検査したい部分ではないため、あまり詳細な動作は検査結果に影響を与えない。検査結果に影響を与えない場合には必要以上に詳細な記述はモデル検査の処理効率の低下を招くため望ましくない。そのため、利用者は検査したい部分との入出力、および検査項目に影響する振る舞いのみを抽出して外部環境として記述する必要がある。そこで、検査対象のソフトウェアをモジュール分割し、モジュールごとに単体でのモデル検査を行おうとすると、それぞれのモジュールに対応する外部環境を用意する必要があり、適用の準備に手間がかかる。
【００１１】
非特許文献１に記載されているツールを用いてソフトウェアの動作を検証するためには、検査対象のソフトウェアの外部環境を用意する必要があり、適用の準備に手間がかかる。
【００１２】
特許文献１に記載されているシミュレーション装置は、あらかじめ利用者が外部環境コンポーネントデータベースに必要な情報を登録する必要があるため、適用に関しての手間は削減されない。
【００１３】
特許文献２に記載されているシステムは、関数の引数の型などをもとにスタブまたはドライバの生成を行うため、スタブまたはドライバを生成させるために、スタブまたはドライバのインタフェース定義情報やデータ定義情報画面の基本仕様の情報を入力する必要があり、適用の準備に手間がかかる。
【００１４】
特許文献３に記載されているシステムは、テスト項目に対応したドライバファイルを予め用意する必要があり、適用の準備に手間がかかる。
【００１５】
また、メッセージの送受信の動作には通信相手が必要であること、および、外部環境の動作が検査結果に影響を与える場合があり、検査項目によっては外部環境に関する情報が別途必要なため、ソフトウェアの検査において、検査したい部分とそうでない部分との間でメッセージ送受信がある場合は外部環境の記述が必要であり、検査の準備に手間がかかる。
【００１６】
そこで、本発明は、ソフトウェアを検査するための外部環境の作成の手間を軽減できる情報処理システム、情報処理方法、および情報処理プログラムを提供することを目的とする。
【課題を解決するための手段】
【００１７】
本発明による情報処理システムは、動作検査対象のソフトウェアの処理で送受信されるメッセージの情報を入力し、情報にもとづいて、動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を生成する検査対象入力手段と、検査対象入力手段が生成した状態遷移情報にもとづいて、動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、生成した状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力する外部環境生成手段とを備え、検査対象入力手段が、生成した状態遷移情報を動作検査手段に出力することを特徴とする。
【００１８】
本発明による他の形態の情報処理システムは、動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を入力する検査対象入力手段と、検査対象入力手段に入力された状態遷移情報にもとづいて、動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、生成した状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力する外部環境生成手段とを備え、検査対象入力手段が、入力された状態遷移情報を動作検査手段に出力することを特徴とする。
【００１９】
本発明による情報処理方法は、動作検査対象のソフトウェアの処理で送受信されるメッセージの情報を入力し、情報にもとづいて、動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を生成し、生成した状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力し、生成した状態遷移情報にもとづいて、動作検査対象のソフトウェアの処理で送受信されるメッセージを送受信する通信相手の状態の遷移を示す状態遷移情報を生成し、生成した状態遷移情報を動作検査手段に出力することを特徴とする。
【００２０】
本発明による他の形態の情報処理方法は、動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を入力し、入力された状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力し、入力された状態遷移情報にもとづいて、動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、生成した状態遷移情報を動作検査手段に出力することを特徴とする。
【００２１】
本発明による情報処理プログラムは、コンピュータに、動作検査対象のソフトウェアの処理で送受信されるメッセージの情報を入力し、情報にもとづいて、動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を生成する検査対象入力処理と、検査対象入力処理で生成された状態遷移情報にもとづいて、動作検査対象のソフトウェアの処理で送受信されるメッセージを送受信する通信相手の状態の遷移を示す状態遷移情報を生成し、生成した状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力する外部環境生成処理とを実行させ、検査対象入力処理で、生成させた状態遷移情報を動作検査手段に出力する処理を実行させることを特徴とする。
【００２２】
本発明による他の形態の情報処理プログラムは、コンピュータに、動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を入力する検査対象入力処理と、検査対象入力処理で入力された状態遷移情報にもとづいて、動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、生成した状態遷移情報をソフトウェアの動作を検査する動作検査手段に出力する外部環境生成処理とを実行させ、検査対象入力処理で、入力された状態遷移情報を動作検査手段に出力する処理を実行させることを特徴とする。
【発明の効果】
【００２３】
本発明によれば、ソフトウェア検査のための外部環境の記述の作業を軽減し、効率よく検査の準備ができる。その理由は、メッセージ送受信の通信相手としての外部環境を自動的に生成するためである。
【発明を実施するための最良の形態】
【００２４】
実施形態１．
本発明の第１の実施形態について、図面を参照して説明する。図１は、本発明の第１の実施形態の情報処理システムの構成例を示すブロック図である。
【００２５】
図１に示すように、本発明の第１の実施形態の情報処理システムは、検査対象入力手段３００と、外部環境生成手段３１０とを含み、検査対象入力手段３００および外部環境生成手段３１０はモデル検査手段３４０に接続されている。
【００２６】
検査対象入力手段３００は、利用者によって入力された検査対象のソフトウェアに関する記述（検査対象情報）を受け取る。なお、検査対象のソフトウェアは複数のモジュールによって構成されていてもよい。検査対象入力手段３００は、入力された情報（検査対象情報）がモデル検査手段３４０で検査可能な記述形式でない場合にはモデル検査手段３４０で検査可能な記述形式に変換する。
【００２７】
また、検査対象入力手段３００は、メッセージ（ソフトウェア（モジュールであってもよい）の制御に従ってハードウェアによって送受信されるデータ）の送信先および受信元（受信したメッセージの送信元）である通信相手（本実施形態ではモジュール）に関する情報を明確化して得られる状態遷移の情報（状態遷移情報）を、外部環境生成手段３１０に渡す。状態遷移情報は、例えば、メッセージを送信先に送信することによるソフトウェアの処理の状態の遷移と、メッセージを送信元から受信したことによるソフトウェアの処理の状態の遷移とを示す情報である。
【００２８】
なお、ソフトウェア（モジュールであってもよい）の制御に従ってハードウェアがメッセージを送受信することを、単に、ソフトウェアがメッセージを送受信するともいう。
【００２９】
外部環境生成手段３１０は、検査対象入力手段３００から検査対象のソフトウェアの状態遷移情報を受け取り、検査対象のソフトウェアの状態遷移を網羅するように外部環境の状態遷移情報を生成してモデル検査手段３４０に渡す。
【００３０】
モデル検査手段３４０は、検査対象入力手段３００から検査対象のソフトウェアに関する記述（検査対象情報。状態遷移情報であってもよい）を受け取り、外部環境生成手段３１０で生成された外部環境の状態遷移情報とあわせてモデル検査を実行する。
【００３１】
なお、検査対象入力手段３００および外部環境生成手段３１０は、例えば、動作検査対象のソフトウェアの処理で送受信されるメッセージの情報を入力し、前記情報にもとづいて、前記動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を生成する検査対象入力処理と、検査対象入力処理で生成された状態遷移情報にもとづいて、前記動作検査対象のソフトウェアの処理で送受信されるメッセージを送受信する通信相手の状態の遷移を示す状態遷移情報を生成し、生成した前記状態遷移情報をソフトウェアの動作を検査するモデル検査手段３４０に出力する外部環境生成処理とを実行させ、検査対象入力処理で、生成させた状態遷移情報をモデル検査手段３４０に出力する処理を実行させるための情報処理プログラムを搭載したコンピュータによって実現されてもよい。
【００３２】
また、検査対象入力手段３００および外部環境生成手段３１０は、例えば、動作検査対象のソフトウェアの処理の状態の遷移を示す状態遷移情報を入力する検査対象入力処理と、前記検査対象入力処理で入力された状態遷移情報にもとづいて、前記動作検査対象のソフトウェアの処理で送受信されるメッセージの通信相手の状態の遷移を示す状態遷移情報を生成し、生成した前記状態遷移情報をソフトウェアの動作を検査するモデル検査手段３４０に出力する外部環境生成処理とを実行させ、前記検査対象入力処理で、入力された状態遷移情報をモデル検査手段３４０に出力する処理を実行させるための情報処理プログラムを搭載したコンピュータによって実現されてもよい。
【００３３】
次に、本発明の第１の実施形態の動作について、図面を参照して説明する。図２は、本発明の第１実施形態の情報処理システムの動作を示すフローチャートである。
【００３４】
検査対象入力手段３００は、利用者から検査対象のソフトウェア（本実施形態では複数）に関する記述（検査対象情報）を受け取り、モデル検査手段３４０で検査可能な記述形式に変換する。また、検査対象入力手段３００は、検査対象のソフトウェアが送受信するメッセージの送信先および受信元に関する情報を明確化して得られた状態遷移情報を、外部環境生成手段３１０に渡す。モデル検査手段３４０は、検査対象入力手段３００から状態遷移情報を受け取る（ステップＳ３１）。
【００３５】
次に、外部環境生成手段３１０は、状態遷移情報から入力モデル（検査対象ソフトウェア）のメッセージの送信先のモジュールおよび受信元のモジュールを示す情報を抽出する（ステップＳ３２）。さらに、外部環境生成手段３１０は、メッセージの送信先のモジュールおよび受信元のモジュールの中で、検査対象として状態遷移情報に記述されていないモジュールを外部環境として状態遷移情報を生成するべきモジュールとして抽出する（ステップＳ３３）。次に、外部環境生成手段３１０は、外部環境として状態遷移情報を生成するべきモジュールのそれぞれについて、下記ステップＳ３４からステップＳ３７の作業を行い、外部環境の状態遷移情報を生成する。
【００３６】
まず、外部環境生成手段３１０は、検査対象の各モジュールの状態遷移情報から、状態遷移情報を生成しようとしているモジュールとのメッセージ送受信を抽出し、それ以外のメッセージ送受信の情報を消去する（ステップＳ３４）。外部環境生成手段３１０は、消去の結果内容のなくなった遷移および状態を状態遷移情報から消去する（ステップＳ３５）。
【００３７】
外部環境生成手段３１０は、検査対象のソフトウェアが外部環境のモジュールにメッセージを送信したことを、当該外部環境のモジュールが当該検査対象のソフトウェアからメッセージを受信したこととして当該外部環境のモジュールの状態遷移情報を生成し、検査対象のソフトウェアが外部環境のモジュールからメッセージを受信したことを、当該外部環境のモジュールが当該検査対象のソフトウェアにメッセージを送信したこととして当該外部環境のモジュールの状態遷移情報を生成するため、送信と受信とを反転させる（ステップＳ３６）。
【００３８】
最後に、外部環境生成手段３１０は、検査対象の各モジュールの検査対象情報から作成したすべてのモジュールの状態遷移情報を組み合わせて、単一の状態遷移とした状態遷移情報をモデル検査手段３４０に渡す（ステップＳ３７）。必要なすべての外部環境の状態遷移情報された場合に（ステップＳ３０のＹ）、モデル検査手段３４０は、検査対象入力手段３００から検査対象のソフトウェアの状態遷移情報を受け取り、外部環境生成手段３１０で生成された外部環境のモジュールの状態遷移情報とあわせてモデル検査を実行する（ステップＳ３８）。
【００３９】
なお、本実施形態では検査手段としてモデル検査の場合を例示したが、メッセージの送受信に着目した検査であれば他の検査手法にも適用可能である。
【００４０】
次に、本実施形態の効果について説明する。本実施形態では、検査対象のソフトウェアに関する記述のみから外部環境（具体的には、外部環境のモジュールの状態遷移情報）を生成できるように構成されているため、外部環境の記述の作業を軽減し、効率よく検査の準備ができる。
【００４１】
実施形態２．
次に、上述した第１の実施形態のより具体的な実施形態として、本発明の第２の実施形態について説明する。本発明の第２の実施形態の情報処理システムの構成は、図１に示す本発明の第１の実施形態の情報処理システムの構成と同様なため、説明を省略する。
【００４２】
本発明の第２の実施形態の情報処理システムの動作について、上述した第１の実施形態の場合と同様に、図２に示すフローチャートを参照して説明する。
【００４３】
まず、検査対象入力手段３００は、利用者から検査対象のソフトウェア（本実施形態ではモジュールＡ５００およびモジュールＢ６００）に関する記述を受け取る（ステップＳ３１）。ここでは、図３の状態遷移図で記述されたモデルによって示される状態遷移情報を受け取るものとする。図３は、利用者から検査対象入力手段３００に入力された状態遷移情報を示す状態遷移図である。図３に模式的に示す状態遷移情報は、そのままモデル検査手段３４０で検査可能であり、メッセージの送信先・受信元に関する情報も明確であるとする。
【００４４】
図３（ａ）に示すように、モジュールＡ５００は、状態（１）でモジュールＣ７００にメッセージＸを送信して状態（２）に状態遷移する。そして、状態（２）でモジュールＢ６００にメッセージＺを送信して状態（３）に状態遷移する。そして、状態（３）でモジュールＢ６００からメッセージＺを受信して状態（４）に状態遷移する。状態（４）でモジュールＣ７００からメッセージＹを受信して状態（１）に状態遷移する。
【００４５】
また、図３（ｂ）に示すように、モジュールＢ６００は、状態（５）でモジュールＡ５００からメッセージＺを受信して状態（６）に状態遷移する。そして、状態（６）でモジュールＣ７００からメッセージＹを受信して状態（７）に状態遷移する。そして、状態（７）でモジュールＣ７００にメッセージＸを送信して状態（８）に状態遷移する。状態（８）でモジュールＡ５００にメッセージＺを送信して状態（５）に状態遷移する。
【００４６】
本実施形態の検査対象はモジュールＡ５００，Ｂ６００であり、利用者から検査対象入力手段３００に入力された状態遷移情報には、モジュールＡ５００，Ｂ６００，Ｃ７００の間のメッセージの送受信が記述されている。
【００４７】
図４は、モジュールＡ５００，Ｂ６００，Ｃ７００間のメッセージ送受信の関係を示す説明図である。図４に示すように、モジュールＡ５００，Ｂ６００は、それぞれ検査対象外のモジュールＣ７００とメッセージを送受信している。具体的には、図４に示すように、モジュールＡ５００は、モジュールＢ６００にメッセージＺを送信し、モジュールＣ７００にメッセージＸを送信する。モジュールＢ６００は、モジュールＡ５００にメッセージＺを送信し、モジュールＣ７００にメッセージＸを送信する。モジュールＣ７００は、モジュールＡ５００にメッセージＹを送信し、モジュールＢ６００にメッセージＹを送信する。
【００４８】
外部環境生成手段３１０は、状態遷移情報から入力モデル（本実施形態では検査対象ソフトウェアであるモジュールＡ５００，Ｂ６００）のメッセージの送信先のモジュールおよび受信元のモジュールを示す情報を抽出する（ステップＳ３２）。さらに、外部環境生成手段３１０は、メッセージの送信先のモジュールおよび受信元のモジュールの中で、検査対象として状態遷移情報に記述されていないモジュールを、外部環境として状態遷移情報を生成するべきモジュールとして抽出する（ステップＳ３３）。
【００４９】
本実施形態では、図４に示すように、メッセージの送信先および受信元としてモジュールＡ５００，Ｂ６００，Ｃ７００があるが、そのうち検査対象として状態遷移情報に記述されているものはモジュールＡ５００，Ｂ６００のみである。そのため、外部環境として状態遷移情報を生成するべきモジュールはモジュールＣ７００である。
【００５０】
次に、外部環境生成手段３１０は、外部環境として状態遷移情報を生成するべきモジュールについて、以下に示す作業を行い、外部環境の状態遷移情報を生成する。まず、外部環境生成手段３１０は、検査対象の各モジュールの状態遷移情報から、状態遷移情報を生成しようとしているモジュールとのメッセージ送受信を抽出し、それ以外のメッセージ送受信の情報を消去する（ステップＳ３４）。図５は、状態遷移情報を生成しようとしているモジュール以外とのメッセージ送受信の情報が消去された状態遷移情報を示す状態遷移図である。
【００５１】
図５（ａ）には、モジュールＡ５００が、状態（１）でモジュールＣ７００にメッセージＸを送信して状態（２）に状態遷移すること、状態（２）から状態（３）に状態遷移すること、状態（３）から状態（４）に状態遷移すること、および状態（４）でモジュールＣ７００からメッセージＹを受信して状態（１）に状態遷移することが示され、図３（ａ）に示す状態遷移図から、モジュールＢ６００とのメッセージ送受信の情報が消去されている。
【００５２】
また、図５（ｂ）には、モジュールＢ６００が、状態（５）から状態（６）に状態遷移すること、状態（６）でモジュールＣ７００からメッセージＹを受信して状態（７）に状態遷移すること、状態（７）でモジュールＣ７００にメッセージＸを送信して状態（８）に状態遷移すること、および状態（８）から状態（５）に状態遷移することが示され、図３（ｂ）に示す状態遷移図から、モジュールＡ５００とのメッセージ送受信の情報が消去されている。
【００５３】
外部環境生成手段３１０は、ステップＳ３４の処理で、状態遷移情報を生成しようとしているモジュール以外とのメッセージ送受信の情報を消去した結果、内容のなくなった遷移および状態を状態遷移情報から消去する（ステップＳ３５）。図６は、状態遷移情報を生成しようとしているモジュール以外とのメッセージ送受信の情報が消去された結果、内容のなくなった遷移および状態を状態遷移情報を示す状態遷移図である。
【００５４】
図６（ａ）には、モジュールＡ５００が、状態（１）でモジュールＣ７００にメッセージＸを送信して状態（４）に状態遷移すること、および状態（４）でモジュールＣ７００からメッセージＹを受信して状態（１）に状態遷移することが示され、モジュールＢ６００とのメッセージ送受信の情報が消去された結果、図５（ａ）に示す状態遷移図から、内容のなくなった遷移および状態が消去されている。
【００５５】
図６（ｂ）には、モジュールＢ６００が、状態（６）でモジュールＣ７００からメッセージＹを受信して状態（７）に状態遷移すること、および状態（７）でモジュールＣ７００にメッセージＸを送信して状態（６）に状態遷移することが示され、モジュールＡ５００とのメッセージ送受信の情報が消去された結果、図５（ｂ）に示す状態遷移図から、内容のなくなった遷移および状態が消去されている。
【００５６】
外部環境生成手段３１０は、検査対象のソフトウェアであるモジュールＡ５００，Ｂ６００が外部環境のモジュールであるモジュールＣ７００にメッセージを送信したことを、モジュールＣ７００がモジュールＡ５００，Ｂ６００からメッセージを受信したこととしてモジュールＣ７００の状態遷移情報を生成し、モジュールＡ５００，Ｂ６００がモジュールＣ７００からメッセージを受信したことを、モジュールＣ７００がモジュールＡ５００，Ｂ６００にメッセージを送信したこととしてモジュールＣ７００の状態遷移情報を生成するため、メッセージの送信と受信との処理を反転させる（ステップＳ３６）。図７は、図６に示す状態遷移図におけるメッセージの送信と受信との処理を反転した状態遷移情報を示す状態遷移図である。なお、図７に示す状態遷移図は、モジュールＣ７００の状態遷移情報を示す状態遷移図でもある。
【００５７】
図７（ａ）には、モジュールＣ７００が、状態（１）でモジュールＡ５００からメッセージＸを受信して状態（４）に状態遷移すること、および状態（４）でモジュールＡ５００にメッセージＹを送信して状態（１）に状態遷移することが示されている。また、図７（ｂ）には、モジュールＣ７００が、状態（６）でモジュールＢ６００へメッセージＹを送信して状態（７）に状態遷移すること、および状態（７）でモジュールＢ６００からメッセージＸを受信して状態（６）に状態遷移することが示されている。
【００５８】
最後に、外部環境生成手段３１０は、すべてのモジュールの状態遷移情報を組み合わせて、単一の状態遷移とした状態遷移情報をモデル検査手段３４０に渡す（ステップＳ３７）。図８は、単一の状態遷移とした状態遷移情報を示す状態遷移図である。
【００５９】
本実施形態の検査対象であるモジュールＡ５００，Ｂ６００と、本実施形態の検査対象外のモジュールＣ７００とを組み合わせて単一の状態遷移とした状態遷移情報は、図８に示すように、状態（１−６）でモジュールＣ７００がモジュールＢ６００にメッセージＹを送信して状態（１−７）に状態遷移すること、状態（１−７）でモジュールＣ７００がモジュールＡ５００からメッセージＸを受信して状態（４−７）に状態遷移すること、状態（４−７）でモジュールＣ７００がモジュールＢ６００からメッセージＸを受信して状態（４−６）に状態遷移すること、および状態（４−６）でモジュールＣ７００がモジュールＡ５００にメッセージＹを送信して状態（１−６）に状態遷移することを示す情報である。
【００６０】
また、本実施形態の検査対象であるモジュールＡ５００，Ｂ６００と、本実施形態の検査対象外のモジュールＣ７００とを組み合わせて単一の状態遷移とした状態遷移情報は、図８に示すように、状態（１−６）でモジュールＣ７００がモジュールＡ５００からメッセージＸを受信して状態（４−６）に状態遷移すること、状態（４−６）でモジュールＣ７００がモジュールＢ６００にメッセージＹを送信して状態（４−７）に状態遷移すること、状態（４−７）でモジュールＣ７００がモジュールＡ５００にメッセージＹを送信して状態（１−７）に状態遷移すること、および状態（１−７）でモジュールＣ７００がモジュールＢ６００からメッセージＸを受信して状態（１−６）に状態遷移することを示す情報である。
【００６１】
必要なすべての外部環境の状態遷移情報された場合に（ステップＳ３０のＹ）、モデル検査手段３４０は、検査対象入力手段３００から検査対象のソフトウェアの状態遷移情報を受け取り、外部環境生成手段３１０で生成されたモジュールＡ５００，Ｂ６００、およびモジュールＣ７００を組み合わせて単一の状態遷移とした状態遷移情報とあわせてモデル検査を実行する（ステップＳ３８）。
【００６２】
本実施形態の効果について説明する。本実施形態では、検査対象のソフトウェアに関する記述のみから外部環境（具体的には、外部環境のモジュールＣ７００の状態遷移情報）を生成できるように構成されているため、外部環境の記述の作業を軽減し、効率よく検査の準備ができる。
【００６３】
実施形態３．
本発明の第３の実施形態について、図面を参照して説明する。図９は、本発明の第３の実施形態の情報処理システムの構成例を示すブロック図である。
【００６４】
図９に示すように、本発明の第３の実施形態は、検査対象入力手段１００と、外部環境生成手段１１０と、外部環境保存手段１２０と、外部環境編集手段１３０とを含み、検査対象入力手段１００および外部環境保存手段１２０は、モデル検査手段１４０に接続されている。
【００６５】
検査対象入力手段１００は、利用者によって入力された検査対象のソフトウェアに関する記述（検査対象情報）を受け取る。なお、検査対象のソフトウェアは複数のモジュールによって構成されていてもよい。検査対象入力手段１００は、入力された情報（検査対象情報）がモデル検査手段１４０で検査可能な記述形式でない場合にはモデル検査手段１４０で検査可能な記述形式に変換する。
【００６６】
また、検査対象入力手段１００は、メッセージ（ソフトウェア（モジュールであってもよい）で送受信されるデータ）の送信先および受信元（受信したメッセージの送信元）である通信相手（本実施形態ではモジュール）に関する情報を明確化して得られる状態遷移の情報（状態遷移情報）を、外部環境生成手段１１０に渡す。
【００６７】
外部環境生成手段１１０は、検査対象入力手段１００から検査対象のソフトウェアの状態遷移情報を受け取り、検査対象のソフトウェアの状態遷移を網羅するように外部環境の状態遷移情報を生成して、生成した状態遷移情報を外部環境保存手段１２０に保存する。
【００６８】
外部環境編集手段１３０は、必要に応じて利用者から入力された情報を受け取り、受け取った情報にもとづいて、外部環境保存手段１２０に保存された状態遷移情報を更新する。
【００６９】
モデル検査手段１４０は、検査対象入力手段１００から検査対象のソフトウェアに関する記述（検査対象情報。状態遷移情報であってもよい）を受け取り、外部環境保存手段１２０に保存された状態遷移情報とあわせてモデル検査を実行する。
【００７０】
次に、本発明の第３の実施形態の動作について、図面を参照して説明する。図１０は、本発明の第３の実施形態の情報処理システムの動作を示すフローチャートである。
【００７１】
検査対象入力手段１００は、利用者から検査対象のソフトウェア（本実施形態では複数）に関する記述（検査対象情報）を受け取り、モデル検査手段１４０で検査可能な記述形式に変換する。また、検査対象入力手段１００は、検査対象のソフトウェアが送受信するメッセージの送信先および受信元に関する情報を明確化して得られた状態遷移情報を、外部環境生成手段１１０に渡す。モデル検査手段１４０は、検査対象入力手段１００から状態遷移情報を受け取る（ステップＳ１１）。
【００７２】
次に、外部環境生成手段１１０は、状態遷移情報から入力モデル（検査対象ソフトウェア）のメッセージの送信先のモジュールおよび受信元のモジュールを示す情報を抽出する（ステップＳ１２）。さらに、外部環境生成手段１１０は、メッセージの送信先のモジュールおよび受信元のモジュールの中で、検査対象として状態遷移情報に記述されていないモジュールを外部環境として状態遷移情報を生成するべきモジュールとして抽出する（ステップＳ１３）。次に、外部環境生成手段１１０は、外部環境として状態遷移情報を生成するべきモジュールのそれぞれについて、下記ステップＳ１４からステップＳ１７の作業を行い、外部環境の状態遷移情報を生成する。
【００７３】
まず、外部環境生成手段１１０は、検査対象の各モジュールの状態遷移情報から、状態遷移情報を生成しようとしているモジュールとのメッセージ送受信を抽出し、それ以外のメッセージ送受信の情報を消去する（ステップＳ１４）。外部環境生成手段１１０は、消去の結果内容のなくなった遷移および状態を状態遷移情報から消去する（ステップＳ１５）。
【００７４】
外部環境生成手段１１０は、検査対象のソフトウェアが外部環境のモジュールにメッセージを送信したことを、当該外部環境のモジュールが当該検査対象のソフトウェアからメッセージを受信したこととして当該外部環境のモジュールの状態遷移情報を生成し、検査対象のソフトウェアが外部環境のモジュールからメッセージを受信したことを、当該外部環境のモジュールが当該検査対象のソフトウェアにメッセージを送信したこととして当該外部環境のモジュールの状態遷移情報を生成するため、送信と受信とを反転させる（ステップＳ１６）。
【００７５】
最後に、外部環境生成手段１１０は、検査対象の各モジュールの検査対象情報から作成したすべてのモジュールの状態遷移情報を組み合わせて、単一の状態遷移とした状態遷移情報を外部環境保存手段１２０に保存する（ステップＳ１７）。必要なすべての外部環境の状態遷移情報された場合に（ステップＳ１０のＹ）、利用者は必要に応じて外部環境編集手段１３０を利用して、外部環境保存手段１２０に保存された状態遷移情報を確認し、修正する（ステップＳ１８）。
【００７６】
モデル検査手段１４０は、検査対象入力手段１００から検査対象のソフトウェアの状態遷移情報を受け取り、外部環境保存手段１２０に保存された外部環境のモジュールの状態遷移情報とあわせてモデル検査を実行する（ステップＳ１９）。
【００７７】
なお、本実施形態では検査手段としてモデル検査の場合を例示したが、メッセージの送受信に着目した検査であれば他の検査手法にも適用可能である。
【００７８】
次に、本実施形態の効果について説明する。本実施形態では、検査対象のソフトウェアに関する記述のみから外部環境（具体的には、外部環境のモジュールの状態遷移情報）を生成できるように構成されているため、外部環境の記述の作業を軽減し、効率よく検査の準備ができる。また、検査結果に影響を与える振る舞いが存在する場合、利用者は自動生成された外部環境のモジュールの状態遷移情報を元に、外部環境編集手段１３０を用いて、必要な部分のみ修正を加えればよいため、検査結果に影響を与える振る舞いの記述が効率化できる。また、利用者は、自動的に生成された外部環境のモジュールの状態遷移情報が期待と異なる場合に、外部環境編集手段１３０を用いて、当該状態遷移情報を修正することができる。
【００７９】
実施形態４．
次に、上述した第３の実施形態のより具体的な実施形態として、本発明の第４の実施形態について説明する。本発明の第４の実施形態の情報処理システムの構成は、図９に示す本発明の第３の実施形態の情報処理システムの構成と同様なため、説明を省略する。
【００８０】
本発明の第４の実施形態の情報処理システムの動作について、上述した第３の実施形態の場合と同様に、図１０に示すフローチャートを参照して説明する。
【００８１】
まず、検査対象入力手段１００は、利用者から検査対象のソフトウェア（本実施形態ではモジュールＡ５００およびモジュールＢ６００）に関する記述を受け取る（ステップＳ１１）。ここでは、図３の状態遷移図で記述されたモデルを示す状態遷移情報を受け取るものとする。図３に模式的に示す状態遷移情報は、そのままモデル検査手段１４０で検査可能であり、メッセージの送信先および受信元に関する情報も明確であるとする。
【００８２】
本実施形態の検査対象はモジュールＡ５００，Ｂ６００であり、利用者から検査対象入力手段１００に入力された状態遷移情報には、モジュールＡ５００，Ｂ６００，Ｃ７００の間のメッセージの送受信が記述されている。ここで、本実施形態では、図４に示すようにモジュールＡ５００，Ｂ６００，Ｃ７００の間でメッセージが送受信されるとする。
【００８３】
外部環境生成手段１１０は、状態遷移情報から入力モデル（本実施形態では検査対象ソフトウェアであるモジュールＡ５００，Ｂ６００）のメッセージの送信先のモジュールおよび受信元のモジュールを示す情報を抽出する（ステップＳ１２）。さらに、外部環境生成手段１１０は、メッセージの送信先のモジュールおよび受信元のモジュールの中で、検査対象として状態遷移情報に記述されていないモジュールを外部環境として状態遷移情報を生成するべきモジュールとして抽出する（ステップＳ１３）。
【００８４】
本実施形態では、図４に示すように、メッセージの送信先および受信元としてモジュールＡ５００，Ｂ６００，Ｃ７００があるが、そのうち検査対象として状態遷移情報に記述されているものはモジュールＡ５００，Ｂ６００のみである。そのため、外部環境として状態遷移情報を生成するべきモジュールはモジュールＣ７００である。
【００８５】
次に、外部環境生成手段１１０は、外部環境として状態遷移情報を生成するべきモジュールについて、以下に示す作業を行い、外部環境の状態遷移情報を生成する。まず、外部環境生成手段１１０は、検査対象の各モジュールの状態遷移情報から、状態遷移情報を生成しようとしているモジュールとのメッセージ送受信を抽出し、それ以外のメッセージ送受信の情報を消去する（ステップＳ１４）。本実施形態では、状態遷移情報を生成しようとしているモジュール以外とのメッセージ送受信の情報が消去された状態遷移情報は、図５の状態遷移図に示される状態遷移情報と同様であるとする。
【００８６】
外部環境生成手段１１０は、ステップＳ１４の処理で、状態遷移情報を生成しようとしているモジュール以外とのメッセージ送受信の情報を消去した結果、内容のなくなった遷移および状態を状態遷移情報から消去する（ステップＳ１５）。本実施形態では、状態遷移情報を生成しようとしているモジュール以外とのメッセージ送受信の情報が消去された結果、内容のなくなった遷移および状態を状態遷移情報は、図６の状態遷移図に示される状態遷移情報と同様であるとする。
【００８７】
外部環境生成手段１１０は、検査対象のソフトウェアであるモジュールＡ５００，Ｂ６００が外部環境のモジュールであるモジュールＣ７００にメッセージを送信したことを、モジュールＣ７００がモジュールＡ５００，Ｂ６００からメッセージを受信したこととしてモジュモジュールＣ７００ールＣの状態遷移情報を生成し、モジュールＡ５００，Ｂ６００がモジュールＣ７００からメッセージを受信したことを、モジュールＣ７００がモジュールＡ５００，Ｂ６００にメッセージを送信したこととしてモジュールＣ７００の状態遷移情報を生成するため、送信と受信とを反転させる（ステップＳ１６）。本実施形態では、図６に示す状態遷移図におけるメッセージの送信と受信とを反転した状態遷移情報は、図７の状態遷移図に示される状態遷移情報と同様であるとする。なお、図７に示す状態遷移図は、モジュールＣ７００の状態遷移情報を示す状態遷移図でもある。
【００８８】
最後に、外部環境生成手段３１０は、すべてのモジュールの状態遷移情報を組み合わせて、単一の状態遷移とした状態遷移情報を外部環境保存手段１２０に保存する（ステップＳ１７）。必要なすべての外部環境の状態遷移情報された場合に（ステップＳ１０のＹ）、利用者は必要に応じて外部環境編集手段１３０を利用して、外部環境保存手段１２０に保存された状態遷移情報を確認し、修正する（ステップＳ１８）。
【００８９】
モデル検査手段１４０は、検査対象入力手段１００から検査対象のソフトウェアの状態遷移情報を受け取り、外部環境保存手段１２０に保存された外部環境のモジュールの状態遷移情報とあわせてモデル検査を実行する（ステップＳ１９）。本実施形態では、単一の状態遷移とした状態遷移情報は、図８の状態遷移図に示される状態遷移情報と同様であるとする。
【００９０】
次に、本実施形態の効果について説明する。本実施形態では、検査対象のソフトウェアに関する記述のみから外部環境（具体的には、外部環境のモジュールの状態遷移情報）を生成できるように構成されているため、外部環境の記述の作業を軽減し、効率よく検査の準備ができる。また、検査結果に影響を与える振る舞いが存在する場合、利用者は自動生成された外部環境のモジュールの状態遷移情報を元に、外部環境編集手段１３０を用いて、必要な部分のみ修正を加えればよいため、検査結果に影響を与える振る舞いの記述が効率化できる。また、利用者は、自動的に生成された外部環境のモジュールの状態遷移情報が期待と異なる場合に、外部環境編集手段１３０を用いて、当該状態遷移情報を修正することができる。
【００９１】
実施形態５．
本発明の第５の実施形態について、図面を参照して説明する。図１１は、本発明の第５実施形態の情報処理システムの構成例を示すブロック図である。
【００９２】
図１１に示すように、本発明の第５の実施形態は、検査対象入力手段２００と、外部環境生成手段２１０と、外部環境保存手段２２０と、外部環境編集手段２３０とを含み、検査対象入力手段２００、外部環境生成手段２１０、および外部環境保存手段２３０は、モデル検査手段２４０に接続されている。
【００９３】
検査対象入力手段２００は、利用者によって入力された検査対象のソフトウェアに関する記述（検査対象情報）を受け取る。なお、検査対象のソフトウェアは複数であってもよい。検査対象入力手段２００は、入力された情報（検査対象情報）がモデル検査手段２４０で検査可能な記述形式でない場合にはモデル検査手段２４０で検査可能な記述形式に変換する。また、検査対象入力手段２００は、メッセージ（ソフトウェア（モジュールであってもよい）で送受信されるデータ）の送信先および受信元（受信したメッセージの送信元）のモジュールに関する情報を明確化して得られる状態遷移の情報（状態遷移情報）を、外部環境生成手段２１０に渡す。
【００９４】
外部環境生成手段２１０は、検査対象入力手段２００から検査対象のソフトウェアの状態遷移情報を受け取り、検査対象のソフトウェアの状態遷移を網羅するように外部環境の状態遷移情報を生成して、生成した状態遷移情報を外部環境保存手段２２０に保存する。また、外部環境生成手段２１０は、モデル検査に失敗した場合（具体的には、デッドロックが発生する可能性があることを検出した場合）に、失敗箇所の情報（デッドロックが発生した状態等を示す情報）をモデル検査手段２４０から受け取り、外部環境保存手段２２０に保存された状態遷移情報を修正する。
【００９５】
外部環境編集手段２３０は、必要に応じて利用者から入力された情報を受け取り、受け取った情報にもとづいて、外部環境保存手段２２０に保存された状態遷移情報を更新する。
【００９６】
モデル検査手段２４０は、検査対象入力手段２００から検査対象のソフトウェアに関する記述（検査対象情報。状態遷移情報であってもよい）を受け取り、外部環境保存手段２２０に保存された状態遷移情報とあわせてモデル検査を実行する。ここで外部環境のモジュールとのメッセージ送受信ができずにデッドロックが発生する可能性が検出された場合、失敗箇所の情報を外部環境生成手段２１０に渡す。なお、デッドロックとは、２つ以上の処理が互いの処理終了を待ち、結果としてプログラムが停止してしまうことをいう。
【００９７】
次に、本発明の第５の実施形態の動作について、図面を参照して説明する。図１２は、本発明の第５の実施形態の情報処理システムの動作を示すフローチャートである。
【００９８】
検査対象入力手段２００は、利用者から検査対象のソフトウェア（本実施形態では複数）に関する記述（検査対象情報）を受け取り、モデル検査手段２４０で検査可能な記述形式に変換する。また、検査対象入力手段２００は、検査対象のソフトウェアが送受信するメッセージの送信先および受信元に関する情報を明確化して得られた状態遷移情報を、外部環境生成手段２１０に渡す。モデル検査手段２４０は、検査対象入力手段２００から状態遷移情報を受け取る（ステップＳ２１）。
【００９９】
次に、モデル検査手段２４０は、検査対象入力手段２００から検査対象のソフトウェアの状態遷移情報を受け取り、デッドロックが発生する可能性があるか否かを検査する（ステップＳ２２）。検査の結果、検査対象のソフトウェアが、外部環境のモジュールとのメッセージ送受信ができずにデッドロックが発生すする可能性があることが検出された場合（ステップＳ２０のＹ）、モデル検査手段２４０は、発生したデッドロックを解消するために必要なメッセージと、そのメッセージの送信元および受信先と、各モジュールの状態とを示す情報を外部環境生成手段２１０に送る（ステップＳ２３）。
【０１００】
外部環境生成手段２１０は、モデル検査手段２４０から受信した情報にもとづいて、外部環境の状態と遷移とに応じた状態遷移情報を生成し（ステップＳ２４）、発生したデッドロックを解消するために必要とされるメッセージ送受信が可能になるようにし、外部環境保存手段２２０に外部環境の状態遷移情報を保存する。検査対象のソフトウェアが、外部環境とのメッセージ送受信ができずにモデル検査手段２４０によってデッドロックが発生する可能性が検出されている間は、モデル検査手段２４０および外部環境生成手段２１０は、ステップＳ２２からステップＳ２４までの処理を繰り返し、外部環境を順次拡張する。具体的には、外部環境生成手段２１０は、ステップＳ２４の処理で、外部環境保存手段２２０に保存されている状態遷移情報に、モデル検査手段２４０から受信した情報にもとづいて、外部環境の状態と遷移とを追加する。
【０１０１】
デッドロック検査に成功した場合（デッドロックが発生する可能性がないと判断した場合）や、デッドロックの原因が外部環境のモジュールとのメッセージ送受信以外であった場合、モデル検査手段２４０および外部環境生成手段２１０は、外部環境を拡張する処理を終了する。
【０１０２】
利用者は必要に応じて外部環境編集手段２３０を利用して、外部環境保存手段２２０に保存された外部環境の状態遷移情報を確認し、修正する（ステップＳ２５）。モデル検査手段２４０は、検査対象入力手段２００から検査対象のソフトウェアの状態遷移情報を受け取り、外部環境保存手段２２０に保存された外部環境のモジュールの状態遷移情報とあわせてモデル検査を実行する（ステップＳ２６）。
【０１０３】
なお、本実施形態では検査手段としてモデル検査の場合を例示したが、他の検査手法にも適用可能である。
【０１０４】
次に、本実施形態の効果について説明する。本実施形態では、検査対象のソフトウェアに関する記述のみから外部環境（具体的には、外部環境のモジュールの状態遷移情報）を生成できるように構成されているため、外部環境の記述の作業を軽減し、効率よく検査の準備ができる。また、本実施形態では、モデル検査手段２４０および外部環境生成手段２１０によって、モデル検査の実行により必要となった部分のみを拡張して外部環境を生成するように構成されているため、より簡潔で理解しやすい外部環境を自動で構築できる。そして、より簡潔で理解しやすい外部環境が構築されるため、検査結果に影響を与える振る舞いの記述も効率化できる。
【０１０５】
実施形態６．
次に、上述した第５の実施形態をより具体的な実施形態として、本発明の第６の実施形態について説明する。本発明の第６の実施形態の情報処理システムの構成は、図１１に示す本発明の第５の実施形態の情報処理システムの構成と同様なため、説明を省略する。
【０１０６】
本発明の第６の実施形態の情報処理システムの動作について、上述した第５の実施形態の場合と同様に、図１２に示すフローチャートを参照して説明する。
【０１０７】
まず、検査対象入力手段２００は、利用者から検査対象のソフトウェア（本実施形態ではモジュールＡ５００およびモジュールＢ６００）に関する記述を受け取る（ステップＳ２１）。ここでは、図３の状態遷移図で記述されたモデルを示す状態遷移情報を受け取るものとする。図３に模式的に示す状態遷移情報は、そのままモデル検査手段２４０で検査可能であり、メッセージの送信先および受信元に関する情報も明確であるとする。
【０１０８】
本実施形態の検査対象はモジュールＡ５００，Ｂ６００であり、利用者から検査対象入力手段２００に入力された状態遷移情報には、モジュールＡ５００，Ｂ６００，Ｃ７００の間のメッセージの送受信が記述されている。ここで、本実施形態では、図４に示すようにモジュールＡ５００，Ｂ６００，Ｃ７００の間でメッセージが送受信されるとする。
【０１０９】
検査対象入力手段２００は、利用者から受け取った状態遷移情報をモデル検査手段２４０に渡す。モデル検査手段２４０は、検査対象入力手段２００から検査対象のソフトウェアの状態遷移情報を受け取り、デッドロックが発生する可能性があるか否かを検査する（ステップＳ２２）。
【０１１０】
モデル検査手段２４０は、検査の結果、モジュールＡ５００が状態（１）、モジュールＢ６００が状態（５）でデッドロックが発生することを検出する（ステップＳ２０のＹ）。具体的には、モデル検査手段２４０は、例えば、モジュールＡ５００が状態（１）で送信するメッセージＸの送信先に応じた状態遷移情報が存在しないことにもとづいて、モジュールＡ５００が状態（１）で、外部環境へメッセージＸを送信しようとして失敗し、デッドロックが発生することを検出する。そして、モデル検査手段２４０は、例えば、モジュールＡ５００が状態（１）でデッドロックが発生することによって状態（２）に遷移せず、モジュールＢ６００にメッセージＺを送信しないことから、モジュールＢ６００は、メッセージＺを受信しようとして失敗し、デッドロックが発生することを検出する。
【０１１１】
モデル検査手段２４０は、発生したデッドロックを解消するために必要なメッセージの送信元および受信先と、各モジュールの状態とを示す情報を外部環境生成手段２１０に送る（ステップＳ２３）。具体的には、本実施形態では、モデル検査手段２４０は、モジュールＡ５００のデッドロックを解消するために、メッセージＸと、メッセージＸの送信元であるモジュールＡ５００と、メッセージＸの受信先であるモジュールＣ７００と、モジュールＡ５００が状態（１）であることとを示す情報を外部環境生成手段２１０に送る。また、本実施形態では、モデル検査手段２４０は、モジュールＢ６００のデッドロックを解消するために、メッセージＺと、メッセージＺの送信元であるモジュールＡ５００と、メッセージＺの受信先であるモジュールＢ６００と、モジュールＢ６００が状態（５）であることとを示す情報を外部環境生成手段２１０に送る。
【０１１２】
外部環境生成手段２１０は、モジュールＡ５００が状態（１）であり、モジュールＢ６００が状態（５）である時に応じた状態（１−５）に対応するモジュールＣ７００の状態遷移情報を生成し、その状態でメッセージＸを受信可能とする（ステップＳ２４）。図１３は、状態（１−５）に対応するモジュールＣ７００の状態遷移情報を示す状態遷移図である。図１３に示すように、モジュールＣ７００は、状態（１−５）でモジュールＡ５００からメッセージＸを受信した場合に、他の状態に状態遷移する。外部環境生成手段２１０は、作成した状態遷移情報を外部環境保存手段２２０に保存する。
【０１１３】
モデル検査手段２４０は、検査対象入力手段２００から受け取った検査対象のソフトウェアの状態遷移情報と、外部環境保存手段２２０に保存された状態遷移情報とをあわせて、モデル検査を実行し、デッドロックが発生する可能性があるか否かを検査する（ステップＳ２２）。本実施形態では、前述したステップＳ２４の処理で生成されて外部環境保存手段２２０に保存された状態遷移情報によって、モジュールＡ５００が状態（１）でメッセージＸを送信することに成功し、モジュールＢ６００が状態（５）でメッセージＺを受信することに成功するが、モジュールＡ５００が状態（３）であり、モジュールＢ６００が状態（６）であるときにデッドロックが発生することが検出される（ステップＳ２０のＹ）。
【０１１４】
このとき、モデル検査手段２４０は、モジュールＢ６００が状態（６）で外部環境（本実施形態ではモジュールＣ７００）からメッセージＹを受信しようとして失敗し、デッドロックが発生することを検出する。また、モデル検査手段２４０は、モジュールＡ５００が状態（３）でモジュールＢ６００からメッセージＺを受信しようとして失敗し、デッドロックが発生することを検出する。
【０１１５】
モデル検査手段２４０は、発生したデッドロックを解消するために必要なメッセージと、そのメッセージの送信元および受信先と、各モジュールの状態とを示す情報を外部環境生成手段２１０に送る（ステップＳ２３）。具体的には、本実施形態では、モデル検査手段２４０は、モジュールＢ６００のデッドロックを解消するために、メッセージＹと、メッセージＹの送信元であるモジュールＣ７００と、メッセージＸの受信先であるモジュールＢ６００と、モジュールＢ６００が状態（６）であることとを示す情報を外部環境生成手段２１０に送る。また、本実施形態では、モデル検査手段２４０は、モジュールＡ５００のデッドロックを解消するために、メッセージＺと、メッセージＺの送信元であるモジュールＢ６００と、メッセージＺの受信先であるモジュールＡ５００と、モジュールＡ５００が状態（３）であることとを示す情報を外部環境生成手段２１０に送る。
【０１１６】
外部環境生成手段２１０は、モジュールＡ５００が状態（３）であり、モジュールＢ６００が状態（６）である時に応じた状態（３−６）に対応するモジュールＣ７００の状態遷移情報を生成し、その状態でモジュールＢ６００にメッセージＹを送信可能とする（ステップＳ２４）。図１４は、状態（３−６）に対応するモジュールＣ７００の状態遷移情報を示す状態遷移図である。図１４に示すように、モジュールＣ７００は、状態（３−６）でモジュールＢ６００にメッセージＹを送信した場合に、他の状態に状態遷移する。外部環境生成手段２１０は、作成した状態遷移情報を外部環境保存手段２２０に保存する。
【０１１７】
本実施形態では、モデル検査の結果にもとづいて外部環境が拡張される。具体的には、外部環境保存手段２２０に保存される状態遷移情報が示す状態が追加される。図１５は、本実施形態において、発生したデッドロックがすべて解消したときに外部環境保存手段２２０に保存される状態遷移情報を示す状態遷移図である。図１５には、モジュールＣ７００が、状態（１−５）でモジュールＡ５００からメッセージＸを送信して状態（３−６）に状態遷移すること、状態（３−６）でモジュールＢ６００にメッセージＹを送信して状態（３−７）に状態遷移すること、状態（３−７）でモジュールＢ６００からメッセージＸを受信して状態（４−５）に状態遷移すること、および状態（４−５）でモジュールＡ５００にメッセージＹを送信して状態（１−５）に状態遷移することが示されている。
【０１１８】
利用者は必要に応じて外部環境編集手段２３０を利用して、外部環境保存手段２２０に保存された状態遷移情報を確認し、修正する（ステップＳ２５）。モデル検査手段２４０は、外部環境保存手段２２０に保存された状態遷移情報を用いてモデル検査を実行すると（ステップＳ２６）、外部環境（本実施形態ではモジュールＣ７００）が存在しないことに起因するデッドロックは検出されず、本来検査したい検査項目による検査が実行可能となる。
【０１１９】
次に、本実施形態の効果について説明する。本実施形態では、検査対象のソフトウェアに関する記述のみから外部環境（具体的には、外部環境のモジュールの状態遷移情報）を生成できるように構成されているため、外部環境の記述の作業を軽減し、効率よく検査の準備ができる。さらに、本実施形態では、モデル検査手段２４０および外部環境生成手段２１０によって、モデル検査の実行により必要となった部分のみを拡張して外部環境を生成するように構成されているため、より簡潔で理解しやすい外部環境を自動で構築できる。そして、より簡潔で理解しやすい外部環境が構築されるため、検査結果に影響を与える振る舞いの記述も効率化できる。
【産業上の利用可能性】
【０１２０】
本発明によれば、ソフトウェアの仕様策定時に、仕様に不備がないかを検査するといった用途に適用できる。また、ソフトウェア開発完了時に、開発したソフトウェアがどのような動作タイミングでも期待通りに動くことを検査するといった用途にも適用可能である。検査においては、すべての可能性を網羅的に検査するモデル検査の他、典型的な処理の流れを確認するシミュレーションなど他の検査手法にも適用できる。
【図面の簡単な説明】
【０１２１】
【図１】本発明の第１の実施形態の情報処理システムの構成例を示すブロック図である。
【図２】本発明の第１実施形態の情報処理システムの動作を示すフローチャートである。
【図３】利用者から検査対象入力手段に入力された状態遷移情報を示す状態遷移図である。
【図４】モジュールＡ，Ｂ，Ｃ間のメッセージ送受信の関係を示す説明図である。
【図５】状態遷移情報を生成しようとしているモジュール以外とのメッセージ送受信の情報が消去された状態遷移情報を示す状態遷移図である。
【図６】状態遷移情報を生成しようとしているモジュール以外とのメッセージ送受信の情報が消去された結果、内容のなくなった遷移および状態を状態遷移情報を示す状態遷移図である。
【図７】図６に示す状態遷移図におけるメッセージの送信と受信との処理を反転した状態遷移情報を示す状態遷移図である。
【図８】単一の状態遷移とした状態遷移情報を示す状態遷移図である。
【図９】本発明の第３の実施形態の情報処理システムの構成例を示すブロック図である。
【図１０】本発明の第３の実施形態の情報処理システムの動作を示すフローチャートである。
【図１１】本発明の第５実施形態の情報処理システムの構成例を示すブロック図である。
【図１２】本発明の第５の実施形態の情報処理システムの動作を示すフローチャートである。
【図１３】状態（１−５）に対応するモジュールＣの状態遷移情報を示す状態遷移図である。
【図１４】状態（３−６）に対応するモジュールＣの状態遷移情報を示す状態遷移図である。
【図１５】発生したデッドロックがすべて解消したときに外部環境保存手段に保存される状態遷移情報を示す状態遷移図である。
【符号の説明】
【０１２２】
１００、２００、３００  検査対象入力手段
１１０、２１０、３１０  外部環境生成手段
１２０、２２０  外部環境保存手段
１３０、２３０  外部環境編集手段
１４０、２４０、３４０  モデル検査手段
５００  モジュールＡ
６００  モジュールＢ
７００  モジュールＣ
【図１】
2009123159.tif 000003
【図２】
2009123159.tif 000004
【図３】
2009123159.tif 000005
【図４】
2009123159.tif 000006
【図５】
2009123159.tif 000007
【図６】
2009123159.tif 000008
【図７】
2009123159.tif 000009
【図８】
2009123159.tif 000010
【図９】
2009123159.tif 000011
【図１０】
2009123159.tif 000012
【図１１】
2009123159.tif 000013
【図１２】
2009123159.tif 000014
【図１３】
2009123159.tif 000015
【図１４】
2009123159.tif 000016
【図１５】
2009123159.tif 000017