"方法であって、検証ツールキット環境を静的に解析する工程と、前記検証ツールキット環境の解析に基づいて、データ構造を互いに共有しない複数の計算スレッドを識別する工程と、前記計算スレッドの計算要件を算出する工程と、前記計算スレッドの全体的な計算要件が複数のリソース間でほぼ均一にバランスがとられるように複数のリソースの間で前記スレッドを分散する工程とを含む方法。請求項1記載の方法であって、前記検証ツールキット環境を静的に解析する工程は、前記検証ツールキット環境のモデル生成器を解析する工程と、前記モデル生成器によって生成されるモデルを解析する工程と、前記検証ツールキット環境の検証ツールキットを解析する工程とを含む方法。請求項1記載の方法であって、前記検証ツールキット環境を静的に解析する工程は、前記検証ツールキット環境から生成されるモデルから複数の実行経路を抽出する工程を含み、互いにデータ構造を共有しない複数の計算スレッドを識別する工程は、互いにデータ構造を共有しない前記複数の実行経路それぞれを表すスレッドを識別する工程を含み、前記計算スレッドの計算要件を算出する工程は、前記実行経路を表す前記計算スレッドを実行するために必要な計算リソースを算出する工程を含む方法。請求項1記載の方法であって、計算要件は、計算時間、処理要件、及びメモリ要件の少なくとも1つを含む方法。請求項1記載の方法であって、前記リソースはクラウド計算環境の構成部分である方法。実行されると、検証ツールキット環境を静的に解析する機能と、前記検証ツールキット環境の解析に基づいて、データ構造を互いに共有しない複数の計算スレッドを識別する機能と、前記計算スレッドの計算要件を算出する機能と、前記計算スレッドの全体的な計算要件が複数のリソース間でほぼ均一にバランスがとられるように複数のリソースの間で前記スレッドを分散する機能とを行うよう動作可能なソフトウェアをコード化した1つ又は複数のコンピュータ読み取り可能な有形の記憶媒体。システムであって、検証ツールキット環境を静的に解析するロジックと、前記検証ツールキット環境の解析に基づいて、データ構造を互いに共有しない複数の計算スレッドを識別するロジックと、前記計算スレッドの計算要件を算出するロジックと、前記計算スレッドの全体的な計算要件が複数のリソース間でほぼ均一にバランスがとられるように複数のリソースの間で前記スレッドを分散するロジックとを備えるシステム。本発明は、従来の方法及びシステムに関連した欠点及び課題の少なくとも一部をかなりなくすか、又は軽減する、検証計算を分散するための方法及びシステムを提供する。本発明の特定の実施例によれば、方法は、検証ツールキット環境を静的に解析する工程を含む方法を含み得る。方法は、検証ツールキット環境の解析に基づいて、データ構造を互いに共有しない複数の計算スレッドを識別する工程も含み得る。方法は更に、計算スレッドの計算要件を算出する工程を含み得る。方法は、計算スレッドの全体的な計算要件が複数のリソース間でほぼ均一にバランスがとられるように複数のリソース間でスレッドを分散する工程を更に含み得る。本発明の特定の実施例の技術上の利点は、アプリケーション検証に必要な時間を低減させることができ、計算リソースのクラウドに対する検証タスクの動的アロケーションを可能にすることにより、柔軟性を増加することができる方法論を含む。他の技術上の利点は、図面、明細書、及び特許請求の範囲から、当業者に容易に明らかになるであろう。更に、特定の利点は上述しているが、種々の実施例は、上述された利点の全部、一部を含み得るか、又は、上述の利点の何れも含まないことがあり得る。図1は、本開示の実施例による、検証ツールキット102の例示的な環境100を示す。特定の実施例では、検証ツールキット102は、1つ又は複数のユースケース108を行い、前述の検査の結果を出力する場合にシステムが1つ又は複数の要件又は仕様106を満たしているか否かを検査して、ソフトウェア若しくはハードウェア又はそれらの組合せの検査対象システムSUTの検証を容易にする。例として、ソフトウェアのシステムへの言及は、適宜、アプリケーション又はプログラムを包含し、逆も同様であり得る。SUT104の要件106は、システムの実行中にあてはまらなければならない特定の特性、又は、生じなければならないシステムの特定の振る舞いであり得る。一部の実施例では、オブジェクト間仕様は要件として表し得る一方、オブジェクト内仕様は実行可能な仕様と表し得る。振る舞い又は特性への言及は、適宜、要件106を包含し、逆も同様であり得る。SUT104のユースケース108は、例えば、特定のシーケンスでSUT104によって受け取られたユーザからの一連の特定の入力などのSUT104をユーザが使用する場合にSUT104が遭遇し得るシナリオの表現であり得る。シナリオへの言及は、適宜、ユースケースを包含し得、逆も同様であり得る。特定の実施例では、SUT104は、製品の開発中に生成される設計プロトタイプである。他の実施例では、SUT104は、検証ツールキット102によって生成されるステートマシン又は他の表現であり得る。例示的な環境100の構成部分は、図5を参照して以下に更に詳細に説明するものなどの1つ又は複数のコンピュータシステム内で実行又は動作し得る。検証ツールキット102のユーザは、SUT104の1つ又は複数の仕様若しくは要件106及び/又はユースケース108を規定し、それらをモデル生成器110に入力として通信し得る。モデル生成器110は、更なる入力のためにSUT104にアクセスし得る。モデル生成器110は次いで、SUT104のモデル112を生成し得る。特定の実施例では、モデル生成器110は、形式的視覚言語又はグラフィカルモデリング言語を使用してモデル112を生成するうえでユーザ相互作用を容易にするグラフィカルユーザインタフェースGUIを含む。グラフィカルモデリング言語は何れかの適切な言語であり得、モデル112は、何れかの適切なプログラミング言語又は開発ツ―ルを使用して作成し得る。特定の実施例では、モデル112は、統一モデリング言語UML、例えば、UML2.0を使用して生成されたSUT104の高水準設計仕様である。概して、UMLは、主にソフトウェアエンジニアリングの分野において利用されており、より少ない程度で、ハードウェアエンジニアリングの分野において利用されている標準化された汎用モデリング言語である。UMLは、特定のシステムの抽象モデルを作成するためのグラフィカル表記手法の組を含む。特に、UMLは、ソフトウェア及び/又はハードウェアシステムの要件及び設計などの別々のアーチファクトの規定するためのモデリング表記の集合である。例として、UMLは、開発中のオブジェクト指向ソフトウェア集約型システムのアーチファクトの仕様、視覚化、構成、及び文書化を容易にするよう利用し得る。しかし、UMLは、更に、実現又は生成の前、及び生成の後に他のシステムをモデリングするよう利用し得る。UMLモデル112は一般に、SUT104の別々の属性を記載又は例証するために使用される1つ又は複数の図を含む。現実的なサイズのシステムの実用的なアプリケーションでは、数十若しくは数百又はそれを超える数のUML図は、SUT104を正確にかつ完全に表すために使用し得る。前述のUML図の一部又は全部は階層的に配置し得る。すなわち、種々のUML図は、他の高位UML図に組み入れ得る。このようにして、高位UML図は、階層型高位UML図における低位UML図それぞれの詳細全てを表示するのでなく、低位UML図を参照することにより、SUT104の視覚的に快い概要を提供し得るこの逆は、高位UML図を構成する低位UML図の詳細全てを含め、表示するよう、階層的に配置されたUMLが肉付けされる平坦化として知られている。更に、特定の実施例では、検証ツールキット102は、UMLモデル112に基づいて、SUT104を確認し、検証するために、実行可能な検証テストスイート118を自動的に生成し得る。例として、検証テストスイート118は、VERILOG、SYSTEMCやJAVAなどの言語で生成し得る。UML図は一般に、システムモデルのどのビューを提供するかに基づいて3つのカテゴリのうちの1つに分類し得る。前述のカテゴリは、一般に、構造図、振る舞い図、及び相互作用図として表し得る。特に、UML2.0は、前述の3つのカテゴリに分けられる別々の13のタイプの図を提供する。前述の図は、図2に示すように階層的に分類することが可能である。構造図又は静止図202は、例として、オブジェクト、属性、動作、及び関係を利用するシステムの静的構造のビューを提供する。構造図202は、例として、クラス図204、コンポーネント図206、複合構造図208,配置図210、オブジェクト図212、及びパッケージ図214を含む。振る舞い図又は動的図216は、オブジェクトの内部状態に対する変更、及びオブジェクト間のコラボレーションを示すことにより、システムの動的な振る舞いを強調する。振る舞い図216は、例として、アクティビティ図218、状態又は状態マシン図220、及びユースケース図222を含む。相互作用図224は、振る舞い図216の部分集合とみなし得る。相互作用図224は、モデリングされているシステムにおける対象のうちのデータ及び制御のフローを強調する。相互作用図は例として、通信図226、相互作用概要図228、タイミング図230、及びシーケンス図232を含む。UMLにおけるシーケンス図は、特に、オブジェクト又はプロセスが互いに、どのようにして動作するか、及びどの順序で動作するかを示す種々の相互作用図である。特に、シーケンス図の主な用途は、相互作用が行われる順番にオブジェクト間の相互作用を示すということである。すなわち、シーケンス図は、特定の所望の結果をもたらすイベントシーケンスを規定するために使用し得る。シーケンス図は、ユースシナリオ又は使用シナリオのロジックを検証し、肉付けするために利用し得る。本明細書及び特許請求の範囲に記載された使用シナリオは、SUT104が使用される潜在的なやり方の記述として定義し得る。特に、使用シナリオは、2つ以上のプロセス間で伝達されるメッセージの特定の順序及び組合せを表し得る。使用シナリオのロジックは、ユースケースの一部であり、場合によっては別のコースであり、基本計画、又は基本計画の一部分に、別の1つ又は複数のシナリオを加えたものによって表されるロジックなどの、ユースケースを介した一パス全体であり、又は、いくつかのユースケースに含まれるロジックを介したパスであり得る。シーケンス図は、ユーザのクラスによって定義される動作の呼び出しを、ユーザが視覚的に進んでいくことを可能にするので、設計の探索を容易にする。シーケンス図は、メッセージシーケンス図MSCのUML構成体とみなし得る。当業者が理解するように、MSCは、プロセス間又はオブジェクト間の相互作用のパターンを表すシナリオを規定するうえで利用し得る。例として、多くのオブジェクト指向システム開発方法論では、ユーザはまず、システムのユースケースを規定し、各ユースケースの一部の特定のインスタンス化が次いで、MSCを使用して表される。シーケンス図は多くの場合、ソフトウェア開発において利用されるが、組織のビジネススタッフは、更に、種々のビジネスオブジェクトがどのようにして相互作用するかを示すことにより、ビジネスが現在、機能しているかを伝達するためにシーケンス図を利用し得る。組織の現在のモデルの文書化に加えて、シーケンス図は、更に、将来のビジネスシステムの実現形態の要件を規定するために使用し得る。シーケンス図の主な用途の1つには、ユースケースとして表される要件から次の、よりフォーマルなレベルの精緻化への遷移におけるものがある。ユースケースは多くの場合、1つ又は複数のシーケンス図に精緻化される。上述したように、新たなシステムの設計における使用に加えて、シーケンス図は、既存の又はレガシーのシステムにおけるオブジェクトがどのようにして現在、相互作用しているかを文書化するために使用し得る。これは例えば、システムを別の個人又は組織に遷移させる場合に有用であり得る。図3は、本開示の実施例による例示的なシーケンス図300を示す。平行の垂直線又はライフライン302は、同時に実行するか、又は動作する別々のプロセス又はオブジェクト304を示す一方、水平の矢印306は、生じる順序で、それらの間で交換されるメッセージを表す時間は垂直線に沿って上から下に流れる。このようにして、シーケンス図は、ランタイムシナリオの規定をグラフィックに提供する。一部のシステムは、固定の少数のオブジェクト又はプロセス間のメッセージの特定のシーケンスで表し得る単純な動的な振る舞いを有する。前述の場合、シーケンス図は完全に、システムの振る舞いを完全に規定し得る。しかし、システムの振る舞いは多くの場合、例として、多くの分岐点例えば、例外が存在している場合、リソース競合などの同期化の課題、又は複雑な反復が存在している場合などのように、複雑度が更にずっと高い。前述の場合には、シーケンス図は、状態図状態チャートなどの他の振る舞い図及び上述したその他の図とともに使用し得る。多くの実用的なシステムでは、メッセージをオブジェクトに送出するために1つ又は複数の条件が満たされなければならない場合が存在する。よって、オブジェクト相互作用をモデリングする場合、ガードやループなどの条件付構成体は、フローを制御するためにUML図にわたって利用し得る。特定の実施例では、UMLシーケンス図などの図中のエレメントは、それぞれ、考えられる条件及び必要な条件に対応する仮のガード、又は必須のガードで規定し得る。特に、仮のガードが実行中に有効である場合、制御がガード直後のオブジェクトに渡され、そうでない場合、この条件が生じるコンテキストを退出し、実行が続き得る。例として、仮ガードは、分岐、及びif-then-else構成体をプログラムするために使用し得る。UMLは、更に、有限ループ及び無限ループを可能にし、これらは、仮ガードと組み合わせると、whileループ及びrepeat-untilループを構成するために使用し得る。対照的に、必須ガード条件は常に真でなければならない。偽と求められる必須ガードに実行が達した場合、これは、SUT104の要件の違反である。UML2.0は、シーケンス図における、より複雑な制御フローを表すために、InteractionUse及びCombinedFragmentなどの構造化された制御又は条件付構成体を導入した。InteractionUseは、一シーケンス図が別のシーケンス図を表すことを可能にする。一般に、CombinedFragmentは、ガードの一形式であり、シーケンス図中の条件付フローを示すために、メッセージの組を併せてグループ化するために使用し得る。CombinedFragmentsは、同時性、選択、及びループなどの各種制御フローを表す。CombinedFragmentは、InteractionOperator、及び1つ又は複数のInteractionOperandを含む。InteractionOperandはInteractionFragmentであり、InteractionConstraintブール表現であり得るを含み得る。InteractionOperatorsは例えば、AlternativeAlt、OptionOpt、Break、Parallel、CriticalRegion、及びLoopを含む。前述のInteractionOperatorsそれぞれの詳細は当該技術分野において知られており、本明細書では更なる詳細は説明しない。条件付構成体を組み入れるこの能力があれば、UML2.0は、ソフトウェア及びハードウェアシステムの形式仕様記述に一層多く使用されている。しかし、形式仕様記述を実現形態に変換することが可能であり、よって、実現形態を体系的にかつ自動的に検査することが可能である方法が存在しない場合、形式仕様記述を使用することの利点が失われ得る設計は大容量であり、人間ベースの検査は誤りがちであり、不完全なことがあるからである。実現形態が仕様要件を満たしているということを証明することが可能でない場合、仕様に対して実現形態を検査することは特に重要である例えば、実現形態が、体系的に、かつ、証明して正しいやり方で、仕様から生成されない場合、このことがあてはまり得る。そういうものとして、実現形態を検査するために形式仕様記述例えば、UMLから検証スイートを生成する方法が望ましい。よって、上述のように、検証は基本的に、3つの層モデル抽出、モデル縮退、及びモデル検証を備え得る。各層は、計算集約的であり、実行するためにかなりの時間がかかり得る。以下に更に詳細に説明するように、計算時間を削減するために、検証を行うために必要な種々の計算スレッドを、1つ又は複数の計算リソース例えば、1つ又は複数のプロセッサ、1つ又は複数のコンピュータ等に動的に割り当てて、前述のスレッドの並列計算を可能にし得る。図4は、本開示の実施例による、プロセススケジューラ402の例示的な環境400を示す。図示したように、プロセススケジューラ402は、モデル抽出層404、モデル縮退層406、及びモデル検証層408を静的に解析し得る。例えば、モデル抽出層404は、モデル生成器110の解析によって解析し得る。別の例として、モデル縮退層406は、モデル112の解析によって解析し得る。更なる例として、モデル検証層408は検証ツールキット102の解析によって解析し得る。種々の解析は、データ構造を互いに共有しない種々の計算スレッド410を識別し得、かつ/又は、各スレッド410によって必要とされる計算リソース例えば、計算時間、処理要件、メモリ要件等を算出し得、前述のスレッドを複数のリソース412例えば、プロセッサ、計算装置等に、計算スレッドの全体的な計算要件の複数のリソース間でのバランスが均一にとれるように分散し得る。更に図示したように、モデル縮退層406の解析の特定の例として、プロセススケジューラ402は、モデル112の特定の図例えば、シーケンス図232、状態マシン図220等を解析し得、前述の解析を行ううえで、前述の図から種々の実行経路を抽出し得る。ここで、各経路は、図を横切る状態シーケンスを含み得る。一部の実施例では、考えられる実行経路それぞれが表されるように実行経路の網羅的な集合を抽出し得る。前述の経路毎に、プロセススケジューラ402は、経路を表すスレッドを実行するために必要な計算リソースを算出し得、かつ/又は、前述のスレッドが、別のスレッドによって使用されるデータ構造を必要とするか否かを判定し得る。別のスレッドによって使用されるデータ構造を必要としないスレッド410毎に、プロセス素ジューラ402は、前述の分散スレッド全てによって必要とされる計算リソースのバランスがほぼとれているように前述のスレッド410をリソース412に分散し得る。よって、スレッド410は、検証に関連付けられた計算時間を削減するために、リソース412間で動的に供給し得る。更に、特定の実施例では、リソース412は、アプリケーション検証の実行がクラウドで行われることを可能にする、クラウド計算環境の構成部分であり得る。図5は、本開示の実施例による、例示的なコンピュータシステム600を示す。特定の実施例では、1つ又は複数のコンピュータシステム600は、本明細書及び特許請求の範囲に記載又は例証された1つ又は複数の方法のうちの1つ又は複数の工程を行う。特定の実施例では、1つ又は複数のコンピュータシステム600は、本明細書及び特許請求の範囲に記載又は例証された機能を提供する。特定の実施例では、1つ又は複数のコンピュータシステム600上で実行されるソフトウェアは、本明細書及び特許請求の範囲に記載又は例証された1つ又は複数の方法のうちの1つ又は複数の工程を行うか、又は、本明細書及び特許請求の範囲記載の機能を提供する。特定の実施例は、1つ又は複数のコンピュータシステム600の1つ又は複数の部分を含む。本開示は、何れかの適切な数のコンピュータシステム600を想定している。本開示は、何れかの適切な物理的形式を呈するコンピュータシステム600を想定している。限定でなく、例として、コンピュータシステム600は、組み込み型コンピュータシステム、システムオンチップSOC、シングルボードコンピュータシステムSBC例えば、コンピュータオンモジュールCOM又はシステムオンモジュールSOM、デスクトップ型コンピュータシステム、ラップトップ型又はノートブック型コンピュータシステム、インタアクティブキオスク、汎用コンピュータ、コンピュータシステムのメッシュ、携帯電話機、携帯情報端末PDA、サ―バ、又は、前述の2つ以上の組合せであり得る。コンピュータシステム600は、適宜、1つ又は複数のコンピュータシステム600を含み、ユニタリー型であっても分散型であってもよく、複数の場所にまたがってもよく、複数のマシンにまたがってもよく、クラウド1つ又は複数のネットワーク内の1つ又は複数のクラウド構成部分を含み得るに常駐していてもよい。1つ又は複数のコンピュータシステム600は、適宜、本明細書及び特許請求の範囲に記載されたか又は例証された1つ又は複数の方法のうちの1つ又は複数の工程を、実質的な空間制約又は時間制約なしで行い得る。限定でなく、例として、1つ又は複数のコンピュータシステム600は、本明細書及び特許請求の範囲記載の1つ又は複数の方法のうちの1つ又は複数の工程をリアルタイムで又はバッチモードで行い得る。1つ又は複数のコンピュータシステム600は、適宜、本明細書及び特許請求の範囲に記載又は例証された1つ又は複数の方法のうちの1つ又は複数の工程を別々の時点で、又は別々の場所で行い得る。特定の実施例では、コンピュータシステム600は、プロセッサ602、メモリ604、記憶装置606、入出力I/Oインタフェース608、通信インタフェース610、及びバス612を含む。本開示は、特定の構成において特定数の特定の構成部分を有する特定のコンピュータシステムを記載し、例証しているが、本開示は、何れかの適切な構成における何れかの適切な数の何れかの適切な構成部分を有する何れかの適切なコンピュ―タシステムを想定している。特定の実施例では、プロセッサ602は、コンピュータプログラムを構成するものなどの、命令を実行するためのハードウェアを含む。限定でなく例として、プロセッサ602は、命令を実行するために、内部レジスタ、内部キャッシュ、メモリ604、又は記憶装置606から命令を取り出し又はフェッチし、デコードし、実行し、次いで、1つ又は複数の結果を内部レジスタ、内部キャッシュ、メモリ604,又は記憶装置606に書き込み得る。特定の実施例では、プロセッサ602は、データ、命令、又はアドレスのために1つ又は複数の内部キャッシュを含み得る。本開示は、適宜、何れかの適切な数の何れかの適切な内部キャッシュを含むプロセッサ602を想定している。限定でなく、例として、プロセッサ602は、1つ又は複数の命令キャッシュ、1つ又は複数のデータキャッシュ、及び1つ又は複数のトランスレーションルックアサイドバッファTLBを含み得る。命令キャッシュ内の命令は、メモリ604内又は記憶装置606内の命令の複製であり得、命令キャッシュはプロセッサ602による前述の命令の取り出しを高速化し得る。データキャッシュ内のデータは、プロセッサ602で命令が処理する対象の、メモリ604内又は記憶装置606内のデータの複製、プロセッサ602で実行するその後の命令によるアクセスのための、又は、メモリ604若しくは記憶装置606への書き込みのための、プロセッサ602で実行される先行する命令の結果、又は、他の適切なデータであり得る。データキャッシュは、プロセッサ602による読み出し又は書き込みの動作を高速化し得る。TLBは、プロセッサ602のための仮想アドレス変換を高速化し得る。特定の実施例では、プロセッサ602は、データ、命令、又はアドレスの1つ若しくは複数の内部レジスタを含み得る。本開示は、何れかの適切な数の何れかの適切な内部レジスタを適宜含むプロセッサ602を想定している。プロセッサ602は、適宜、1つ又は複数の論理演算装置ALUを含むか、マルチコアプロセッサであるか、又は1つ又は複数のプロセッサ602を含み得る。本開示は特定のプロセッサを記載し、例証するが、本開示は何れかの適切なプロセッサを想定している。特定の実施例では、メモリ604は、プロセッサ602が実行するための命令、又はプロセッサ602が処理するためのデータを記憶する主メモリを含む。限定でなく例として、コンピュータシステム600は、記憶装置606、又は例えば、別のコンピュータシステム600などの別のソースからメモリ604に命令をロードし得る。プロセッサ602は次いで、メモリ604から内部レジスタ又は内部キャッシュに命令をロードし得る。命令を実行するために、プロセッサ602は、内部レジスタ又は内部キャッシュから命令を取り出し、デコードし得る。命令の実行中又は実行後、プロセッサ602は、中間結果又は最終結果であり得る1つ若しくは複数の結果を内部レジスタ又は内部キャッシュに書き込み得る。プロセッサ602は、前述の結果のうちの1つ又は複数をメモリ604に書き込み得る。特定の実施例では、プロセッサ602は、1つ又は複数の内部レジスタ内若しくは内部キャッシュ内、又はメモリ604内の命令のみを実行し、記憶装置606内又はそれ以外の場所内の命令は実行せず、1つ又は複数の内部レジスタ内若しくは内部キャッシュ内、又はメモリ604内のデータのみを処理する記憶装置606内又はそれ以外の場所内の命令は実行しない。アドレスバス及びデータバスをそれぞれが含み得る1つ又は複数のメモリバスは、プロセッサ602をメモリ604に結合し得る。バス612は、以下に説明するように、1つ又は複数のメモリバスを含み得る。特定の実施例では、1つ又は複数のメモリ管理装置MMUはプロセッサ602とメモリ604との間に常駐し、プロセッサ602によって要求されるメモリ604に対するアクセスを容易にする。特定の実施例では、メモリ604はランダムアクセスメモリRAMを含む。このRAMは、揮発性メモリであり得る。このRAMは、適宜、ダイナミックRAMDRAM又はスタティックRAMSRAMであり得る。更に、このRAMは、適宜、単一ポートのRAM又はマルチポートのRAMであり得る。本明細書及び特許請求の範囲は、何れかの適切なRAMを想定している。メモリ604は、適宜、1つ又は複数のメモリ604を含み得る。本開示は特定のメモリを記載し、例証しているが、本開示は何れかの適切なメモリを想定している。特定の実施例では、記憶装置606は、データ又は命令用の大容量記憶装置を含む。限定でなく、例として、記憶装置606は、HDD、フロッピー登録商標ディスクドライブ、フラッシュメモリ、光ディスク、光磁気ディスク、磁気テープ、若しくは、ユニバーサルシリアルバスUSBドライブ、又は前述の2つ以上の組合せを含み得る。記憶装置606は、適宜、取り外し可能な媒体、又は取り外し可能でない若しくは固定の媒体を含み得る。記憶装置606は、適宜、コンピュータシステム600の内部にあっても外部にあってもよい。特定の実施例では、記憶装置606は、不揮発性のソリッドステートメモリである。特定の実施例では、記憶装置606はリードオンリメモリROMを含む。このROMは、適宜、マスクプログラムされたROM、プログラム可能なROMPROM、消去可能なPROMEPROM、電気的に消去可能なPROMEEPROM、電気的に改変可能なROMEAROM、若しくは、フラッシュメモリ、又は、前述の2つ以上の組合せであり得る。本開示は、何れかの適切な物理的形式を呈する大容量記憶装置606を想定している。記憶装置606は、適宜、プロセッサ602と記憶装置606との間の通信を容易にする1つ又は複数の記憶制御装置を含み得る。記憶装置606は、適宜、1つ又は複数の記憶装置606を含み得る。本開示は特定の記憶装置を記載し、例証しているが、本開示は何れかの適切な記憶装置を想定している。特定の実施例では、I/Oインタフェース608は、コンピュータシステム600と、1つ又は複数のI/O装置との間の通信のための1つ又は複数のインタフェースを提供するハードウェア、ソフトウェア、又は両方を含む。コンピュータシステム600は、適宜、前述のI/O装置のうちの1つ又は複数を含み得る。前述のI/O装置の1つ又は複数は、個人とコンピュータシステム600との間の通信を可能にし得る。限定でなく、例として、I/O装置は、キーボード、キーパッド、マイクロフォン、モニタ、プリンタ、スキャナ、スピーカ、スチルカメラ、スタイラス、タブレット、タッチスクリーン、トラックボール、ビデオカメラ、別の適切なI/O装置、又は前述の2つ以上の組合せを含み得る。I/O装置は1つ又は複数のセンサを含み得る。本開示は、何れかの適切なI/O装置、及び上記何れかの適切なI/O装置との何れかの適切なI/Oインタフェース608を想定している。I/Oインタフェース608は、適宜、プロセッサ602が前述のI/O装置のうちの1つ又は複数を駆動させることを可能にする1つ又は複数の装置若しくはソフトウェアドライバを含み得る。I/Oインタフェース608は、適宜、1つ又は複数のI/Oインタフェース608を含み得る。本開示は特定のI/Oインタフェースを記載し、例証しているが、本開示は何れかの適切なI/Oインタフェースを想定している。特定の実施例では、通信インタフェース610は、コンピュータシステム600と、1つ若しくは複数の他のコンピュータシステム600、又は1つ若しくは複数のネットワークとの間の例えば、パケットベースの通信などの通信のための1つ又は複数のインタフェースを提供するハードウェア、ソフトウェア、又は両方を含む。限定でなく例として、通信インタフェース610は、イーサネット登録商標若しくは他の有線ベースのネットワークと通信するためのネットワークインタフェースコントローラNIC若しくはネットワークアダプタ、又は、ワイファイネットワークなどの無線ネットワークと通信するための無線アダプタ若しくは無線NICWNICを含み得る。この開示は、何れかの適切なネットワーク、及び上記何れかの適切なネットワークとの何れかの適切な通信インタフェース610を想定している。限定でなく例として、コンピュータシステム600は、アドホックネットワーク、パーソナルエリアネットワークPAN、ローカルエリアネットワークLAN、ワイドエリアネットワークWAN、メトロポリタンエリアネットワークMAN、若しくは、インターネットの1つ若しくは複数の部分、又は、前述の2つ以上の組合せと通信し得る。前述の1つ又は複数のネットワークの1つ又は複数の部分は有線であっても無線であってもよい。例として、コンピュータシステム600は、例えば、ブルートゥースWPANなどの無線PANWPAN、ワイファイネットワーク、ワイマックスネットワーク、例えば、ジーエスエムGSMネットワークなどの携帯電話ネットワーク、若しくは他の適切な無線ネットワーク、又は前述のうちの2つ以上の組合せと通信し得る。コンピュータシステム600は、適宜、前述のネットワークの何れかのための、何れかの適切な通信インタフェース610を含み得る。通信インタフェース610は、適宜、1つ又は複数の通信インタフェース610を含み得る。本開示は特定の通信インタフェースを記載し、例証しているが、本開示は何れかの適切な通信インタフェースを想定している。特定の実施例では、バス612は、コンピュータシステム600の構成部分を互いに結合するハードウェア、ソフトウェア、又は両方を含む。限定でなく、例として、バス612は、アクセラレーテッドグラフィクスポートAGP若しくは他のグラフィクスバス、拡張業界標準アーキテクチャEISAバス、フロントサイドバスFSB、ハイパートランスポートHT相互接続、業界標準アーキテクチャISAバス、インフィニバンド相互接続、低ピンカウントLPCバス、メモリバス、マイクロチャネルアーキテクチャMCAバス、周辺装置相互接続PCIバス、PCIエクスプレスPCI-Xバス、シリアル高度技術アタッチメントSATAバス、ビデオ電子標準協会局所VLBバス、若しくは、別の適切なバス、又は、前述の2つ以上の組合せを含み得る。バス612は、適宜、1つ又は複数のメモリ612を含み得る。本開示は特定のバスを記載し、例証しているが、本開示は何れかの適切なバス又は相互接続を想定している。本明細書及び特許請求の範囲では、コンピュータ読み取り可能な記憶媒体への参照は、1つ又は複数の有形のコンピュータ読み取り可能な記憶媒体を有する構造を含む。限定でなく、例として、コンピュータ読み取り可能な記憶媒体は、適宜、例えば、フィールドプログラマブルゲートアレイFPGA又は特定用途向ICASICなどの半導体ベース又は他の集積回路IC、ハードディスク、HDD、ハイブリッドハードドライブHHD、光ディスク、光ディスクドライブODD、光磁気ディスク、光磁気ドライブ、フロッピー登録商標ディスク、フロッピー登録商標ディスクドライブFDD、磁気テープ、ホログラフィック記憶媒体、ソリッドステートドライブSSD、RAMドライブ、セキュアなディジタルカード、セキュアなディジタルドライブ、若しくは、別の適切なコンピュータ読み取り可能な媒体、又は、前述のうちの2つ以上の組合せを含み得る。本明細書及び特許請求の範囲では、コンピュータ読み取り可能な記憶媒体への言及は、米国特許法第101条の特許の保護の対象でない何れかの媒体である。本明細書及び特許請求の範囲では、コンピュータ読み取り可能な記憶媒体への言及は、米国特許法第101条の下で特許の保護の対象でない範囲で本来的には、伝搬する電気信号又は電磁気信号などの信号伝送の一時的な形態を除く。本開示は、何れかの適切な記憶装置を実現する1つ又は複数のコンピュータ読み取り可能な記憶媒体を想定している。特定の実施例では、コンピュータ読み取り可能な記憶媒体は、適宜、例えば、1つ若しくは複数の内部レジスタ又はキャッシュなどの、プロセッサ602の1つ若しくは複数の部分、メモリ604の1つ若しくは複数の部分、記憶装置606の1つ若しくは複数の部分、又は、前述の組合せを実現する。特定の実施例では、コンピュータ読み取り可能な記憶媒体はRAM又はROMを実現する。特定の実施例では、コンピュータ読み取り可能な記憶媒体は揮発性メモリ又はパーシスタントメモリを実現する。特定の実施例では、1つ又は複数のコンピュータ読み取り可能な記憶媒体はソフトウェアを実施する。本明細書及び特許請求の範囲では、ソフトウェアへの言及は、適宜、1つ若しくは複数のアプリケーション、バイトコード、1つ若しくは複数のコンピュータプログラム、1つ若しくは複数の実行可能形式、1つ若しくは複数の命令、ロジック、マシンコード、1つ若しくは複数のスクリプト、又はソースコード等を包含し得る。特定の実施例では、ソフトウェアは、1つ又は複数のアプリケーションプログラミングインタフェースAPIを含む。本明細書及び特許請求の範囲は、何れかの適切なプログラミング言語、又はプログラミング言語の組合せで記述されたか、又はその他のやり方で表現された何れかの適切なソフトウェアを想定している。特定の実施例では、ソフトウェアは、ソースコード又はオブジェクトコードとして表現される。特定の実施例では、ソフトウェアは、例えば、C、パール、又はその適切な拡張などの高水準プログラミング言語で表現される。特定の実施例では、ソフトウェアは、アセンブラ言語又はマシンコードなどの低水準プログラミング言語で表現される。特定の実施例では、ソフトウェアはJAVAで表現される。特定の実施例では、ソフトウェアは、ハイパテキストマークアップ言語HTML、拡張マークアップ言語XML、又は他の適切なマークアップ言語で表現される。例示的な環境100の構成部分はロジック及び/又はその他の適切な構成要素を含み得る。ロジックは、構成部分の動作を行い、例えば、入力から出力を生成する旨の命令を実行する。ロジックは、ハードウェア、ソフトウェア、及び/又は他のロジックを含み得る。ロジックは、1つ又は複数の有形なコンピュータ読み取り可能な記憶媒体にコード化され得、コンピュータによって実行されると動作を行い得る。プロセッサなどの特定のロジックは構成部分の動作を管理し得る。プロセッサの例には、1つ若しくは複数のコンピュータ、1つ若しくは複数のマイクロプロセッサ、1つ若しくは複数のアプリケーション、及び/又は他のロジックが含まれる。本発明は、特定の構成部分を識別して、詳細に説明してきたが、種々の変更及び修正を当業者に連想させ得、更に、本発明が、特許請求の範囲記載の範囲内に明らかに収まる前述の何れの変更及び修正も包含することが意図されている。更に、開示された特定の処理フローに関し、フロー内に記載された工程は何れも、本発明の範囲から逸脱しない限り、修正し、強化し、又は割愛し得る。更に、工程は、本発明の範囲から逸脱しない限り、何れかの適切な順序で、又は同時に行い得る。本開示は、適宜、当業者が理解するであろう、本明細書及び特許請求の範囲記載の例示的な実施例に対する変更、置換、変形、改変、及び修正全てを包含する。同様に、特許請求の範囲は、当業者が理解するであろう、本明細書及び特許請求の範囲記載の例示的な実施例に対する変更、置換、変形、改変、及び修正全てを包含する。付記1検証ツールキット環境を静的に解析する工程と、前記検証ツールキット環境の解析に基づいて、データ構造を互いに共有しない複数の計算スレッドを識別する工程と、前記計算スレッドの計算要件を算出する工程と、前記計算スレッドの全体的な計算要件が複数のリソース間でほぼ均一にバランスがとられるように複数のリソースの間で前記スレッドを分散する工程とを含むことを特徴とする方法。付記2前記検証ツールキット環境を静的に解析する工程は、前記検証ツールキット環境のモデル生成器を解析する工程と、前記モデル生成器によって生成されるモデルを解析する工程と、前記検証ツールキット環境の検証ツールキットを解析する工程とを含むことを特徴とする付記1に記載の方法。付記3前記検証ツールキット環境を静的に解析する工程は、前記検証ツールキット環境から生成されるモデルから複数の実行経路を抽出する工程を含み、互いにデータ構造を共有しない複数の計算スレッドを識別する工程は、互いにデータ構造を共有しない前記複数の実行経路それぞれを表すスレッドを識別する工程を含み、前記計算スレッドの計算要件を算出する工程は、前記実行経路を表す前記計算スレッドを実行するために必要な計算リソースを算出する工程を含むことを特徴とする付記1に記載の方法。付記4計算要件は、計算時間、処理要件、及びメモリ要件の少なくとも1つを含むことを特徴とする付記1に記載の方法。付記5前記リソースはクラウド計算環境の構成部分であることを特徴とする付記1に記載の方法。付記6実行されると、検証ツールキット環境を静的に解析する機能と、前記検証ツールキット環境の解析に基づいて、データ構造を互いに共有しない複数の計算スレッドを識別する機能と、前記計算スレッドの計算要件を算出する機能と、前記計算スレッドの全体的な計算要件が複数のリソース間でほぼ均一にバランスがとられるように複数のリソースの間で前記スレッドを分散する機能とを行うよう動作可能なソフトウェアをコード化したことを特徴とする1つ又は複数のコンピュータ読み取り可能な有形の記憶媒体。付記7前記検証ツールキット環境を静的に解析する機能は、前記検証ツールキット環境のモデル生成器を解析する機能と、前記モデル生成器によって生成されるモデルを解析する機能と、前記検証ツールキット環境の検証ツールキットを解析する機能とを含むことを特徴とする付記6に記載の媒体。付記8前記検証ツールキット環境を静的に解析する機能は、前記検証ツールキット環境から生成されるモデルから複数の実行経路を抽出する機能を含み、互いにデータ構造を共有しない複数の計算スレッドを識別する機能は、互いにデータ構造を共有しない前記複数の実行経路それぞれを表すスレッドを識別する機能を含み、前記計算スレッドの計算要件を算出する機能は、前記実行経路を表す前記計算スレッドを実行するために必要な計算リソースを算出する機能を含むことを特徴とする付記6に記載の媒体。付記9計算要件は、計算時間、処理要件、及びメモリ要件の少なくとも1つを含むことを特徴とする付記6に記載の媒体。付記10前記リソースはクラウド計算環境の構成部分であることを特徴とする付記6に記載の媒体。付記11検証ツールキット環境を静的に解析するロジックと、前記検証ツールキット環境の解析に基づいて、データ構造を互いに共有しない複数の計算スレッドを識別するロジックと、前記計算スレッドの計算要件を算出するロジックと、前記計算スレッドの全体的な計算要件が複数のリソース間でほぼ均一にバランスがとられるように複数のリソースの間で前記スレッドを分散するロジックとを備えることを特徴とするシステム。付記12前記検証ツールキット環境を静的に解析するロジックは、前記検証ツールキット環境のモデル生成器を解析するロジックと、前記モデル生成器によって生成されるモデルを解析するロジックと、前記検証ツールキット環境の検証ツールキットを解析するロジックとを含むことを特徴とする付記11に記載のシステム。付記13前記検証ツールキット環境を静的に解析するロジックは、前記検証ツールキット環境から生成されるモデルから複数の実行経路を抽出するロジックを含み、互いにデータ構造を共有しない複数の計算スレッドを識別するロジックは、互いにデータ構造を共有しない前記複数の実行経路それぞれを表すスレッドを識別するロジックを含み、前記計算スレッドの計算要件を算出するロジックは、前記実行経路を表す前記計算スレッドを実行するために必要な計算リソースを算出するロジックを含むことを特徴とする付記11に記載のシステム。付記14計算要件は、計算時間、処理要件、及びメモリ要件の少なくとも1つを含むことを特徴とする付記11に記載のシステム。付記15前記リソースはクラウド計算環境の構成部分であることを特徴とする付記11に記載のシステム。"