(57)【要約】【課題】  ネットワーク検証のための技術を開示する。【解決手段】  ネットワーク検証方法は、データプレーンの中の複数のスイッチのうちの各スイッチのための１又は複数の転送テーブルを含むデータプレーンを識別するステップを有して良い。方法は、データプレーンの１又は複数の転送テーブルの転送ルールのブール結合を表すために、データプレーンの転送動作表現を生成するステップを更に有して良い。さらに、方法は、データプレーンの中の１又は複数のエラーを検出するために、データプレーンの転送動作表現を１又は複数のネットワーク特性と比較するステップを有して良い。【選択図】  図８
2018046549.tif 000002
【特許請求の範囲】
【請求項１】
ネットワーク検証方法であって、
データプレーンの中の複数のスイッチのうちの各スイッチのための１又は複数の転送テーブルを有する前記データプレーンを識別するステップと、
前記データプレーンの前記１又は複数の転送テーブルの転送ルールのブール結合を表すために、前記データプレーンの転送動作表現を生成するステップと、
前記データプレーンの中の１又は複数のエラーを検出するために、前記データプレーンの前記転送動作表現を１又は複数のネットワーク特性と比較するステップと、
を有する方法。
【請求項２】
前記転送動作表現を生成するステップは、前記１又は複数の転送テーブルの転送ルールのブール結合を表すために、複数の最小単位を含む前記転送動作表現を生成するステップを有する、請求項１に記載の方法。
【請求項３】
前記転送動作表現を生成するステップは、前記データプレーンの論理表現を生成するステップを有する、請求項１に記載の方法。
【請求項４】
転送ルールが前記複数のスイッチのうちのスイッチの転送テーブルに追加されることに応答して更新されたデータプレーンを識別するステップと、
前記更新されたデータプレーンの別の転送動作表現を生成するステップと、
前記更新されたデータプレーンの中の１又は複数のエラーを検出するために、前記更新されたデータプレーンの前記別の転送動作表現を前記１又は複数のネットワーク特性と比較するステップと、
を更に有する請求項１に記載の方法。
【請求項５】
前記データプレーンの前記転送動作表現を生成するステップは、辺ラベル付きグラフを生成するステップを有し、前記辺ラベル付きグラフの各エッジは、前記データプレーンの転送ルールのインターネットプロトコル（ＩＰ）プレフィックスを表すために、１又は複数の最小単位に関連付けられる、請求項１に記載の方法。
【請求項６】
転送ルールが前記１又は複数の転送テーブルのうちの転送テーブルから削除されることに応答して、更新辺ラベル付きグラフを生成するために、前記辺ラベル付きグラフを更新するステップ、を更に有する請求項５に記載の方法。
【請求項７】
転送ルールが前記１又は複数の転送テーブルのうちの転送テーブルに追加されることに応答して、更新辺ラベル付きグラフを生成するために、前記辺ラベル付きグラフを更新するステップ、を更に有する請求項５に記載の方法。
【請求項８】
前記１又は複数の転送テーブルの１又は複数の変更に応答して、前記更新辺ラベル付きグラフを増加的に更新するステップ、を更に有する請求項７に記載の方法。
【請求項９】
前記転送動作表現を１又は複数のネットワーク特性と比較するステップは、前記転送動作表現を１又は複数のネットワーク到達可能性特性と比較するステップを有する、請求項１に記載の方法。
【請求項１０】
命令を有する１又は複数の非一時的コンピュータ可読媒体であって、前記命令は、１又は複数のプロセッサにより実行されると、前記１又は複数のプロセッサに動作を実行させるよう構成され、前記動作は、
データプレーンの中の複数のスイッチのうちの各スイッチのための１又は複数の転送テーブルを有する前記データプレーンを識別するステップと、
前記データプレーンの前記１又は複数の転送テーブルの転送ルールのブール結合を表すために、前記データプレーンの転送動作表現を生成するステップと、
前記データプレーンの中の１又は複数のエラーを検出するために、前記データプレーンの前記転送動作表現を１又は複数のネットワーク特性と比較するステップと、
を有する、コンピュータ可読媒体。
【請求項１１】
前記動作は、
転送ルールが前記複数のスイッチのうちのスイッチの転送テーブルに追加されることに応答して更新されたデータプレーンを識別するステップと、
前記データプレーンの別の転送動作表現を生成するステップと、
前記更新されたデータプレーンの中の１又は複数のエラーを検出するために、前記川迫インされたデータプレーンの前記別の転送動作表現を前記１又は複数のネットワーク特性と比較するステップと、
を更に有する、請求項１０に記載のコンピュータ可読媒体。
【請求項１２】
前記データプレーンの前記転送動作表現を生成するステップは、辺ラベル付きグラフを生成するステップを有し、前記辺ラベル付きグラフの各エッジは、前記データプレーンの転送ルールのインターネットプロトコル（ＩＰ）プレフィックスを表すために、１又は複数の最小単位に関連付けられる、請求項１０に記載のコンピュータ可読媒体。
【請求項１３】
前記動作は、転送ルールが前記１又は複数の転送テーブルのうちの転送テーブルに追加されることに応答して、更新辺ラベル付きグラフを生成するために、前記辺ラベル付きグラフを更新するステップ、を更に有する、請求項１２に記載のコンピュータ可読媒体。
【請求項１４】
前記動作は、前記１又は複数の転送テーブルの１又は複数の変更に応答して、前記更新辺ラベル付きグラフを増加的に更新するステップ、を更に有する、請求項１３に記載のコンピュータ可読媒体。
【請求項１５】
前記動作は、転送ルールが前記複数のスイッチのうちのスイッチの転送テーブルに追加されることに応答して、前記転送動作表現を更新するステップ、を更に有する、請求項１０に記載のコンピュータ可読媒体。
【請求項１６】
ネットワーク検証システムであって、
１又は複数のプロセッサ、
を有し、前記１又は複数のプロセッサは、
データプレーンの中の複数のスイッチのうちの各スイッチのための１又は複数の転送テーブルを有する前記データプレーンを識別し、
前記データプレーンの前記１又は複数の転送テーブルの転送ルールのブール結合を表すために、前記データプレーンの転送動作表現を生成し、
前記データプレーンの中の１又は複数のエラーを検出するために、前記データプレーンの前記転送動作表現を１又は複数のネットワーク特性と比較する、
よう構成される、システム。
【請求項１７】
前記１又は複数のプロセッサは、
転送ルールが前記複数のスイッチのうちのスイッチの転送テーブルに追加されることに応答して更新されたデータプレーンを識別し、
前記更新されたデータプレーンの別の転送動作表現を生成し、
前記更新されたデータプレーンの中の１又は複数のエラーを検出するために、前記更新されたデータプレーンの前記別の転送動作表現を前記１又は複数のネットワーク特性と比較する、
よう更に構成される、請求項１６に記載のシステム。
【請求項１８】
前記データプレーンの前記転送動作表現は、辺ラベル付きグラフを有し、前記辺ラベル付きグラフの各エッジは、前記データプレーンの転送ルールのインターネットプロトコル（ＩＰ）プレフィックスを表すために、１又は複数の最小単位に関連付けられる、請求項１６に記載のシステム。
【請求項１９】
前記１又は複数のプロセッサは、前記１又は複数の転送テーブルの１又は複数の変更に応答して、更新辺ラベル付きグラフを生成するために、前記辺ラベル付きグラフを更新するよう更に構成される、請求項１８に記載のシステム。
【請求項２０】
前記１又は複数の変更は、前記１又は複数の転送テーブルのうちの少なくとも１つの転送テーブルに１又は複数の転送ルールを追加することを有する、請求項１９に記載のシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本願明細書で議論される実施形態は、ネットワーク検証に関する。
【背景技術】
【０００２】
ソフトウェア定義ネットワーク（software−defined  network：ＳＤＮ）は、１又は複数の要件（例えば、ネットワーク管理者の要件）に従い市販の又はオープンソースツールにより自動化され得る一連のネットワークオブジェクト（例えば、スイッチ、ルータ、ファイアウォール）を有し得る。ネットワーク機能の仮想化（Network  functions  virtualization：ＮＦＶ）は、専用ハードウェアにより実行されるネットワーク機能（例えば、ルータ、ファイアウォール、負荷バランサにより実行される機能）を仮想化環境へ移行することを含む。
【０００３】
本願明細書で請求される主題は、上述のような欠点を解決する実施形態や上述のような環境でのみ機能する実施形態に限定されない。むしろ、この背景技術は、単に、本願明細書に記載される複数の実施形態が実施される技術分野の一例を説明するために提供される。
【発明の概要】
【０００４】
本開示の１又は複数の実施形態は、ネットワーク仮想化方法を含み得る。当該方法は、データプレーンの中の複数のスイッチのうちの各スイッチのための１又は複数の転送テーブルを含むデータプレーンを識別するステップを有して良い。方法は、データプレーンの１又は複数の転送テーブルの転送ルールのブール結合を表すために、データプレーンの転送動作表現を生成するステップを更に有して良い。さらに、方法は、データプレーンの中の１又は複数のエラーを検出するために、データプレーンの転送動作表現を１又は複数のネットワーク特性と比較するステップを有して良い。
【０００５】
実施形態の目的及び利点が理解され、少なくとも特に特許請求の範囲で指摘された要素、特徴及び組合せを用いて達成されるだろう。上述の全体的説明及び以下の詳細な説明の両方は、例示的であり及び説明のためであり、本発明の範囲を限定しない。
【図面の簡単な説明】
【０００６】
例示的な実施形態は、添付の図面を用いて、更なる特異性及び詳細事項と共に記載され説明される。
【図１】ネットワーク検証のために使用され得る例示的なシステムを示す。
【図２】ネットワーク検証のために使用され得る例示的なコンポーネントを示す。
【図３】ネットワークの中のエラーを検出する例示的な方法のフローチャートである。
【図４Ａ】例示的なネットワークトポロジを示す。
【図４Ｂ】図４Ａのネットワークトポロジに関連する例示的な転送グラフを示す。
【図４Ｃ】図４Ａのネットワークトポロジに関連する例示的な転送グラフを示す。
【図４Ｄ】図４Ａのネットワークトポロジに関連する例示的な転送グラフを示す。
【図５】例示的な辺ラベル付きグラフを示す。
【図６Ａ】例示的な転送グラフを示す。
【図６Ｂ】種々の転送ルールの例示的な間隔を示す。
【図６Ｃ】例示的な辺ラベル付きグラフを示す。
【図７Ａ】例示的な転送グラフを示す。
【図７Ｂ】種々の転送ルールの例示的な間隔を示す。
【図７Ｃ】例示的な辺ラベル付きグラフを示す。
【図７Ｄ】例示的な辺ラベル付きグラフを示す。
【図８】ネットワークを検証する例示的な方法のフローチャートである。
【図９】ネットワークトポロジ及び転送テーブルを示す。
【図１０】種々の転送ルールの例示的な最小単位を示す。
【図１１】例示的なハッセ図を示す。
【図１２Ａ】転送ルールをネットワークに挿入する例示的な方法のフローチャートを示す。
【図１２Ｂ】転送ルールをネットワークに挿入する例示的な方法のフローチャートを示す。
【図１３Ａ】転送ルールをネットワークから削除する例示的な方法のフローチャートを示す。
【図１３Ｂ】転送ルールをネットワークから削除する例示的な方法のフローチャートを示す。
【図１４】例示的なコンピューティングシステムのブロック図である。
【発明を実施するための形態】
【０００７】
リアルタイムネットワーク検証は、データプレーン上のネットワーク全体に渡る到達可能性不変条件に対する違反を、自動的に検出できる。実用において有用であるために、これらの違反は、間違った警報を上げることなく、ほぼミリ秒程度で検出できる。
【０００８】
とめどもなく続く相互接続された世界では、ネットワークトラフィックは、益々多様であり、要求が高く、小型の日常の装置間の通信から大規模データセンタまでに及ぶ。この多様性は、プログラマブルネットワークスイッチ上に構築される、新しいオープンネットワーキングアーキテクチャの設計及び迅速な採用を駆動している。これは、制御プレーンをデータプレーンから分離することを可能にする。この分離は、ネットワーク関連バグを検出するための綿密なネットワーク分析を含む、革新への興味深い道を切り開く。これらのバグの発見は、自動的に、１又は複数の課題を提起し得る。
【０００９】
例えば、制御プレーンは標準的にチューリング完全プログラムであるので、制御プレーンにバグが存在しないことを自動的に証明する問題は、通常、決定不要である。しかしながら、制御プレーンにより生成されるデータプレーンは、自動的に分析できる。データプレーンにおける到達可能性特性を調べる問題は、通常、ＮＰ困難であるが、問題は、ネットワークスイッチがインターネットプロトコル（ＩＰ）プレフィックスを照合することによりパケットを転送するだけの限られた場合に多項式時間可解になるが、しかし珍しいことではない。この論理的事実は、間違った警報を上げることなくほぼミリ秒程度でネットワーク全体に渡るデータプレーン上の違反を自動的に検出できるリアルタイムネットワーク検証ツールの根拠になる。
【００１０】
従来のシステムは、２つのデータプレーンスナップショットの間に生じる変化を調べることのみによって、増加的にネットワーク検証を実行し得る。具体的には、従来のシステムは、２つの観察を利用する。つまり、（ｉ）ネットワークの小部分のみがデータプレーンに対する標準的な変化により影響を受ける傾向があること、（ｉｉ）ネットワーク全体の全ての転送ルールの間に有意な程度の共通性が存在する傾向があること、である。この目的のために、従来の方法は、ゼロから、データプレーン変化により誘起される各々の機能変化について１つの転送動作表現がある、転送動作表現のセットを構築し及び検証することを含む。これは、検証のための空間及び計算時間において非効率をもたらす。
【００１１】
さらに、従来のシステム及び方法は、データプレーン及び制御プレーンを分離して検証し、データプレーンのみが一度に検証される。さらに、制御コードの中の特定アーチファクトに検出したバグをマッピングすることは困難であり、制御プレーン検証は繊細なデータプレーンバグを見逃すことがある。さらに、従来のシステム及び方法は、半自動化されるだけであり、自動定理証明のための専門知識を要求することがある。
【００１２】
本開示の種々の実施形態は、ネットワークの検証に関し、特に、ソフトウェア定義ネットワーク（software−defined  network：ＳＤＮ）又はネットワーク機能の仮想化（network  function  virtualization：ＮＦＶ）を利用するネットワークの検証に関する。ネットワーク検証は、リアルタイムに（例えば、展開されたネットワーク上で）、又はオフラインで、ネットワークの展開及び再展開テスト中に、実行されて良い。ネットワーク検証は、ネットワークデータプレーンの個々のスナップショットの正確さを検証することを含んで良い。
【００１３】
上述のように、ネットワークの小部分のみがデータプレーンに対する標準的な変化により影響を受ける傾向があり、ネットワーク内の全ての転送ルールの間に有意な程度の共通性が存在する傾向がある。従来のシステム及び方法とは対照的に、本開示の種々の実施形態は、別の観察、つまり、ネットワーク全体ではなく、ネットワークの部分を通るパケットフローの間の共通性を効果的に利用し得る。一実施形態によると、リアルタイムデータプレーンチェッカは、ここでは「デルタネット」として参照されて良く、全てのペア到達可能性クエリを解決するよう構成されて良い。
【００１４】
この観察を利用して、ネットワーク全体の転送動作の単一の軽量な表現が構築できる。ここで、単一の軽量な表現は、各々のデータプレーン変化により増加的に且つ効率的に更新される。したがって、変化がより効率的に検証できる。さらに、変化の機能的影響がローカライズできない場合（例えば、リンク又はノード障害の場合）には、表現は、従来の方法に優る有意な空間効率も適用できる。
【００１５】
種々の実施形態によると、以下に更に詳述するように、リアルタイム（「デルタネット」）ネットワーク検証は、ネットワーク内の全てのパケットのフローを辺ラベル付きグラフとして表現するために、格子説抽象ドメイン（lattice−theoretical  abstract  domain）を自動的に精緻化することを含み得る。より具体的には、ネットワーク内のパケットフローを表す複数の転送グラフを構築する代わりに、本開示の実施形態は、ネットワーク内の転送ルールのブール結合を表し得る最小単位の格子説概念を増加的に維持することにより、単一の辺ラベル付きグラフを変形することを含み得る。一実施形態によると、グラフは、ネットワーク内の転送ルールの全てのブール結合を表し得る。
【００１６】
最小単位表現は、格子説に基づいて良く、したがって、インターネットプロトコル（ＩＰ）プレフィックス転送ルールを分析する抽象ドメインとして考えることができる。抽象ドメインの精度は動的に精緻化でき、したがって、間違った警報を制限し、及び場合によっては防ぐ。種々の実施形態によると、ルール挿入又はルール削除の分析は、例えば、平均約４０マイクロ秒で実行されて良い。これは、従来の方法に優る改良である。
【００１７】
データプレーンチェッカは、製造環境において展開されて良い。リアルタイム制約により、これは、当然に、チェックできる安全特性の種類を制限し得る。しかしながら、制限は、事前展開テストシナリオでは存在しない場合がある。本開示の種々の実施形態は、全てのペア到達可能性クエリのような、広範なクラスの到達可能性クエリの回答を実現できる。
【００１８】
さらに、種々の実施形態は、主として単一ソース到達可能性特性をチェックする目的で転送グラフを構築する知られている増加的ネットワーク検証技術との後方互換性を有して良い。これは、データプレーンをチェックするために形式的検証における専門知識が要求されない機能的特徴を持続できる。
【００１９】
本開示の実施形態を、添付の図面を参照して以下に説明する。
【００２０】
図１は、ネットワーク検証処理において使用され得るシステム１００を示す。システム１００は、ネットワーク管理者１０２、ソフトウェア定義ネットワーク（ＳＤＮ）１０４、特性１０６、及びデータプレーン１０８を有する。ＳＤＮ１０４は、ＳＤＮ制御部１０５、データプレーン１０８を含み得る物理ネットワーク１０７、及びネットワークアプリケーション１１０を有して良い。
【００２１】
特性１０６は、例えば、１又は複数の目標を達成するためにネットワーク管理者１０２により定められて良い、１又は複数のネットワーク全体に渡る不変条件を有して良い。例えば、１又は複数のネットワーク全体に渡る不変条件は、１又は複数の「到達可能性不変条件」を有して良い。「制御プレーン」は、ＳＤＮ制御部１０５、及びネットワークアプリケーション１１０を有して良い。「データプレーン」（例えば、データプレーン１０８）は、所与の時間において、種々のネットワークスイッチの構成のスナップショットを有して良い。
【００２２】
ネットワークの動作中、イベント（例えば、障害イベント（例えば、ノード、リンク）、トラフィックイベント（例えば、装置から制御部へのフィードバック、接続要求の追加／終了）、等）は、ＳＤＮ制御部１０５にデータプレーン１０８を変更させて良い。
【００２３】
図２は、特性１０６及びデータプレーン１０８を示す。データプレーン１０８の中の各スイッチＳは、１又は複数の転送テーブル１６０を有して良い。転送テーブル１６０は、例示低名転送ルール１６２のような、１又は複数の転送ルールを有して良い。図２は、１又は複数のバグ１３９を検出するよう構成され得るデータプレーンチェッカ１３８を更に示す。一例として、バグは、参照符号１４１により示すように、望ましくない転送ループを含み得る。
【００２４】
図３は、本開示の少なくとも一実施形態による、ネットワーク内のエラー（「バグ」）を検出する例示的な方法２００のフローチャートである。方法２００は、任意の適切なシステム、機器、又は装置により実行されて良い。例えば、図１４のシステム９００又はそのコンポーネントのうちの１又は複数は、方法２００に関連する動作のうちの１又は複数を実行して良い。上述及び他の実施形態では、コンピュータ可読媒体に格納されるプログラム命令は、方法２００の動作のうちの１又は複数を実行するために実行されて良い。さらに、方法２００の各動作は、静的又は動的であって良く、オンラインで（例えば、リアルタイムに）又はオフラインで実行されて良い。さらに、各々の動作は、増加的に又は非増加的に実行されて良い。
【００２５】
ブロック２０２で、ネットワークトポロジ及びデータプレーンが読み出されて良い。そして、方法２００はブロック２０４へ進んで良い。例えば、データプレーン１０８（例えば、図２を参照）及び関連するネットワークトポロジ（例えば、データプレーン１０８の中の各スイッチのための１又は複数の転送テーブルを含む）が識別されて良い。
【００２６】
ブロック２０４で、（例えば、検証のために）特性が読み出されて良い。そして、方法２００はブロック２０６へ進んで良い。例えば、特性１０６（例えば、図２を参照）は、データプレーン１０８が特性１０６を満たすことを検証するために、読み出されて良い。
【００２７】
ブロック２０６で、適切な場合には、１又は複数のデータプレーン更新が読み出されて良い。そして、方法２００はブロック２０８へ進んで良い。例えば、データプレーン１０８（例えば、図２を参照）は、各々の更新の後に、読み出されて良い。
【００２８】
ブロック２０８の後、１又は複数の転送テーブルから決定された転送動作表現が、生成され及び／又は更新されて良い。そして、方法２００はブロック２１０へ進んで良い。「転送動作表現」は、データプレーンの論理的（例えば、機械チェック可能な）表現を有し得ることに留意する。より具体的には、「転送動作表現」は、以下により完全に記載するように、辺ラベル付きグラフを有して良い。
【００２９】
ブロック２１０で、特性（例えば、特性１０６）の履行を検証するために、転送動作表現がチェックされて良い。そして、方法２００はブロック２１２へ進んで良い。ブロック２１２で、任意の知られているエラー（「バグ」）が出力されて良い。そして、方法２００はブロック２０６へ戻って良い。
【００３０】
本開示の範囲から逸脱することなく方法２００に対し変更、追加又は省略が行われて良い。例えば、方法２００の工程は、異なる順序で実施されて良い。さらに、概略のステップ及び動作は、単に例として提供され、幾つかのステップ及び動作は、開示の実施形態の本質から逸脱することなく、任意であり、より少ないステップ及び動作に組み合わされ、又は追加ステップ及び動作に拡張されて良い。
【００３１】
図４Ａは、スイッチＳ０〜Ｓ３を含むネットワークトポロジ３００を示す。図４Ｂは、ネットワークパケットｘのためのフローを含むネットワークトポロジ３００の転送グラフ３１０を示す。図４Ｃは、ネットワークパケットｙのためのフローを含むネットワークトポロジ３００の転送グラフ３２０を示す。図４Ｄは、ネットワークパケットｚのためのフローを含むネットワークトポロジ３００の転送グラフ３３０を示す。転送グラフ３１０及び３２０は、転送ループを含まず、特性に違反しない。しかしながら、転送グラフ３３０は、転送ループを含み、その結果、（例えば、特性１０６のうちの）特性に違反する。
【００３２】
転送グラフの構築は高価である。本開示の種々の実施形態によると、ネットワークを通じるパケットフローの間の共通性は、グラフを構築するオーバヘッドを削減するために利用できる。例えば、転送グラフは、辺ラベル付きグラフにより、より簡潔に表現できる。図５は、ネットワークパケットｘ、ｙ、ｚのためのフローを示す例示的な辺ラベル付きグラフ３５０を示す。辺ラベル付きグラフ３５０は、それぞれ図４Ｂ、４Ｃ、４Ｄに示す転送グラフ３１０、３２０、３３０を表して良い。
【００３３】
図６Ａは、スイッチｓ１〜ｓ４及びルールｒ１〜ｒ３を含むネットワークの例示的な転送グラフ４５０を示す。ネットワーク内のＩＰプレフィックスの集合は、半分閉じた間隔を有する。半分閉じた間隔の各々は、本願明細書では最小単位として参照される場合がある。本願明細書で使用されるとき、「最小単位」又は「複数の最小単位」は、一群のネットワークパケットセットを形成して良い。したがって、ネットワーク全体の中のルールのブール結合が表現できる。最小単位のセットは、ＩＰプレフィックスを表して良い。
【００３４】
図６Ｂは、ルールｒ１、ｒ２、ｒ３の間隔を示す。図６Ｂに示すように、ルールｒ１の間隔は最小単位α１、α２、α３、α４、を有し、ルールｒ２の間隔は最小単位α２、α３を有し、ルールｒ３の間隔は最小単位α３を有する。図６Ｃは、単一の辺ラベル付きグラフ４７０を示す。ここで、最小単位α１、α２、α３はルールｒ１の間隔を表し、最小単位α２、α３はルールｒ２の間隔を表し、最小単位α３はルールｒ３の間隔を表す。
【００３５】
図７Ａは、スイッチｓ１〜ｓ４及びルールｒ１〜ｒ４を含むネットワークの例示的な転送グラフ５００を示す。本例では、ルールｒ４は、ネットワークに挿入された新しいルールであり、ルールｒ４はルールｒ１に優る優先度を有する。図７Ｂは、ルールｒ１、ｒ２、ｒ３及びｒ４の間隔を示す。図７Ｂに示すように、ルールｒ１の間隔は最小単位α１、α２、α３、α４、を有し、ルールｒ２の間隔は最小単位α２、α３を有し、ルールｒ３の間隔は最小単位α３を有し、ルールｒ４の間隔は最小単位α２、α３、α４を有する。
【００３６】
図７Ｃは、単一の辺ラベル付きグラフ５２０を示す。ここで、最小単位α１、α２、α３はルールｒ１の間隔を表し、最小単位α２、α３はルールｒ２の間隔を表し、最小単位α３はルールｒ３の間隔を表す。さらに、種々の実施形態によると、辺ラベル付きグラフ５２０は、ルールｒ４がネットワークに追加されることに応答して、変形されて良い。図７Ｄは、辺ラベル付きグラフ５２０から変形される辺ラベル付きグラフ５４０を示す。ここで、最小単位α１はルールｒ１の間隔を表し、最小単位α２、α３はルールｒ２の間隔を表し、α３はルールｒ３の間隔を表し、最小単位α２、α３、α４は新しく追加されたルールｒ４の間隔を表す。グラフ変形は、単一の辺ラベル付きグラフを変形することにより、複数の重複する転送グラフの構築を回避できることに留意する。
【００３７】
図８は、本開示の少なくとも一実施形態による、ネットワークを検出する例示的な方法５５０のフローチャートである。方法５５０は、任意の適切なシステム、機器、又は装置により実行されて良い。例えば、図１４のシステム９００又はそのコンポーネントのうちの１又は複数は、方法５５０に関連する動作のうちの１又は複数を実行して良い。上述及び他の実施形態では、コンピュータ可読媒体に格納されるプログラム命令は、方法５５０の動作のうちの１又は複数を実行するために実行されて良い。
【００３８】
ブロック５５２で、転送テーブルは変更されて良い。そして、方法５５０はブロック５５４へ進んで良い。例えば、転送テーブル１６０（図２を参照）は、転送テーブルにルールを追加すること、転送テーブルからルールを削除すること、又はその両者により、変更されて良い。
【００３９】
ブロック５５４で、変更転送テーブルを表現するために、任意の追加最小単位が必要か否かが決定されて良い。１又は複数の追加最小単位が必要であると決定された場合、方法５５０はブロック５６０へ進んで良い。１又は複数の追加最小単位が必要ではないと決定された場合、方法５５０はブロック５５６へ進んで良い。
【００４０】
ブロック５５６で、辺ラベル付きグラフ（例えば、変形辺ラベル付きグラフ）は、転送テーブルに基づき生成されて良い。そして、方法５５０はブロック５５８へ進んで良い。例えば、辺ラベル付きグラフ５４０（図７Ｄを参照）が生成されて良い。さらに、ブロック５６２で、特性がチェックされて良い。例えば、１又は複数のエラーを検出するために、各々の辺ラベル付きグラフは、特性１０６（図２を参照）と比較されて良い。
【００４１】
ブロック５５８で、（例えば、転送テーブルへのルールの追加、転送テーブルからのルールの削除、又はその両方に応答して）転送テーブルに対する任意の変更が必要か否かが決定されて良い。転送テーブルに対する１又は複数の変更が必要であると決定された場合、方法５５０はブロック５５２に戻って良い。１又は複数の変更が必要ではないと決定された場合、方法５５０は終了して良い。
【００４２】
ブロック５６０で、新しい最小単位が生成されて良い。そして、方法５５０はブロック５５６へ進んで良い。ブロック５６２で、ネットワークを検証するために、１又は複数の辺ラベル付きグラフは、１又は複数の特性と比較されて良い。
【００４３】
転送グラフを含む各ネットワークパケットと等価なクラスが別個にチェックされる必要のある従来の方法と対照的に、本開示の実施形態は、ネットワーク全体の転送動作の表現を構築することを含み、この表現は、各々のデータプレーン変更と共に増加的且つ効率的に更新されて良い。
【００４４】
本開示の範囲から逸脱することなく方法５５０に対し変更、追加又は省略が行われて良い。例えば、方法５５０の工程は、異なる順序で実施されて良い。さらに、概略のステップ及び動作は、単に例として提供され、幾つかのステップ及び動作は、開示の実施形態の本質から逸脱することなく、任意であり、より少ないステップ及び動作に組み合わされ、又は追加ステップ及び動作に拡張されて良い。
【００４５】
少なくとも１つの従来の方法は、ルールが挿入され又は削除される度に、等価なクラスを再計算することを含む。これは、概して、異なる転送テーブルの中のルールのトラバースを必要とする。したがって、例えば、ルールｒ４がスイッチｓ４に挿入されると、従来の方法は４個全てのルールをトラバースする。これに対し、本開示の実施形態は、より持続的な形式のパケット等価クラス（例えば、最小単位）を含む。
【００４６】
最小単位を増加的に維持することは、種々の利点を有し得る。第一に、ネットワーク内のルールより少ない最小単位が存在する傾向があり、最小単位は、ネットワーク内でパケットがどのように流れるかに関する情報を効率的に圧縮できる。第二に、最小単位は、どのルールがルールの削除及び／又は挿入により影響を受けるかを、ネットワークが効率的に推測することを可能にできる。より具体的には、図９Ａ〜９Ｄを参照して記載される例では、辺ラベル付きグラフを変形するために、複数の転送グラフを構築する従来のシステムにおけるような全てのルールではなく、スイッチｓ１にあるルールｒ１及びｒ４のみしか検査される必要がない。
【００４７】
図９は、ネットワークトポロジ６００、及びネットワークスイッチのための転送テーブル６１０を示す。転送テーブル６１０は、２つのルールのエントリ、つまり高優先度を有するルールｒＨと低優先度を有するルールｒＬとを有する。ルールｒＨは、宛先アドレスがＩＰプレフィックス「０．０．０．１０／３１」（ＩＰｖ４  ＣＩＤＲフォーマットを使用する）と一致するパケットをドロップし、ルールｒＬは、ＩＰプレフィックス「０．０．０．０／２８」宛てのパケットを転送する。
【００４８】
上述のように、ＩＰプレフィックスは、間隔、より具体的には半分閉じた間隔として考えられる。ＩＰプレフィックス「０．０．０．１０／３１」は、＊が任意のビットを示すとき、全部０で開始し１０１＊で終了する３２ビットシーケンスと等価なので、ルールｒＨのＩＰプレフィックスは、半分閉じた間隔［１０：１２）に対応する。同様に、０．０．０．０／２８＝０．．．０＊＊＊＊なので、ＩＰプレフィックス「０．０．０．０／２８」＝［０：１６）である。
【００４９】
ネットワークの中の全てのルールのＩＰプレフィックスは、互いに素な半分閉じた間隔に解剖できる。図１０及び図９のルールｒＨ及びルールｒＬを参照すると、結果として生じる半分閉じた間隔の各々は、「最小単位」として参照され得る。これは、図１１のハッセ図６３０により示されるように、各々の最小単位がブール格子を有するからである。ハッセ図６３０では、最小単位［０：１０）、［１０：１２）、［１２：１６）は、それぞれ図１０のα０、α１、α２に対応する。
【００５０】
最小単位の構築により、ルールｒのＩＰプレフィックスは、最小単位のセットとして表現できる。ＩＰプレフィックス表現は、間隔（ｒ）により示すことができる。例えば、ルールｒＨのＩＰプレフィックスは、間隔（ｒＨ）であり、最小単位α１を含むシングルトン（singleton）セットに対応して良い。一方、ルールｒＬのＩＰプレフィックスは、間隔（ｒＬ）であり、最小単位α１、α１、α２に対応して良い。これらの最小単位を用いて、セット差分［間隔（ｒＬ）−間隔（ｒＨ）］は、ルールｒＬのＩＰプレフィックスが高優先度ルールｒＨによりドロップされないパケットにのみ一致し得ることを形式化するために使用されて良い。
【００５１】
図１２Ａ及び１２Ｂは、本開示の少なくとも一実施形態による、ネットワークのスイッチｓにルールｒを挿入する例示的な方法７００のフローチャートを示す。方法７００は、任意の適切なシステム、機器、又は装置により実行されて良い。例えば、図１４のシステム９００又はそのコンポーネントのうちの１又は複数は、方法７００に関連する動作のうちの１又は複数を実行して良い。上述及び他の実施形態では、コンピュータ可読媒体に格納されるプログラム命令は、方法７００の動作のうちの１又は複数を実行するために実行されて良い。
【００５２】
ブロック７０２で、ルールｒのＩＰプレフィックスは、（図１１及び１２を参照して上述したように）最小単位表現に変換されて良い。そして、方法７００はブロック７０４へ進んで良い。
【００５３】
ブロック７０４で、前の最小単位が分割できるか否かが決定されて良い。１又は複数の前の最小単位が分割できると決定された場合、方法７００はブロック７０６へ進んで良い。１又は複数の前の最小単位が分割できないと決定された場合、方法７００はブロック７０８へ進んで良い。
【００５４】
ブロック７０６で、分割されるべき最小単位によりラベル付けされた各々の辺は、更新されて良い。そして、方法７００はブロック７０８へ進んで良い。例えば、単一の最小単位αにより前に表現された半分閉じた間隔は、２つの最小単位（例えば、最小単位α及び最小単位α’）により表現されて良い。これは、「最小単位分割」として参照されて良く、抽象ドメインの精度を増加的に精緻化する効率的なメカニズムを提供できる。この増加的な抽象の精緻化は、ネットワークの中のルールの全てのブール結合の正確且つ効率的表現を可能にできる。
【００５５】
ブロック７０８で、各最小単位αについて、ルールｒのＩＰプレフィックスを表現する必要がある。方法７００は、ブロック７４０へ進んで良い。ルールｒが１又は複数の最小単位により十分に表現される場合、方法７００はブロック７２０で終了して良い。
【００５６】
ブロック７１０で、スイッチ固有平衡二分探索木（binary  search  tree：ＢＳＴ）は、最小単位αからのパケット転送を決定する、スイッチｓの中の最高優先度ルールｒ’を決定するために使用されて良い。そして、方法７００はブロック７１２へ進んで良い。
【００５７】
ブロック７１２で、スイッチｓの中に別のルールｒ’が存在するか否かが決定されて良い。ルールｒ’が存在すると決定された場合、方法７００はブロック７１４に進んで良い。ルールｒ’が存在しないと決定された場合、方法７００はブロック７１６に進んで良い。
【００５８】
ブロック７１４で、ルールｒ’の優先度がルールｒの優先度より低いか否かが決定されて良い。ルールｒ’の優先度がルールｒの優先度より低くないと決定された場合、方法７００はブロック７１６へ進んで良い。ルールｒ’の優先度がルールｒの優先度より低いと決定された場合、方法７００はブロック７１８へ進んで良い。
【００５９】
ブロック７１６で、スイッチｓに付帯する各辺のラベルは、更新されて良い。そして、方法７００はブロック７１８に進んで良い。
【００６０】
ブロック７１８で、ルールｒは、（例えば、ルールｒ’が削除される場合）スイッチ固有ＢＳＴに挿入されて良い。そして、方法７００はブロック７０８に戻って良い。
【００６１】
ＢＳＴの中のルールは、例えば、２つのＩＰプレフィックスが分離していること、又は１つのＩＰプレフィックスが他のものに含まれること、に起因して取り除かれて良いことに留意する。したがって、挿入又は削除されるべきルールの間隔の中にある全ての最小単位の間のパケットの転送動作を決定する最高優先度ルールは、該ルールのＩＰプレフィックスに含まれるスイッチの中の全てのルールを線形的にトラバースすることにより決定できる。
【００６２】
本開示の範囲から逸脱することなく方法７００に対し変更、追加又は省略が行われて良い。例えば、方法７００の工程は、異なる順序で実施されて良い。さらに、概略のステップ及び動作は、単に例として提供され、幾つかのステップ及び動作は、開示の実施形態の本質から逸脱することなく、任意であり、より少ないステップ及び動作に組み合わされ、又は追加ステップ及び動作に拡張されて良い。
【００６３】
図１３Ａ及び１３Ｂは、本開示の少なくとも一実施形態による、ネットワーク内のスイッチからルールｒを削除する例示的な方法８００のフローチャートを示す。方法８００は、任意の適切なシステム、機器、又は装置により実行されて良い。例えば、図１４のシステム９００又はそのコンポーネントのうちの１又は複数は、方法８００に関連する動作のうちの１又は複数を実行して良い。上述及び他の実施形態では、コンピュータ可読媒体に格納されるプログラム命令は、方法８００の動作のうちの１又は複数を実行するために実行されて良い。
【００６４】
ブロック８０２で、ルールｒのＩＰプレフィックスは、（図１１及び１２を参照して上述したように）最小単位表現に変換されて良い。そして、方法８００はブロック８０４へ進んで良い。
【００６５】
ブロック８０４で、各最小単位αについて、ルールｒのＩＰプレフィックスを表現する必要がある。方法８００は、ブロック８０６へ進んで良い。ルールｒが１又は複数の最小単位により十分に表現される場合、方法８００はブロック８２２で終了して良い。
【００６６】
ブロック８０６で、スイッチ固有ＢＳＴ  Ｂが最小単位αに関連付けられて良い。そして、方法８００はブロック８０８へ進んで良い。
【００６７】
ブロック８０８で、ＢＳＴ  Ｂの中で、最小単位αからのパケット転送動作を決定する、スイッチｓの中の最高優先度ルールｒ１が識別されて良い。そして、方法８００はブロック８１０へ進んで良い。
【００６８】
ブロック８１０で、ルールｒは、ＢＳＴ  Ｂから削除されて良い。そして、方法８００はブロック８１２へ進んで良い。
【００６９】
ブロック８１２で、スイッチｓの中のルールｒ１がスイッチｓの中のルールｒと同じルールであるか否かが決定されて良い。ルールｒ１がルールｒと同じルールであると決定された場合、方法８００はブロック８１３へ進んで良い。ルールｒ１がルールｒと同じルールではないと決定された場合、方法８００はブロック８０４に戻って良い。
【００７０】
ブロック８１３で、最小単位ラベルはルールｒの辺から削除されて良い。そして、方法８００はブロック８１４へ進んで良い。
【００７１】
ブロック８１４で、Ｂの中で、最小単位αからのパケット転送動作を決定する、スイッチｓの中の次の最高優先度ルールｒ２が識別されて良い。そして、方法８００はブロック８１６へ進んで良い。
【００７２】
ブロック８１６で、スイッチｓの中にルールｒ２が存在するか否かが決定されて良い。ルールｒ２が存在すると決定された場合、方法８００はブロック８１８に進んで良い。ルールｒ２が存在しないと決定された場合、方法８００はブロック８０４に戻って良い。
【００７３】
ブロック８１８で、最小単位ラベルはルールｒ２の辺に追加されて良い。そして、方法８００はブロック８０４に戻って良い。
【００７４】
ＢＳＴの中のルールは、例えば、２つのＩＰプレフィックスが分離していること、又は１つのＩＰプレフィックスが他のものに含まれること、に起因して取り除かれて良いことに留意する。したがって、挿入又は削除されるべきルールの間隔の中にある全ての最小単位の間のパケットの転送動作を決定する最高優先度ルールは、該ルールのＩＰプレフィックスに含まれるスイッチの中の全てのルールを線形的にトラバースすることにより決定できる。
【００７５】
本開示の範囲から逸脱することなく方法８００に対し変更、追加又は省略が行われて良い。例えば、方法８００の工程は、異なる順序で実施されて良い。さらに、概略のステップ及び動作は、単に例として提供され、幾つかのステップ及び動作は、開示の実施形態の本質から逸脱することなく、任意であり、より少ないステップ及び動作に組み合わされ、又は追加ステップ及び動作に拡張されて良い。
【００７６】
図１４は、本開示の少なくとも一実施形態による、例示的なコンピューティングシステム９００のブロック図である。コンピューティングシステム９００は、デスクトップコンピュータ、ラップトップコンピュータ、サーバコンピュータ、タブレットコンピュータ、携帯電話機、スマートフォン、パーソナルデジタルアシスタント（ＰＤＡ）、電子リーダ装置、ネットワークスイッチ、ネットワークルータ、ネットワークハブ、他のネットワーキング装置、又は他の適切なコンピューティング装置を有して良い。
【００７７】
コンピューティングシステム９００は、プロセッサ９１０、記憶装置９２０、メモリ９３０及び通信装置９４０を有して良い。プロセッサ９１０、記憶装置９２０、メモリ９３０及び／又は通信装置９４０は、全て通信可能に結合されて良い。したがって、コンポーネントの各々は他のコンポーネントと通信できる。コンピューティングシステム９００は、本開示に記載の動作のうちの任意の動作を実行するよう構成されて良い。
【００７８】
概して、プロセッサ９１０は、任意の適切な特定用途向け又は汎用コンピュータ、コンピューティングエンティティ、又は種々のコンピュータハードウェア若しくはソフトウェアモジュールを有して良く、任意の適切なコンピュータ可読媒体に格納された命令を実行するよう構成され得る処理装置を用いて実施されて良い。例えば、プロセッサ９１０は、マイクロプロセッサ、マイクロコントローラ、デジタシグナルプロセッサ（ＤＳＰ）、特定用途向け集積回路（ＡＳＩＣ）、フィールドプログラマブルゲートアレイ（FPGA）又はプログラム命令を解釈し及び／若しくは実行し並びに／又はデータを処理するよう構成された任意の他のデジタル若しくはアナログ回路を有して良い。図１４には単一のプロセッサを示したが、プロセッサ９１０は、本開示で説明される任意の数の工程を個々に又は共同で実行するよう構成される任意の数のプロセッサを有して良い。
【００７９】
幾つかの実施形態では、プロセッサ９１０は、プログラム命令を解釈し及び／又は実行し、及び／又は記憶装置９２０、メモリ９３０又は記憶装置９２０及びメモリ９３０に格納されたデータを処理して良い。幾つかの実施形態では、プロセッサ９１０は、記憶装置９２０からプログラム命令をフェッチし、該プログラム命令をメモリ９３０にロードして良い。プログラム命令がメモリ９３０にロードされた後、プロセッサ９１０は該プログラム命令を実行して良い。
【００８０】
例えば、幾つかの実施形態では、ネットワーク検証のための処理工程のうちの１又は複数は、プログラム命令としてデータ記憶装置９２０に含まれて良い。プロセッサ９１０は、処理工程のうちの１又は複数のプログラム命令をフェッチして良く、処理工程の該プログラム命令をメモリ９３０にロードして良い。処理工程のプログラム命令がメモリ９３０にロードされた後、プロセッサ９１０は、コンピューティングシステム９００がプログラム命令により指示されるように処理工程に関連する工程を実施できるように、プログラム命令を実行して良い。
【００８１】
記憶装置９２０及びメモリ９３０は、格納されたコンピュータ実行可能命令又はデータ構造を伝える又は有するコンピュータ可読記憶媒体を含み得る。このようなコンピュータ可読媒体は、プロセッサ９１０のような汎用又は特定目的コンピュータによりアクセスできる任意の利用可能な媒体を含み得る。例として且つ限定ではなく、このようなコンピュータ可読記憶媒体は、ＲＡＭ、ＲＯＭ、ＥＥＰＲＯＭ、ＣＤ−ＲＯＭ又は他の光ディスク記憶装置、磁気ディスク記憶装置又は他の磁気記憶装置、フラッシュメモリ装置（例えば、固体メモリ素子）を含む有形又は非一時的コンピュータ可読記憶媒体、又はコンピュータにより実行可能な命令若しくはデータ構造の形式で所望のプログラムコード手段を伝える若しくは格納するために用いられ汎用若しくは特定目的コンピュータによりアクセス可能な他の記憶媒体を有し得る。上述の組合せも、コンピュータ可読記憶媒体の範囲に包含され得る。コンピュータ実行可能命令は、例えば、プロセッサ９１０に特定の工程又は工程のグループを実行させるよう構成される命令及びデータを含み得る。
【００８２】
幾つかの実施形態では、記憶装置９２０及び／又はメモリ９３０は、ネットワーク検証に関連するデータを格納して良い。例えば、記憶装置９２０及び／又はメモリ９３０は、特性、データプレーン、ネットワークアプリケーション、転送テーブル、転送ルール、転送動作表現、及びグラフ（例えば、辺ラベル付きグラフ及び／又は変形辺ラベル付きグラフ）を格納して良い。
【００８３】
通信装置９４０は、コンピューティングシステム９００と別の電子装置との間の通信を可能にし又は助けるよう構成される任意の装置、システム、コンポーネント、又はコンポーネントの集合を有して良い。例えば、通信装置９４０は、モデム、ネットワークカード（無線又は有線）、赤外線通信装置、光通信装置、（アンテナのような）無線通信装置、及び／又は（Ｂｌｕｅｔｏｏｔｈ（登録商標）装置、８０２．６装置（例えば、ＭＡＮ（Metropolitan  Area  Network））、ＷｉＦｉ装置、ＷｉＭａｘ装置、セルラ通信設備、等のような）チップセット、及び／又は同様のものを含み得るが、これらに限定されない。通信装置９４０は、少数の例を挙げると、セルラネットワーク、ＷｉＦｉネットワーク、ＭＡＮ、光ネットワーク、等のような任意のネットワーク、及び／又はリモート装置を含む本開示に記載される任意の他の装置と、データを交換させることができる。
【００８４】
本開示の範囲から逸脱することなく図１４に対し変更、追加又は省略が行われて良い。例えば、コンピューティング装置９００は、本開示で示され説明されたものより多くの又は少ない要素を有して良い。例えば、コンピューティングシステム９００は、タブレット又は携帯電話機の画面のような統合型ディスプレイ装置を有して良く、又は、コンピューティングシステム９００と別個の及びそれに通信可能に結合され得る外部モニタ、プロジェクタ、テレビジョン、又は他の適切なディスプレイ装置を有して良い。
【００８５】
本開示で用いられるように、用語「モジュール」又は「コンポーネント」は、モジュール若しくはコンポーネントのアクションを実行するよう構成される特定ハードウェア実装、及び／又はコンピューティングシステムの汎用ハードウェア（例えばコンピュータ可読媒体、処理装置、等）に格納され及び／又はそれらにより実行され得るソフトウェアオブジェクト又はソフトウェアルーチンを表して良い。幾つかの実施形態では、本開示に記載されたのと異なるコンポーネント、モジュール、エンジン及びサービスは、（例えば、別個のスレッドとして）コンピューティングシステムで実行されるオブジェクト又は処理として実施されて良い。本開示に記載のシステム及び方法の幾つかは概して（汎用ハードウェアに格納される及び／又はそれにより実行される）ソフトウェアで実装されるように記載されたが、専用ハードウェアの実装又はソフトウェアと専用ハードウェアの組み合わせの実装も可能であり考えられる。本開示では、「コンピュータエンティティ」は、本開示で先に定められたようにコンピューティングシステム、又はコンピューティングシステムで実行されるモジュール若しくはモジュールの組合せであって良い。
【００８６】
本開示で及び特に添付の特許請求の範囲（例えば、添付の特許請求の範囲の本体）で使用される用語は、概して、広義の（open）用語と考えられる（例えば、用語「含む（including）」は「含むが、限定されない」と解釈されるべきであり、用語「有する（having）」は「少なくとも有する」と解釈されるべきであり、用語「含む（includes）」は「含むが、限定されない」と解釈されるべきである）。
【００８７】
さらに、特定数の導入された請求項の引用が意図される場合、このような意図は、請求項の中に明示的に示され、このような引用が存在しない場合はこのような意図が存在しない。例えば、理解の助けとして、以下の添付の特許請求の範囲は、請求項の引用を導入するために、「少なくとも１つの」及び「１又は複数の」をいう前置語句の使用を含み得る。しかしながら、このような語句の使用は、同じ請求項が前置語句「１又は複数」又は「少なくとも１つの」及び「ａ又はａｎ」のような不定冠詞を含むときでも、不定冠詞「ａ、ａｎ」による請求項引用の導入がこのような導入された請求項引用を含む任意の特定の請求項をこのような引用を１つだけ含む実施形態に限定することを示すと考えられてはならない（例えば、「ａ」及び／又は「ａｎ」は「少なくとも１つの」又は「１又は複数の」を意味すると解釈されるべきである）。同様のことは、請求項引用を導入するために使用される定冠詞の使用についても該当する。
【００８８】
さらに、特定数の導入された請求項引用が明示的に引用される場合、当業者は、このような引用が少なくとも引用された番号を意味することと解釈されるべきであることを認識するだろう（例えば、「２つの引用」はそのままで、他の変更が無ければ、少なくとも２つの引用、又は２以上の引用を意味する）。さらに、「Ａ、Ｂ、Ｃ、等のうちの少なくとも１つ」又は「Ａ、Ｂ、Ｃ、等のうちの１又は複数」に類似する慣例が用いられる例では、通常、このような構成は、Ａのみ、Ｂのみ、Ｃのみ、Ａ及びＢを一緒に、Ａ及びＣを一緒に、Ｂ及びＣを一緒に、又はＡ、Ｂ、Ｃを一緒に、等を含むと意図される。
【００８９】
さらに、２以上の代替用語を表す任意の離接語又は語句は、説明、請求項、又は図面の中であるかに係わらず、用語のうちの１つ、用語のうちのいずれか、又は両方の用語を含む可能性を包含すると理解されるべきである。例えば、語句「Ａ又はＢ」は、「Ａ」又は「Ｂ」又は「Ａ及びＢ」の可能性を含むと理解されるべきである。
【００９０】
本開示に記載された全ての例及び条件文は、教育上の目的で、読者が本発明の原理及び発明者により考案された概念を理解するのを助け、技術を促進させるためであり、これらの特に記載された例及び条件に限定されないものと考えられるべきである。本開示の実施形態が詳細に記載されたが、種々の変更、置換及び修正が本開示の精神及び範囲から逸脱することなく行われ得る。
【００９１】
以上の実施形態に加えて、更に以下の付記を開示する。
（付記１）  ネットワーク検証方法であって、
データプレーンの中の複数のスイッチのうちの各スイッチのための１又は複数の転送テーブルを有する前記データプレーンを識別するステップと、
前記データプレーンの前記１又は複数の転送テーブルの転送ルールのブール結合を表すために、前記データプレーンの転送動作表現を生成するステップと、
前記データプレーンの中の１又は複数のエラーを検出するために、前記データプレーンの前記転送動作表現を１又は複数のネットワーク特性と比較するステップと、
を有する方法。
（付記２）  前記転送動作表現を生成するステップは、前記１又は複数の転送テーブルの転送ルールのブール結合を表すために、複数の最小単位を含む前記転送動作表現を生成するステップを有する、付記１に記載の方法。
（付記３）  前記転送動作表現を生成するステップは、前記データプレーンの論理表現を生成するステップを有する、付記１に記載の方法。
（付記４）  転送ルールが前記複数のスイッチのうちのスイッチの転送テーブルに追加されることに応答して更新されたデータプレーンを識別するステップと、
前記更新されたデータプレーンの別の転送動作表現を生成するステップと、
前記更新されたデータプレーンの中の１又は複数のエラーを検出するために、前記更新されたデータプレーンの前記別の転送動作表現を前記１又は複数のネットワーク特性と比較するステップと、
を更に有する付記１に記載の方法。
（付記５）  前記データプレーンの前記転送動作表現を生成するステップは、辺ラベル付きグラフを生成するステップを有し、前記辺ラベル付きグラフの各エッジは、前記データプレーンの転送ルールのインターネットプロトコル（ＩＰ）プレフィックスを表すために、１又は複数の最小単位に関連付けられる、付記１に記載の方法。
（付記６）  転送ルールが前記１又は複数の転送テーブルのうちの転送テーブルから削除されることに応答して、更新辺ラベル付きグラフを生成するために、前記辺ラベル付きグラフを更新するステップ、を更に有する付記５に記載の方法。
（付記７）  転送ルールが前記１又は複数の転送テーブルのうちの転送テーブルに追加されることに応答して、更新辺ラベル付きグラフを生成するために、前記辺ラベル付きグラフを更新するステップ、を更に有する付記５に記載の方法。
（付記８）  前記１又は複数の転送テーブルの１又は複数の変更に応答して、前記更新辺ラベル付きグラフを増加的に更新するステップ、を更に有する付記７に記載の方法。
（付記９）  前記転送動作表現を１又は複数のネットワーク特性と比較するステップは、前記転送動作表現を１又は複数のネットワーク到達可能性特性と比較するステップを有する、付記１に記載の方法。
（付記１０）  命令を有する１又は複数の非一時的コンピュータ可読媒体であって、前記命令は、１又は複数のプロセッサにより実行されると、前記１又は複数のプロセッサに動作を実行させるよう構成され、前記動作は、
データプレーンの中の複数のスイッチのうちの各スイッチのための１又は複数の転送テーブルを有する前記データプレーンを識別するステップと、
前記データプレーンの前記１又は複数の転送テーブルの転送ルールのブール結合を表すために、前記データプレーンの転送動作表現を生成するステップと、
前記データプレーンの中の１又は複数のエラーを検出するために、前記データプレーンの前記転送動作表現を１又は複数のネットワーク特性と比較するステップと、
を有する、コンピュータ可読媒体。
（付記１１）  前記動作は、
転送ルールが前記複数のスイッチのうちのスイッチの転送テーブルに追加されることに応答して更新されたデータプレーンを識別するステップと、
前記データプレーンの別の転送動作表現を生成するステップと、
前記更新されたデータプレーンの中の１又は複数のエラーを検出するために、前記川迫インされたデータプレーンの前記別の転送動作表現を前記１又は複数のネットワーク特性と比較するステップと、
を更に有する、付記１０に記載のコンピュータ可読媒体。
（付記１２）  前記データプレーンの前記転送動作表現を生成するステップは、辺ラベル付きグラフを生成するステップを有し、前記辺ラベル付きグラフの各エッジは、前記データプレーンの転送ルールのインターネットプロトコル（ＩＰ）プレフィックスを表すために、１又は複数の最小単位に関連付けられる、付記１０に記載のコンピュータ可読媒体。
（付記１３）  前記動作は、転送ルールが前記１又は複数の転送テーブルのうちの転送テーブルに追加されることに応答して、更新辺ラベル付きグラフを生成するために、前記辺ラベル付きグラフを更新するステップ、を更に有する、付記１２に記載のコンピュータ可読媒体。
（付記１４）  前記動作は、前記１又は複数の転送テーブルの１又は複数の変更に応答して、前記更新辺ラベル付きグラフを増加的に更新するステップ、を更に有する、付記１３に記載のコンピュータ可読媒体。
（付記１５）  前記動作は、転送ルールが前記複数のスイッチのうちのスイッチの転送テーブルに追加されることに応答して、前記転送動作表現を更新するステップ、を更に有する、付記１０に記載のコンピュータ可読媒体。
（付記１６）  ネットワーク検証システムであって、
１又は複数のプロセッサ、
を有し、前記１又は複数のプロセッサは、
データプレーンの中の複数のスイッチのうちの各スイッチのための１又は複数の転送テーブルを有する前記データプレーンを識別し、
前記データプレーンの前記１又は複数の転送テーブルの転送ルールのブール結合を表すために、前記データプレーンの転送動作表現を生成し、
前記データプレーンの中の１又は複数のエラーを検出するために、前記データプレーンの前記転送動作表現を１又は複数のネットワーク特性と比較する、
よう構成される、システム。
（付記１７）  前記１又は複数のプロセッサは、
転送ルールが前記複数のスイッチのうちのスイッチの転送テーブルに追加されることに応答して更新されたデータプレーンを識別し、
前記更新されたデータプレーンの別の転送動作表現を生成し、
前記更新されたデータプレーンの中の１又は複数のエラーを検出するために、前記更新されたデータプレーンの前記別の転送動作表現を前記１又は複数のネットワーク特性と比較する、
よう更に構成される、付記１６に記載のシステム。
（付記１８）  前記データプレーンの前記転送動作表現は、辺ラベル付きグラフを有し、前記辺ラベル付きグラフの各エッジは、前記データプレーンの転送ルールのインターネットプロトコル（ＩＰ）プレフィックスを表すために、１又は複数の最小単位に関連付けられる、付記１６に記載のシステム。
（付記１９）  前記１又は複数のプロセッサは、前記１又は複数の転送テーブルの１又は複数の変更に応答して、更新辺ラベル付きグラフを生成するために、前記辺ラベル付きグラフを更新するよう更に構成される、付記１８に記載のシステム。
（付記２０）  前記１又は複数の変更は、前記１又は複数の転送テーブルのうちの少なくとも１つの転送テーブルに１又は複数の転送ルールを追加することを有する、付記１９に記載のシステム。
【符号の説明】
【００９２】
１００  システム
１０２  ネットワーク管理者
１０４  ＳＤＮ
１０５  ＳＤＮ制御部
１０６  特性
１０７  物理ネットワーク
１０８  データプレーン
１１０  ネットワークアプリケーション
【図１】
2018046549.tif 000003
【図２】
2018046549.tif 000004
【図３】
2018046549.tif 000005
【図４Ａ】
2018046549.tif 000006
【図４Ｂ】
2018046549.tif 000007
【図４Ｃ】
2018046549.tif 000008
【図４Ｄ】
2018046549.tif 000009
【図５】
2018046549.tif 000010
【図６Ａ】
2018046549.tif 000011
【図６Ｂ】
2018046549.tif 000012
【図６Ｃ】
2018046549.tif 000013
【図７Ａ】
2018046549.tif 000014
【図７Ｂ】
2018046549.tif 000015
【図７Ｃ】
2018046549.tif 000016
【図７Ｄ】
2018046549.tif 000017
【図８】
2018046549.tif 000018
【図９】
2018046549.tif 000019
【図１０】
2018046549.tif 000020
【図１１】
2018046549.tif 000021
【図１２Ａ】
2018046549.tif 000022
【図１２Ｂ】
2018046549.tif 000023
【図１３Ａ】
2018046549.tif 000024
【図１３Ｂ】
2018046549.tif 000025
【図１４】
2018046549.tif 000026