(57)【要約】  本発明は、ネットワークの網羅的な検証の効率化に貢献する。ネットワーク検証装置は、検証対象のネットワークの構成及びネットワークに含まれる機器の動作モデルを定義した検証情報の入力を受け付ける検証情報入力部と、前記検証情報から、前記ネットワークにおいて、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正した過大近似モデルの検証を行う検証コードを生成する検証コード生成部と、前記検証コードを用いてモデル検査を実行するモデル検査実行部と、前記モデル検査において得られる反例が、前記ネットワークの本来の動作にも存在するか否か確認する反例妥当性確認部と、前記モデル検査実行部及び前記反例妥当性確認部の出力に基づき、検証の結果を出力する検証結果出力部と、を含む。
2014115759.tif 000002
【特許請求の範囲】
【請求項１】
検証対象のネットワークの構成及びネットワークに含まれる機器の動作モデルを定義した検証情報の入力を受け付ける検証情報入力部と、
前記検証情報から、前記ネットワークにおいて、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正した過大近似モデルの検証を行う検証コードを生成する検証コード生成部と、
前記検証コードを用いてモデル検査を実行するモデル検査実行部と、
前記モデル検査において得られる反例が、前記ネットワークの本来の動作にも存在するか否か確認する反例妥当性確認部と、
前記モデル検査実行部及び前記反例妥当性確認部の出力に基づき、検証の結果を出力する検証結果出力部と、
を含むネットワーク検証装置。
【請求項２】
前記検証対象のネットワークに、ＯｐｅｎＦｌｏｗスイッチと、ＯｐｅｎＦｌｏｗコントローラとが含まれ、前記検証情報には、ＯｐｅｎＦｌｏｗスイッチとＯｐｅｎＦｌｏｗコントローラの動作モデルが定義されている請求項１のネットワーク検証装置。
【請求項３】
前記反例妥当性確認部は、
前記反例から、前記反例が実際に実行される際に満たされるべき制約に関する制約情報を取得して、前記制約情報から制約充足問題を生成する制約充足問題生成部と、
前記制約充足問題の解を求めることで、前記反例がネットワークの本来の動作でも実行可能かどうか判断する制約充足問題解決部と、
を備える請求項１又は２のネットワーク検証装置。
【請求項４】
前記検証情報入力部は、
ユーザから、前記検証情報の一部として、検証対象のネットワークのプロパティの入力を受け付ける請求項１から３のいずれか一のネットワーク検証装置。
【請求項５】
前記検証情報入力部は、
ユーザに対し、前記検証情報の一部あるいは全部について典型的な内容を定めた雛形を提供し、
前記雛形の選択により、前記検証情報の少なくとも一部の入力を受け付ける請求項１から４のいずれか一のネットワーク検証装置。
【請求項６】
検証対象のネットワークの構成及びネットワークに含まれる機器の動作モデルを定義した検証情報の入力を受け付けるステップと、
前記検証情報から、前記ネットワークにおいて、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正した過大近似モデルの検証を行う検証コードを生成するステップと、
前記検証コードを用いてモデル検査を実行するステップと、
前記モデル検査において得られる反例が、前記ネットワークの本来の動作にも存在するか否か確認するステップと、
前記モデル検査実行部及び前記反例妥当性確認部の出力に基づき、検証の結果を出力するステップと、
を含むネットワーク検証方法。
【請求項７】
ネットワークの動作検証を行うコンピュータに、
検証対象のネットワークの構成及びネットワークに含まれる機器の動作モデルを定義した検証情報の入力を受け付ける処理と、
前記検証情報から、前記ネットワークにおいて、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正した過大近似モデルの検証を行う検証コードを生成する処理と、
前記検証コードを用いてモデル検査を実行する処理と、
前記モデル検査において得られる反例が、前記ネットワークの本来の動作にも存在するか否か確認する処理と、
前記モデル検査実行部及び前記反例妥当性確認部の出力に基づき、検証の結果を出力する処理と、
を実行させるプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
（関連出願についての記載）
本発明は、日本国特許出願：特願２０１３−００９８６６号（２０１３年１月２３日出願）の優先権主張に基づくものであり、同出願の全記載内容は引用をもって本書に組み込み記載されているものとする。
本発明は、ネットワーク検証装置、ネットワーク検証方法及びプログラムに関し、特に、検証対象のネットワークをモデル化して検証を行うネットワーク検証装置、ネットワーク検証方法及びプログラムに関する。
【背景技術】
【０００２】
ネットワークの運用管理に関して、ＯｐｅｎＦｌｏｗという技術が注目されている（非特許文献１、２参照）。ＯｐｅｎＦｌｏｗは、Ｓｏｆｔｗａｒｅ−Ｄｅｆｉｎｅｄ  Ｎｅｔｗｏｒｋ（以下、「ＳＤＮ」）の概念を実現する技術としても注目されている。ＳＤＮは、ネットワーク制御をプログラマブルな方法で一元管理するという、ネットワークの分野の新たなパラダイムであり、特にＯｐｅｎＦｌｏｗは、ネットワーク運用の自動化・効率化・省電力化等、様々な期待を集めている。【０００３】
一方で、ＯｐｅｎＦｌｏｗでは、ネットワーク制御の柔軟性が増す分、それに伴う不具合の発生が懸念されている。例えば開発者の考慮漏れや、複数のプログラムを組み合わせたことによる不具合が多くなる。そのためＯｐｅｎＦｌｏｗネットワークの安定運用には、そのネットワークが安全なものかを事前に検証することが重要となる。例えば、非特許文献３には、モデル検査によりＯｐｅｎＦｌｏｗネットワークの状態探索を行う“ＮＩＣＥ”というツールが開示されている。非特許文献３によると、“ＮＩＣＥ”は、ＯｐｅｎＦｌｏｗコントローラのプログラムを記号実行し、すべてのコードパスを実行するためのパケットの代表値の集合を求め、それを用いて状態探索を行っている。
【先行技術文献】
【非特許文献】
【０００４】
【非特許文献１】Ｎｉｃｋ  ＭｃＫｅｏｗｎほか７名、“ＯｐｅｎＦｌｏｗ：  Ｅｎａｂｌｉｎｇ  Ｉｎｎｏｖａｔｉｏｎ  ｉｎ  Ｃａｍｐｕｓ  Ｎｅｔｗｏｒｋｓ”、［ｏｎｌｉｎｅ］、［平成２４（２０１２）年１２月２６日検索］、インターネット〈URL: http://www.openflow.org/documents/openflow-wp-latest.pdf〉
【非特許文献２】“ＯｐｅｎＦｌｏｗ  Ｓｗｉｔｃｈ  Ｓｐｅｃｉｆｉｃａｔｉｏｎ”  Ｖｅｒｓｉｏｎ  １．０．０．  （Ｗｉｒｅ  Ｐｒｏｔｏｃｏｌ  ０ｘ０１）、［ｏｎｌｉｎｅ］、［平成２４年１２月２６日検索］、インターネット〈ＵＲＬ：https://www.opennetworking.org/images/stories/downloads/specification/openflow-spec-v1.0.0.pdf〉
【非特許文献３】Ｍａｒｃｏ  Ｃａｎｉｎｉほか４名、“Ａ  ＮＩＣＥ  Ｗａｙ  ｔｏ  Ｔｅｓｔ  ＯｐｅｎＦｌｏｗ  Ａｐｐｌｉｃａｔｉｏｎｓ”、［ｏｎｌｉｎｅ］、［平成２５（２０１３）年１月４日検索］、インターネット〈URL: http://infoscience.epfl.ch/record/170618/files/nsdi-final.pdf〉
【発明の概要】
【発明が解決しようとする課題】
【０００５】
以下の分析は、本発明によって与えられたものである。非特許文献３に代表される手法の問題点は、現実的なコスト（時間及びマシンリソース）で、ＯｐｅｎＦｌｏｗネットワークの主要な動作を網羅的に検証できないこと、あるいは、（現実的なコストでできないため）網羅的な検証をしないことである。【０００６】
例えば、非特許文献３が開示している技術では、ＯｐｅｎＦｌｏｗコントローラのプログラムのすべてのコードパスを網羅する検証を行うが、前記プログラムが影響を与えるＯｐｅｎＦｌｏｗネットワークの動作（ＯｐｅｎＦｌｏｗスイッチによる通信パケットの転送動作等）を網羅する検証は行われない。そのため、ＯｐｅｎＦｌｏｗネットワークの主要な動作に関わる不具合が検出できない可能性がある。【０００７】
上記の問題点は、非特許文献１、２のＯｐｅｎＦｌｏｗに固有のものではなく、ＳＤＮと呼ばれるネットワークに共通するものといえる。【０００８】
本発明は、ＳＤＮに代表されるネットワークの網羅的な検証の効率化に貢献できるネットワーク検証装置、プログラム及び方法を提供することを目的とする。
【課題を解決するための手段】
【０００９】
第１の視点によれば、検証対象のネットワークの構成及びネットワークに含まれる機器の動作モデルを定義した検証情報の入力を受け付ける検証情報入力部と、前記検証情報から、前記ネットワークにおいて、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正した過大近似モデルの検証を行う検証コードを生成する検証コード生成部と、前記検証コードを用いてモデル検査を実行するモデル検査実行部と、前記モデル検査において得られる反例が、前記ネットワークの本来の動作にも存在するか否か確認する反例妥当性確認部と、前記モデル検査実行部及び前記反例妥当性確認部の出力に基づき、検証の結果を出力する検証結果出力部と、を含むネットワーク検証装置が提供される。【００１０】
第２の視点によれば、検証対象のネットワークの構成及びネットワークに含まれる機器の動作モデルを定義した検証情報の入力を受け付けるステップと、前記検証情報から、前記ネットワークにおいて、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正した過大近似モデルの検証を行う検証コードを生成するステップと、前記検証コードを用いてモデル検査を実行するステップと、前記モデル検査において得られる反例が、前記ネットワークの本来の動作にも存在するか否か確認するステップと、前記モデル検査実行部及び前記反例妥当性確認部の出力に基づき、検証の結果を出力するステップと、を含むネットワーク検証方法が提供される。本方法は、ネットワークのモデル検査を実行するコンピュータという、特定の機械に結びつけられている。【００１１】
第３の視点によれば、ネットワークの動作検証を行うコンピュータに、検証対象のネットワークの構成及びネットワークに含まれる機器の動作モデルを定義した検証情報の入力を受け付ける処理と、前記検証情報から、前記ネットワークにおいて、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正した過大近似モデルの検証を行う検証コードを生成する処理と、前記検証コードを用いてモデル検査を実行する処理と、前記モデル検査において得られる反例が、前記ネットワークの本来の動作にも存在するか否か確認する処理と、前記モデル検査実行部及び前記反例妥当性確認部の出力に基づき、検証の結果を出力する処理と、を実行させるプログラムが提供される。なお、このプログラムは、コンピュータが読み取り可能な（非トランジエントな）記憶媒体に記録することができる。即ち、本発明は、コンピュータプログラム製品として具現することも可能である。
【発明の効果】
【００１２】
本発明によれば、ＳＤＮに代表されるネットワークの網羅的な検証の効率化に貢献することが可能となる。
【図面の簡単な説明】
【００１３】
【図１】本発明の一実施形態の構成を示す図である。
【図２】本発明の第１の実施形態のネットワーク検証装置の構成を示す図である。
【図３】非特許文献２のＯｐｅｎＦｌｏｗスイッチの最小の動作モデルの一例である。
【図４】非特許文献２のＯｐｅｎＦｌｏｗコントローラの最小の動作モデルの一例である。
【図５】本発明の第１の実施形態のネットワーク検証装置の動作を示すシーケンス図である。
【図６】本発明の第１の実施形態のネットワーク検証装置の過大近似モデル生成部の動作（端末の動作モデルからの過大近似モデルの生成）を示す流れ図である。
【図７】本発明の第１の実施形態のネットワーク検証装置の過大近似モデル生成部の動作（スイッチの動作モデルからの過大近似モデルの生成）示す流れ図である。
【図８】本発明の第１の実施形態のネットワーク検証装置の過大近似モデル生成部の動作（コントローラの動作モデルからの過大近似モデルの生成）を示す流れ図である。
【図９】本発明の第２の実施形態において想定するネットワーク機器の最小の動作モデルの一例である。
【図１０】本発明の第２の実施形態のネットワーク検証装置の過大近似モデル生成部の動作（ネットワーク機器の動作モデルからの過大近似モデルの生成）を示す流れ図である。
【図１１】本発明の第３の実施形態のネットワーク検証装置の構成を示す図である。
【発明を実施するための形態】
【００１４】
はじめに本発明の一実施形態の概要について図面を参照して説明する。なお、この概要に付記した図面参照符号は、理解を助けるための一例として各要素に便宜上付記したものであり、本発明を図示の態様に限定することを意図するものではない。
【００１５】
本発明は、その一実施形態において、図１に示すように、検証情報入力部１１と、検証コード生成部１２と、モデル検査実行部１３と、反例妥当性確認部１４と、検証結果出力部１５と、を含むネットワーク検証装置１Ａにて実現できる。
【００１６】
より具体的には、検証情報入力部１１は、検証対象のネットワークの構成及びネットワークに含まれる機器の動作モデルを定義した検証情報の入力を受け付ける。検証コード生成部１２は、前記検証情報から、前記ネットワークにおいて、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正した過大近似モデルの検証を行う検証コードを生成する。モデル検査実行部１３は、前記検証コードを用いてモデル検査を実行する。前記モデル検査の結果、プロパティ（要求仕様）を満たさない状態があることを示す証拠が見つかった場合、モデル検査実行部１３は、反例（ｃｏｕｎｔｅｒ−ｅｘａｍｐｌｅ）を出力する。反例妥当性確認部１４は、前記反例が、前記ネットワークの本来の動作にも存在するか否かを確認する。そして、検証結果出力部１５は、前記モデル検査実行部及び前記反例妥当性確認部１４の出力に基づき、検証の結果を出力する。
【００１７】
上記構成によれば、モデル検査実行部１３にて網羅的なモデル検査が行われる。また、反例妥当性確認部１４が、モデル検査にて得られた反例の妥当性確認が行われるため、不具合の検出が可能となる。
【００１８】
［第１の実施形態］
［構成の説明］
続いて、本発明の第１の実施形態について図面を参照して詳細に説明する。図２は、本発明の第１の実施形態のネットワーク検証装置の構成を示す図である。図２を参照すると、本発明の第１の実施の形態におけるネットワーク検証装置は、検証情報入力部１１と、検証コード生成部１２と、モデル検査実行部１３と、反例妥当性確認部１４と、検証結果出力部１５と、を含む構成が示されている。また、以下の説明で用いる符号Ｄ１１〜Ｄ１７は、ネットワーク検証装置の入出力情報や中間コード等を表している（図５参照）。
【００１９】
また、検証コード生成部１２は、後述のように、過大近似モデル生成部１２１と、過大近似モデル変換部１２２と、を含む。また、反例妥当性確認部１４は、後述のように、制約充足問題生成部１４１と、制約充足問題解決部１４２と、を含む。
【００２０】
検証情報入力部１１は検証コード生成部１２と接続されている。検証コード生成部１２はモデル検査実行部１３と接続されている。モデル検査実行部１３は反例妥当性確認部１４及び検証結果出力部１５と接続されている。反例妥当性確認部１４は検証結果出力部１５と接続されている。
【００２１】
検証情報入力部１１は、検証対象のネットワークを構成するすべての端末、スイッチ及びコントローラの動作モデル並びにこれらの接続関係と、前記ネットワークが満たすべきプロパティと、を定義した検証情報Ｄ１１を入力として受け付ける。
【００２２】
ここで、「動作モデル」について説明する。動作モデルは、プリミティブな動作単位である動作ステップを実行しながら遷移を行う状態機械として定義されるものとする。前記動作モデルは、ネットワークを構成する個々の端末、スイッチ及びコントローラについてそれぞれ個別に定義される。ただし、同一の動作を行うもの同士については、同一の動作モデルを参照することで個別の定義を省略してもよい。ネットワーク全体の動作モデルは、前記ネットワークを構成する個々の端末、スイッチ及びコントローラの全動作モデルを合成した動作モデルとして定義される。また、本実施形態では、前記スイッチ及びコントローラの動作モデル並びにこれらの接続関係は非特許文献２のＯｐｅｎＦｌｏｗの仕様に則っていることを前提とする。
【００２３】
図３は、非特許文献２のＯｐｅｎＦｌｏｗスイッチの最小の動作モデルの一例である。図３の例では、ＯｐｅｎＦｌｏｗスイッチは、通信パケットＰの受信を待ち（ステップＳＳ１）、パケットを受信すると、コントローラから受信済みのエントリ（フローエントリ）の中から、受信パケットＰに適合するマッチ条件を持つエントリを探し（ステップＳＳ２）、受信パケットに適合するマッチ条件を持つエントリがあれば、そのアクションフィールドの内容を実行する（ステップＳＳ３）。ここで、受信パケットＰに適合するマッチ条件を持つエントリがない場合、ＯｐｅｎＦｌｏｗスイッチは、通信パケットＰをコントローラに転送すると共にエントリの送信を要求する（ステップＳＳ４）。そして、ＯｐｅｎＦｌｏｗスイッチは、コントローラの応答を待ち（ステップＳＳ５）、応答内容に応じて処理を実行し（ステップＳＳ６）、それを繰り返す、という動作を最低限包含する（非特許文献２の「３．４  Ｍａｔｃｈｉｎｇ」も参照）。
【００２４】
図４は、非特許文献２のＯｐｅｎＦｌｏｗコントローラの最小の動作モデルの一例である。図４の例では、ＯｐｅｎＦｌｏｗコントローラは、スイッチからのエントリ要求を待ち（ステップＳＣ１）、スイッチからエントリ要求を受けると、転送されてきた通信パケットＰの処理内容を決定する（ステップＳＣ２）。そして、ＯｐｅｎＦｌｏｗコントローラは、ＯｐｅｎＦｌｏｗスイッチに、応答として、前記決定した処理内容（フローエントリも含む）を返し（ステップＳＣ３）、以上の処理を繰り返す、という動作を最低限包含する。
【００２５】
なお、図３、図４は、非特許文献２のＯｐｅｎＦｌｏｗ  Ｓｗｉｔｃｈ  Ｓｐｅｃｉｆｉｃａｔｉｏｎ  Ｖｅｒｓｉｏｎ  １．０．０に規定された動作をモデル化したものであるが、ネットワーク検証装置１が適切に対応できるのであれば、その他のバージョンのＯｐｅｎＦｌｏｗ仕様に則っていても問題ない。また、検証情報Ｄ１１において、前記プロパティは必ずしも定義されていなくてもよい。前記プロパティが定義されていない場合、典型的なプロパティを検証することとし、以降はその他の装置も含めて前記典型的なプロパティが検証情報Ｄ１１に定義されているかのように動作することとすればよい。
【００２６】
検証コード生成部１２は、過大近似モデル生成部１２１と、過大近似モデル変換部１２２と、を含む。過大近似モデル生成部１２１は、検証情報Ｄ１１から前記ネットワークの動作の過大近似モデルＤ１２を生成する。過大近似モデル変換部１２２は、過大近似モデルＤ１２が前記プロパティを満たすかを検証する検証コードＤ１３を生成する。
【００２７】
ここで、「過大近似モデル（Ｏｖｅｒ  ａｐｐｒｏｘｉｍａｔｅ  ｍｏｄｅｌ）」について説明する。過大近似モデルＤ１２は、その内部において通信パケットのフィールドの具体値を取り扱わないように、即ち、通信パケットを特定するマッチ条件に依存しないよう前記動作モデルを修正することにより、ネットワークの動作を過大近似したモデルである。本実施形態では、スイッチ及びコントローラについて、通信パケットを特定するマッチ条件に依存せずフローエントリを前記通信パケットに適用する動作を行う過大近似モデルＤ１２を生成することになる。
【００２８】
過大近似モデルＤ１２は、前記動作モデルと同様、プリミティブな動作単位である動作ステップを実行しながら遷移を行う状態機械として定義されるものとする。過大近似モデルＤ１２は、ネットワークを構成する個々の端末、スイッチ及びコントローラについてそれぞれ個別に定義される。ただし、同一の動作を行うもの同士については、同一の過大近似モデルを参照することで個別の定義を省略してもよい。ネットワーク全体の過大近似モデルは、前記ネットワークを構成する個々の端末・スイッチ・コントローラの全過大近似モデルを合成した過大近似モデルとして定義される。本実施形態では、過大近似モデル変換部１２２は、前記ネットワーク全体の過大近似モデルを用いて検証コードＤ１３を生成する。なお、「過大近似モデル」については、後に動作例を示してより具体的に説明する。
【００２９】
ここで、「検証コード」について説明する。検証コードＤ１３は、過大近似モデルＤ１２をモデル検査実行部１３の入力言語で記述したものである。モデル検査実行部１３として、例えばモデル検査ツールＳｐｉｎを利用するのであれば、検証コードＤ１３は、Ｓｐｉｎの入力言語Ｐｒｏｍｅｌａで過大近似モデルＤ１２を記述したものとなる。
【００３０】
また、過大近似モデルＤ１２は、それそのものが検証コードＤ１３であってもよい。例えば検証情報Ｄ１１で定義されている動作モデルがモデル検査実行部１３の入力言語で記述されており、前記動作モデルを過大近似モデルＤ１２に変換することで直接的に検証コードＤ１３を生成する構成になっていてもよい。その場合、図２の構成から、過大近似モデル変換部１２２は不要となるため検証コード生成部１２から除外することができる。この場合、過大近似モデル生成部１２１は生成した過大近似モデルＤ１２を直接モデル検査実行部１３に渡すことになる。
【００３１】
モデル検査実行部１３は、検証コードＤ１３を用いてモデル検査を実行し、プロパティの成否Ｄ１４を出力する。また、前記モデル検査の結果、過大近似モデルＤ１２が前記プロパティを満たさないことが判明した場合、モデル検査実行部１３は、その動作の例である反例Ｄ１５を出力する。なお、このモデル検査は、すべての反例Ｄ１５が得られるまで実行を続ける。前記のとおり、検証コードＤ１３の元になっている過大近似モデルＤ１２は、通信パケットのフィールドの具体値を取り扱わないので、効率的にモデル検査を実行することが可能である。
【００３２】
反例妥当性確認部１４は、制約充足問題生成部１４１と、制約充足問題解決部１４２と、を含む。制約充足問題生成部１４１は、前記モデル検査により得られた反例Ｄ１５から、反例Ｄ１５が前記ネットワークの本来の動作にも存在するかどうか確認するための制約充足問題Ｄ１６を生成する。
【００３３】
制約充足問題解決部１４２は、制約充足問題（Ｃｏｎｓｔｒａｉｎｔ  ｓａｔｉｓｆａｃｔｉｏｎ  ｐｒｏｂｌｅｍ）Ｄ１６を解き、解Ｄ１７を１つ求める。反例Ｄ１５が前記ネットワークの本来の動作にも存在する場合には解Ｄ１７が求まり、存在しない場合には解Ｄ１７は求まらない（解なし）。
【００３４】
前記モデル検査により反例Ｄ１５が複数得られた場合、制約充足問題生成部１４１及び制約充足問題解決部１４２は、それぞれの反例Ｄ１５について前述の処理を個別に実行する。例えば反例Ｄ１５がｎ個得られた場合、解Ｄ１７は最大でｎ個得られる。解Ｄ１７が求まった場合、解Ｄ１７が求まった反例Ｄ１５と組み合わせて検証結果出力部１５に渡す。
【００３５】
モデル検査により反例Ｄ１５が検出された検証コードＤ１３の元になっている過大近似モデルＤ１２は通信パケットのフィールドの具体値を取り扱わないので、反例Ｄ１５がどのような通信パケットにより発現するかは、反例Ｄ１５から直接的には知ることができない。反例妥当性確認部１４は、そのために設けられたものであり、反例Ｄ１５がどのような通信パケットにより発現するか示す具体値を提供する。反例Ｄ１５を発現させる通信パケットの具体値が存在しない場合、前記ネットワークの本来の動作では反例Ｄ１５が発現しないことを示している。
【００３６】
検証結果出力部１５は、モデル検査実行部１３の出力であるプロパティの成否Ｄ１４と、反例妥当性確認部１４の出力である反例Ｄ１５及び解Ｄ１７に基づき、検証の結果を出力する。プロパティの成否Ｄ１４が偽であり（＝過大近似モデルＤ１２が前記プロパティを満たさない）、解Ｄ１７が１個でも得られた場合、検証結果出力部１５は、前記ネットワークが前記プロパティを満たさないという結果を出力すると共に反例Ｄ１５と及び解Ｄ１７の組み合わせをすべて出力する。一方、プロパティの成否Ｄ１４が真である（＝過大近似モデルＤ１２が前記プロパティを満たす）場合、検証結果出力部１５は、前記ネットワークが前記プロパティを満たすという結果を出力する。また、解Ｄ１７が１個も得られなかった場合も、検証結果出力部１５は、前記ネットワークが前記プロパティを満たすという結果を出力する。
【００３７】
なお、図２に示したネットワーク検証装置１の各部（処理手段）は、ネットワーク検証装置を構成するコンピュータに、そのハードウェアを用いて、上記した各処理を実行させるコンピュータプログラムにより実現することができる。
【００３８】
［動作の説明］
続いて、本発明の第１の実施形態の動作について詳細に説明する。図５は、本発明の第１の実施形態のネットワーク検証装置の動作を示すシーケンス図である。図５を参照すると、ユーザは、検証情報Ｄ１１を作成し、検証情報入力部１１に入力する（ステップＳ１１）。
【００３９】
検証コード生成部１２では、まず過大近似モデル生成部１２１が検証情報Ｄ１１から過大近似モデルＤ１２を生成し（ステップＳ１２）、次に過大近似モデル変換部１２２が過大近似モデルＤ１２を検証コードＤ１３に変換する（ステップＳ１３）。
【００４０】
過大近似モデルＤ１２の生成ステップ（ステップＳ１２）では、検証情報Ｄ１１で定義されている端末、スイッチ及びコントローラの動作モデルのそれぞれを参照し処理を行うことで過大近似モデルＤ１２を生成する。過大近似モデル変換部１２２が検証コードＤ１３を生成する動作は、モデル検査実行部１３の入力言語に依存するが、変換元の過大近似モデルＤ１２は状態機械のような形式で定義されているため、前記入力言語が異なる場合でもその変換方法に本質的な違いは生じない。これは、検証情報Ｄ１１で定義されている動作モデルがモデル検査実行部１３の入力言語で記述されており、前記動作モデルを過大近似モデルＤ１２に変換することで直接的に検証コードＤ１３を生成する構成になっている場合でも同様である。
【００４１】
ここで、過大近似モデルＤ１２の生成ステップ（ステップＳ１２）における端末の動作モデルの処理に関わる部分について詳細に説明する。図６は、本実施形態の過大近似モデル生成部の動作（端末の動作モデルからの過大近似モデルの生成）を示す流れ図である。図６を参照すると、まず、過大近似モデル生成部１２１が、端末の動作モデルから、転送する通信パケットを生成（宣言）する動作ステップＡＳ１１をすべて抽出する（ステップＳ１２１１）。
【００４２】
そして、過大近似モデル生成部１２１は、前記抽出した動作ステップの直後に、前記通信パケットにそれを一意に特定するためのＩＤと転送回数を保持するためのフィールドを付与し、適切な値で初期化する動作ステップを挿入する（ステップＳ１２１２）。ここでは前記ＩＤを各通信パケットの通し番号で、転送回数を０で初期化することとするが、前記通信パケットを一意に特定できるのであればこれに限られるものではない。過大近似モデル生成部１２１は、ステップＳ１２１１で抽出したすべての動作ステップＡＳ１１について、ステップＳ１２１２の処理を実行する。
【００４３】
次に、過大近似モデル生成部１２１は、前記端末の動作モデルから、通信パケットのフィールドの値を指定（代入）する動作ステップをすべて抽出する（ステップＳ１２１３）。
【００４４】
そして、過大近似モデル生成部１２１は、前記抽出した動作ステップを、前記通信パケットにどのような値が代入されるかを前記ＩＤ及び前記転送回数と共に制約情報として表示する動作ステップに置き換える（ステップＳ１２１４）。この制約情報は、以降登場する制約情報と同様、後述する反例妥当性確認部１４において利用される。ステップＳ１２１４では、代入する動作ステップを、表示する（だけの）動作ステップに置き換えるので、結果として代入は実際には行われなくなることに注意されたい。過大近似モデル生成部１２１は、ステップＳ１２１３で抽出したすべての動作ステップについて、ステップＳ１２１４の処理を実行する。
【００４５】
最後に、過大近似モデル生成部１２１は、前記端末の動作モデルから、通信パケットを転送する動作ステップをすべて抽出する（ステップＳ１２１５）。
【００４６】
そして、過大近似モデル生成部１２１は、前記動作ステップの直前に、前記通信パケットの転送回数を１増やす動作ステップを挿入する（ステップＳ１２１６）。そして、過大近似モデル生成部１２１は、ステップＳ１２１５で抽出したすべての動作ステップについて、ステップＳ１２１６の処理を実行する。端末の動作モデルが個別に複数定義されている場合は、それぞれ端末の動作モデルについて、過大近似モデル生成部１２１は、上記処理を実行する。
【００４７】
続いて、過大近似モデルＤ１２の生成ステップ（ステップＳ１２）におけるスイッチの動作モデルの処理に関わる部分について詳細に説明する。図７は、本実施形態の過大近似モデル生成部の動作（スイッチの動作モデルからの過大近似モデルの生成）を示す流れ図である。図７を参照すると、まず、過大近似モデル生成部１２１が、スイッチの動作モデルから、受信した通信パケットＰに合うマッチ条件を持つエントリを探す動作ステップ（図３のＳＳ２に相当するもの）を抽出する（ステップＳ１２２０）。
【００４８】
過大近似モデル生成部１２１は、抽出した動作ステップを、前記マッチ条件に拘らず任意のエントリを選択するという動作ステップ又は、前記マッチ条件に合うエントリがないと判断する動作ステップに置き換える（ステップＳ１２２１）。さらに、過大近似モデル生成部１２１は、置き換えた前記動作ステップの直後に、前記通信パケットのＩＤ及び転送回数と共に制約情報を表示する動作ステップを挿入する（ステップＳ１２２２）。前ステップＳ１２２１において、前記マッチ条件に拘らず任意の処理ルールを選択するという動作ステップに置き換えた場合、制約情報として、そのエントリのマッチ条件を表示する動作ステップが挿入される。また、前ステップＳ１２２１において、マッチ条件に合う処理ルールがないと判断する動作ステップに置き換えた場合、制約情報として、すべてのエントリのマッチ条件に合わないとされたそのマッチ条件を表示する動作ステップが挿入される。
【００４９】
次に、過大近似モデル生成部１２１は、前記スイッチの動作モデルから、コントローラにエントリを要求する動作ステップ列ＡＳＳ２１を抽出する（ステップＳ１２２３）。そして、過大近似モデル生成部１２１は、前記抽出した動作ステップ列の先頭に、制約情報として、コントローラの前記要求の際に転送する通信パケットのヘッダフィールドが前回転送時と同じ値であることを表示する動作ステップを挿入する（ステップＳ１２２４）。
【００５０】
さらに、過大近似モデル生成部１２１は、前記スイッチの動作モデルから、通信パケットＰにエントリに設定されたアクションを適用する動作ステップ列ＡＳＳ２２を抽出する（Ｓ１２２５）。次に、過大近似モデル生成部１２１は、前記抽出した動作ステップ列から、ヘッダフィールドの値の書き換え（代入）を行う動作ステップをすべて抽出する（ステップＳ１２２６）。さらに、過大近似モデル生成部１２１は、前記抽出した前記動作ステップを、前記通信パケットのＩＤ及び前記転送回数と共に制約情報を表示する動作ステップに置き換える（ステップＳ１２２７）。ここでの制約情報は、ヘッダフィールドの値の書き換え（代入）アクションによって、通信パケットＰに代入される値となる。
【００５１】
過大近似モデル生成部１２１は、ステップＳ１２２６で抽出したすべての動作ステップについて、ステップＳ１２２７の処理を実行する。上記ステップＳ１２２７では、ヘッダフィールドの値の書き換え（代入）を行う動作ステップを、制約情報を表示する（だけの）動作ステップに置き換えるので、結果として代入は実際には行われなくなることに注意されたい。
【００５２】
次に、過大近似モデル生成部１２１は、ステップＳ１２２５で抽出した動作ステップ列内で通信パケットを転送する動作の直前（存在しない場合は前記動作ステップ列の最後）に制約情報を表示する動作ステップを挿入する（ステップＳ１２２８）。ここでの制約情報は、上記ヘッダフィールドの値の書き換え（代入）時に値の書き換え（代入）が行われないヘッダフィールドのそれぞれについて、そのフィールドが前記通信パケットの前回転送時と同じ値であるという内容となる。
【００５３】
次に、過大近似モデル生成部１２１は、前記スイッチの動作モデルから、通信パケットを転送する動作ステップをすべて抽出する（ステップＳ１２２９）。さらに、過大近似モデル生成部１２１は、前記抽出した動作ステップの直前に、前記通信パケットの転送回数を１増やす動作ステップを挿入する（ステップＳ１２２Ａ）。過大近似モデル生成部１２１は、ステップＳ１２２９で抽出したすべての動作ステップについて、ステップＳ１２２Ａの処理を実行する。また、スイッチの動作モデルが個別に複数定義されている場合、過大近似モデル生成部１２１は、各動作モデルについて、上述の処理を実行する。
【００５４】
続いて、過大近似モデルＤ１２の生成ステップ（ステップＳ１２）におけるコントローラの動作モデルの処理に関わる部分について詳細に説明する。図８は、本実施形態の過大近似モデル生成部の動作（コントローラの動作モデルからの過大近似モデルの生成）を示す流れ図である。図８を参照すると、まず、過大近似モデル生成部１２１が、コントローラの動作モデルから、スイッチからのエントリ要求への対応処理を行う動作ステップ列ＡＳＳ３１を抽出する（ステップＳ１２３０）。
【００５５】
次に、過大近似モデル生成部１２１は、前記抽出した動作ステップ列を１つ選択し、その実行順序に従い、変数に代入を行う動作ステップ（代入文）をすべて抽出する（ステップＳ１２３１）。そして、過大近似モデル生成部１２１は、前記抽出した動作ステップの代入元（代入文の右辺）を参照し、変数が用いられている場合には、その変数の代入回数を、変数名の最後に付与した新たな変数名に置き換える（ステップＳ１２３２）。
【００５６】
なお、変数の代入回数はこの処理全体を通して変数毎に常に記憶しておくものとする。ここでは変数の代入回数の初期値は０であるとするが、一意に特定できるのであればこれに限定されるものではない。例えばｘ＝ｘ＋１という動作ステップが抽出され、ｘの代入回数がその時点で０回であれば、過大近似モデル生成部１２１は、ｘ＝ｘ＋１という動作ステップをｘ=ｘ０＋１と置き換える。
【００５７】
次に、過大近似モデル生成部１２１は、動作ステップの代入先（代入文の左辺）を参照し、用いられている変数の代入回数を１増加し、その変数の代入回数を変数名の最後に付与した新たな変数名に置き換える（ステップＳ１２３３）。例えば先程の例でｘ=ｘ０＋１に置き換えた動作ステップは、ｘ１=ｘ０＋１とさらに置き換えられる。
【００５８】
さらに、過大近似モデル生成部１２１は、ステップＳ１２３３で得られた動作ステップ（置き換えた代入文）の直後に、制約情報としてその内容を表示する動作ステップを挿入する（ステップＳ１２３４）。
【００５９】
過大近似モデル生成部１２１は、ステップＳ１２３１で抽出したすべての動作ステップについて、ステップＳ１２３２〜１２３４の処理を実行する。
【００６０】
次に、過大近似モデル生成部１２１は、ステップＳ１２３１で選択した動作ステップ列からスイッチから転送されてきた通信パケットＰを受信する動作ステップを抽出する（ステップＳ１２３５）。そして、過大近似モデル生成部１２１は、前記抽出した動作ステップの直後に、スイッチから転送されてきた通信パケットのＩＤ及び転送回数と共に、制約情報として、前記動作ステップ列内において、どの通信パケットのフィールドが参照されるかを表示する動作ステップを挿入する（ステップＳ１２３６）。
【００６１】
さらに、過大近似モデル生成部１２１は、ステップＳ１２３１で選択した動作ステップ列から、スイッチに応答を返す動作ステップを抽出する（ステップＳ１２３７）。そして、過大近似モデル生成部１２１は、前記抽出した動作ステップの直前に、スイッチから転送されてきた通信パケットの転送回数を１増やす動作ステップを挿入する（ステップＳ１２３８）。加えて、過大近似モデル生成部１２１は、ステップＳ１２３８で挿入した動作ステップの直後に、前記通信パケットのＩＤ及び転送回数と共に制約情報として、スイッチへの応答としてヘッダフィールドにどのような値を持つ通信パケットを転送するかを表示する動作ステップを挿入する（Ｓ１２３９）。
【００６２】
過大近似モデル生成部１２１は、ステップＳ１２３０で抽出したすべての動作ステップ列について、ステップＳ１２３１〜１２３９の処理を実行する。また、コントローラの動作モデルが個別に複数定義されている場合、過大近似モデル生成部１２１は、各動作モデルについて、上述の処理を実行する。
【００６３】
なお、上述した端末、スイッチ及びコントローラの各動作モデルに実施する処理の順序には特に制限はない。検証情報Ｄ１１で定義されている順序に従って処理を実施してもよいし、特定の順序に並び替えてから処理を実施してもよい。すべての端末、スイッチ及びコントローラの動作モデルについて前記処理を実施することで、過大近似モデル生成部１２１は、ネットワーク全体の過大近似モデルＤ１２を生成する。
【００６４】
モデル検査実行部１３は、検証コード生成部１２で生成された検証コードＤ１３に対してモデル検査を実行し、プロパティの成否Ｄ１４と、前記プロパティが満たされない場合には反例Ｄ１５と、を生成する（ステップＳ１４）。
【００６５】
通常のモデル検査では反例を１つ検出した時点でモデル検査を終了する場合が多いが、本実施形態のモデル検査実行部１３は、反例を１つ検出してもモデル検査を終了せず、すべての反例を検出するまでモデル検査を実行する。
【００６６】
反例Ｄ１５が検出されると、まず反例妥当性確認部１４の制約充足問題生成部１４１が反例Ｄ１５から制約充足問題Ｄ１６を生成する（ステップＳ１５）。次に、制約充足問題解決部１４２が、制約充足問題Ｄ１６を解くことでその解Ｄ１７を求める（ステップＳ１６）。
【００６７】
より具体的には、制約充足問題生成部１４１は、反例Ｄ１５内の、検証コード生成部１２の処理により制約情報として表示されている内容をすべて抽出し、それぞれ制約充足問題の式に変換することで、制約充足問題Ｄ１６を生成する。制約充足問題解決部１４２は、その解Ｄ１７が求まった場合、解Ｄ１７が求まった反例Ｄ１５と組み合わせて検証結果出力部１５に渡す。
【００６８】
検証結果出力部１５は、モデル検査実行部１３の出力であるプロパティの成否Ｄ１４と、反例妥当性確認部１４の出力である反例Ｄ１５及び解Ｄ１７に基づき、検証の結果を出力する（ステップＳ１７）。プロパティの成否Ｄ１４が偽であり（＝過大近似モデルＤ１２が前記プロパティを満たさない）、解Ｄ１７が１個でも得られた場合、検証結果出力部１５は、前記ネットワークが前記プロパティを満たさないという結果を出力すると共に反例Ｄ１５と及び解Ｄ１７の組み合わせをすべて出力する。
【００６９】
プロパティの成否Ｄ１４が真である（＝過大近似モデルＤ１２が前記プロパティを満たす）場合か、解Ｄ１７が１個も得られなかった場合、検証結果出力部１５は、前記ネットワークが前記プロパティを満たすという結果を出力する。
【００７０】
ユーザは、ステップＳ１７で出力された結果を確認する（ステップＳ１８）。
【００７１】
以上説明したように、本実施形態のネットワーク検証装置１は、検証コード生成部１２で、通信パケットのフィールドの具体値を取り扱わないようＯｐｅｎＦｌｏｗネットワークの動作を過大近似したモデルを生成し、前記過大近似モデルがプロパティを満たすか検証する検証コードを生成する。そして、そのモデル検査実行部１３が前記検証コードを用いてモデル検査を実行することで、前記ＯｐｅｎＦｌｏｗネットワーク内の端末が送信するパケットの内容の違いを考慮する必要のない効率的なモデル検査が実施される。また、前記モデル検査において前記過大近似モデルが前記プロパティを満たさないという結果が出た場合、反例妥当性確認部１４により、得られた反例が前記ＯｐｅｎＦｌｏｗネットワークの本来の動作にも存在するかどうかを効率よく確認できる。これにより、ＯｐｅｎＦｌｏｗネットワークの網羅的な検証が効率的に実施可能になり、不具合を漏れなく検出することができる。
【００７２】
［第２の実施形態］
続いて、ＯｐｅｎＦｌｏｗネットワーク以外のネットワークの検証動作を行う本発明の第２の実施形態について図面を参照して詳細に説明する。以下、前記第１の実施形態と同様の部分は省略し、異なる部分についてのみ説明する。
【００７３】
［構成の説明］
再度、図２を参照して、本発明の第２の実施形態の構成について詳細に説明する。本発明の第２の実施形態の検証情報入力部１１は、ネットワークを構成するすべての端末・ネットワーク機器の動作モデル及びそれらの接続関係と、前記ネットワークが満たすべきプロパティと、を定義した検証情報Ｄ１１を入力として受け付ける。前記動作モデルは、複数の逐次的な動作ステップにより構成されるものとする。図９は、本発明の第２の実施形態において想定するネットワーク機器の最小の動作モデルの一例である。図９の例では、ネットワーク機器は、通信パケットＰの受信を待ち（ステップＳＮ１）、パケットを受信すると、自装置に設定・実装済みのエントリの中から、受信パケットＰの宛先等に適合するエントリを探し（ステップＳＮ２）、受信パケットの宛先等に適合するエントリがあれば、そのエントリに定められた処理内容を実行する（ステップＳＮ３）。一方、受信パケットＰの宛先等に適合するエントリがない場合、ネットワーク機器は、デフォルトの動作として設定・実装されている処理を実行する（ステップＳＮ４）。ネットワーク機器は、以上を繰り返す、という動作を最低限包含する。
【００７４】
［動作の説明］
次に、図２及び図５を参照して、本発明の第２の実施形態の動作について詳細に説明する。検証コード生成部１２では、まず過大近似モデル生成部１２１が検証情報Ｄ１１から過大近似モデルＤ１２を生成し（ステップＳ１２）、次に過大近似モデル変換部１２２が過大近似モデルＤ１２を検証コードＤ１３に変換する（ステップＳ１３）。
【００７５】
過大近似モデルＤ１２の生成ステップ（ステップＳ１２）では、検証情報Ｄ１１で定義されている端末及びネットワーク機器の動作モデルのそれぞれを参照し処理を行うことで過大近似モデルＤ１２を生成する。前記端末の動作モデルからの過大近似モデルＤ１２の生成処理は本発明の第１の実施形態と同様のため省略する。
【００７６】
続いて、過大近似モデルＤ１２の生成ステップ（ステップＳ１２）におけるネットワーク機器の動作モデルの処理に関わる部分について詳細に説明する。図１０は、本実施形態の過大近似モデル生成部の動作（ネットワーク機器の動作モデルからの過大近似モデルの生成）を示す流れ図である。図１０を参照すると、まず、過大近似モデル生成部１２１が、ネットワーク機器の動作モデルから、受信した通信パケットＰの宛先等に合うエントリを探す動作ステップ（図９のＳＮ２に相当するもの）を抽出する（ステップＳ２２２０）。
【００７７】
過大近似モデル生成部１２１は、抽出した動作ステップを、通信パケットＰの宛先等に拘らずエントリを選択するという動作ステップ又は、前記通信パケットＰの宛先等に合うエントリがないと判断する動作ステップに置き換える（ステップＳ２２２１）。さらに、過大近似モデル生成部１２１は、置き換えた前記動作ステップの直後に、前記通信パケットのＩＤ及び転送回数と共に制約情報を表示する動作ステップを挿入する（ステップＳ２２２２）。前ステップＳ２２２１において、前記通信パケットＰの宛先等に拘らず任意のエントリを選択するという動作ステップに置き換えた場合、制約情報として、そのエントリの宛先等の条件を表示する動作ステップが挿入される。また、前ステップＳ２２２１において、通信パケットＰの宛先等に合うエントリがないと判断する動作ステップに置き換えた場合、制約情報として、すべてのエントリの条件に合わないとされたその条件を表示する動作ステップが挿入される。
【００７８】
次に、過大近似モデル生成部１２１は、前記ネットワーク機器の動作モデルから、通信パケットＰにエントリに設定された処理内容を実行する動作ステップ列ＡＳＳ４１を抽出する（Ｓ２２２３）。次に、過大近似モデル生成部１２１は、前記抽出した動作ステップ列から、ヘッダフィールドの値の書き換え（代入）を行う動作ステップをすべて抽出する（ステップＳ２２２４）。さらに、過大近似モデル生成部１２１は、前記抽出した前記動作ステップを、前記通信パケットのＩＤ及び前記転送回数と共に制約情報を表示する動作ステップに置き換える（ステップＳ２２２５）。ここでの制約情報は、ヘッダフィールドの値の書き換え（代入）によって、通信パケットＰに代入される値となる。
【００７９】
過大近似モデル生成部１２１は、ステップＳ２２２４で抽出したすべての動作ステップについて、ステップＳ２２２５の処理を実行する。上記ステップＳ２２２５では、ヘッダフィールドの値の書き換え（代入）を行う動作ステップを、制約情報を表示する（だけの）動作ステップに置き換えるので、結果として代入は実際には行われなくなることに注意されたい。
【００８０】
次に、過大近似モデル生成部１２１は、ステップＳ１２２５で抽出した動作ステップ列内で通信パケットを転送する動作の直前（通信パケットを転送する動作が存在しない場合は前記動作ステップ列の最後）に制約情報を表示する動作ステップを挿入する（ステップＳ２２２６）。ここでの制約情報は、上記ヘッダフィールドの値の書き換え（代入）時に値の書き換え（代入）が行われないヘッダフィールドのそれぞれについて、そのフィールドが前記通信パケットの前回の転送時と同じ値であるという内容となる。
【００８１】
過大近似モデル生成部１２１は、ステップＳ２２２３で抽出したすべての動作ステップ列について、ステップＳ２２２４〜Ｓ２２２６の処理を実行する。
【００８２】
次に、過大近似モデル生成部１２１は、前記ネットワーク機器の動作モデルから、通信パケットを転送する動作ステップをすべて抽出する（ステップＳ２２２７）。さらに、過大近似モデル生成部１２１は、前記抽出した動作ステップの直前に、前記通信パケットの転送回数を１増やす動作ステップを挿入する（ステップＳ２２２８）。過大近似モデル生成部１２１は、ステップＳ２２２７で抽出したすべての動作ステップについて、ステップＳ２２２８の処理を実行する。また、ネットワーク機器の動作モデルが個別に複数定義されている場合、過大近似モデル生成部１２１は、各動作モデルについて、上述の処理を実行する。
【００８３】
以上のように、第２の実施形態においても、ネットワーク検証装置１の検証コード生成部１２が、通信パケットのフィールドの具体値を取り扱わないようネットワークの動作を過大近似したモデルを生成し、前記過大近似モデルがプロパティを満たすか検証する検証コードを生成する。そして、モデル検査実行部１３が、前記検証コードを用いてモデル検査を実行することで、前記ネットワーク内の端末が送信するパケットの内容の違いを考慮する必要のない効率的なモデル検査を実施する。前記モデル検査において、前記過大近似モデルが前記プロパティを満たさないという結果が出た場合、反例妥当性確認部１４が、反例が対象ネットワークの本来の動作にも存在するかどうかを確認する。
【００８４】
従って、本実施形態によれば、ＯｐｅｎＦｌｏｗネットワーク以外のネットワークについても、効率的に網羅的な検証を実施し、不具合を漏れなく検出することができる。
【００８５】
［第３の実施形態］
続いて、上記第１、第２の実施形態のユーザインタフェースに改良を加えた本発明の第３の実施形態について図面を参照して詳細に説明する。以下、前記第１の実施形態と同様の部分は省略し、異なる部分についてのみ説明する。
【００８６】
［構成の説明］
図１１は、本発明の第３の実施形態のネットワーク検証装置の構成を示す図である。本実施形態の検証情報入力部３１は、検証情報受付部３１１と、検証情報雛形提供部３１２と、を含む。検証情報受付部３１１は、ネットワークを構成するすべての端末、スイッチ、コントローラ、ネットワーク機器等の動作モデル及びそれらの接続関係と、前記ネットワークが満たすべきプロパティと、を定義した検証情報Ｄ１１を入力として受け付ける。
【００８７】
検証情報雛形提供部３１２は、ユーザから検証情報の入力を受け付ける際、検証情報Ｄ１１の一部あるいは全部について典型的な雛形（テンプレート）を提供し、ユーザが前記雛形を選択することで、それを検証情報Ｄ１１の一部あるいは全部として利用し、検証情報受付部３１１に入力することが可能な機能を備える。
【００８８】
［動作の説明］
ユーザは、図５のステップＳ１１において、検証情報Ｄ１１を作成する際、検証情報雛形提供部３１２から所望の雛形をいくつか選択し、それらを用いて検証情報Ｄ１１を完成させ、検証情報受付部３１１に入力する。もちろん、第１の実施形態と同様に、ユーザが雛形を全く用いずに検証情報Ｄ１１を作成して入力してもよい。その他の動作は、本発明の第１の実施形態と同様のため省略する。
【００８９】
以上のように、本実施形態によれば、ネットワーク検証装置を利用する際の、ユーザの検証情報Ｄ１１の作成に要する負担を軽減することができる。さらに、本実施形態によれば、前記ユーザの負担軽減の結果として、検証全体の効率を向上させることもできる。
【００９０】
以上、本発明の各実施形態を説明したが、本発明は、上記した実施形態に限定されるものではなく、本発明の基本的技術的思想を逸脱しない範囲で、更なる変形・置換・調整を加えることができる。例えば、各図面に示した装置の構成は、本発明の理解を助けるための一例であり、これらの図面に示した構成に限定されるものではない。
【００９１】
最後に、本発明の好ましい形態を要約する。
［第１の形態］
（上記第１の視点によるネットワーク検証装置参照）
［第２の形態］
第１の形態のネットワーク検証装置において、
前記検証対象のネットワークに、ＯｐｅｎＦｌｏｗスイッチと、ＯｐｅｎＦｌｏｗコントローラとが含まれ、前記検証情報には、ＯｐｅｎＦｌｏｗスイッチとＯｐｅｎＦｌｏｗコントローラの動作モデルが定義されているネットワーク検証装置。
［第３の形態］
第１又は第２の形態のネットワーク検証装置において、
前記反例妥当性確認部は、
前記反例から、前記反例が実際に実行される際に満たされるべき制約に関する制約情報を取得して、前記制約情報から制約充足問題を生成する制約充足問題生成部と、
前記制約充足問題の解を求めることで、前記反例がネットワークの本来の動作でも実行可能かどうか判断する制約充足問題解決部と、
を備えるネットワーク検証装置。
［第４の形態］
第１から第３いずれか一の形態のネットワーク検証装置において、
前記検証情報入力部は、
ユーザから、前記検証情報の一部として、検証対象のネットワークのプロパティの入力を受け付けるネットワーク検証装置。
［第５の形態］
第１から第４いずれか一の形態のネットワーク検証装置において、
前記検証情報入力部は、
ユーザに対し、前記検証情報の一部あるいは全部について典型的な内容を定めた雛形を提供し、
前記雛形の選択により、前記検証情報の少なくとも一部の入力を受け付けるネットワーク検証装置。
［第６の形態］
（上記第２の視点によるネットワーク検証方法参照）
［第７の形態］
（上記第３の視点によるプログラム参照）
なお、上記第６、第７の形態は、第１の形態と同様に、第２〜第５の形態に展開することが可能である。
【００９２】
なお、上記の非特許文献の各開示を、本書に引用をもって繰り込むものとする。本発明の全開示（請求の範囲を含む）の枠内において、さらにその基本的技術思想に基づいて、実施形態ないし実施例の変更・調整が可能である。また、本発明の請求の範囲の枠内において種々の開示要素（各請求項の各要素、各実施形態ないし実施例の各要素、各図面の各要素等を含む）の多様な組み合わせ、ないし選択が可能である。すなわち、本発明は、請求の範囲を含む全開示、技術的思想にしたがって当業者であればなし得るであろう各種変形、修正を含むことは勿論である。特に、本書に記載した数値範囲については、当該範囲内に含まれる任意の数値ないし小範囲が、別段の記載のない場合でも具体的に記載されているものと解釈されるべきである。
【符号の説明】
【００９３】
１、１Ａ、３  ネットワーク検証装置
１１、３１  検証情報入力部
１２  検証コード生成部
１３  モデル検査実行部
１４  反例妥当性確認部
１５  検証結果出力部
１２１  過大近似モデル生成部
１２２  過大近似モデル変換部  
１４１  制約充足問題生成部
１４２  制約充足問題解決部
３１１  検証情報受付部
３１２  検証情報雛形提供部
【図１】
2014115759.tif 000003
【図２】
2014115759.tif 000004
【図３】
2014115759.tif 000005
【図４】
2014115759.tif 000006
【図５】
2014115759.tif 000007
【図６】
2014115759.tif 000008
【図７】
2014115759.tif 000009
【図８】
2014115759.tif 000010
【図９】
2014115759.tif 000011
【図１０】
2014115759.tif 000012
【図１１】
2014115759.tif 000013
【国際調査報告】
2014115759.tif 000014
2014115759.tif 000015