(57)【要約】【課題】モデル検査においてプロパティの設定漏れの可能性を検出するとともに、計算コストを減少するモデル検査プログラム、モデル検査方法、モデル検査装置を提供する。【解決手段】検査対象プログラムをシミュレーション実行して、画面ごとにプロパティが成立するかを検査するモデル検査であって、検査対象プログラムをシミュレーション実行したとき表示される画面と画面に表示されるデータの入出力に関する画面項目と検査対象プログラムに記述されている変数とを対応付け、対応付けられた変数から画面遷移において複数の画面で共有して利用される変数を抽出し、抽出した変数から、前記画面遷移に関係するプロパティに使用されている変数を除外した変数を監視変数として設定し、各画面において監視変数だけを監視し、画面遷移の前後で記監視変数の値を比較し、前後の画面で値が相違する監視変数を検出して記録するモデル検査である。【選択図】図２
2011003109.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータに、
記録部から検査対象プログラムとプロパティを取得し、前記検査対象プログラムをシミュレーション実行して、プログラム実行状態ごとに前記プロパティが成立するかを検査するモデル検査を実行させるモデル検査プログラムであって、
前記検査対象プログラムをシミュレーション実行したとき表示される画面と前記画面に表示されるデータの入出力に関する画面項目と前記検査対象プログラムに記述されている変数とを対応付ける画面・変数対応解析処理と、
前記画面・変数対応解析処理により前記画面と前記画面項目に対応付けた変数から画面遷移において複数の画面で共有して利用される変数を抽出する監視変数候補抽出処理と、
前記プロパティから前記画面遷移に関係するプロパティだけを抽出する画面遷移関連プロパティ抽出処理と、
前記監視変数候補抽出処理により抽出された変数から、前記画面遷移関連プロパティ抽出処理で抽出されたプロパティに使用されている変数を除外した変数を監視変数として設定する監視変数設定処理と、
前記監視変数設定処理により設定された前記監視変数だけを監視し、画面遷移の前後で前記監視変数の値を比較し、前後の画面で値が相違する前記監視変数を検出して記録部に記録するプロパティ設定漏れ監視処理と、
を実行させることを特徴とするモデル検査プログラム。
【請求項２】
前記プロパティ設定漏れ監視処理で検出された前記監視変数と、画面遷移の前後の画面の情報を入出力装置の表示画面に出力するプロパティ設定漏れ出力処理を実行させることを特徴とする請求項１に記載のモデル検査プログラム。
【請求項３】
前記プロパティ設定漏れ監視処理は、
前記監視変数設定処理で設定された前記監視変数に対して、該監視変数の値が画面遷移しても等しいと記述した監視用プロパティを作成して前記記録部に記録し、
前記監視用プロパティに対してシミュレーション実行して状態ごとに前記監視用プロパティが成立しているかを検査した結果を取得し、前記監視用プロパティが不成立となったとき、該監視用プロパティを作成するもとの監視用変数を検出して記録部に記録することを特徴とする請求項１または２に記載のモデル検査プログラム。
【請求項４】
前記監視変数候補抽出処理は、
画面遷移の順を記録した画面遷移情報を取得し、画面遷移において連続する画面の遷移前後画面だけで利用される変数を抽出することを特徴とする請求項１〜３のいずれかひとつに記載のモデル検査プログラム。
【請求項５】
前記監視変数候補抽出処理は、
画面遷移の順を記録した画面遷移情報を取得し、自画面遷移する画面に関連する変数を抽出することを特徴とする請求項１〜４のいずれかひとつに記載のモデル検査プログラム。
【請求項６】
記録部から検査対象プログラムとプロパティを取得し、前記検査対象プログラムをシミュレーション実行して、プログラム実行状態ごとに前記プロパティが成立するかを検査するモデル検査方法であって、
前記検査対象プログラムをシミュレーション実行したとき表示される画面と前記画面に表示されるデータの入出力に関する画面項目と前記検査対象プログラムに記述されている変数とを対応付け、対応付けられた変数から画面遷移において複数の画面で共有して利用される変数を抽出し、
抽出した変数から、前記プロパティから前記画面遷移に関係するプロパティに使用されている変数を除外した変数を監視変数として設定し、
各状態において前記監視変数だけを監視し、画面遷移の前後で前記監視変数の値を比較し、前後の画面で値が相違する前記監視変数を検出して記録部に記録する
ことを特徴とするモデル検査方法。
【請求項７】
記録部から検査対象プログラムとプロパティを取得し、前記検査対象プログラムをシミュレーション実行して、プログラム実行状態ごとに前記プロパティが成立するかを検査するモデル検査部と、
前記検査対象プログラムをシミュレーション実行したとき表示される画面と前記画面に表示されるデータの入出力に関する画面項目と前記検査対象プログラムに記述されている変数とを対応付ける画面・変数対応解析部と、
前記画面・変数対応解析部により前記画面と前記画面項目に対応付けた変数から画面遷移において複数の画面で共有して利用される変数を抽出する監視変数候補抽出部と、
前記プロパティから前記画面遷移に関係するプロパティだけを抽出する画面遷移関連プロパティ抽出部と、
前記監視変数候補抽出部により抽出された変数から、前記画面遷移関連プロパティ抽出部で抽出されたプロパティに使用されている変数を除外した変数を監視変数として設定する監視変数設定部と、
各状態において前記監視変数設定部により設定された前記監視変数だけを監視し、画面遷移の前後で前記監視変数の値を比較し、前後の画面で値が相違する前記監視変数を検出して記録するプロパティ設定漏れ監視部と、を備えるプロパティ設定漏れ検出部と、
を備えることを特徴とするモデル検査装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラムのモデル検査におけるプロパティの設定漏れを検出する技術に関する。
【背景技術】
【０００２】
プログラムのモデル検査において、プロパティの設定に漏れがある場合、プロパティの設定漏れに係るモデル検査が十分に実行されず、プロパティの設定漏れに起因するプログラムの不具合が検出されず、プログラムが正常に動作しないことがある。そこで、プロパティがプログラムの挙動を網羅的に漏れなくカバーする設定をするために、漏れている可能性のあるプロパティを検出する提案がされている。
【０００３】
例えば、ユーザ操作等によりプログラム状態（変数値）が変化した時、業務ロジックを実装した処理が実行されたとみなして、モデル検査実施時の状態遷移時に変数を監視する。そして、プロパティに記述のない変数の値変化が検出されたら、該変数に関するプロパティが漏れていると判定する技術が知られている。
【０００４】
また、論理シミュレーションにおいて状態遷移の動作を確認し網羅率と動作部分と未動作部分を求める技術が知られている。例えば、分岐条件抽出部では、ソースファイルを入力として、分岐条件を抽出し分岐条件ファイルに出力する。分岐条件分割部では、分岐条件ファイルから各分岐条件を個々の信号へと分割し分岐条件が成立するときの信号値と共に分岐条件信号ファイルを作成する。網羅率測定部では、分岐条件信号ファイルから分岐条件の個々の信号が成立するかの組合せ数を算出し、シミュレーション結果ファイルからその組合せのうち実際に実行された数の算出と実行されていない組合せのリスト作成を行う。論理検証の網羅率として「実行された組合せ数／全組合せ数」を未実行組合せリストと共に網羅率ファイルに出力する。
【０００５】
また、論理回路の動的検証、静的検証のいずれによっても検証されない変数と条件式とを判別できる論理回路設計検証の技術が知られている。例えば、被検証対象のＲＴＬ記述中に含まれるすべての変数と条件式とを抽出して、記憶部に格納する。次に、動的検証ツールである論理シミュレーションを実行し、テストパターンにより活性化した変数や条件式を記憶部に格納する。静的検証ツールであるプロパティ検証ツールを実行し、プロパティ単位で切り分けられた論理コーンに含まれるすべての変数と条件式を記憶部に格納する。記憶部に格納されたＲＴＬ記述中に含まれるすべての変数と条件式と、動的検証ツール、静的検証ツールによって検証された変数と条件式とを比較し、検証されなかった変数と条件式とを出力する。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開平７−３１９９２７号公報
【特許文献２】特開平１０−６３５３７号公報
【特許文献３】特開２００１−３１８９５９号公報
【特許文献４】特開２００６−２２１４７３号公報
【特許文献５】特開２００６−１０６８６５号公報
【特許文献６】特開２００８−２６９５８５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
プログラムのモデル検査において、検査対象システムの全ての変数に関してプロパティを設定することや、シミュレーション実行時に、抽出した全ての変数や条件を監視対象にするのは、計算コストが大きく、実システムにおいては実施が困難である。
【０００８】
上記のような実情に鑑みてなされたものであり、モデル検査においてプロパティの設定漏れの可能性を検出するとともに、計算コストを減少するモデル検査プログラム、モデル検査方法、モデル検査装置を提供することを目的とする。
【課題を解決するための手段】
【０００９】
態様のひとつであるモデル検査は、監視変数候補抽出処理、監視変数候補抽出処理、画面遷移関連プロパティ抽出処理、画面遷移関連プロパティ抽出処理、監視変数設定処理、プロパティ設定漏れ監視処理、プロパティ設定漏れ出力処理を実行させる。
【００１０】
画面・変数対応解析処理は、検査対象プログラムをシミュレーション実行したとき表示される画面と前記画面に表示されるデータの入出力に関する画面項目と前記検査対象プログラムに記述されている変数とを対応付ける。監視変数候補抽出処理は、画面・変数対応解析処理により前記画面と前記画面項目に対応付けた変数から画面遷移において複数の画面で共有して利用される変数を抽出する。画面遷移関連プロパティ抽出処理は、プロパティから画面遷移に関係するプロパティだけを抽出する。監視変数設定処理は、監視変数候補抽出処理により抽出された変数から、画面遷移関連プロパティ抽出処理で抽出されたプロパティに使用されている変数を除外した変数を監視変数として設定する。プロパティ設定漏れ監視処理は、各状態において前記監視変数設定処理により設定された前記監視変数だけを監視し、画面遷移の前後で前記監視変数の値を比較し、前後の画面で値が相違する前記監視変数を検出して記録部に記録する。
【発明の効果】
【００１１】
モデル検査においてプロパティの設定漏れの可能性を検出するとともに、計算コストを減少させることができる。
【図面の簡単な説明】
【００１２】
【図１】検査対象プログラムのモデル検査を実行する装置の一例を示す図である。
【図２】モデル検査部、プロパティ設定漏れ検出部の構成の一例を示すブロック図である。
【図３】制御部の動作の一例を示すフロー図である。
【図４】ウェブアプリケーションの画面遷移を示した例であり、オンラインショッピングの一部として、商品検索、カート内容、購入内容の画面遷移を示している。
【図５】ウェブアプリケーションの画面遷移を示した例であり、オンラインショッピングの一部として、商品検索、カート内容、購入内容の画面遷移を示している。
【図６】画面・変数対応解析部の動作の一例を示すフロー図である。
【図７】図４で示したウェブアプリケーションでの、画面とＪＳＰとＪａｖａＢｅａｎの関係を示す図である。
【図８】ＪＳＰファイルの一例を示すカート内容．ｊｓｐのソースを示す図である。
【図９】画面・変数対応解析部の解析結果である画面・変数対応テーブルの一例を示す図である。
【図１０】監視変数候補抽出部の動作の一例を示すフロー図である。
【図１１】画面遷移情報をＸＭＬ形式で記述した例を示す図である。
【図１２】監視変数候補を示す図である。
【図１３】図４または図１１のウェブアプリケーションを例とした場合の、監視変数候補抽出部が監視変数候補テーブルから連続する画面の遷移後画面だけで利用される変数を抽出した結果である。
【図１４】自画面遷移図５のウェブアプリケーションの自画面遷移を例とした場合の、監視変数候補抽出部の出力（画面に関連する変数）である。
【図１５】画面遷移関連プロパティ抽出部の動作の一例を示すフロー図である。
【図１６】図４で示したウェブアプリケーションのプロパティの例を示す図である。
【図１７】画面遷移関連プロパティ抽出部の結果の例（画面遷移関連プロパティ）である。
【図１８】監視変数設定部の動作の一例を示すフロー図である。
【図１９】プロパティ「３」「５」に対応する行を除外し、プロパティ「２」に対応する行の一部を削除した図である。
【図２０】画面遷移関連プロパティ抽出部の結果が図１９であった場合の、監視変数設定部の結果を示す図である。
【図２１】プロパティ設定漏れ監視部の動作の一例を示すフロー図である。
【図２２】監視変数設定部において、カート内容画面と購入内容画面の間で、監視変数の値を示した図である。
【図２３】プロパティ設定漏れ出力部の出力例を示す図である。
【図２４】プロパティ設定漏れ出力部の出力例を示す図である。
【図２５】実施例２におけるプロパティ漏れ監視部で作成される監視用プロパティを示す図である。
【図２６】監視用プロパティ設定の一例を示すフロー図である。
【図２７】監視用プロパティによるプロパティ設定漏れ監視の一例を示すフロー図である。
【図２８】実施例がコンピュータプログラムとして実現される場合の構成を示す図である。
【発明を実施するための形態】
【００１３】
プログラムのモデル検査とは、プログラム（モデル）が性質（プロパティ）を満足するか否かをシミュレーションし、シミュレーション実行時の全ての状態（例えば変数の値など）を、プロパティを用いてチェックすることで検査する方法である。プロパティとは、プログラムが実現すべきロジックを記述したものであり、プロパティは、検査したい内容を論理式として表現したものである。
【００１４】
また、ソフトウェア開発においてモデルとは、開発要件や処理内容を記述したものである。モデルには、記述の詳細度によって種々のレベルがある。例えば、概要設計のレベルでは、ＵＭＬ（Unified Modeling Language）を用いて、情報の静的構造や処理シーケンスや配置情報が記述されたモデルが利用される。また、開発仕様を厳密に記述する場合には、仕様記述言語を用いて開発仕様がモデルとして記述される例もある。さらに、開発要件の動的な側面をモデル化する場合には、例えば、Ｐｒｏｍｅｌａ等のモデル記述用の専用言語を用いて状態遷移等を記述する。Ｐｒｏｍｅｌａで記述されたモデルに対しては、ＳＰＩＮモデルチェッカなどのツールがあり、これらのツールによりモデル検査が実行される。Ｊａｖａ（登録商標）等の実行可能なプログラム言語を用いて記述されたソフトウェアも、記述が最も詳細なモデルであると見ることができる。Ｊａｖａで記述されたプログラムに対するモデル検査ツールには、例えば、ＪＰＦ（Java Path Finder）がある。
【００１５】
以下図面に基づいて、実施形態について詳細に説明する。
（実施例１）
図１は、検査対象プログラムのモデル検査を実行する装置の一例を示す図である。図１に示す装置１は、制御部２、記録部３を備え、入出力装置４と接続されている。装置１は、入出力装置４から入力された検査対象プログラム７のモデル検査を実行する。例えば、装置１はコンピュータや専用のハードウェアである。
【００１６】
制御部２は、モデル検査部５、プロパティ設定漏れ検出部６を備えている。制御部２はモデル検査部５、プロパティ設定漏れ検出部６以外に、入出力装置４、不図示の外部記録装置などの周辺機器とのやり取りの制御を行う。また、制御部２はＣＰＵ（Central Processing Unit）やプログラマブルなデバイス（ＦＰＧＡ（Field Programmable Gate Array）、ＰＬＤ（Programmable Logic Device）など）を用いることができる。
【００１７】
モデル検査部５は、検査対象プログラム７をシミュレーション実行させて状態遷移を起こさせ、各状態においてプロパティ８を評価することによって、検査対象プログラム７が、設定されたプロパティ８に記述された条件を満足しているか検査する。
【００１８】
なお、上記状態とは、例えばユーザ操作等により入出力装置４から入力された入力データや現在の状態の変数値を用いてプログラムに含まれる関数を実行したときに変化する変数値などの状態を示すものである。また、ユーザ操作等により入出力装置４から入力された入力データや現在の状態の変数値を用いて関数が実行され、プログラム状態（変数の値など）が変化して次の状態に変化することを状態遷移という。
【００１９】
プロパティ設定漏れ検出部６は、モデル検査部５と設定したプロパティ８と共同して動作し、設定済みのプロパティ８が検査対象プログラム７の挙動（動作の仕方）を十分にカバーしているかを調査し、設定済みプロパティ８に対応しない挙動を検出することによって、プロパティ８に設定漏れの可能性があることを検出する。
【００２０】
なお、モデル検査部５、プロパティ設定漏れ検出部６は、ソフトウェアとしてコンピュータに実装され、コンピュータにより実行してもよい。
記録部３は、検査対象プログラム７、プロパティ８、入出力装置４から入力される不図示の入力データや、ドライバ、データベーススタブ、ネットワークスタブなどが記録されている。また、記録部３は、例えばＲＯＭ（Read Only Memory）、ＲＡＭ（Random Access Memory）、ハードディスクなどのメモリである。また、記録部３は、パラメータ値、変数値などのデータを記録してもよいし、ワークエリアとして用いることもできる。
【００２１】
図２は、モデル検査部５、プロパティ設定漏れ検出部６の一例を示すブロック図である。モデル検査部５は、モデル検査実行部２１、検査対象プログラム保持部２２、プロパティ保持部２３を備えている。
【００２２】
プロパティ設定漏れ検出部６は、画面・変数対応解析部２４、監視変数候補抽出部２５、画面遷移関連プロパティ抽出部２６、監視変数設定部２７、プロパティ設定漏れ監視部２８、プロパティ設定漏れ出力部２９を備えている。
【００２３】
モデル検査実行部２１は、従来の技術を用いてプログラムのモデル検査を実行する。
検査対象プログラム保持部２２は、記録部３から検査対象プログラム７を取得して保持する。ただし、検査対象プログラム保持部２２は記録部３からモデル検査実行部２１が直接検査対象プログラム７を取得する場合にはなくてもよい。
【００２４】
プロパティ保持部２３は、記録部３からプロパティ８を取得して保持する。
画面・変数対応解析部２４は、検査対象プログラム保持部２２に保持された検査対象プログラム７のうち、入出力装置４の表示画面に表示される画面項目に関する入出力処理を記述したプログラムを解析し、表示画面とプログラムで用いる変数の対応関係を抽出する。
【００２５】
監視変数候補抽出部２５は、画面・変数対応解析部２４で抽出した結果、および画面遷移情報を利用して、複数の表示画面で共有して利用される変数を抽出する。
画面遷移関連プロパティ抽出部２６は、プロパティ保持部２３が保持するプロパティ８から画面遷移に関係するプロパティを抽出する。
【００２６】
監視変数設定部２７は、監視変数候補抽出部２５によって抽出された変数から、画面遷移関連プロパティ抽出部２６で抽出された画面遷移に関係するプロパティに使用されている変数を除外した変数を監視変数として設定する。
【００２７】
プロパティ設定漏れ監視部２８は、モデル検査実行部２１によるシミュレーション実行における状態遷移において、監視変数設定部２７により設定された監視変数について画面遷移の前後で監視変数の値を比較し、監視変数の値が画面遷移の前後で相違があった場合に、値が相違であった監視変数、遷移前画面、遷移後画面などの情報を、記録部３に記録する。その後、プロパティ設定漏れ監視部２８は、モデル検査実行終了後にプロパティ設定漏れ出力部２９に記録した結果（情報）を出力する。
プロパティ設定漏れ出力部２９は、プロパティ設定漏れ監視部２８によって検出されたプロパティ設定漏れの可能性のある変数について情報を入出力装置４に出力する。
【００２８】
（動作説明）
図３は、制御部２の動作の一例を示すフロー図である。
コンピュータに、画面・変数対応解析処理、監視変数候補抽出処理、画面遷移関連プロパティ抽出処理、監視変数設定処理、プロパティ設定漏れ監視処理、プロパティ設定漏れ出力処理を実行させる。
【００２９】
画面・変数対応解析処理は、検査対象プログラムをシミュレーション実行したとき表示される画面と前記画面に表示されるデータの入出力に関する画面項目と前記検査対象プログラムに記述されている変数とを対応付ける。監視変数候補抽出処理は、画面・変数対応解析処理により対応付けた変数から画面遷移において複数の状態で共有して利用される変数を抽出する。画面遷移関連プロパティ抽出処理は、プロパティから画面遷移に関係するプロパティだけを抽出する。監視変数設定処理は、監視変数候補抽出処理により抽出された変数から、画面遷移関連プロパティ抽出処理で抽出されたプロパティに使用されている変数を除外した変数を監視変数として設定する。プロパティ設定漏れ監視処理は、各状態において監視変数設定処理により設定された監視変数だけを監視し、画面遷移の前後で監視変数の値を比較し、前後の画面で値が相違する監視変数を検出して記録部に記録する。
【００３０】
ステップＳ１（画面・変数対応解析処理）では、画面・変数対応解析部２４が検査対象プログラム保持部２２に保持されている検査対象プログラム７のうち表示画面の入出力に関するプログラム（画面入出力プログラム）を解析する。そして、画面・変数対応解析部２４は、表示画面に表示される画面項目に関する変数を抽出し、画面項目と変数の対応関係を抽出する。なお、画面・変数対応解析部２４の動作については後述する。
【００３１】
ステップＳ２（監視変数候補抽出処理）では、監視変数候補抽出部２５がステップＳ１の結果の対応関係から、検査対象プログラム７の画面遷移において、複数画面の画面項目が共有するプログラム変数を抽出し、画面遷移と該変数を対応付ける。なお、監視変数候補抽出部２５の動作については後述する。
【００３２】
ステップＳ３（画面遷移関連プロパティ抽出処理）では、画面遷移関連プロパティ抽出部２６が、プロパティ保持部２３が保持するプロパティ群の中から、画面遷移に関係するプロパティだけを抽出し、画面遷移関連プロパティとする。なお、画面遷移関連プロパティ抽出部２６の動作については後述する。
【００３３】
ステップＳ４（監視変数設定処理）では、監視変数設定部２７がステップＳ２で抽出された複数画面対応変数のうちから、ステップＳ３で抽出された画面遷移関連プロパティに使用されている変数を除外した変数を監視変数に設定する。
【００３４】
ステップＳ５（モデル検査実行処理）では、モデル検査実行部２１がモデル検査を開始する。
ステップＳ６（モデル検査実行処理）では、モデル検査実行部２１がモデル検査を終了するかどうかを判定する。モデル検査の終了の条件は種々に設定される。例えば、モデル検査の終了条件は、プロパティ設定漏れ監視部２８によってプロパティ設定漏れが検出された場合、あるいは、モデル検査実行部２１が検査対象プログラム７の全ての状態遷移についてシミュレーションを実行した場合が考えられる。また、プロパティ保持部２３が、保持するプロパティ８でプロパティ違反が検出された場合などがある。モデル検査の終了条件が成立した場合に、モデル検査部５とプロパティ設定漏れ検出部６は実行を終了する。
【００３５】
ステップＳ７（モデル検査実行処理）では、モデル検査実行部２１が、検査対象プログラム保持部２２が保持する検査対象プログラム７に対して、シミュレーション実行とプロパティ評価を継続する。
【００３６】
ステップＳ８（モデル検査実行処理）では、シミュレーション実行により監視対象プログラムの状態が遷移したとき、モデル検査実行部２１がその状態が画面遷移かどうかを判定する。状態遷移が画面遷移ではない場合は、ステップＳ６に移行し、画面遷移の場合はステップＳ９へ移行する。
【００３７】
ステップＳ９（プロパティ設定漏れ監視処理）では、プロパティ設定漏れ監視部２８が、画面遷移が発生したとき画面遷移前後でのステップＳ４で設定された監視変数の値を比較する。ステップＳ１０（プロパティ設定漏れ監視処理）では、プロパティ設定漏れ監視部２８が画面遷移前後で監視変数の値が等しいかを評価する。監視変数の値が等しい場合はステップＳ６に移行し、監視変数の値が変化した場合はステップＳ１１に移行する。なお、プロパティ設定漏れ監視部２８の動作については後述する。
【００３８】
ステップＳ１１（プロパティ設定漏れ出力処理）では、ステップＳ１０で値の変化が検出された監視変数に関して、プロパティ設定漏れ出力部２９がプロパティの設定漏れの可能性を出力する。出力後はステップＳ６に移行する。なお、プロパティ設定漏れ出力部２９の動作については後述する。
【００３９】
次に、ウェブ（Ｗｅｂ）アプリケーションの例を用いて動作を説明する。
図４、図５は、ウェブアプリケーションの画面遷移を示した例であり、オンラインショッピングの一部として、商品検索、カート内容、購入内容確認の画面遷移を示している。
【００４０】
なお、本例では検査対象プログラムが、Ｊａｖａを用いて開発されたウェブアプリケーションである場合を想定して説明する。しかし、特定のプログラム言語の種別やアプリケーションのアーキテクチャ／フレームワークに限定されるものではない。
【００４１】
以下、画面とは、ＨＴＭＬ等で記述されたウェブページ記述（画面プログラム）をウェブブラウザで表示したページを意味する。また、Ｊａｖａを利用したウェブアプリケーションにおける画面としてのウェブページは、ＪＳＰ（Java Server Pages）で記述され、利用時にＳｅｒｖｌｅｔにコンパイルされ実行処理される。そして、処理結果がＨＴＭＬ形式でウェブブラウザに送信されることによって、画面（ウェブページ）が表示される。
【００４２】
図４の例では、入出力装置４の表示画面に表示された商品検索画面４１を用いて商品検索を行ったのち、「商品の追加」ボタン４６を押すと、カート内容画面４２に遷移する。図４の例では、商品検索の画面（破線範囲）は表示内容を省略しているが、例えば商品名と商品に対する値段の一覧表が表示されている。
【００４３】
カート内容画面４２には、ユーザにより入出力装置４から入力された「お客さま氏名」「会員種別」とともに追加された商品の一覧が表示される。本例では、「お客さま氏名」にはユーザの氏名として「冨士タロウ」が入力され、「会員種別」にはユーザの会員の種別を示す「ゴールド」が入力されている。また、商品の一覧には、「商品名」「単価（円）」「割引（円）」「数量」が表示される。「商品名」にはユーザが選んだ商品の商品名が表示され（本例では商品Ａ、商品Ｂ）、「単価（円）」には商品に対応する単価が表示される（本例では１，０００、３，０００）。また、「割引（円）」には商品に対応する割引額が表示され（本例では割引が未確定のため「−」）、「数量」には商品に対応する数量が表示されている（本例では「４」「２」）。
【００４４】
ユーザがカート内容画面４２で商品の購入数量（本例では「４」「２」）を入力した後、「購入」ボタン４８を押すと購入内容画面４３に遷移する。また、カート内容画面４２で「商品検索」ボタン４７を押すと、商品検索画面４１に戻り、商品を追加できる。
【００４５】
購入内容画面４３では、入力された「お客さま氏名」と「会員種別」、購入商品の一覧、および「正価合計（円）」（合計金額）、「割引合計（円）」（会員種別により異なる割引金額）、「お支払い（円）」（支払い金額）が表示される。本例では、「商品Ａ」に対応する「割引（円）」に「１００」が表示され、「商品Ｂ」に対応する「割引（円）」に「３００」が表示される。「正価合計（円）」「割引合計（円）」「お支払い（円）」にはそれぞれ「１０，０００」「１，０００」「９，０００」が表示される。
【００４６】
ユーザが「購入実施」ボタン４１０を押すと購入処理が実行されて完了画面４４に遷移して購入が完了し、「カートに戻る」ボタン４９を押すとカート内容画面４２に戻る。なお、購入処理とは、購入する商品とその商品に対応する情報（購入内容画面４３に表示された情報）を、販売元のサーバなどに送信する処理などである。なお、販売元のサーバなどへの通信についてのモデル検査は、ネットワークスタブなどを用いて検査している。
【００４７】
図５の例では、入出力装置４の表示画面に表示された商品検索画面５１において商品検索を行ったのち、「商品の追加」ボタン５４を押すと、購入内容画面５２に遷移する。
購入内容画面５２には、ユーザにより入出力装置４から入力された「お客さま氏名」「会員種別」とともに追加された商品の一覧が表示される。本例では、「お客さま氏名」にはユーザの氏名として「冨士タロウ」が入力され、「会員種別」にはユーザの会員の種別を示す「ゴールド」が入力されている。また、商品の一覧には、「商品名」「単価（円）」「数量」が表示される。「商品名」にはユーザが選んだ商品の商品名が表示され（本例では商品Ａ、商品Ｂ）、「単価（円）」には商品に対応する単価が表示される（本例では１，０００、３，０００）、「数量」には商品に対応する数量が表示されている（本例では「４」「２」）。
【００４８】
ユーザが購入内容画面５２において購入数量（本例では「４」「２」）を入力した後、「合計計算」ボタン５７を押すと購入内容画面５２に自己画面遷移して、合計金額、会員種別により異なる割引金額、支払い金額が表示される。
【００４９】
ユーザが購入内容画面５２では、入力された「お客さま氏名」と「会員種別」、購入商品の一覧、および「正価合計（円）」（合計金額）、「割引合計（円）」（会員種別により異なる割引金額）、「お支払い（円）」（支払い金額）が表示される。本例では、「正価合計（円）」「割引合計（円）」「お支払い（円）」にはそれぞれ「１０，０００」「１，０００」「９，０００」が表示される。
【００５０】
「商品検索」ボタン５５を押すと、商品検索画面５１に戻り、商品を追加できる。「購入実施」ボタン５６を押すと購入処理が実行されて完了画面５３に遷移して購入が完了する。
【００５１】
図４と図５のウェブアプリケーションの例は、同一の購入処理機能を提供するが、図４の例ではカート内容画面４２と購入内容画面４３が別画面となっている。一方、図５の例では、一つの購入内容画面５２で、上記カート内容画面４２と購入内容画面４３の内容を表示する。
【００５２】
図６は、画面・変数対応解析部２４の動作の一例を示すフロー図である。
ステップＳ６１では、画面・変数対応解析部２４が画面項目の入出力に関連するプログラム（画面入出力プログラム）を検査対象プログラム保持部２２から読み込む。
【００５３】
検査対象プログラム保持部２２が保持するプログラム群（検査対象プログラム）のうち、どのプログラムが画面項目の入出力に関連するかは、プログラム言語、フレームワーク、アーキテクチャなどに依存する。
【００５４】
プログラムには、画面の入出力に関するプログラム、制御に関するプログラム、データベース周りに関するプログラムなどが含まれる。これらプログラム全体から、画面項目の入出力に関連するプログラムだけを抽出する処理は、前記依存事項に関する抽出ルールに従って実行される。例えば、検査対象プログラムがＪＳＰを利用するアーキテクチャであった場合、ＪＳＰが画面項目の入出力に関連するプログラムとして抽出するルールに従ってプログラムが抽出される。あるいは、ＪＳＰを用いずＳｅｒｖｌｅｔで直接にＨＴＭＬを生成するアーキテクチャであった場合は、Ｓｅｒｖｌｅｔのプログラムを抽出するルールに従って、画面入出力のプログラムが抽出される。
【００５５】
ステップＳ６２では、画面・変数対応解析部２４により読み込まれた画面入出力プログラムを解析して画面項目に関連する変数を抽出する。プログラムの解析処理の内容は、抽出された画面入出力プログラムの種別に依存する。例えば、画面入出力プログラムがＪＳＰの場合、ＪＳＰタグのｕｓｅＢｅａｎタグを解析することによってＪａｖａＢｅａｎを抽出する。その後、ｇｅｔＰｒｏｐｅｔｙタグやｓｅｔＰｒｏｐｅｒｔｙタグを解析することによって、画面項目に関連するプログラム変数として利用されているＪａｖａＢｅａｎとプロパティを抽出する。また、画面入出力プログラムがＳｅｒｖｌｅｔである場合は、ＳｅｒｖｌｅｔのｄｏＧｅｔメソッドやｄｏＰｏｓｔメソッド等のＨｔｔｐＳｅｒｖｅｌｔＲｅｓｐｏｎｓｅ型の引数に対して設定処理されるＨＴＭＬの部分を解析する。解析することによって、画面項目に関連する変数を抽出する。画面入出力プログラムがＪＳＰの場合でも、ＪＳＰをコンパイルして生成されたＳｅｒｖｌｅｔを解析対象とすることもできる。
【００５６】
ステップＳ６３では、画面・変数対応解析部２４がステップＳ６２の解析結果として、画面と画面項目と変数の対応関係表（図９の画面・変数対応テーブル）を出力する。
ここで、検査対象プログラムがＪＳＰを利用するアーキテクチャである場合について説明する。図７は、図４で示したウェブアプリケーションでの、画面とＪＳＰとＪａｖａＢｅａｎの関係を示す図である。本例では画面はＪＳＰにより表示され、ＪＳＰ内ではＪＳＰタグを利用してＪａｖａＢｅａｎと連携している。
【００５７】
図７に示した商品検索画面４１（図４と同じ）は、商品検索．ｊｓｐ７５（ＪＳＰファイル）により表示され、商品検索．ｊｓｐ７５はＪＳＰタグを用いＩｔｅｍＢｅａｎ７１（クラス）と連携している。例えば、商品検索画面４１の場合、ＩｔｅｍＢｅａｎ７１により管理されている商品検索の画面（破線範囲）に表示される商品名（ｎａｍｅ）と商品に対応する値段（ｐｒｉｃｅ）などのデータを商品検索．ｊｓｐ７５から参照更新する。
【００５８】
図７に示したカート内容画面４２（図４と同じ）は、カート内容．ｊｓｐ７６（ＪＳＰファイル）により表示され、カート内容．ｊｓｐ７６はＪＳＰタグを用いＵｓｅｒＢｅａｎ７２、ＣａｒｔＢｅａｎ７３（クラス）と連携している。例えば、カート内容画面４２の場合、ＵｓｅｒＢｅａｎ７２とＣａｒｔＢｅａｎ７３により管理されているデータをカート内容．ｊｓｐ７６から参照更新する。ＵｓｅｒＢｅａｎ７２は、カート内容画面４２の画面項目「お客さま氏名」「会員種別」に関する変数として、「お客さま氏名」に対応するｎａｍｅ、「会員種別」に対応するｍｅｍｂｅｒＴｙｐｅを有している。また、ＣａｒｔＢｅａｎ７３はカート内容画面４２の画面項目「商品名」「単価（円）」「割引（円）」「数量」に関する変数をＩｔｅｍ７４に有している。Ｉｔｅｍｓ７４には「商品名」「単価（円）」「割引（円）」「数量」にそれぞれ対応するｎａｍｅ、ｕｎｉｔＰｒｉｃｅ、ｕｎｉｔＤｉｓｃｏｕｎｔ、ｏｒｄｅｒｅｄＱｕａｎｔｉｔｙを有している。
【００５９】
図７に示した購入内容画面４３（図４と同じ）は、購入内容．ｊｓｐ７７（ＪＳＰファイル）により表示され、購入内容．ｊｓｐ７７はカート内容．ｊｓｐ７６と同様、ＪＳＰタグを用いＵｓｅｒＢｅａｎ７２、ＣａｒｔＢｅａｎ７３（クラス）と連携している。購入内容画面４３の場合、ＣａｒｔＢｅａｎ７３の「正価合計（円）」「割引合計（円）」「お支払い（円）」にそれぞれ対応するｔｏｔａｌＰｒｉｃｅ、ｔｏｔａｌＤｉｓｃｏｕｎｔ，ｐａｙｍｅｎｔについても購入内容．ｊｓｐ７７から参照更新する。
【００６０】
図８は、ＪＳＰファイルの一例を示すカート内容．ｊｓｐ７６のソースを示す図である。カート内容．ｊｓｐ７６とＵｓｅｒＢｅａｎ７２とＣａｒｔＢｅａｎ７３との連携は、図８の破線範囲８１に記載されているコードにより行われる。
【００６１】
破線範囲８１のコードを示す。
<jsp:useBean class="UserBean" id="user" scope="session">
<jsp:useBean class="CartBean" id="user" scope="session">
カート内容画面４２の画面項目「お客さま氏名」「会員種別」との関連付けは、図８の破線範囲８２、８３に記載のコードにより行われる。
【００６２】
破線範囲８２のコードを示す。
<TD>お客さま氏名</TD>
<TD><jsp:getProperty name="user" property="name"></TD>
破線範囲８３のコードを示す。
【００６３】
<TD>会員種別</TD>
<TD><jsp:getProperty name="user" property="memberType"></TD>
なお、カート内容画面４２の他の画面項目の説明は省略する。
【００６４】
図９は、画面・変数対応解析部２４の解析結果である画面・変数対応テーブルの一例を示す図である。画面・変数対応テーブルは、「画面」「画面項目」「変数」を記録する行を有し、「画面」には画面の名称（クラス名）、「画面項目」には画面に表示される項目、「変数」には「画面項目」に対応する変数（本例ではＪａｖａＢｅａｎに記述されている変数）。例えば、図９に示す行９１の場合であれば、画面・変数対応解析部２４が、図８のカート内容．ｊｓｐの破線範囲８４の<TITLE>カート内容</TITLE>を抽出して、「カート内容」を「画面」に記録する。例えば、「画面」に記録する画面の名称の抽出は<TITLE>や</TITLE>を検索してその間に記録されているテキスト（本例、カート内容）を抽出して記録する。
【００６５】
次に、図９に示す行９１の場合であれば、画面・変数対応解析部２４は、図８のカート内容．ｊｓｐの破線範囲８２の<TD>お客さま氏名</TD>を検出して、「画面」に対応する「画面項目」に「お客さま氏名」を記録する。例えば、「画面項目」に記録する画面項目の抽出は<TD>や</TD>を検索してその間に記録されているテキスト（本例、お客さま氏名）を抽出して記録する。
【００６６】
次に、図９に示す行９１の場合であれば、画面・変数対応解析部２４は、図８のカート内容．ｊｓｐの破線範囲８２の<TD>お客さま氏名</TD>に続く<TD><jsp:getProperty name="user" property="name"></TD>を検出する。そして、「画面項目」に対応付けて「変数」に「ＵｓｅｒＢｅａｎ．ｎａｍｅ」を記録する。例えば、「変数」に記録する変数の抽出は「画面項目」に対応する<TD>や</TD>の次の<TD>や</TD>を検索してその間に記録されているテキスト内容を抽出し、テキスト内容から変数を抽出して記録する。
【００６７】
図１０は、監視変数候補抽出部２５の動作の一例を示すフロー図である。
ステップＳ１０１では、監視変数候補抽出部２５が画面・変数対応解析部２４の結果（画面・変数対応テーブル）および画面遷移情報を読み込む。画面遷移情報は、図４、図５に示したように、ある画面（ウェブページ）がボタン押下等のアクションによってどの画面に遷移するかを示す情報である。画面遷移情報は、例えば、図１１に示すように、テキストファイルにＸＭＬ形式で記述されたものでもよい。ただし、画面遷移情報は必須ではない。
【００６８】
ステップＳ１０２では、監視変数候補抽出部２５への入力として、画面遷移情報が入力されたかを判定する。入力されていない場合（Ｎｏ）の場合はステップＳ１０３に移行し、入力されている場合（Ｙｅｓ）はステップＳ１０４に移行する。
【００６９】
ステップＳ１０３では、監視変数候補抽出部２５が画面・変数対応解析部２４の解析結果から、複数の画面に共有して利用される変数を抽出して監視変数候補テーブルに記録する。監視変数候補テーブルは、例えば、図４のウェブアプリケーションにおいて、図９の画面・変数対応解析部２４の結果が得られた場合、図１２に示すように、カート内容画面４２と購入内容画面４３で共有されている変数を監視変数候補として記録する。図１２の例では、抽出された変数(監視変数候補)として、ＵｓｅｒＢｅａｎ．ｎａｍｅ、ＣａｒｔＢｅａｎ．ｉｔｅｍｓ［］．ｎａｍｅ・・・などが抽出され「変数」に対応する箇所に記録される。なお、図１２例のでは、「変数」を「ＪａｖａＢｅａｎ」と「属性」に分けて記録しているが必ずしも分けなくてもよい。また、図１２の画面項目のリストは変数に対応する画面項目が記録されている。
【００７０】
ステップＳ１０４では、監視変数候補抽出部２５が入力された画面遷移情報を解析して、画面遷移内に自画面遷移があるか判定する。自画面遷移が検出された場合（Ｙｅｓ）はステップＳＳ１０６に移行し、自画面遷移が検出されない場合（Ｎｏ）はステップＳＳ１０５に移行する。自画面遷移とは、ある画面においてボタン押下などの操作をした後、元の画面と同じ画面が表示される遷移である。自画面遷移の検出は、監視変数候補抽出部２５が上記と同様<action path=を検出し、<action path=に続くテキストを解析して画面を抽出し、同じ画面が連続していることを認識する。図４のウェブアプリケーション例では自画面遷移が無いのでステップＳ１０３に移行し、ステップＳ１０３の処理が実行され図１３の表の上５行１３１が抽出される。
【００７１】
ステップＳ１０５では、監視変数候補抽出部２５が入力された画面遷移情報を解析して、画面遷移において連続する画面の遷移前後画面だけで利用される変数を抽出する。
図１３は、図４または図１１のウェブアプリケーションを例とした場合の、監視変数候補抽出部２５が監視変数候補テーブルから連続する画面の遷移後画面だけで利用される変数を抽出した結果である。連続する画面の検出は、図１１の場合であれば、画面遷移情報の<action path="/cart" type="xxx.CartAction" name="カート内容">、<action path="/purchase" type="xxx. PurchaseAction" name="購入内容">などの<action path=を検出する。その後、監視変数候補抽出部２５は<action path=に続くテキストを解析して「カート内容」「購入内容」などを抽出し、カート内容画面４２と購入内容画面４３が連続していることを認識する。すなわち、ステップＳ１０５の処理では、画面遷移情報を参照することにより連続する画面を認識できるため、ステップＳ１０３のように複数の画面で共有している変数について処理しないので計算量を削減することができる。
【００７２】
図１３の例では、カート内容画面から購入内容画面への遷移において、ＣａｒｔＢｅａｎ．ｔｏｔａｌＰｒｉｃｅ、ＣａｒｔＢｅａｎ．ｔｏｔａｌＤｉｓｃｏｕｎｔ、Ｃａｒｔ．ｐａｙｍｅｎｔが、遷移前後の購入内容画面だけで利用されている。よって、図１３の表の下３行１３２に示すように、これらの変数が抽出される。なお、ＣａｒｔＢｅａｎ．ｔｏｔａｌＰｒｉｃｅは「正価合計（円）」、ＣａｒｔＢｅａｎ．ｔｏｔａｌＤｉｓｃｏｕｎｔは「割引合計（円）」、ＣａｒｔＢｅａｎ．ｐａｙｍｅｎｔは「お支払い（円）」を示している。なお、連続する画面の遷移前後画面だけで利用される変数は、監視変数候補テーブルにフラグなどを付して記録するか、記録部３などのメモリに監視変数候補テーブルとは別に記録してもよい。
【００７３】
ステップＳ１０６では、監視変数候補抽出部２５が自画面遷移する画面に関連する変数を抽出する。図５のウェブアプリケーションの例は、購入内容画面５２において「合計計算」ボタンを押下すると、正価合計、割引合計、お支払いの金額が計算されて、同じ購入内容画面５２に表示される。よって、自画面遷移する画面に関連する変数(連続する画面で共通の変数）は、図５の「購入内容」で用いる全ての変数が抽出される。
【００７４】
図１４は、図５のウェブアプリケーションの自画面遷移を例とした場合の、監視変数候補抽出部２５の出力（画面に関連する変数）である。なお、画面に関連する変数は、監視変数候補テーブルにフラグなどを付して記録するか、記録部３などのメモリに監視変数候補テーブルとは別に記録してもよい。また、図１４の画面項目のリストには変数(監視変数候補)に対応した画面項目のリストが記録される。すなわち、ステップＳ１０６の処理では、画面遷移情報を参照することにより自画面遷移を認識できるため、ステップＳ１０３のように複数の画面で共有している変数について処理しないので、計算量を削減することができる。
【００７５】
ステップＳ１０７では、監視変数候補抽出部２５が監視変数候補テーブルの変数を監視変数設定部２７に出力する。
図１５は、画面遷移関連プロパティ抽出部２６の動作の一例を示すフロー図である。
【００７６】
ステップＳ１５１では、画面遷移関連プロパティ抽出部２６がプロパティ保持部２３の保持する複数のプロパティから順にプロパティを選択する。図１６は、図４で示したウェブアプリケーションのプロパティの例であり、「Ｎｏ」「プロパティ記述」を有する行を記録する。「Ｎｏ」にはプロパティを選択した順に番号が割り振られ、「プロパティ記述」に選択したプロパティ記述が記録されている。
【００７７】
本表記において、@XXX_Invoke（例えば図１６の「１」に記載されている@purchase_Invokeなど）は、画面上のXXXボタン押下の操作が実行された時点を表す。これらの時点は、ウェブアプリケーションの特定の時点を指定できる。例えば、((UserBean.name != "") AND (UserBean.memberType != ""))@purchase_Invokeは、purchaseボタン（“カート内容”画面の“購入”ボタン）が押された時点で、 UserBean.name とUserBean.memberTypeの値は共に空文字列でないこを意味する。
【００７８】
図１６のプロパティについて説明する。
プロパティ「１」：
カート内容画面において「購入」ボタンが押下された時にお客さま氏名と会員種別が共に空文字列でなければ、「購入」ボタン押下後の購入内容画面とカート内容画面において、お客さま氏名と会員種別が等しい。
【００７９】
プロパティ「２」：
カート内容画面において「購入」ボタンが押下された時に商品の個数が０より大きければ、「購入」ボタン押下後の購入内容画面において、全ての商品に関して購入内容画面とカート内容画面で、商品名と単価と数量が等しい。
【００８０】
プロパティ「３」：
カート内容画面において「購入」ボタンが押下された時に商品の個数が０より大きく、かつ、会員種別が空文字列でなければ、購入内容画面の全ての商品に関して、割引は、商品の単価に割引率関数FunctionDiscountを乗算した値に等しい。
【００８１】
プロパティ「４」：
「カート内容」画面において「購入」ボタンが押下された時に商品の個数が０より大きければ、購入内容画面の正価合計の値は、正価合計関数FunctionTotalPriceの値に等しい。
【００８２】
プロパティ「５」：
カート内容画面において「購入」ボタンが押下された時に商品の個数が０より大きく、かつ、会員種別が空文字列でなければ、購入内容画面の割引合計の値は、割引合計関数FunctionTotalDiscountの値に等しい。
【００８３】
プロパティ「６」：
カート内容画面において「購入」ボタンが押下された時に商品の個数が０より大きければ、購入内容画面のお支払いの値は、正価合計関数FunctionTotalPriceの値から割引合計関数FunctionTotalDiscountの値を減算したものに等しい。
【００８４】
プロパティ「７」：
会員種別によって割引率を計算する関数FunctionDiscountの性質を記述したものである。
【００８５】
プロパティ「８」：
注文数量が在庫数を超過しないかチェックする関数FunctionZaikoCheckの性質を記述したものである。
【００８６】
プロパティ「９」：
正価合計を計算する関数FunctionTotalPriceの性質を記述したものである。
プロパティ「１０」：
割引合計を計算する関数FunctionTotalDiscountの性質を記述したものである。
【００８７】
ステップＳ１５２では、画面遷移関連プロパティ抽出部２６が未処理のプロパティを選択したかを判定し、未処理のプロパティを選択した場合（Ｙｅｓ）はステップＳ１５３に移行し、全てのプロパティを処理した場合（Ｎｏ）はステップＳ１５８に移行する。例えば、図１６の場合であればプロパティ「１」〜「１０」を全て処理した場合にはステップＳ１５８に移行する。
【００８８】
ステップＳ１５３では、画面遷移関連プロパティ抽出部２６がプロパティを構成する変数を抽出する。例えば、図１６のプロパティ「１」の場合であればプロパティ「１」に対応する「プロパティ記述」からＵｓｅｒＢｅａｎ．ｎａｍｅ、ＵｓｅｒＢｅａｎ．ｍｅｍｂｅｒＴｙｐｅなどの変数だけを抽出して記録する。
【００８９】
ステップＳ１５４では、画面遷移関連プロパティ抽出部２６が抽出した変数を順に選択する。
ステップＳ１５５では、画面遷移関連プロパティ抽出部２６が未処理の変数を選択したか否かを判定し、未処理の変数を選択した場合（Ｙｅｓ）はステップＳ１５６に移行し、全ての変数を処理した場合（Ｎｏ）はステップＳ１５１に移行する。例えば、図１６のプロパティ「１」の場合であれば変数ＵｓｅｒＢｅａｎ．ｎａｍｅ、ＵｓｅｒＢｅａｎ．ｍｅｍｂｅｒＴｙｐｅを全て処理した場合にはステップＳ１５１に移行する。
【００９０】
ステップＳ１５６では、画面遷移関連プロパティ抽出部２６が選択した変数が画面・変数対応解析部２４の結果に含まれるか否かを判定し、含まれていればステップＳ１５７に移行し、含まれていなければステップＳ１５４に移行する。例えば、図１６の場合であれば変数ＵｓｅｒＢｅａｎ．ｎａｍｅが図９に示した画面・変数対応テーブルの「変数」に記録されているかを判定し、画面・変数対応テーブルの「変数」にＵｓｅｒＢｅａｎ．ｎａｍｅがあるのでステップＳ１５７に移行する。
【００９１】
ステップＳ１５７では、画面遷移関連プロパティ抽出部２６が現在選択しているプロパティを抽出してステップＳ１５１に移行する。
ステップＳ１５８では、画面遷移関連プロパティ抽出部２６が抽出した画面遷移関連プロパティを監視変数設定部２７に出力する。
【００９２】
図１７は、画面遷移関連プロパティ抽出部２６の結果の例（画面遷移関連プロパティ）である。図１６のプロパティのうち、画面・変数対応解析部２４の結果（画面・変数対応テーブル）である変数を含まない、プロパティ「７」〜「１０」が削除され、プロパティ「１」〜「６」が抽出されている。
【００９３】
図１８は、監視変数設定部２７の動作の一例を示すフロー図である。
ステップＳ１８１では、監視変数設定部２７が監視変数候補抽出部２５の結果（監視変数候補テーブルの変数）と画面遷移関連プロパティ抽出部２６の結果（プロパティ）を読み込む。
【００９４】
ステップＳ１８２では、監視変数設定部２７が監視変数候補抽出部２５の結果から変数を順に選択する。例えば、監視変数候補テーブルの変数を取得する。
ステップＳ１８３では、監視変数設定部２７が未処理の変数を選択したか否かを判定して、選択できた場合（Ｙｅｓ）でればステップＳ１８４に移行し、全ての変数を処理している場合（Ｎｏ）であればステップＳ１８８に移行する。例えば、ステップＳ１８２で選択した変数を記録しておき、記録されている変数に今回取得した変数があるかを検索し、今回取得した変数が既に記録されている変数と一致するか否かを判定する。
【００９５】
ステップＳ１８４では、監視変数設定部２７が画面遷移関連プロパティ抽出部２６の結果のプロパティを順に選択する。例えば、画面遷移関連プロパティ抽出部２６から出力される画面遷移関連プロパティを取得する。
【００９６】
ステップＳ１８５では、監視変数設定部２７が未処理のプロパティを選択したか否かを判定して、選択できた場合（Ｙｅｓ）でればステップＳ１８６に移行し、全てのプロパティを処理している場合（Ｎｏ）であればステップＳ１８２に移行する。例えば、ステップＳ１８４で選択したプロパティを記録しておき、記録されているプロパティに今回取得したプロパティがあるかを検索し、今回取得したプロパティが既に記録されているプロパティと一致するか否かを判定する。
【００９７】
ステップＳ１８６では監視変数設定部２７が、当該変数が当該プロパティで利用されているか否かを判定し、利用されている場合（Ｙｅｓ）であればステップＳ１８７に移行し、利用されていない場合（Ｎｏ）であればステップＳ１８４に移行する。すなわち、ステップＳ１８２で取得した変数が、ステップＳ１８４で取得したプロパティに記述されているかを判定する。
【００９８】
ステップＳ１８７では、監視変数設定部２７が当該変数を除外変数として記録する。つまり、ステップＳ１８４で取得したプロパティに、ステップＳ１８２で取得した変数が記述されているので、この変数を除外変数として記録する。
【００９９】
ステップＳ１８８では、監視変数設定部２７が監視変数候補抽出部２５の結果から除外変数を除いた変数（監視変数）を結果としてプロパティ設定漏れ監視部２８に出力する。
図１６のプロパティの例において、プロパティ「３」とプロパティ「５」、およびプロパティ「２」の一部に設定漏れがあったとする。画面遷移関連プロパティ抽出部２６により抽出される画面遷移関連プロパティは、図１９のようにプロパティ「３」「５」に対応する行を除外し（図では×を記載した）、プロパティ「２」に対応する行の一部を削除（取り消し線）する。図２０は、画面遷移関連プロパティ抽出部２６の結果が図１９であった場合の、監視変数設定部２７の結果である。つまり、図１３に示した監視変数候補抽出部２５の結果に列挙された変数のうち、CartBean.items[].unitDiscountはプロパティ「３」だけで利用され、CartBean.totalDiscountはプロパティ「５」だけで利用され、CartBean.items[].unitpriceはプロパティ「３」およびプロパティ「２」の削除部分だけで利用される。よって、上記の想定した場合、図２０に示すように、CartBean.items[].unitprice 、CartBean.items[].unitDiscount、CartBean.totalDiscountが監視変数設定部２７の結果となる。
【０１００】
図２１は、プロパティ設定漏れ監視部２８の動作の一例を示すフロー図である。
ステップＳ２１１では、モデル検査実行部２１が検査対象プログラムのシミュレーション実行を開始する
ステップＳ２１２では、モデル検査実行部２１が検査対象プログラムの全ての状態を検査したか否かを判定する。全ての状態を検査した場合（Ｙｅｓ）であればステップＳ２１８に移行し、操作待ちの状態でない場合（Ｎｏ）であればステップＳ２１３に移行する。なお、ここで全ての状態を検査したか否かは既存の技術により行っている。
【０１０１】
ステップＳ２１３では、モデル検査実行部２１がシミュレーション実行によって検査対象プログラムを状態遷移させる。
ステップＳ２１４ではモデル検査実行部２１が、遷移状態が画面での操作待ちの状態か否かを判定する。操作待ちの状態の場合（Ｙｅｓ）であればステップＳ２１５に移行し、全ての状態を検査していない場合（Ｎｏ）であればステップＳ２１２に移行する。
【０１０２】
ステップＳ２１５では、プロパティ設定漏れ監視部２８が監視変数の値を取得し、画面と対応付けて記録する。
ステップＳ２１６ではプロパティ設定漏れ監視部２８が、監視変数の値が画面遷移の前後で違いがあるか否かを判定する。違いがある場合（Ｙｅｓ）であればステップＳ２１７に移行し、違いがない場合（Ｎｏ）であればステップＳ２１２に移行する。
【０１０３】
ステップＳ２１７ではプロパティ設定漏れ監視部２８が、値が相違であった監視変数、遷移前画面、遷移後画面などを記録する。
ステップＳ２１８ではプロパティ設定漏れ監視部２８が、値が相違であった監視変数、遷移前画面、遷移後画面などをプロパティ設定漏れ出力部２９に出力する
図４のウェブアプリケーションで、図１６のようなプロパティを設定してモデル検査を実行すべきとき、図１９に示したようなプロパティ設定漏れがあった場合のプロパティ設定漏れ監視部２８の動作を説明する。
【０１０４】
プロパティ設定漏れ監視部２８が監視する監視変数は、図２０に示した変数である。図４のウェブアプリケーションでのシミュレーション実行において、カート内容画面で商品を追加され、「購入」ボタン４８が押下され、購入内容画面４３が表示された状態で、監視変数の値の取得、および比較が実行される。
【０１０５】
図２２は、監視変数設定部２７において、カート内容画面４２と購入内容画面４３の間で、監視変数の値を示したものである。画面遷移の前後で監視変数の値を比較することにより、CartBean.items[].unitDiscountとCartBean.totalDiscountの二つの変数に関して、プロパティ設定漏れの可能性を検出する。
【０１０６】
プロパティ設定漏れ出力部２９は、プロパティ設定漏れ監視部２８から値が相違であった監視変数、遷移前画面、遷移後画面などを取得して入出力装置４の画面に表示する。
図２３、２４はプロパティ設定漏れ出力部２９の出力例である。図２３の表では、プロパティ設定漏れの可能性がある「監視変数」「遷移前画面」の「画面名」と「項目名」と「値」、「遷移後画面」の「画面名」と「項目名」と「値」を示す。ユーザは、図２３の表を参考にして、どのようなプロパティが設定漏れとなったかを検討することができる。
【０１０７】
図２４の出力例では、プロパティ設定漏れの可能性がある監視変数に関して、「表示」ボタン２３１を押すと、遷移前画面（４２）と遷移後画面（４３）の画面イメージが表示され、さらに、対応する画面項目フィールドに色（斜め線範囲）を着色するような情報を提供することもできる。これらの情報により、ユーザによるプロパティ設定漏れ確認作業を支援することができる。
【０１０８】
上記のように検査対象プログラムをシミュレーション実行して、状態ごとに前記プロパティが成立するかを検査するモデル検査に、プロパティ設定漏れを検出する機能を設けることにより、監視する変数の個数を削減することができる。
【０１０９】
プロパティ設定漏れを検出は、まず検査対象プログラムをシミュレーション実行したとき表示される画面と画面に表示されるデータの入出力に関する画面項目と検査対象プログラムに記述されている変数とを対応付ける。次に、対応付けられた変数から画面遷移において複数の状態で共有して利用される変数を抽出する。抽出した変数から、プロパティから画面遷移に関係するプロパティに使用されている変数を除外した変数を監視変数として設定し、各状態において監視変数だけを監視し、画面遷移の前後で監視変数の値を比較する。比較した結果、前後の画面で値が相違する監視変数を検出し、検出されたプロパティ設定漏れの可能性のある変数として情報を出力することができる。
【０１１０】
また、従来技術ではハードウェア記述言語やプログラム等のソースファイルから、全ての変数と条件式を抽出し、シミュレーション実行時に、抽出した全ての変数や条件を監視対象とする必要がある。また、全ての状態遷移において変数や条件の値を計算する必要があるため、計算コストが大きく、業務システムのような実システムにおいては実施が困難である。
【０１１１】
しかし、監視対象をプログラム変数全体から監視変数に限定することにより、従来の技術より計算コストを減少させることができる（監視変数の個数／全変数の個数）。また、監視対象をプログラム変数全体から監視変数に限定することにより、計算コストを減少させることにより実システムでのプロパティ漏れ検出を実行可能とする。
【０１１２】
（実施例２）
プロパティ設定漏れ監視部２８のもう一つの実施例は、監視変数設定部で設定された変数に対して、該変数は画面遷移時に不変であるとした監視用の特別なプロパティを作成して、プロパティ保持部２３に追加するものである。なお、該プロパティは記録部３のプロパティ８に追加してもよい。
【０１１３】
追加される監視用プロパティは、監視変数設定部２７の結果で、複数画面に関連する監視変数についてのプロパティである。図２０の場合は、CartBean.items[].unitPriceとCartBean.items[].unitDiscountが複数画面に関連する変数である。CartBean.totalDiscountは、一つの画面だけで使用されるので、監視用プロパティは作成されない。
【０１１４】
図２５は、プロパティ設定漏れ監視部２８の他の実施例において、作成される監視用プロパティの例である。監視用プロパティは、設定済みの他のプロパティと同様に、シミュレーション実行時の各状態で評価される。監視用プロパティが不成立となったとき、該監視用プロパティを作成するために用いた監視変数に関して、プロパティ設定漏れの可能性が検出される。
【０１１５】
図２６は、監視用プロパティを設定するフロー図である。
ステップＳ２６１では、監視変数設定部２７が監視変数候補抽出部２５の結果と画面遷移関連プロパティ抽出部の結果を読み込む。
【０１１６】
ステップＳ２６２では、監視変数設定部２７が監視変数候補抽出部２５の結果から変数を順に選択する。
ステップＳ２６３では、監視変数設定部２７が未処理の変数を選択できたかを判定し、未処理の変数を選択した場合（Ｙｅｓ）はステップＳ２６４に移行し、未処理の変数がない場合（Ｎｏ）はステップＳ２６８に移行する。
【０１１７】
ステップＳ２６４では、監視変数設定部２７が画面遷移関連プロパティ抽出部２６の結果のプロパティを順に選択する。
ステップＳ２６５では、監視変数設定部２７が未処理のプロパティを選択できたか判定し、未処理のプロパティを選択した場合（Ｙｅｓ）はステップＳ２６６に移行し、未処理の変数がない場合（Ｎｏ）はステップＳ２６２に移行する。
【０１１８】
ステップＳ２６６では監視変数設定部２７が、当該変数が当該プロパティで利用されているか判定し、利用されている場合（Ｙｅｓ）はステップＳ２６７に移行し、利用されていない場合（Ｎｏ）はステップＳ２６２に移行する。
【０１１９】
ステップＳ２６７では、監視変数設定部２７が当該変数を除外変数とする。
ステップＳ２６８では、監視変数設定部２７が監視変数候補抽出部２５の結果から除外変数を除いた変数（監視変数）を抽出する。
【０１２０】
上記ステップＳ２６１〜Ｓ２６８の処理は、図１８のステップＳ１８１〜Ｓ１８８の処理と同じである。
ステップＳ２６９ではプロパティ設定漏れ監視部２８が、ステップＳ２６８で抽出された監視変数を用いて、監視変数の値が画面遷移時に等しいと仮定した監視用プロパティを作成する。
【０１２１】
ステップＳ２６１０では、プロパティ設定漏れ監視部２８が作成した監視用プロパティをプロパティ保持部２３に追加する。このとき、監視用プロパティは検査用プロパティと区別できるようにしておく。
【０１２２】
図２７は、監視用プロパティによるプロパティ設定漏れ監視の一例を示すフロー図である。
ステップＳ２７１〜Ｓ２７４は図２１のステップＳ２１１〜Ｓ２１４と同じ処理を行う。
【０１２３】
ステップＳ２７１では、モデル検査実行部２１が検査対象プログラムのシミュレーション実行を開始する。
ステップＳ２７２では、モデル検査実行部２１が検査対象プログラムの全ての状態を検査したか否かを判定する。全ての状態を検査した場合（Ｙｅｓ）であればステップＳ２１８に移行し、全ての状態を検査していない場合（Ｎｏ）であればステップＳ２７３に移行する。なお、ここで全ての状態を検査したか否かは既存の技術により行っている。
【０１２４】
ステップＳ２７３では、モデル検査実行部２１がシミュレーション実行によって検査対象プログラムを状態遷移させる。
ステップＳ２７４ではモデル検査実行部２１が、遷移状態が画面での操作待ちの状態か否かを判定する。操作待ちの状態の場合（Ｙｅｓ）であればステップＳ２７５に移行し、操作待ちでない場合（Ｎｏ）であればステップＳ２７２に移行する。遷移状態が画面での操作待ちの状態とは、図４、５に示した画面項目などにユーザが入力を完了するまでの状態である。
【０１２５】
ステップＳ２７５では、モデル検査実行部２１が検査用プロパティと監視用プロパティが成立するかをチェックする。
ステップＳ２７６ではプロパティ設定漏れ監視部２８が、監視用プロパティが不成立であったか否かを判定する。監視用プロパティが不成立の場合（Ｙｅｓ）であればステップＳ２７７に移行し、監視用プロパティが成立の場合（Ｎｏ）であればステップＳ２７２に移行する。例えば、プロパティ設定漏れ監視部２８はモデル検査実行部２１に対して、監視用プロパティのチェック結果を通知するように指示をする。その指示を受信したモデル検査実行部２１は、プロパティ設定漏れ監視部２８に監視用プロパティのチェック結果を送信する。その後、プロパティ設定漏れ監視部２８は監視用プロパティのチェック結果を参照して判定をする。
【０１２６】
ステップＳ２７７ではプロパティ設定漏れ監視部２８が、監視用プロパティが不成立の場合の変数値、遷移前画面、遷移後画面などを記録する。
ステップＳ２７８ではプロパティ設定漏れ監視部２８が、監視用プロパティが不成立の場合の変数値、遷移前画面、遷移後画面などを出力する。
【０１２７】
上記のように検査対象プログラムをシミュレーション実行して、状態ごとに前記プロパティが成立するかを検査するモデル検査に、プロパティ設定漏れを検出する機能を設けることにより、監視する変数の個数を削減することができる。
【０１２８】
プロパティ設定漏れ検出では、まず検査対象プログラムをシミュレーション実行したとき表示される画面と画面に表示されるデータの入出力に関する画面項目と検査対象プログラムに記述されている変数とを対応付ける。次に、対応付けられた変数から画面遷移において複数の場面で共有して利用される変数を抽出する。抽出した変数から、プロパティから画面遷移に関係するプロパティに使用されている変数を除外した変数を監視変数として設定し、各画面において監視変数だけを監視し、画面遷移の前後で監視変数の値を比較する。比較した結果、前後の画面で値が相違する監視変数を検出し、検出されたプロパティ設定漏れの可能性のある変数として情報を出力することができる。
【０１２９】
従来技術ではハードウェア記述言語やプログラム等のソースファイルから、全ての変数と条件式を抽出し、シミュレーション実行時に、抽出した全ての変数や条件を監視対象とする必要がある。また、全ての状態遷移において変数や条件の値を計算する必要があるため、計算コストが大きく、業務システムのような実システムにおいては実施が困難である。
【０１３０】
しかし、監視対象をプログラム変数全体から監視変数に限定することにより、従来の技術より計算コストを減少させることができる（監視変数の個数／全変数の個数）。また、監視対象をプログラム変数全体から監視変数に限定することにより、計算コストを減少させることにより実システムでのプロパティ漏れ検出を実行可能とする。
【０１３１】
また、監視用プロパティを用いてシミュレーション実行して状態ごとに監視用プロパティが成立しているかを検査した結果を取得し、監視用プロパティが不成立であるとき、該監視用プロパティを作成するために用いた監視変数に関して、プロパティ漏れの可能性が検出できる。
【０１３２】
（本実施例がコンピュータプログラムとして実現される場合の構成）
図２８は、上記本発明の実施形態の装置を実現できるコンピュータのハードウェア構成の一例を示す図である。
コンピュータのハードウェア２８０は、ＣＰＵ２８１、記録部２８２（ＲＯＭ、ＲＡＭ、ハードディスクドライブなど）、記録媒体読取装置２８３、入出力インタフェース２８４（入出力Ｉ／Ｆ）、通信インタフェース２８５（通信Ｉ／Ｆ）などを備えている。また、上記各構成部はバス２８６によってそれぞれ接続されている。
【０１３３】
ＣＰＵ２８１は、記録部２８２に格納されている上記説明したモデル検査実行処理、画面・変数対応解析処理、監視変数候補抽出処理、画面遷移関連プロパティ抽出処理、監視変数設定処理、プロパティ設定漏れ監視処理、プロパティ設定漏れ出力処理などを実行する。
【０１３４】
記録部２８２には、ＣＰＵ２８１が実行するプログラムやデータが記録されている。また、ワークエリアなどとして使用される。
記録媒体読取装置２８３は、ＣＰＵ２８１の制御にしたがって記録媒体２８３ａに対するデータのリード／ライトを制御する。そして、記録媒体２８３ａ、記録媒体読取装置２８３の制御で書き込まれたデータを記憶したり、記録媒体２８３ａに記憶されたデータを読み取らせたりする。また、着脱可能な記録媒体２８３ａは、コンピュータで読み取り可能な記録媒体として、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記録装置には、ハードディスク装置（ＨＤＤ）などがある。光ディスクには、ＤＶＤ(Digital Versatile Disc)、ＤＶＤ−ＲＡＭ(Random Access Memory)、ＣＤ−ＲＯＭ(Compact Disc Read Only Memory)、ＣＤ−Ｒ(Recordable)／ＲＷ(ReWritable)などがある。光磁気記録媒体には、ＭＯ(Magneto-Optical disk)などがある。
【０１３５】
入出力インタフェース２８４には、入出力装置２８４ａ（図１の入出力装置４、マウス、キーボード、ディスプレイなど）が接続され、ユーザが入力した情報を受信し、バス２８６を介してＣＰＵ２８１に送信する。また、ＣＰＵ２８１からの命令に従ってディスプレイの画面上に操作情報などを表示する。
【０１３６】
通信インタフェース２８５は、必要に応じ、他のコンピュータとの間のＬＡＮ接続やインターネット接続や無線接続のためのインタフェースである。また、他の装置に接続され、外部装置からのデータの入出力を制御する。
【０１３７】
このようなハードウェア構成を有するコンピュータを１台または２台以上用いることによって、上記説明した各種処理機能（実施例で説明した処理（フローチャートなど））が実現される。その場合システムが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体２８３ａに記録しておくことができる。
【０１３８】
プログラムを流通させる場合には、例えば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭなどの可搬型記録媒体が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【０１３９】
プログラムを実行するコンピュータは、例えば、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、サーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムに従った処理を実行することもできる。
【０１４０】
また、本発明は、上記実施の形態に限定されるものでなく、本発明の要旨を逸脱しない範囲内で種々の改良、変更が可能である。
【符号の説明】
【０１４１】
１  装置
２  制御部
３  記録部
４  入出力装置
５  モデル検査部
６  プロパティ設定漏れ検出部
７  検査対象プログラム
８  プロパティ
２１  モデル検査実行部
２２  検査対象プログラム保持部
２３  プロパティ保持部
２４  画面・変数対応解析部
２５  監視変数候補抽出部
２６  画面遷移関連プロパティ抽出部
２７  監視変数設定部
２８  プロパティ設定漏れ監視部
２９  プロパティ設定漏れ出力部
４１  商品検索画面
４２  カート内容画面
４３  購入内容画面
４４  完了画面
４６  「商品の追加」ボタン
４７  「商品検索」ボタン
４８  「購入」ボタン
４９  「カートに戻る」ボタン
４１０  「購入実施」ボタン
５１  商品検索画面
５２  購入内容画面
５３  完了画面
５４  「商品の追加」ボタン
５５  「商品検索」ボタン
５６  「購入実施」ボタン
５７  「合計計算」ボタン
２３１  「表示」ボタン
２８０  ハードウェア
２８２  記録部
２８３  記録媒体読取装置
２８３ａ  記録媒体
２８４  入出力インタフェース
２８４ａ  入出力装置
２８５  通信インタフェース
２８６  バス
【図１】
2011003109.tif 000003
【図２】
2011003109.tif 000004
【図３】
2011003109.tif 000005
【図４】
2011003109.tif 000006
【図５】
2011003109.tif 000007
【図６】
2011003109.tif 000008
【図７】
2011003109.tif 000009
【図８】
2011003109.tif 000010
【図９】
2011003109.tif 000011
【図１０】
2011003109.tif 000012
【図１１】
2011003109.tif 000013
【図１２】
2011003109.tif 000014
【図１３】
2011003109.tif 000015
【図１４】
2011003109.tif 000016
【図１５】
2011003109.tif 000017
【図１６】
2011003109.tif 000018
【図１７】
2011003109.tif 000019
【図１８】
2011003109.tif 000020
【図１９】
2011003109.tif 000021
【図２０】
2011003109.tif 000022
【図２１】
2011003109.tif 000023
【図２２】
2011003109.tif 000024
【図２３】
2011003109.tif 000025
【図２４】
2011003109.tif 000026
【図２５】
2011003109.tif 000027
【図２６】
2011003109.tif 000028
【図２７】
2011003109.tif 000029
【図２８】
2011003109.tif 000030