(57)【要約】【課題】従来の方法とシステムに付随する不利益や問題の少なくとも一部を実質的に除去または低減する、ウェブアプリケーションのための効果的なテスト生成を提供することを課題とする。【解決手段】一実施形態による方法は、ウェブアプリケーションのモデルチェッキングを用いて自動テストケース生成を生成する段階を含み、前記自動テストケース生成は、仕様を作成する段階と、前記仕様のモデルチェッキングを用いて特性を検証する段階と、反例を取得し、前記反例をウェブテストケースにマッピングする段階と、実装で前記ウェブテストケースを実行する段階とを含む。【選択図】図３
2009087354.tif 000002
【特許請求の範囲】
【請求項１】
ウェブアプリケーションのモデル検査を用いて自動テストケース生成を生成する段階を含み、前記自動テストケース生成は、
仕様を作成する段階と、
前記仕様のモデル検査を用いて特性を検証する段階と、
反例を取得し、前記反例をウェブテストケースにマッピングする段階と、
実装で前記ウェブテストケースを実行する段階とを含む方法。
【請求項２】
所望の特性を否定して前記仕様をモデル検査することにより、一組のウィットネスを表し前記ウェブテストケースにマッピングされる反例を生成する段階と、
前記実装において前記ウェブテストケースを実行する段階とをさらに含む、請求項１に記載の方法。
【請求項３】
前記反例を生成する段階と、前記ウェブテストケースを実行する段階とを利用できる特性とその反例について繰り返す、請求項２に記載の方法。
【請求項４】
前記ウィットネスを前記ウェブテストケースにマッピングし、前記マッピングは前記ウェブアプリケーションのネイティブ言語における実行可能テストへの抽象ウィットネスランのマッピングを含む段階とをさらに含む、請求項２に記載の方法。
【請求項５】
シナリオ分析と、前記仕様をカバーするだろうモデルのカバレッジとに基づき一組のテストを生成し、ユーザ規定の特性ベースの一組のウィットネスに加えて前記一組のテストを使用する、請求項１に記載の方法。
【請求項６】
前記ウェブテストケースがフェイルした場合、前記実装に問題があることを示す、請求項１に記載の方法。
【請求項７】
前記ウェブテストケースがフェイルした場合、前記仕様にエラーがあることを示す、請求項１に記載の方法。
【請求項８】
前記ウェブテストケースがパスした場合、前記ウェブアプリケーションの設計論理に不具合がある、請求項１に記載の方法。
【請求項９】
コンピュータに、
ウェブアプリケーションのモデルチェッキングを用いて自動テストケース生成を生成させるコンピュータプログラムであって、前記自動テストケース生成は、
仕様を作成する段階と、
前記仕様のモデルチェッキングを用いて特性を検証する段階と、
反例を取得し、前記反例をウェブテストケースにマッピングする段階と、
実装で前記ウェブテストケースを実行する段階とを含むコンピュータプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ウェブアプリケーションの分野に関し、特にウェブアプリケーションの自動テストを生成するシステム及び方法に関する。
【背景技術】
【０００２】
ほとんどのウェブアプリケーションでは、既存の実装はエラーを含んでおり、ユーザが登録してもユーザデータベースが正しく更新されなかったり、ユーザがチェックアウトしてもショッピングカートが空にならなかったりすることがある。これらのエラーは内部のビヘイビア（behaviors）のみに関連し、特定することは困難である。レガシー（legacy）なウェブアプリケーションの形式的なテスト方法を考えるとき、すぐに問題となるのは、初期設定では形式的な検証（verification）が不可能だということである。確かに、レガシーアプリケーションにはハイレベルの仕様（specification）が欠けていて、その仕様が検証の基幹となる要素である場合がある。また、ソースコードレベルでの検証はもともと困難であり、スケーラブルではなく、プラットフォームに依存する。とくにウェブアプリケーションの場合はそうである。
【０００３】
一般的に実装をテストしてもエラーは発見できない。しかし、効果的なテストを構成することも難しいことは容易に分かる。レガシーなウェブアプリケーションのテストに関する既存の研究は、実装のローレベルの詳細事項に関する専門知識を有するテスターを必要とする傾向があった。また、命題抽象化（propositional  abstraction）（すなわち、命題を用いたアプリケーションの抽象化）がまだ一般的に使用されているが、これは理想とはかけ離れたものである。データドリブン（data-driven）・ウェブアプリケーションの仕様及び検証のフレームワークに着想を得ているため、多くの設計担当者による研究の目標は、必要なテストをするためにデータアウェア（data-aware）検証をいかに使用できるかの探求となっている。
【０００４】
それゆえ、ウェブアプリケーションにおけるテスト問題の解決は、興味深い課題である。こうした処理作業と同様に、速度、精度、及び自動化に関連する問題が非常に重要である。
【発明の開示】
【発明が解決しようとする課題】
【０００５】
従来の方法とシステムに付随する不利益や問題の少なくとも一部を実質的に除去または低減する、ウェブアプリケーションのための効果的なテスト生成を提供することを課題とする。
【課題を解決するための手段】
【０００６】
一実施形態による方法は、ウェブアプリケーションのモデルチェッキングを用いて自動テストケース生成を生成する段階を含み、前記自動テストケース生成は、仕様を作成する段階と、前記仕様のモデルチェッキングを用いて特性を検証する段階と、反例を取得し、前記反例をウェブテストケースにマッピングする段階と、実装で前記ウェブテストケースを実行する段階とを含む。
【０００７】
より具体的な実施形態では、本方法は、所望の特性を否定して前記仕様をモデル検証することにより、一組のウィットネスを表し前記ウェブテストケースにマッピングされる反例を生成する段階と、前記実装において前記ウェブテストケースを実行する段階とをさらに含む。
【０００８】
さらに他の実施形態では、前記反例を生成する段階と、前記ウェブテストケースを実行する段階とを利用できる特性とその反例について繰り返す。前記ウィットネスを前記ウェブテストケースにマッピングし、前記マッピングは前記ウェブアプリケーションのネイティブ言語における実行可能テストへの抽象ウィットネスラン（witness  runs）のマッピングを含む。前記マッピングは選択されたフレームワーク技術により実行される。シナリオ分析と、前記仕様をカバーするだろうモデルのカバレッジとに基づき一組のテストを生成し、ユーザ規定の特性ベースの一組のウィットネスに加えて前記一組のテストを使用する。
【０００９】
さらに他の実施形態では、前記ウェブテストケースがフェイルすることは、前記実装に問題があることを示す。前記ウェブテストケースがフェイルした場合、前記仕様にエラーがあることを示す。前記ウェブテストケースがパスした場合、前記ウェブアプリケーションの設計論理に不具合がある。アサーションを自動的に生成し、テストモニタコードに挿入できる。テスト担当者はウェブテストケースの結果に基づき仕様を修正できる。
【００１０】
前記自動テストケース生成はユーザ規定の特性を利用する。前記仕様を作成して、前記実装上で前記ウェブテストケースを実行してから前記仕様を改良できる。
【００１１】
本発明の実施形態の技術的な利点の１つとして、完全な検証ソリューションを提供できる。具体的には、本発明は形式的仕様をリバースエンジニアリング技術（例えば、コード分析、モデルチェッキング、シナリオ生成、及びウィットネスとシナリオからの実行可能コードの生成）と組み合わせて、レガシーなウェブアプリケーションの完全な検証ソリューションを提供する。対照的に、従来の方法ではかかる相乗的方法をうまく（または信頼できるように）提供することができなかった。ここに提案するアーキテクチャのテスト生成方法は両者に基づくテストを提供する。
【００１２】
また、言うまでもなく本発明の設定（configuration）は自動的である。開発担当者に長いテスト用のコードを書いてもらう必要はない。アサーションを自動的に生成し、テストモニタコードに挿入する。さらに、ユーザ定義の特性（例えば、チェックアウト後はショッピングカートを空にしなければならない）を明確にする。また、仕様書モデルの包括的シナリオ分析を比較的容易に行える。
【００１３】
他の技術的な有利性は、以下の図面、詳細な説明、及び特許請求の範囲に基づき、当業者には容易に明らかとなるであろう。さらに、具体的な有利性を上記したが、様々な実施形態は上記の有利性のすべてまたは一部を含んでもよいし、全く含まなくてもよい。
【発明を実施するための最良の形態】
【００１４】
本発明の具体的な実施形態とそれらの優位性をよりよく理解するために、添付した図面を参照しつつ以下に説明する。
【００１５】
図１は、本発明の一実施形態に関係するモデルチェッカーとシンボリック実行１０の一例を示すブロック図である。図１は、典型的なユーザレベルの、検証ウェブサービスアーキテクチャのアプリケーションの詳細を表している。図１は、Ｊａｖａ(登録商標)モデルチェッカー１４と、一組のユースケース１６と、アプリケーションモデル１８と、環境／モデルジェネレータ２０と、ウェブアプリケーション２２とを含む。（（Ｊａｖａ）モデルチェッカー１４とインタフェースする）図１の要求コンポーネント（requirements  component）は、論理、セキュリティ、ナビゲーション、機能、及び性能の問題に分けられる。
【００１６】
本発明の実施形態の教示によると、図示したアーキテクチャは、ウェブアプリケーションの理想的なテスト生成ソリューションを提供する。最初に、言うまでもなく、ここに開示するアーキテクチャがターゲットとするのは、ユーザが登録してもユーザデータベースが正しく更新されなかったり、ユーザがチェックアウトしてもショッピングカートが空にならなかったりするエラーを、既存の実装が含んでいるウェブアプリケーションである。これらのエラーは内部のビヘイビア（behaviors）のみに関連し、特定することは困難である。レガシー（legacy）なウェブアプリケーションの形式的なテスト方法を考えるとき、すぐに問題となるのは、初期設定では形式的な検証（verification）が不可能だということである。確かに、レガシーアプリケーションにはハイレベルの仕様（specification）が欠けていて、そのスペックが検証の基幹となる要素である場合がある。また、ソースコードレベルでの検証はもともと困難であり、スケーラブルではなく、プラットフォームに依存し、ウェブアプリケーションの場合は特にそうである。
【００１７】
一般的に実装をテストしてもエラーは発見できない。しかし、明らかに、効果的なテストを構成するのは自明ではない。レガシーなウェブアプリケーションのテストに関する既存の研究は、実装のローレベルの詳細事項に関する専門知識を有するテスターを必要とする傾向があった。また、命題抽象化（propositional  abstraction）、すなわち命題を用いたアプリケーションの抽象化は、まだ一般的に使用されている。データドリブン（data-driven）・ウェブアプリケーションの仕様及び検証のフレームワークに着想を得て、ここで詳細に説明するシステムの目標は、データアウェア（data-aware）検証をいかに使用してテストをするか調べて解決することである。
【００１８】
１つのフレームワークにより提案されたパラダイムでは、ウェブアプリケーションの開発担当者は、アプリケーションのハイレベル仕様から始めて、いろいろな特性を検査して検証を行い、最終的には自動的に生成されたアプリケーションの実装を得る。ここで提案されたテストパラダイムでは、上で触れたように、テスターは既存の実装から開始する。一見するとこれは大きなミスマッチ（mismatch）のように思われる。しかし、注目すべきことは、フレームワークが出力する検証結果は実際のテストと密接な関係を有することである。確かに、間違った特性（property）が与えられると、検証部（verifier）はユーザとウェブアプリケーションとの間の一連のインターラクションを表示する。この一連のインターラクションは特性違反を表している。
【００１９】
ウェブアプリケーションのテストへの理想的なアプローチを説明する前に、ウェブテストケース（web  test  cases）を知っていると役に立つ。ウェブテストケースは実際のウェブサイトでユーザの入力とナビゲーション（navigations）とを行い、プロセス中にアサーション（assertions）を生成する特別なプログラムである。ウェブテストケースは、（すべてのアサーションが真である）ウェブサイトの有効な実行を表すときは「パス（pass）」するといい、そうでないときは「フェイル（fail）」するという。実施形態によっては、ウェブテストケースはＪＷｅｂＵｎｉｔライブラリを用いたＪａｖａ(登録商標)プログラムである。
【００２０】
こうした背景の下、本発明により得られるアーキテクチャが提供する方法論では、検証ベースのテストアプローチを実装する。最初に、アプリケーションの実装担当者（implementer）はテスト担当者（tester）とは異なることがあり、テスト担当者がアプリケーションのハイレベルの仕様と検証した特性とを作成していることに留意する。これにより、すぐに２〜３の潜在的な問題が生じる：（１）（［図３に示したように］テスト担当者が書いた）仕様は、（実装担当者が書いた）実装に対して忠実であるという保証はなく；（２）ウェブアプリケーションの設計論理に欠陥があるかも知れない。こうした最初からの問題（original  problem）に加えて実装にエラーがあるかも知れない。
【００２１】
ここに開示するアプローチは２つのステップよりなる。最初の段階では、仕様を作成（develop）して改良する。仕様は様々な方法で作成することができる。例えば、テスト担当者は実装を見て、フレームワークやＵＭＬタイプのモデルを手で作成する。自動コード分析ツールを使用してコードベース（code  base）をリバースエンジニアリングして、ＵＭＬタイプのモデルを作成することもできる。サーバログとネットワークトラフィック分析を使って、一般的にウェブページをどのように行き来するかに関するシナリオやユースケースを構成することもできる。仕様モデルを作成すると、標準的な方法を用いてその仕様モデル上のモデル検査（model  checking）を用いて特性を検証し、反例を取得してウェブテストケースにマッピングする。そのウェブテストケースを実装上で実行する。フェイルすれば、上記の問題（１）があることになる。パスすれば、上記の問題（２）があることになる。何れの場合でもテスト担当者は必要に応じて適当に仕様を修正する。このプロセスを利用できるすべての特性とその反例に対して繰り返す。
【００２２】
第１段階が終わるまでに仕様は利用できるすべての方法で改良（refine）されているので、テスト担当者は仕様を凍結し（信頼して）、実装中のエラーを特定する元の問題に焦点を絞ることができる。このフェーズの目標は、実装中のできるだけ多くのエラーをつかまえることができる包括的な一組のテストケースを作成することである。これは異なる２つの方法で解決することができる。
【００２３】
第１の方法では、この段階では仕様上の所望の特性はどれも真なので、この所望の特性を否定することにより反例を作成し、仕様をモデル検査する。特性は仕様上では有効なので、それを否定すると有効でなくなり、反例（ウィットネス（witness））が生まれる。このウィットネスをウェブテストケースにマッピングする。抽象ウィットネスラン（abstract  witness  runs）をウェブアプリケーションのネイティブ言語中の実行可能テストにマッピングする技術を使用して、このタイプのマッピングが可能である。上記の通り、ウェブテストケースは実装上で実行する。フェイルした場合、上で強調した問題が見つかる。この場合、テスト担当者は実装中のエラーの修正を試みる。このプロセスは、利用できるすべての特性とそのウィットネスに対して繰り返される。
【００２４】
複数組のテスト（test  suites）を作成する第２の方法は、シナリオ分析と、おそらく仕様全体をカバーするモデルのカバレッジ（coverage）とに基づき一般的な複数組のテストを作成する技術を利用するものである。この複数組のテストを、上で作成したユーザが決めた特性ベースの複数組のウィットネスに加えて利用できる。これらの２つの組のテストを組み合わせることにより、シナリオのカバレッジと主要特性のカバレッジとの両方を確保できる。
【００２５】
かかるフレームワークはレガシーなウェブアプリケーションをテストする新しいアプローチを提供する。このアプローチはフレームワークを備えたデータアウェア検証（data-aware  verification）に基づき、ローレベルのディテール（details）に関する知識はほとんど必要とせず、抽象化はまったく必要としない。これにより顕著な利点が生じる。例えば、このプロトコルは形式的仕様をリバースエンジニアリング技術（例えば、コード分析、モデル検査、シナリオ生成、及びウィットネスとシナリオからの実行可能コードの生成）と組み合わせて、レガシーなウェブアプリケーションの完全な検証ソリューションを提供する。対照的に、従来の方法ではかかる相乗的方法をうまく（または信頼できるように）提供することができなかった。ここに提案するアーキテクチャのテスト生成方法は両者に基づくテストを提供する。
【００２６】
さらに、本発明の構成は自動的である。開発担当者に長いテスト用のコードを書いてもらう必要はない。アサーションを自動的に生成し、テストモニタコードに挿入する。さらに、ユーザ定義の特性（チェックアウト後はショッピングカートを空にしなければならない）を明確にする。また、仕様モデルの包括的シナリオ分析を比較的容易に行える。
【００２７】
図２は、モデル検査ドリブン・テスト生成のシステム例３０を示すブロック図である。図２は、抽象モデル３２と、テスト生成コンポーネント４２と、反例４０と、モデルチェック３６と、ソフトウェアコンポーネント３８とを含む。生来的に簡単化され、または「比較的容易な」ソリューションと、抽象モデル３２に関するもっと複雑な、すなわち「困難な」ソリューションとが区別されていることに留意せよ。
【００２８】
テストに関して、対象は一般的にウェブアプリケーションである。既存の実装（implementations）は多くの場合エラーを含んでいる。例えば、ユーザがチェックアウトしてもショッピングカートが空にならないエラーが発生し得る。問題を簡単に言うと、形式的検証が初期設定ではできないということである。形式的検証に適したものはハイレベル仕様にはない。また、ソースコードの検証はもともと困難であり、プラットフォームに依存する。
【００２９】
実装テストによりエラーを特定することができる。ここで問題となるのは、かかるシナリオにおいて効果的なテストを構成することが困難だということである。既存の研究は、テスト担当者が実装のローレベルの詳細事項に関する専門知識を有することを要求する傾向があった。命題抽象（propositional  abstraction）はまだ一般的に使用されている。データアウェア検証（data-aware  verification）を使ってテストをすることが目標である。
【００３０】
このアイデアには２つの面がある。すなわち（１）実装自体のテストケースの生成と、（２）仕様のテストケースの生成である。設計担当者としては、実装が仕様と一致するかどうか、または仕様自体が正しいかどうかを検査する。確認すべきことは、（１）仕様が正しく、（２）実装が仕様を満たしていることである。この２つが正しければ、実装は正しいと推論できる。
【００３１】
本発明は既存の実装から始まる。１つの問題は、実装中のエラーをいかに特定するかである。検証ベーステスト（verification-based  testing）について、レガシーなウェブアプリケーションに対してテストが必要であると思われる。問題は、エラーを特定する役にたつ効果的なテストを考えることである。
【００３２】
本発明の実施形態は基本的にテストを検証と組み合わせる。検証を使ってテストを容易にする。重要なことは、検証結果（すなわち、反例ラン（counterexample  runs））が実際のテストと密接な関係を有していることである。ここで、（単なるモデルではなく）実装に対してシミュレーションできる実際のテストを生成する技術を利用する。
【００３３】
図３は、モデルベースウェブテストケース生成の一例を示すブロック図である。図３は、テスト担当者５０と、実装担当者５２と、レガシーウェブアプリケーション及びデータベースコンポーネント５８と、ベリファイア６０と、シナリオコンポーネント６８と、仕様６４と、反例ラン（counterexample  run）７０と、ウィットネスラン７２と、マッピングコンポーネント７６とを含む。
【００３４】
このシナリオでは、Ｔ１がフェイルした場合、これは実装にエラーがあることを示す。Ｔ２がフェイルした場合、これは仕様にエラーがあることを示す。Ｔ２がパスした場合、特性にはエラーがあり、したがって設計ロジックにもエラーがある。
【００３５】
モデルベースのウェブテストケースを生成する構成の点では、第１段階において、仕様を合わせる。次に、仕様の特性（property）を検証する。次に、反例ランを（無くなるまで）取得し、ウェブテストケースにマッピングする。実装のテストケースを実行する。必要に応じて仕様を修正し、上記のプロセスを繰り返す。
【００３６】
第２段階において、実装を確定する。ここでのアイデアは、仕様をフリーズ（して信頼）することである。特性（property）のウィットネスランを取得する。これをウェブテストケースにマッピングする。次のステップはテストケースを実装上で実行することである。テストケースがフェイルした場合、実装中のエラーを修正する。上記のプロセスを繰り返す。
【００３７】
テストを生成する場合、仕様は、どんな形式（ＵＭＬ、ステートマシン等）であっても、モデル（階層メッセージシーケンスチャート）に変換される。ウィットネスラン特性もこのモデルで求める。コード生成技術を利用して、実装に対して直接的に使用できるシミュレーション可能テストケースを生成する。
【００３８】
かかるプロセスを用いて、完全なテスト生成方法が実現できる。テスト担当者は、具体的な特性をテストして、（モデル上の）パスした特性を否定して反例を生成する。この反例を実装に対してテストすることができる。また、テスト担当者はモデル及びユースケースからの可能なすべてのシナリオに基づき、完全な一組のテスト（a  complete  suite  of  tests）を生成することができる。アサーションを自動的に生成し、テストモニタコードに挿入する。様々な技術を組み合わせてレバレッジする完全なテスト環境を利用して、完全な検証ソリューションを提供することができる。
【００３９】
図１、図２、及び図３に示したコンポーネントはデジタル回路、アナログ回路、ソフトウェア、またはこれらの適当な組み合わせとして実施できる点に留意することが重要である。また、例示したこれらの構成要素は、ここに説明した機能及び／または適用を効果的にするソフトウェア及び／またはアルゴリズムを含んでいてもよい。ソフトウェアとしてコードを実行して、ここに概要を記載した機能を実行することができる。あるいは、かかる動作や方法は、ハードウェア、コンポーネント、デバイス、ＡＳＩＣ（application  specific  integrated  circuit）、追加的ソフトウェア、ＦＰＧＡ（field  programmable  gate  array）、プロセッサ、ＥＰＲＯＭ、ＥＥＰＲＯＭその他で適宜実現することができる。これらのアーキテクチャの構成により柔軟性が高くなる。このように、言うまでもなく、かかる機能を、概要を記載した環境の外部に設けることも可能である。その場合、かかる機能を別のコンポーネント、デバイス、モジュールなどで容易に実施することができる。
【００４０】
具体的なコンポーネントを特定して本発明を詳細に説明したが、当業者には様々な変更や修正が示唆されたであろう。本発明は、添付した請求項の範囲に明らかに含まれるかかる変更や修正を含むものである。
【００４１】
また、開示した具体的なプロセスフローに関して、本発明の範囲から逸脱することなく、このフロー中で説明したステップは修正、追加、削除してもよい。また、本発明の範囲を逸脱することなく、ステップを任意の好適な順序で実行することができる。
【００４２】
当業者はこの他に多数の変更、追加、変形、置換、修正を考えることができ、本発明は、添付した特許請求の範囲に入るこうした変更、追加、変形、置換、修正を含むものである。
【００４３】
上記実施形態に関し以下の付記を記す。
（付記１）  ウェブアプリケーションのモデル検査を用いて自動テストケース生成を生成する段階を含み、前記自動テストケース生成は、
仕様を作成する段階と、
前記仕様のモデル検査を用いて特性を検証する段階と、
反例を取得し、前記反例をウェブテストケースにマッピングする段階と、
実装で前記ウェブテストケースを実行する段階とを含む方法。
（付記２）  所望の特性を否定して前記仕様をモデル検査することにより、一組のウィットネスを表し前記ウェブテストケースにマッピングされる反例を生成する段階と、
前記実装において前記ウェブテストケースを実行する段階とをさらに含む、付記１に記載の方法。
（付記３）  前記反例を生成する段階と、前記ウェブテストケースを実行する段階とを利用できる特性とその反例について繰り返す、付記２に記載の方法。
（付記４）  前記ウィットネスを前記ウェブテストケースにマッピングし、前記マッピングは前記ウェブアプリケーションのネイティブ言語における実行可能テストへの抽象ウィットネスランのマッピングを含む段階とをさらに含む、付記２に記載の方法。
（付記５）  前記マッピングはフレームワーク技術により実行される、付記４に記載の方法。
（付記６）  シナリオ分析と、前記仕様をカバーするだろうモデルのカバレッジとに基づき一組のテストを生成し、ユーザ規定の特性ベースの一組のウィットネスに加えて前記一組のテストを使用する、付記１に記載の方法。
（付記７）  前記ウェブテストケースがフェイルした場合、前記実装に問題があることを示す、付記１に記載の方法。
（付記８）  前記ウェブテストケースがフェイルした場合、前記仕様にエラーがあることを示す、付記１に記載の方法。
（付記９）  前記ウェブテストケースがパスした場合、前記ウェブアプリケーションの設計論理に不具合がある、付記１に記載の方法。
（付記１０）  アサーションを自動的に生成してテストモニタコードに挿入し、テスト担当者が前記ウェブテストケースの結果に基づき前記仕様を修正する、付記１に記載の方法。
（付記１１）  前記自動テストケース生成はユーザ規定の特性を利用する、付記１に記載の方法。
（付記１２）  前記仕様を作成して、前記実装上で前記ウェブテストケースを実行してから前記仕様を改良する段階をさらに含む、付記１に記載の方法。
（付記１３）  コンピュータに、
ウェブアプリケーションのモデルチェッキングを用いて自動テストケース生成を生成させるコンピュータプログラムであって、前記自動テストケース生成は、
仕様を作成する段階と、
前記仕様のモデルチェッキングを用いて特性を検証する段階と、
反例を取得し、前記反例をウェブテストケースにマッピングする段階と、
実装で前記ウェブテストケースを実行する段階とを含むコンピュータプログラム。
（付記１４）  所望の特性を否定して前記仕様をモデル検証することにより、一組のウィットネスを表し前記ウェブテストケースにマッピングされる反例を生成する段階と、
前記実装において前記ウェブテストケースを実行する段階とをさらに含む、付記１３に記載のコンピュータプログラム。
（付記１５）  前記反例を生成する段階と、前記ウェブテストケースを実行する段階とを利用できる特性とその反例について繰り返す、付記１４に記載のコンピュータプログラム。
（付記１６）  前記ウィットネスを前記ウェブテストケースにマッピングし、前記マッピングは前記ウェブアプリケーションのネイティブ言語における実行可能テストへの抽象ウィットネスランのマッピングを含む段階とをさらに含む、付記１４に記載のコンピュータプログラム。
（付記１７）  前記マッピングはフレームワーク技術により実行される、付記１６に記載のコンピュータプログラム。
（付記１８）  シナリオ分析と、前記仕様をカバーするだろうモデルのカバレッジとに基づき一組のテストを生成し、ユーザ規定の特性ベースの一組のウィットネスに加えて前記一組のテストを使用する、付記１３に記載のコンピュータプログラム。
（付記１９）  前記ウェブテストケースがフェイルすることは、前記実装に問題があることを示す、付記１３に記載のコンピュータプログラム。
（付記２０）  前記ウェブテストケースがフェイルした場合、前記仕様にエラーがあることを示す、付記１３に記載のコンピュータプログラム。
（付記２１）  前記ウェブテストケースがパスした場合、前記ウェブアプリケーションの設計論理に不具合がある、付記１３に記載のコンピュータプログラム。
（付記２２）  アサーションを自動的に生成してテストモニタコードに挿入し、テスト担当者が前記ウェブテストケースの結果に基づき前記仕様を修正する、付記１３に記載のコンピュータプログラム。
（付記２３）  前記自動テストケース生成はユーザ規定の特性を利用する、付記１３に記載のコンピュータプログラム。
（付記２４）  前記仕様を作成して、前記実装上で前記ウェブテストケースを実行してから前記仕様を改良する段階をさらに含む、付記１３に記載のコンピュータプログラム。
【図面の簡単な説明】
【００４４】
【図１】本発明の一実施形態に関係するモデルチェッカーとシンボリック実行の一例を示すブロック図である。
【図２】モデル検査ドリブン・テスト生成シナリオの一例を示すブロック図である。
【図３】本発明の一実施形態によるモデルベースのウェブテストケースジェネレータを一例を示すブロック図である。
【符号の説明】
【００４５】
１４  Ｊａｖａモデルチェッカー
１６  ユースケース
１８  アプリケーションモデル
２０  モデルジェネレータ
２２  ウェブアプリケーション
３２  抽象モデル
３６  モデル検査
３８  ソフトウェア
４０  反例
４２  テスト生成
５０  テスト担当者
５２  実装担当者
５８  レガシーなウェブアプリケーション及びデータベース
６０  ベリファイア
６４  仕様
６８  シナリオ
７０  反例ラン
７２  ウィットネスラン
７６  マッピング
【図１】
2009087354.tif 000003
【図２】
2009087354.tif 000004
【図３】
2009087354.tif 000005