(57)【要約】【課題】ソフトウェアアプリケーションにおける欠陥検出のための設定可能なウェブサービスシステム等を提供する。【解決手段】設定可能なウェブサービスアーキテクチャにより異種言語から成るソフトウェアアプリケーションにおける１又はそれ以上の欠陥を検出する欠陥検出段階を有する方法が提供される。この欠陥検出段階は、ソフトウェアアプリケーションと関連する使用状況を捕らえ、その有効性を確認する段階と、モデルチェックのための特性モニタの自動起動を与える段階と、診断のためにソフトウェアアプリケーションにおける１又はそれ以上の欠陥を視覚化する段階とを有する。欠陥検出段階は、異種ソフトウェアアプリケーションを同種のアプリケーションに変形する段階を更に有する。具体的には、欠陥検出段階は、ソフトウェアアプリケーションと関連するプレゼンテーション層に自動テスト生成を与える段階を更に有する。【選択図】図２
2009087352.tif 000002
【特許請求の範囲】
【請求項１】
設定可能なウェブサービスアーキテクチャにより異種言語から成るソフトウェアアプリケーションにおける１又はそれ以上の欠陥を検出する欠陥検出段階を有し、
前記欠陥検出段階は、
前記ソフトウェアアプリケーションと関連する使用状況を捕らえ、その有効性を確認する段階と、
モデルチェックのための特性モニタの自動起動を与える段階と、
診断のために前記ソフトウェアアプリケーションにおける１又はそれ以上の欠陥を視覚化する段階とを有する、方法。
【請求項２】
前記欠陥検出段階は、異種ソフトウェアアプリケーションを同種のアプリケーションに変形する段階を更に有する、請求項１記載の方法。
【請求項３】
前記欠陥検出段階は、前記ソフトウェアアプリケーションと関連するプレゼンテーション層に自動テスト生成を与える段階を更に有する、請求項１記載の方法。
【請求項４】
前記ソフトウェアアプリケーションと関連する設定は、単純特性ファイルである、請求項１記載の方法。
【請求項５】
前記欠陥検出段階は、ユーザの行動をシミュレーションする段階を更に有する、請求項１記載の方法。
【請求項６】
前記欠陥検出段階は、使用状況又はシナリオからビジネスロジックを試験するドライバを生成する段階を更に有する、請求項１記載の方法。
【請求項７】
前記欠陥検出段階は、空きの又はユーザ供給のスタブによってデータベースを置き換える段階を更に有する、請求項１記載の方法。
【請求項８】
前記欠陥検出段階は、前記ソフトウェアアプリケーションのためのビジネスロジックを検証する段階を更に有する、請求項１記載の方法。
【請求項９】
ソフトウェアアプリケーションの領域に基づき、特性又は必要条件を少数のカテゴリに分類する段階と、
Ｊａｖａアプリケーションのソースコードを走査する段階と、
前記特性又は必要条件を特定する場合にエンドユーザによって選択され得るイベントの組を生成する段階と、
満足される必要がある選択された組の必要条件又は特性を１又はそれ以上のカテゴリと適合させる段階と、
インスタンス化された特性カテゴリに対応するモニタ又は特性チェッカーを、前記モニタ又は前記特性チェッカーへの前記カテゴリの適合完了後に起動する段階と
を有する方法。
【請求項１０】
前記分類段階は、前記ソフトウェアアプリケーションの領域ごとに先験的に行われる、請求項９記載の方法。
【請求項１１】
コンピュータ媒体に組み込まれるロジックであって、
設定可能なウェブサービスアーキテクチャにより異種言語から成るソフトウェアアプリケーションにおける１又はそれ以上の欠陥を検出するよう動作し、
前記欠陥検出動作は、
前記ソフトウェアアプリケーションと関連する使用状況を捕らえ、その有効性を確認する段階と、
モデルチェックのための特性モニタの自動起動を与える段階と、
診断のために前記ソフトウェアアプリケーションにおける１又はそれ以上の欠陥を視覚化する段階とを有する、ロジック。
【請求項１２】
前記欠陥検出動作は、異種ソフトウェアアプリケーションを同種のアプリケーションに変形する段階を更に有する、請求項１１記載のロジック。
【請求項１３】
前記欠陥検出動作は、前記ソフトウェアアプリケーションと関連するプレゼンテーション層に自動テスト生成を与える段階を更に有する、請求項１１記載のロジック。
【請求項１４】
前記ソフトウェアアプリケーションと関連する設定は、単純特性ファイルである、請求項１１記載のロジック。
【請求項１５】
前記欠陥検出動作は、ユーザの行動をシミュレーションする段階を更に有する、請求項１１記載のロジック。
【請求項１６】
前記欠陥検出動作は、使用状況又はシナリオからビジネスロジックを試験するドライバを生成する段階を更に有する、請求項１１記載のロジック。
【請求項１７】
前記欠陥検出動作は、空きの又はユーザ供給のスタブによってデータベースを置き換える段階を更に有する、請求項１１記載のロジック。
【請求項１８】
前記欠陥検出動作は、前記ソフトウェアアプリケーションのためのビジネスロジックを検証する段階を更に有する、請求項１１記載のロジック。
【請求項１９】
ドライバは、テスタ供給される使用状況から、検証されるビジネスロジックを試験するよう自動的に生成され、これによって、特性は、モデルチェックによって自動的に検証される、請求項１１記載のロジック。
【請求項２０】
前記ソフトウェアアプリケーションは、電子商取引アプリケーションに関する、請求項１１記載のロジック。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、概して、ウェブサービスの分野、より具体的には、ソフトウェアアプリケーションにおける欠陥検出のための設定可能なウェブサービスシステム及び方法に関する。
【背景技術】
【０００２】
ウェブアプリケーションは、今日のプロセッシング界の至る所にある。Ｊａｖａ（登録商標）は、多くのソフトウェアアプリケーションのバックボーン（又は重要な部分）を実施するための大衆的な選択であるが、典型的なウェブアプリケーションは、ＨＴＭＬ、ＪａｖａＳｃｒｉｐｔ、ＰＨＰ、Ｐｅｒｌ、及びＭｙｓｑｌを含む、様々な言語及び技術を組み込んだ異種（heterogeneous）システムである。
【０００３】
試験技術は、難しいコーナーケースのバグを捕らえることができないことを含め、多くの点で不十分である。この問題は、ソフトウェアシステムの複雑性が増すにつれ、ますます面倒である。従って、形式的な検証（validation）技術は、特に、複雑なソフトウェアシステムが正当であると確認する場合に及び／又はシステムの安全性若しくはセキュリティの重要な側面を確認する場合に、必要とされる。形式的なソフトウェア検証技術に関して多くの研究がされており、最近では、それらの幾つかを、Ｊａｖａ（登録商標）に基づくシステムに適用することが研究されている。しかし、例えばウェブアプリケーションのような大きな異種システムのためのエンド・ツー・エンドの解決法はない。ポイントツールは、利用可能であろうとも、ウェブアプリケーションで適切に動作するには一般的過ぎる。それらの使用及び形式主義は、平均的なシステムエンジニアにとって理解するのが困難であり、更に、それらのアプリケーションは、十分には自動化されておらず、アドホックであるために容易に反復可能でない。すなわち、それほど標準化されていない。
【０００４】
従って、ウェブサービスにおけるそれらの重要な検証に関する問題を解決する能力は、興味深い課題を生み出す。全てのこのようなプロセッシング動作に関し、決定的に重要なのは、速度、正確性、及び自動化に関する課題である。
【発明の開示】
【発明が解決しようとする課題】
【０００５】
本発明は、従来の方法及びシステムに関連する欠点及び課題の少なくとも幾つかを実質的に取り除き又は軽減する、ソフトウェアアプリケーションにおける欠陥検出のための設定可能なウェブサービスシステム及び方法を提供することを目的とする。
【課題を解決するための手段】
【０００６】
本発明の具体的な実施形態に従って、設定可能なウェブサービスアーキテクチャにより異種言語から成るソフトウェアアプリケーションにおける１又はそれ以上の欠陥を検出する欠陥検出段階を有する方法が提供される。この欠陥検出段階は、前記ソフトウェアアプリケーションと関連する使用状況を捕らえ、その有効性を確認する段階と、モデルチェックのための特性モニタの自動起動を与える段階と、診断のために前記ソフトウェアアプリケーションにおける１又はそれ以上の欠陥を視覚化する段階とを更に有する。
【０００７】
前記欠陥検出段階は、異種ソフトウェアアプリケーションを同種の（homogeneous）アプリケーションに変形する段階を更に有することができる。より具体的な実施例では、前記欠陥検出段階は、前記ソフトウェアアプリケーションと関連するプレゼンテーション層に自動テスト生成を与える段階を更に有する。前記ソフトウェアアプリケーションと関連する設定は、単純特性ファイルでありうる。前記欠陥検出段階は、ユーザの行動をシミュレーションする段階と、使用状況又はシナリオからビジネスロジックを試験するドライバを生成する段階とを更に有する。
【０００８】
更なる他の実施例で、前記欠陥検出段階は、空きの又はユーザ供給のスタブによってデータベースを置き換える段階を有する。前記欠陥検出段階は、前記ソフトウェアアプリケーションのためのビジネスロジックを検証する段階を更に有する。
【０００９】
本発明の具体的な実施例に関する技術的効果には、（ソフトウェアアプリケーションの領域固有性に基づき）大きなソフトウェアコードベースの検証のために短時間のカスタマイズ及び更なる自動化を可能にすることがある。例えば、ウェブアプリケーションは、セキュリティ特性が検証されることを要する金融アプリケーションでありうる。加えて、設定は、このような検証の実行において最大の自動化を達成するためにカスタマイズされうる。設定は、特性ファイル（例えば、ＸＭＬ）を用いて特定され得る。
【００１０】
本発明は、また、エンタープライズ・ストレングス（enterprise-strength）のウェブアプリケーションを形式的に検証するためのエンド・ツー・エンドの解決法を提供することもできる。更に、それは、このようなアプリケーションの性質に上手く適した技術の適切な組の選択を提供する。それは、更に、このようなＪａｖａ（登録商標）アプリケーション類でツールセットの有効性を最大とするよう、ツールセットのカスタマイズをウェブアプリケーションへ提供することができる。例えば、これは、特性テンプレートの特定の選択及び組み立てと、シンボル実行における文字列処理ライブラリの使用とを含みうる。それは、また、単純な仕様言語において又は例えばＵＭＬのような視覚的な形式主義を用いて、必要条件の捕捉における柔軟性を提供する。
【００１１】
他の技術的効果は、以下の図面、記載及び特許請求の範囲から、いわゆる当業者には容易に理解され得る。更に、特定の効果が上で挙げられたが、様々な実施形態は、挙げられている効果の全て又は幾つかを含み、あるいはいずれも含まないことがある。
【発明の効果】
【００１２】
本発明の実施例により、従来の方法及びシステムに関連する欠点及び課題の少なくとも幾つかを実質的に取り除き又は軽減する、ソフトウェアアプリケーションにおける欠陥検出のための設定可能なウェブサービスシステム及び方法を提供することが可能となる。
【００１３】
他の技術的効果は、以下の図面、記載及び特許請求の範囲から当業者には容易に認識されるであろう。更に、具体的な利点が先に列挙されたが、様々な実施形態は、挙げられている利点の全て又は幾つかを含み、あるいは、それらを全く含まないこともある。
【発明を実施するための最良の形態】
【００１４】
本発明及びその効果の具体的な実施例に関するより完全な理解のために、ここで、添付の図面に関連した以下の記載が参照される。
【００１５】
図１は、どのように検証が典型的に実行されるかを表すシステム１０の例を表す略ブロック図である。図１は、条件付きコンポーネント１２と、ウェブアプリケーション１４と、これらの事項の両方に関連するデータセグメント１６を含む。検証は、通常は、ソースコード内でアサーションをマニュアル挿入することによって行われる。小さなモジュールは、マニュアル選択されるが、アプリケーションソースコード全体を扱う方法はない。従来の試験に伴う１つの問題は、マニュアル強制（manually-intensive）であり、従って、高価で、エラーを起こしやすく、且つ、貧しい／未知の機能範囲を提供することである。
【００１６】
図２は、本発明の一実施例に従う、ソフトウェアを検証するための設定可能なウェブサービスアーキテクチャを表す略ブロック図である。図２は、モデルチェック２０と、ウェブサービス２２と、ウェブサービス２４と、テストケース・コンポーネント２８と、欠陥／バグ報告コンポーネント３２と、欠陥の診断のための画像視覚化コンポーネント４０とを含む。集合的に、図２のこれらのコンポーネントは、ソフトウェアアプリケーションのモデルチェックを行う新たな方法を提供するよう協働する。アーキテクチャは試験を自動化し、所与の対象システムに高い機能範囲を提供する。ウェブアプリケーション１４は、異種結合のプログラム言語でありうる。
【００１７】
図２の実施例は、ＳＡＶＥ（Software  Applications  Validation  Environment）と称される設定可能なウェブサービスアーキテクチャと考えられる。それは、Ｊａｖａ（登録商標）に基づくウェブアプリケーションにおいて必要条件を自動で確認するための相互作用サービスを含む。また、現実世界のアプリケーションを有効に検証すべく構成ツールを配置するための関連する方法論が提供される。かかる環境は、必要条件捕捉サービスと、環境／モデル生成サービスと、自動特性テンプレートインスタンス化及びマッチングサービスと、モデルチェッカーと、シンボル実行エンジンとを有する。所与のウェブサービスにＳＡＶＥを適用する典型的なシナリオが、図２には表されている。
【００１８】
図２で（及び以後の図で）提示されるアーキテクチャは、異種言語から成るソフトウェアアプリケーションでの欠陥検出に及ぶ大きな適用範囲を有する。かかるアーキテクチャは、以下の相互作用サービス、すなわち、１）使用状況／シナリオを捕らえ、その有効性を確認すること、２）異種ソフトウェアアプリケーションをスタンドアローンの同種のアプリケーションに変形する環境発生、３）モデルチェックのための特性モニタの自動起動、４）診断のための欠陥の視覚化、５）プレゼンテーション層のための自動試験発生、及び６）設定はまさに単純特性（ＸＭＬ）ファイルでありうること、を含みうるソフトウェアアプリケーションで欠陥を検出することができる。
【００１９】
本質的に、本発明は、ソフトウェアの欠陥検出における最高位の方法論に関する。対象のアーキテクチャは、通常は、メーカー発行の製品のホワイトペーパーで公開されており、従って、ＳＡＶＥとの類似性を識別することは容易である。
【００２０】
（ここに挙げられている試みにおける）目的は、革新的なソフトウェア品質によって仕損じ原価を減らすことである。この分野における不良は、１）金融災害を引き起こすアプリケーションソフトウェアの不備、２）失速（stalling）を引き起こす埋め込みシステム、すなわち、自動ソフトウェアの欠陥、３）不正侵入された又は停止した電子商取引のウェブサイトを含む。これらの課題を解決する費用は、同様に相当なものである。かかる分野におけるバグ修正費用に関するおおまかな推定は、符号化／開発の間のバグ修正の５０００ドルに対して、おおよそ３０，０００ドルである。このようにして、理知的にソフトウェアを評価する革新的な技術を解決することが責務である。具体的には、目標は、１００％の範囲を有して、ソフトウェア開発の間に欠陥を識別することである。これは、従来の試験技術によっては達成不可能である。
【００２１】
このようなアーキテクチャは、ソフトウェアアプリケーションの領域固有性に基づいて、大きなソフトウェアコードベースの検証のために短時間のカスタマイズ及び更なる自動化を可能にすることを含め、多数の利点を有する。例えば、ウェブアプリケーションは、セキュリティ特性が検証されることを要する金融アプリケーションでありうる。加えて、設定は、このような検証の実行において最大の自動化を達成するためにカスタマイズされうる。一実施例で、その設定は、ＸＭＬで特性ファイルを用いて特定され得る。
【００２２】
提供されるシステムは、また、エンタープライズ・ストレングスのウェブアプリケーションを形式的に検証するための実行可能なエンド・ツー・エンドの解決法を提供することもできる。更に、それは、このようなアプリケーションの性質に上手く適した技術の適切な組の選択を提供する。それは、更に、このようなＪａｖａ（登録商標）アプリケーション類でツールセットの有効性を最大とするよう、ツールセットのカスタマイズをウェブアプリケーションへ提供することができる。これは、特性テンプレートの特定の選択及び組み立てや、シンボル実行における文字列処理ライブラリの使用等に適用しうる。単純な仕様言語において又は例えばＵＭＬのような視覚的な形式主義を用いて、必要条件の捕捉では柔軟性が認められる。
【００２３】
本質的に、提案されるシステムは、平均的なシステムエンジニアにとってツールセットの有用性を高めるよう、簡単なユーザフレンドリーなインターフェース及び自動化の重視を提供する。例えば、特性テンプレートの使用は、しばしば複雑且つエラーを起こしやすい、必要条件を特定するタスクを、プルダウンメニューにおける数回のクリック及び幾つかのフォームの最小完了（フォーム入力（form  filling））へ変形する。検証プロセスで各ステップの総体的な能力を高める様々な構成ツールの共生相互作用（symbiotic  interaction）がある。これは、環境発生をより良くするために使用されるシンボル実行に基づく静的解析を含みうる。これは、また、モデルチェックに基づくシンボル実行を有してより多くの表現特性を自動的に特定し且つ検証するために使用される特性テンプレートを含みうる。
【００２４】
図３は、ウェブアプリケーションアーキテクチャを表す略ブロック図を表す。具体的には、図３は、ウェブ／電子商取引（ｅ−コマース）アプリケーションの３段階アーキテクチャを表す。図３は、ＵＩ／ウェブブラウザ４４と、（本例ではＪａｖａ（登録商標）である）ビジネスロジック４６と、サーバ／データベース４８とを含む。ＵＩ／ウェブブラウザ４４は、ナビゲーションエラーを有する。ビジネスロジック４６内深くに隠されたバグは、従来の試験によって見つけるのが困難である。このシナリオでは、ＥＪＢサーバは、正確に動作すると仮定される。
【００２５】
図４は、どのようにＳＡＶＥアーキテクチャが動作することができるかを表す略ブロック図である。ドライバは、テスタ供給される使用状況／シナリオからビジネスロジックを試験するよう自動的に生成される。次いで、ビジネスロジックは検証される。特性“カートは、注文が承認された後に処理される”は、モデルチェックによって自動的に検証される。
【００２６】
続くステップで、データベースは置換される（もみ消される（stubbed  out））。この場合に、ＥＪＢ／サーバ／データベース呼出は、空きの又はユーザ供給されるスタブによって自動的に置換される。
【００２７】
図５を参照する前に、本発明の意義の幾つかを説明するのに役立つ簡単なケーススタディを与えることが有用である。ケーススタディは、ペットストア（ＰｅｔＳｔｏｒｅ）（１３，０００ライン）に関するものである。３つの重要な欠陥が、サンマイクロシステムズのブループリンツ・ウェブサイトから入手可能なペットストアのウェブアプリケーションに関して見つけられた。ペットストアは、２００１年に開発されたベンチマークのウェブアプリケーションであり、そのときから５度の改訂が行われている。２００６年にリリースされた第４の改訂は、試験のために使用された。最新のリリースは、第４のリリースのＡＪＡＸバージョンである。
【００２８】
検証される必要条件に関し：
・買い物かご（カート）は、注文が承認された後のチェックアウトにおいて処理される：
−ＳＡＶＥ環境発生及びモデルチェックによって検証される；
・注文総額＝カート内の物品の総額：
−ＳＡＶＥ環境発生及びモデルチェックによって検証される；
・注文が５００ドルより多い場合には、ステータスは保留である；
−ＳＡＶＥ環境発生及びシンボル実行によって検証される：
・Ｂｒｉｄｓ＿Ｐｒｏｄｕｃｔ＿Ｐａｇｅ（鳥関係製品のページ）は、Ｂｉｒｄｓ＿Ｉｔｅｍ＿Ｐａｇｅ（鳥関係アイテムページ）の前に到達されなければならない：
−ＳＡＶＥモデルチェックに基づく試験発生によって検証される。
【００２９】
検出される欠陥に関し：
・パスワード不一致はチェックされない：
−セキュリティの問題は、ＳＡＶＥ環境発生及びモデルチェックによって検出される；
・空白アカウントプロファイル：
−ユーザアカウントは、空白プロファイル又は幾つかの既存のプロファイルのいずれか一方により生成される；
−ＳＡＶＥ必要条件モデルチェックに基づく自動テストケース発生によって検出される；
・新しいユーザにアカウントユーザ名を再利用する場合の衝突：
−ＳＡＶＥモデルチェックに基づくテスト発生によって検出される。
【００３０】
本例におけるこのような欠陥の識別は、適切な検証の重要性を反映する。例えば本発明によって提供されるようなツールを用いないと、ペットストアモデルは、欠陥に遭遇するために断続的に行き詰まり又は機能しなくなりうる。
【００３１】
図６は、ソフトウェアアプリケーションを伴う１つの例となるシナリオに係る処理フローを表す略図である。図７は、関連するフローチャートを表す略図である。図６は、処理フローで強調される欠陥遷移コンポーネント８０を含む。フローは、アカウント動作と、パスワード設定ステップと、しばしば典型的なソフトウェア環境で出会う一般的な手続ステップとを含む。関連する方法として、図７は、フローチャートでパスワード及び状態ＩＤセグメントを表しており、これらの事項は、カウントが生成されている間に発生する。
【００３２】
図５は、世界的なシステム要求／特性を分類し、特性規格を自動化し、且つ、対応する必要条件チェッカーを自動的に呼び出す方法に関連する幾つかの（しかし、全てではない）教示を強調するために使用され得る。図５は、本発明の１つの態様に関連するモデルチェッカーの例を表す略ブロック図である。図５は、Ｊａｖａ（登録商標）モデルチェッカー／モデルに基づく試験発生器５４と、使用状況の組５６と、ウェブアプリケーション６２と、モデル発生器６０と、アプリケーションモデル５８と、（図５では短縮されて“必要条件”と称される）必要条件／特性規格ツール６８とを含む。図５は、また、“検証される又はエラーを見つけられる”要素とともに、幾つかの視覚化コンポーネントを含む。図５は、更に、シンボルモデル（コード・インストルメンタ（instrumenter））６４と、ナビゲーションチェッカー経路と、Ｊｗｅｂユニット・テストケースコンポーネントとを含む。
【００３３】
本発明の世界的なシステム態様は、第１に、特性／必要条件を、（例えば、電子商取引、金融等の）ソフトウェアアプリケーションの領域（domain）に基づいて、少数のカテゴリに分類することができる。このような分類は、領域ごとに先験的に行われ得る。それは、また、Ｊａｖａ（登録商標）アプリケーションのソースコードを走査し、ユーザが自身の要求を特定する場合に選択することができる関心あるイベントの組を生成する。次いで、（満たされる必要がある）特定の必要条件／特性の組は、カテゴリと適合される。適合の成功後に、モニタ／特性チェッカーは、インスタンス化された特性カテゴリに対応して起動される。
【００３４】
ソフトウェアのための形式的な検証技術には問題がある。例えば、（純粋な）Ｊａｖａ（登録商標）のためのポイントツール（例えば、モデルチェッカー）は、スタンドアローン、すなわち、形式主義を適用するのが困難であり、平均的なシステムエンジニアによって習得することが困難な使用法であり、且つ、ウェブアプリケーションのカスタマイズはない。
【００３５】
（ＬＴＬ（linear  temporal  logic）と呼ばれる）数学的言語で記述される形式的特性／必要条件は、直感的に理解できず且つ複雑であり、更には、設計者は、これを特定するより容易な方法（特に、ＧＵＩに基づくシステム）を必要とする。更に、必要とされるものは、アプリケーションにとって関心ある“イベント”を検出する方法論である。次いで、これらのイベントは、特性を一般化するために使用され得る。このようにして、ウェブアプリケーションのための形式的な検証方法論の有用性を増す必要性が存在する。
【００３６】
特性分類／テンプレートに関し、ＪＰＦにおけるモデルチェック要求は、２つのステップ、すなわち、時相論理（temporal  logic）（例えば、ＣＴＬ、ＬＴＬ）で正確に特性を表す段階と、ＪＰＦ及びチェックとともに実行するＪａｖａ（登録商標）モニタ実施特性を符号化する段階とを要する。特性テンプレートは、ウェブアプリケーションとの関連で、これらのステップを自動化する。ここで、ユーザは、テンプレートの小リストから選択する。この小リストは、ウェブアプリケーションに関して通常確認される必要条件のほとんどを捕捉するよう設計されている。例えば、約５０頁の要件文書は、約１０頁の一般化されたテンプレートにまで減らされる。
【００３７】
次いで、ユーザは、幾つかのパラメータを、確認されるべき特定のアプリケーション及び特性に基づいて、このテンプレートに入力し、その後に、（例えば、選択された特性、すなわち、“買い物かごは、全ての買い物セッションでのチェックアウト後に空にされる”ことを確認するよう）ＳＡＶＥでモデルチェックを呼び出す。ステップは、１）ｂがａの後に従うよう、ＳＡＶＥで応答特性テンプレートを選択する段階と、２）ａ及びｂに夫々対応するイベント“カート・エンプティ（買い物かごを空き状態にする）”及び“チェックアウト”を形式的に満たす段階と、３）ＳＡＶＥでモデルチェックを呼び出す段階とを含みうる。
【００３８】
特性テンプレートの利点は、仕様の容易さにある。更に、自然言語要求をテンプレートの小リストの中の１つと適合させることが容易である。加えて、正確な数学的言語特性を記述する必要性がない。テンプレートのリストは、検証すべき必要条件の組のアセンブルにおいてガイドとして機能することができる。また、モデルチェックも容易である。
【００３９】
自動モニタ発生に関し、特性テンプレートに対応するモニタは、先験的に開発される。領域固有の自動化された静的解析を用いて、（特性仕様に存在する関係に対応する）プログラムオブジェクト／イベントは、有効に見つけられる。その場合に、適切な特性テンプレートは、プログラムオブジェクト／イベントを有してインスタンス化される。テンプレートに対応するモニタは、適切なインスタンス化により呼び出される。次いで、検証されるべきソフトウェアアプリケーションは、実行を監視するモニタにより実行される。集合的に、これらの動作は、ソフトウェア検証のための実行可能なアプローチを実現する。
【００４０】
図１乃至５で表される構成要素は、デジタル回路、アナログ回路、ソフトウェア、又はこれらの要素のいずれかの適切な組み合わせとして実施され得る点に留意すべきことが重要である。加えて、これらの表されている構成要素のいずれも、ここで記載されるようにそれらの特徴及び／又は用途を達成するためのソフトウェア及び／又はアルゴリズムを含みうる。ソフトウェアは、ここに挙げられている機能が実行され得るようにコードを実行することができる。代替的に、このような動作及び技術は、いずれかの適切なハードウェア、コンポーネント、装置、特定用途向け集積回路（ＡＳＩＣ）、付加的なソフトウェア、フィールド・プログラマブル・ゲート・アレイ（ＦＰＧＡ）、プロセッサ、消去可能プログラマブルＲＯＭ（ＥＰＲＯＭ）、電気的消去可能プログラマブルＲＯＭ（ＥＥＰＲＯＭ）、又はこのような動作を促すよう動作するその他の適切なオブジェクトによって実現され得る。この配置に関連したこれらのアーキテクチャの構成によって相当の柔軟性が提供される。このようにして、このような機能が記載される環境の外で提供され得ることは、容易に認識され得る。このような場合に、このような機能性は、別々の構成要素、装置、又はモジュールにおいて容易に具体化され得る。
【００４１】
本発明は、特定の構成要素が区別されるように詳細に記載されてきたが、様々な変更及び改良が、いわゆる当業者に提案され得、更に、本発明は、明らかに添付の特許請求の範囲に包含されるように、このような変更及び改良のいずれも含むことが意図される。
【００４２】
また、留意すべきは、開示される特定の処理フローに関して、そのフローの中で説明されるいずれのステップも、本発明の技術的範囲を逸脱しない範囲で変更、拡大、又は削除をされ得ることである。更に、ステップは、本発明の技術的範囲を逸脱しない範囲で、いずれかの適切な順序で、又は同時に実行され得る。
【００４３】
多数の他の変更、置換、変形、代替、及び改良は当業者には明らかであり、添付の特許請求の範囲の適用範囲内で、本発明が全てのこのような変更、置換、変形、代替、及び改良を包含することが意図される。
【００４４】
以上の実施形態に関し、更に以下の付記を開示する。
【００４５】
（付記１）
設定可能なウェブサービスアーキテクチャにより異種言語から成るソフトウェアアプリケーションにおける１又はそれ以上の欠陥を検出する欠陥検出段階を有し、
前記欠陥検出段階は、
前記ソフトウェアアプリケーションと関連する使用状況を捕らえ、その有効性を確認する段階と、
モデルチェックのための特性モニタの自動起動を与える段階と、
診断のために前記ソフトウェアアプリケーションにおける１又はそれ以上の欠陥を視覚化する段階とを有する、方法。
【００４６】
（付記２）
前記欠陥検出段階は、異種ソフトウェアアプリケーションを同種のアプリケーションに変形する段階を更に有する、付記１記載の方法。
【００４７】
（付記３）
前記欠陥検出段階は、前記ソフトウェアアプリケーションと関連するプレゼンテーション層に自動テスト生成を与える段階を更に有する、付記１記載の方法。
【００４８】
（付記４）
前記ソフトウェアアプリケーションと関連する設定は、単純特性ファイルである、付記１記載の方法。
【００４９】
（付記５）
前記欠陥検出段階は、ユーザの行動をシミュレーションする段階を更に有する、付記１記載の方法。
【００５０】
（付記６）
前記欠陥検出段階は、使用状況又はシナリオからビジネスロジックを試験するドライバを生成する段階を更に有する、付記１記載の方法。
【００５１】
（付記７）
前記欠陥検出段階は、空きの又はユーザ供給のスタブによってデータベースを置き換える段階を更に有する、付記１記載の方法。
【００５２】
（付記８）
前記欠陥検出段階は、前記ソフトウェアアプリケーションのためのビジネスロジックを検証する段階を更に有する、付記１記載の方法。
【００５３】
（付記９）
ソフトウェアアプリケーションの領域に基づき、特性又は必要条件を少数のカテゴリに分類する段階と、
Ｊａｖａ（登録商標）アプリケーションのソースコードを走査する段階と、
前記特性又は必要条件を特定する場合にエンドユーザによって選択され得るイベントの組を生成する段階と、
満足される必要がある選択された組の必要条件又は特性を１又はそれ以上のカテゴリと適合させる段階と、
インスタンス化された特性カテゴリに対応するモニタ又は特性チェッカーを、前記モニタ又は前記特性チェッカーへの前記カテゴリの適合完了後に起動する段階と
を有する方法。
【００５４】
（付記１０）
前記分類段階は、前記ソフトウェアアプリケーションの領域ごとに先験的に行われる、付記９記載の方法。
【００５５】
（付記１１）
コンピュータ媒体に組み込まれるロジックであって、
設定可能なウェブサービスアーキテクチャにより異種言語から成るソフトウェアアプリケーションにおける１又はそれ以上の欠陥を検出するよう動作し、
前記欠陥検出動作は、
前記ソフトウェアアプリケーションと関連する使用状況を捕らえ、その有効性を確認する段階と、
モデルチェックのための特性モニタの自動起動を与える段階と、
診断のために前記ソフトウェアアプリケーションにおける１又はそれ以上の欠陥を視覚化する段階とを有する、ロジック。
【００５６】
（付記１２）
前記欠陥検出動作は、異種ソフトウェアアプリケーションを同種のアプリケーションに変形する段階を更に有する、付記１１記載のロジック。
【００５７】
（付記１３）
前記欠陥検出動作は、前記ソフトウェアアプリケーションと関連するプレゼンテーション層に自動テスト生成を与える段階を更に有する、付記１１記載のロジック。
【００５８】
（付記１４）
前記ソフトウェアアプリケーションと関連する設定は、単純特性ファイルである、付記１１記載のロジック。
【００５９】
（付記１５）
前記欠陥検出動作は、ユーザの行動をシミュレーションする段階を更に有する、付記１１記載のロジック。
【００６０】
（付記１６）
前記欠陥検出動作は、使用状況又はシナリオからビジネスロジックを試験するドライバを生成する段階を更に有する、付記１１記載のロジック。
【００６１】
（付記１７）
前記欠陥検出動作は、空きの又はユーザ供給のスタブによってデータベースを置き換える段階を更に有する、付記１１記載のロジック。
【００６２】
（付記１８）
前記欠陥検出動作は、前記ソフトウェアアプリケーションのためのビジネスロジックを検証する段階を更に有する、付記１１記載のロジック。
【００６３】
（付記１９）
ドライバは、テスタ供給される使用状況から、検証されるビジネスロジックを試験するよう自動的に生成され、これによって、特性は、モデルチェックによって自動的に検証される、付記１１記載のロジック。
【００６４】
（付記２０）
前記ソフトウェアアプリケーションは、電子商取引アプリケーションに関する、付記１１記載のロジック。
【図面の簡単な説明】
【００６５】
【図１】どのように検証は典型的に実行されるかを表すシステムの例を表す略ブロック図である。
【図２】本発明の一実施例に従う、ソフトウェアを検証するための設定可能なウェブサービスアーキテクチャを表す略ブロック図である。
【図３】本発明の一実施例にかかるウェブサービスアーキテクチャを表す略図である。
【図４】どのようにＳＡＶＥアーキテクチャが動作することができるかの例を表す略ブロック図である。
【図５】本発明の一実施例に従う、世界的なシステムの必要条件又は特性を分類する方法に関連した幾つかの教示を表す略ブロック図である。
【図６】１つの例となるシナリオに係る処理フローを表す略図である。
【図７】本発明に関連した１つの例となるシナリオに係るフローチャートを表す略図である。
【符号の説明】
【００６６】
１０  システム
１２  条件付きコンポーネント
１４  ウェブアプリケーション
１６  データセグメント
２０  モデルチェック
２２，２４  ウェブサービス
２８  テストケース・コンポーネント
３２  欠陥／バグ報告コンポーネント
４０  欠陥診断のための画像視覚化コンポーネント
４４  ＵＩ／ウェブブラウザ
４６  ビジネスロジック
４８  サーバ／データベース
５４  試験発生器
５６  使用状況の組
５８  アプリケーションモデル
６０  モデル発生器
６２  ウェブアプリケーション
６４  シンボルモデル
６８  必要条件／特性規格ツール
８０  欠陥遷移コンポーネント
【図１】
2009087352.tif 000003
【図２】
2009087352.tif 000004
【図３】
2009087352.tif 000005
【図４】
2009087352.tif 000006
【図５】
2009087352.tif 000007
【図６】
2009087352.tif 000008
【図７】
2009087352.tif 000009