(57)【要約】  本発明は、状態遷移モデルの遷移で利用されるデータ集合を決定しながら探索を行うモデル検査において、冗長な探索をより十分に削減する技術を提供する。  モデル検査装置１は、検証情報取得部１１、モデル探索部１２、データ集合決定処理部１３、再探索制御部１４および検証結果出力部１５を備える。検証情報取得部１１は、検査対象の検証情報を取得する。検証情報は、状態遷移モデルおよびその検証内容を表す情報を含む。モデル探索部１２は、状態遷移モデルを遷移させて実行パスを得る。データ集合決定処理部１３は、データ利用を伴う遷移で用いられるデータ集合を決定する。再探索制御部１４は、実行パス上のバックトラック地点から再探索を行う際に、以前の探索での利用済みのデータを除外したデータ集合を用いるよう、モデル探索部１２を制御する。検証結果出力部１５は、検証結果を出力する。
2016079962.tif 000002
【特許請求の範囲】
【請求項１】
検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得する検証情報取得手段と、
前記状態遷移モデルを遷移させて実行パスを得るモデル探索手段と、
前記状態遷移モデルのデータ利用を伴う遷移で用いられるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理を行うデータ集合決定処理手段と、
前記実行パス上の遷移間での前記データ集合決定処理に関わる依存関係に基づきバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いるよう、前記モデル探索手段を制御する再探索制御手段と、
前記再探索制御手段の制御に基づく前記モデル探索手段の探索結果に基づいて、前記検証内容の検証結果を出力する検証結果出力手段と、
を備えたモデル検査装置。
【請求項２】
前記再探索制御手段は、前記再探索での前記データ利用を伴う遷移において、前記データ集合決定処理に関わる依存関係のある遷移間の順序を仮に入れ替えた場合の前記データ集合決定処理によるデータ集合から、前記利用済みのデータを除外したデータ集合を用いて、前記順序を入れ替えずに前記再探索を行うことを特徴とする請求項１に記載のモデル検査装置。
【請求項３】
前記再探索制御手段は、前記実行パス上の遷移間での前記データ集合決定処理に関わる依存関係を解析してバックトラック地点を生成する際に、前記バックトラック地点において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を求めることを特徴とする請求項１または請求項２に記載のモデル検査装置。
【請求項４】
前記再探索制御手段は、前記実行パス上の任意の遷移の組合せのうち、一方が前記データ集合決定処理の結果に基づくデータを利用する遷移であり、他方が前記データ集合決定処理の結果に影響を与える遷移である場合に、前記組合せ間に前記データ集合決定処理に関わる依存関係があると判断することを特徴とする請求項１から請求項３のいずれか１項に記載のモデル検査装置。
【請求項５】
前記状態遷移モデルが、端末間で送受信されるパケットを転送するスイッチおよび前記転送を制御するコントローラを含むネットワークを表すとき、
前記再探索制御手段は、前記実行パス上の任意の遷移の組合せのうち、一方が前記端末によるパケット送信を伴う遷移であり、他方が前記コントローラによるプログラム実行を伴う遷移である場合に、前記組合せ間に前記データ集合決定処理に関わる依存関係があると判断することを特徴とする請求項４に記載のモデル検査装置。
【請求項６】
コンピュータが、
検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得し、
前記状態遷移モデルを遷移させて実行パスを得、
前記実行パス上の遷移間で、データ利用を伴う遷移で用いるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理に関わる依存関係を解析し、
前記データ集合決定処理に関わる依存関係に基づいてバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いて再探索を行い、
探索結果に基づいて、前記検証内容の検証結果を出力するモデル検査方法。
【請求項７】
検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得する検証情報取得ステップと、
前記状態遷移モデルを遷移させて実行パスを得るモデル探索ステップと、
前記実行パス上の遷移間で、データ利用を伴う遷移で用いられるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理に関わる依存関係を解析する依存関係解析ステップと、
前記データ集合決定処理に関わる依存関係に基づいてバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いて再探索を行う再探索制御ステップと、
探索結果に基づいて、前記検証内容の検証結果を出力する検証結果出力ステップと、
をコンピュータ装置に実行させるモデル検査プログラムを記憶した記憶媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、状態遷移モデルを用いて検証を行う技術に関する。
【背景技術】
【０００２】
近年、システムやソフトウェアの複雑化・巨大化が進んでいる。複雑化・巨大化に対する一つの解決手段として、モデル検査による検証手法が知られている。モデル検査とは、検証対象を状態遷移系としてモデル化し、それを網羅的に探索することで、検査対象が仕様を満たすか否かを検証する技術である。モデル検査は、設計段階から適用でき、検査対象が仕様を満たすか否かを保証できる。このため、モデル検査は、システムやソフトウェアの信頼性を向上させるための技術として注目されている。また、最近では、モデル検査は、ネットワークの検証への適用も試みられている。【０００３】
例えば、非特許文献１には、ＯｐｅｎＦｌｏｗと呼ばれるネットワーク制御技術により制御されたネットワークを、モデル検査により検証する技術が開示されている。【０００４】
モデル検査は、上記のような特長を持つ一方、計算に必要なメモリや時間が、検査対象の規模に対し指数的に増大するという課題を持つ。そのため、実践的なシステムやソフトウェアの検証を目的としたモデル検査においては、探索の効率化が不可欠である。【０００５】
例えば、非特許文献２には、ＤＰＯＲ（Dynamic Partial Order Reduction）という技術が開示されている。ＤＰＯＲは、マルチスレッド環境モデルに対するモデル検査において、検証の観点で冗長な探索を枝刈りする技術である。ＤＰＯＲは、モデル検査対象の状態遷移系を探索する際、最初に適当なパスを１つ実行する。これを、実行パスと呼ぶ。そして、ＤＰＯＲは、その実行パスを構成する遷移系列の中に、互いの実行順序が実行結果に影響を及ぼす遷移の組合せが存在するか否かを確認する。このような遷移の組合せを、依存関係のある遷移と呼ぶ。依存関係のある遷移が存在する場合、ＤＰＯＲは、その組合せの実行順序を入れ替えたパスを探索するため、バックトラック地点を生成する。バックトラック地点は、その実行パスにおいてその組合せのうち先に行った遷移の直前の状態に生成される。バックトラック地点から探索は、その状態から前回までの実行パスとは異なる遷移（その組合せのうち先に行った遷移とは異なる遷移）を行うところから始められることになる。実行パスから、依存関係のある全ての遷移を検出し、検出した遷移のうち先に行った遷移の直前の状態にバックトラック地点を生成し終えたら、ＤＰＯＲは、実行パス上で一番後ろにあるバックトラック地点から探索を再開する。探索すべきバックトラック地点がなくなるまで、この手順が繰り返される。【０００６】
これにより、ＤＰＯＲは、検査対象の全ての実行パターンのうち、実行結果が異なるパスのみを探索することを可能とする。言い換えると、ＤＰＯＲは、検証結果が異ならないパス、つまり、検証の観点で冗長なパスの探索を枝刈りすることができ、探索を効率化する。【０００７】
非特許文献３には、ＤＰＯＲ−ＤＳ（Dynamic Partial Order Reduction in Distributed Systems）が開示されている。ＤＰＯＲ−ＤＳは、ＤＰＯＲを分散環境モデルのモデル検査向けに拡張した技術である。ＤＰＯＲ−ＤＳは、検査対象のモデルの環境の違いを吸収するため、バックトラック地点を生成する方法を変更している。ＤＰＯＲ−ＤＳは、実行パス上の遷移間の関係について、依存関係とは別に、分散環境モデルにおけるhappens-before関係を定義し、バックトラック地点の生成の判断に利用する。【０００８】
happens-before関係とは、あるモデル上で必ず成り立つ遷移間の実行順序関係である。例えば、あるパケットｐの送受信を行う遷移を考える。このとき、パケットｐの送信を行う遷移は、パケットｐの受信を行う遷移よりも必ず先に起こる。このように、モデル上の因果関係に基づいて、必ず成り立つ遷移間の順序関係を、happens-before関係という。【０００９】
ＤＰＯＲ−ＤＳは、実行パス上の遷移について、依存関係に加えてhappens-before関係の有無も解析する。そして、ＤＰＯＲ−ＤＳは、２つの遷移間に依存関係があったとしても、happens-before関係が成り立つ場合には、バックトラック地点を生成しない。【００１０】
また、ＤＰＯＲ−ＤＳは、バックトラック地点から探索を再開する際にも、依存関係のあった２つの遷移の組合せに関するhappens-before関係を考慮する。ここで、依存関係のあった２つの遷移の組合せのうち、先に行われた遷移をｔ１とし、後に行われた遷移をｔ２とする。このとき、ＤＰＯＲ−ＤＳは、遷移ｔ１およびｔ２の間に行われた遷移の中で、遷移ｔ２に対しhappens-before関係にあった遷移および遷移ｔ２を、再開する探索の最初に連続して行わせる。【００１１】
ＤＰＯＲ−ＤＳにおけるバックトラック地点からの探索の再開の具体例を、図１５に示す。図１５では、円がモデルの状態を表し、矢印が遷移を表す。ここでは、最初の探索においてｔａ、ｔｂ、ｔｃ、ｔｄの順に遷移が実行されたとする。そして、依存関係の解析により、ｔａおよびｔｄに依存関係があることが分かったとする。また、happens-before関係の解析により、ｔｃおよびｔｄにhappens-before関係があることが分かったとする。すなわち、ｔｃはｔｄより必ず先に行われる。【００１２】
すると、ＤＰＯＲ−ＤＳは、ｔａを行う直前の状態ｓ０にバックトラック地点ｂ１を生成する。そして、ＤＰＯＲ−ＤＳは、そのバックトラック地点ｂ１から探索を再開する際に、最初にｔｃおよびｔｄの遷移を行う。つまり、ｔｃは、依存関係のある２つの遷移の組合せ（ｔａおよびｔｄ）の間に行われた遷移（ｔｂおよびｔｃ）の中で、依存関係のある組合せのうち後に行われた遷移（ｔｄ）に対しhappens-before関係にあった遷移である。また、ｔｄは、依存関係のある２つの遷移の組合せのうち後に行われた遷移である。再探索においてその後は、遷移の順序の規定はなく、適当なパスが探索され実行される。つまり、この例では、バックトラック地点ｂ１から、例えばｔｃ、ｔｄ、ｔａ、ｔｂという順に遷移が実行される。このうち、最初のｔｃ、ｔｄは、前述の通り、ＤＰＯＲ−ＤＳの探索アルゴリズムにより実行の順番が規定されている部分である。また、残りのｔａ、ｔｂは、適当に実行の順番が決められた部分である。この最初の部分の順番の規定は、冗長な探索を削減することを目的とする工夫である。【００１３】
この工夫が行われない場合どうなるかを、図１６に具体例で示す。先程の例で、バックトラックにより探索を再開する際に最初に行う遷移を単に一つだけ（ｔｃだけ）規定する場合を想定する。この場合、バックトラック地点ｂ１からｔｃ、ｔａ、ｔｂ、ｔｄという順に遷移が実行され得る。ここで、バックトラック地点ｂ１の探索の再開は、依存関係のあるｔａおよびｔｄの順序を入れ替えて探索を行うことが目的であったが、この探索（２回目の探索）では入れ替えられていない。そこで、この場合、改めてｔｃ、ｔａ、ｔｂ、ｔｄのパスに対して依存関係の解析が行われることになる。そして、ｔａを行う直前の状態ｓ５にバックトラック地点ｂ２が生成されることになる。これにより、バックトラック地点ｂ２からの次の探索においてｔｃ、ｔｄ、ｔａ、ｔｂという所望の順序で遷移を発生させるパスの探索（３回目の探索）が可能となった。【００１４】
しかしながら、この場合、２回目の探索（ｔｃ、ｔａ、ｔｂ、ｔｄのパスの探索）は、検証の観点からは冗長であり、効率の観点からは無駄である。この冗長な探索を削減するため、バックトラックによる探索再開時の最初の遷移列を規定して、冗長なパスの探索を削減するという工夫を、ＤＰＯＲ−ＤＳは行っている。ここで、規定される最初の遷移列は、先程の例では、ｔｃおよびｔｄである。また、削減される冗長なパスは、先ほどの例では、ｔｃ、ｔａ、ｔｂ、ｔｄである。ＤＰＯＲ−ＤＳは、これらの手順により、分散環境モデルのモデル検査において、探索の枝刈りを可能としている。【００１５】
また、前述の非特許文献１には、ＯｐｅｎＦｌｏｗにより制御されたネットワークをモデル検査により状態探索する際に、データ（パケット）の利用を伴う遷移がある場合について記載されている。すなわち、このような遷移において、この関連技術は、ＯｐｅｎＦｌｏｗコントローラのプログラムを記号実行することにより、全ての遷移を実行できるようなパケットの代表値の集合を決定する。そして、この関連技術は、決定したデータ集合を用いて状態の探索を行う。そのようなデータ集合は、その要素であるパケットをそれぞれ入力としてＯｐｅｎＦｌｏｗコントローラプログラムを実行すると、結果的にそのプログラムの動作パターンの全てに基づく遷移を実行できるようなパケットの集合である。【００１６】
このように、主にテストやモデル検査といった技術において、用いるデータの集合を、プログラムの記号実行（あるいはデータの範囲分割を行うその他の技術）に基づき決定する手法を、ｃｏｎｃｏｌｉｃ（な）手法と呼ぶ。また、ｃｏｎｃｏｌｉｃ手法でデータを扱うことを、「ｃｏｎｃｏｌｉｃにデータを扱う」と表現する。以下では、ｃｏｎｃｏｌｉｃ手法により利用するデータの集合を決定する処理を、「ｃｏｎｃｏｌｉｃ処理」とも呼ぶ。
【先行技術文献】
【非特許文献】
【００１７】
【非特許文献１】Canini, M. et al.: “A NICE Way to Test ＯｐｅｎＦｌｏｗ Applications”, Proc. of NSDI, 2012.
【非特許文献２】Flanagan, C. et al.: “Dynamic partial-order reduction for model checking software”, Proc. of POPL ’05, pp. 110-121, 2005.
【非特許文献３】Yabandeh, M. et al.: “DPOR-DS: Dynamic Partial Order Reduction in Distributed Systems”, EPFL Technical Report NSL-REPORT-2009-005, 2009.
【発明の概要】
【発明が解決しようとする課題】
【００１８】
ここで、非特許文献1に記載されたようなｃｏｎｃｏｌｉｃにデータを扱うモデル検査において、非特許文献２、３に記載されたＤＰＯＲまたはＤＰＯＲ−ＤＳを適用して冗長な探索の枝刈りをするケースを考える。この場合、これらの関連技術を単純に組み合わせただけでは、後述するように、無駄な探索が発生する。つまり、このようなケースにおいては、上述した関連技術およびその組合せは、検証の観点で冗長な探索を発生させ、非効率的となるという課題があった。【００１９】
この課題について具体例を用いて説明する。まず、図１７に、検査対象の具体例としてのＯｐｅｎＦｌｏｗネットワークの構成を示す。図１７において、コントローラは、ＭＡＣ（Media Access Control）アドレスの学習を行う。スイッチおよびコントローラは、端末１および端末２のＭＡＣアドレスを既に学習しているものとする。このとき、端末３および端末４が、互いに１回ずつパケットを送信することを想定する。【００２０】
まず、最初の探索Ａでは、以下のように遷移が実行されたとする。
１）端末３がパケット１を送信
２）スイッチがパケット１を受信、コントローラにｐａｃｋｅｔ＿ｉｎ１を送信
３）コントローラがｐａｃｋｅｔ＿ｉｎ１を受信、ｆｌｏｗ＿ｍｏｄ１とｐａｃｋｅｔ＿ｏｕｔ１をスイッチに送信
４）スイッチがｆｌｏｗ＿ｍｏｄ１とｐａｃｋｅｔ＿ｏｕｔ１を受信、フローエントリをインストール、パケット１を端末４に転送
５）端末４がパケット２を送信
６）スイッチがパケット２を受信、コントローラにｐａｃｋｅｔ＿ｉｎ２を送信
７）コントローラがｐａｃｋｅｔ＿ｉｎ２を受信、ｆｌｏｗ＿ｍｏｄ２とｐａｃｋｅｔ＿ｏｕｔ２をスイッチに送信
８）スイッチがｆｌｏｗ＿ｍｏｄ２とｐａｃｋｅｔ＿ｏｕｔ２を受信、フローエントリをインストール、パケット２を端末３に転送
なお、上述の遷移の説明において、“ｐａｃｋｅｔ＿ｉｎ”は、受信したパケットにマッチする転送規則（フローエントリ）をスイッチが持たない場合に、コントローラに対して処理方法を問い合わせるメッセージである。また、“ｆｌｏｗ＿ｍｏｄ”は、スイッチに対してフローエントリの追加・修正を指示するメッセージである。また、“ｐａｃｋｅｔ＿ｏｕｔ”は、スイッチに対してパケットの転送を指示するメッセージである。また、“ｐａｃｋｅｔ＿ｉｎ”、“ｆｌｏｗ＿ｍｏｄ”、“ｐａｃｋｅｔ＿ｏｕｔ”に続く数字は、数字が同一で同種のメッセージが同一の内容を示すことを表している。【００２１】
また、上述の探索Ａにおいて、パケットの内容はｃｏｎｃｏｌｉｃに扱われる。具体的には、探索Ａにおいて遷移１および遷移５は、パケットの送信を行う。そこで、遷移１および遷移５をそれぞれ行う前に、コントローラのプログラムを記号実行することにより、そのプログラムの動作パターンを列挙可能なパケットの代表値の集合が求められる（ｃｏｎｃｏｌｉｃ処理）。そして、これらの遷移では、求められた集合のうち任意の１つのパケットが送信される。【００２２】
まず、遷移１の前のｃｏｎｃｏｌｉｃ処理では、以下の種類のパケットの集合が求まる。
・宛先ＭＡＣアドレスが端末１のＭＡＣアドレスであるパケット
・宛先ＭＡＣアドレスが端末２のＭＡＣアドレスであるパケット
・それ以外のパケット
これは、遷移１の前の状態では、スイッチおよびコントローラは、端末１および端末２のＭＡＣアドレスを既に学習しているためである。【００２３】
また、遷移５の前のｃｏｎｃｏｌｉｃ処理では、以下の種類のパケットの集合が求まる。
・宛先ＭＡＣアドレスが端末１のＭＡＣアドレスであるパケット
・宛先ＭＡＣアドレスが端末２のＭＡＣアドレスであるパケット
・宛先ＭＡＣアドレスが端末３のＭＡＣアドレスであるパケット
・それ以外のパケット
これは、遷移５の前の状態では、遷移３、４が行われているので、スイッチおよびコントローラは、端末１および端末２に加えて、端末３のＭＡＣアドレスを既に学習しているためである。【００２４】
探索Ａでは、遷移１および遷移５において、ｃｏｎｃｏｌｉｃ処理の結果から、それぞれ「それ以外のパケット」が選ばれている。実際には、探索Ａの他に、上記のパケットの種類の組み合わせに応じた探索が個別に行われるが、説明の簡略化のため、ここでは省略する。【００２５】
次に、探索Ａで実行されたパスの依存関係の解析が行われる。その結果、遷移８によるフローエントリのインストールが行われる前後で、遷移１の前のｃｏｎｃｏｌｉｃ処理の結果が変わることが分かる。すなわち、遷移１および遷移８には依存関係があることが分かる。そのため、次の探索では、遷移１を行う前（この場合、一番最初）までバックトラックし、遷移８を遷移１より先に行うパスが再探索される。【００２６】
そして、次の再探索Ｂにおいて、以下のように遷移が実行されたとする。
１）端末４がパケット２を送信（探索Ａの遷移５）
２）スイッチがパケット２を受信、コントローラにｐａｃｋｅｔ＿ｉｎ２を送信（探索Ａの遷移６）
３）コントローラがｐａｃｋｅｔ＿ｉｎ２を受信、ｆｌｏｗ＿ｍｏｄ２とｐａｃｋｅｔ＿ｏｕｔ２をスイッチに送信（探索Ａの遷移７）
４）スイッチがｆｌｏｗ＿ｍｏｄ２とｐａｃｋｅｔ＿ｏｕｔ２を受信、フローエントリをインストール、パケット２を端末３に転送（探索Ａの遷移８）
５）端末３がパケット１を送信（探索Ａの遷移１）
６）スイッチがパケット１を受信、コントローラにｐａｃｋｅｔ＿ｉｎ１を送信（探索Ａの遷移２）
７）コントローラがｐａｃｋｅｔ＿ｉｎ１を受信、ｆｌｏｗ＿ｍｏｄ１とｐａｃｋｅｔ＿ｏｕｔ１をスイッチに送信（探索Ａの遷移３）
８）スイッチがｆｌｏｗ＿ｍｏｄ１とｐａｃｋｅｔ＿ｏｕｔ１を受信、フローエントリをインストール、パケット１を端末４に転送（探索Ａの遷移４）
このような探索Ｂでは、遷移１（探索Ａの遷移５）の前のｃｏｎｃｏｌｉｃ処理では、以下の種類のパケットの集合が求まる。
・宛先ＭＡＣアドレスが端末１のＭＡＣアドレスであるパケット
・宛先ＭＡＣアドレスが端末２のＭＡＣアドレスであるパケット
・それ以外のパケット
これは、遷移１（探索Ａの遷移５）の前の状態では、スイッチおよびコントローラは、端末１および端末２のＭＡＣアドレスを既に学習しているためである。【００２７】
また、遷移５（探索Ａの遷移１）の前のｃｏｎｃｏｌｉｃ処理では、以下の種類のパケットの集合が求まる。
・宛先ＭＡＣアドレスが端末１のＭＡＣアドレスであるパケット
・宛先ＭＡＣアドレスが端末２のＭＡＣアドレスであるパケット
・宛先ＭＡＣアドレスが端末４のＭＡＣアドレスであるパケット
・それ以外のパケット
これは、遷移５（探索Ａの遷移１）の前の状態では、遷移３、４（探索Ａの遷移７、８）が行われているので、スイッチおよびコントローラは、端末１および端末２に加えて、端末４のＭＡＣアドレスを既に学習しているためである。【００２８】
探索Ｂでも、探索Ａと同様、いずれの遷移のｃｏｎｃｏｌｉｃ処理でも「それ以外のパケット」が選ばれている。探索Ａの場合と同様、実際には探索Ｂの他に、上記のパケットの種類の組み合わせに応じた探索が個別に行われるが、説明の簡略化のため、ここでは省略する。【００２９】
上述したように、探索Ｂの遷移５（探索Ａにおける遷移１）の前のｃｏｎｃｏｌｉｃ処理の結果は、探索Ａの遷移１の前のｃｏｎｃｏｌｉｃ処理の結果と変わっている。このように、ｃｏｎｃｏｌｉｃにデータを扱うモデル検査においても、ｃｏｎｃｏｌｉｃ処理の結果が変わる遷移を考慮した依存関係を解析することで、ＤＰＯＲ（あるいはその拡張技術であるＤＰＯＲ−ＤＳ）を適用することができる。【００３０】
一方で、上記の非特許文献１および２、３の組み合わせは、特にＯｐｅｎＦｌｏｗ等のネットワーク制御技術により制御されるネットワークのモデル検査を行う場合には、探索に無駄が多い。その理由について説明する。【００３１】
図１８は、探索した状態遷移を模式的に示す図である。図１８において、遷移を表す矢印の上には、遷移番号を振っている。なお、遷移番号は、説明の都合上、上述の探索Ａにおける遷移番号を示したものである。また、各実行パスの右側には、各探索における遷移１でどのようなパケットが送信されたかを記載している。【００３２】
図１８において、探索Ａ’、Ａ’’は、探索Ａと同様の遷移の順序で、遷移１におけるｃｏｎｃｏｌｉｃ処理の結果から、それぞれ「宛先が端末１のＭＡＣアドレスのパケット」、「宛先が端末２のＭＡＣアドレスのパケット」が選択されたパスである。また、探索Ｂ、Ｂ’、Ｂ’’、Ｂ’’’は、遷移１および遷移８の順序を探索Ａから入れ替え、遷移１におけるｃｏｎｃｏｌｉｃ処理の結果からそれぞれパケットが選択されたパスである。ここで、遷移８を遷移１より先に行った再探索Ｂ、Ｂ’、Ｂ’’、Ｂ’’’のうち、破線で囲った部分は無駄な探索を示している。すなわち、この破線で囲った部分は、遷移の順序こそ違うものの、遷移１を遷移８より先に行った探索に対して、検証の観点から等価な探索を行っていると言える。ここで、遷移１および遷移８の順序を入れ替えた理由は、遷移１および遷移８の順序を入れ替えると、遷移１の前に行うｃｏｎｃｏｌｉｃ処理の結果が変わるという依存関係が存在するからである。【００３３】
一方で、遷移１および遷移８を入れ替えても、遷移１の前に行うｃｏｎｃｏｌｉｃ処理の結果以外は変わらない。遷移１および遷移８の依存関係は、データをｃｏｎｃｏｌｉｃに扱うモデル検査だからこそ生じたものである。つまり、データをｃｏｎｃｏｌｉｃに扱うことのない通常のモデル検査においては、遷移１および遷移８に依存関係はない。そのため、再度の探索Ｂ、Ｂ’、Ｂ’’、Ｂ’’’において、遷移１および遷移８の順序を入れ替える前の遷移１と同じ種類のパケットを送信しているパスの探索は、遷移の順序が入れ替わっているだけで検証の観点から等価である。したがって、そのような実行パスの２回目以降の探索は無駄である。具体的には、探索Ａ、Ａ’、Ａ’’における遷移１で送信しているパケットと同種類のパケットを送信している探索Ｂ、Ｂ’、Ｂ’’の探索は、無駄となる。【００３４】
このように、非特許文献１に記載のｃｏｎｃｏｌｉｃにデータを扱うモデル検査では、非特許文献２または３に記載のＤＰＯＲを適用しても、無駄な探索が発生する。すなわち、状態遷移モデルの遷移で利用されるデータ集合を決定しながら探索を行うモデル検査では、冗長な探索の枝刈りを行う既存の技術を用いるだけでは、無駄な探索の発生を十分に削減できない、という課題があった。【００３５】
本発明は、上述の課題を解決するためになされたものである。すなわち、本発明は、状態遷移モデルの遷移で利用されるデータ集合を決定しながら探索を行うモデル検査において、冗長な探索をより十分に削減する技術を提供することを目的とする。
【課題を解決するための手段】
【００３６】
上記目的を達成するために、本発明のモデル検査装置は、検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得する検証情報取得手段と、前記状態遷移モデルを遷移させて実行パスを得るモデル探索手段と、前記状態遷移モデルのデータ利用を伴う遷移で用いられるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理を行うデータ集合決定処理手段と、前記実行パス上の遷移間での前記データ集合決定処理に関わる依存関係に基づきバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いるよう、前記モデル探索手段を制御する再探索制御手段と、前記再探索制御手段の制御に基づく前記モデル探索手段の探索結果に基づいて、前記検証内容の検証結果を出力する検証結果出力手段と、を備える。【００３７】
また、本発明のモデル検査方法は、コンピュータが、検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得し、前記状態遷移モデルを遷移させて実行パスを得、前記実行パス上の遷移間で、データ利用を伴う遷移で用いるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理に関わる依存関係を解析し、前記データ集合決定処理に関わる依存関係に基づいてバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いて再探索を行い、探索結果に基づいて、前記検証内容の検証結果を出力する。【００３８】
また、本発明の記憶媒体は、検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得する検証情報取得ステップと、前記状態遷移モデルを遷移させて実行パスを得るモデル探索ステップと、前記実行パス上の遷移間で、データ利用を伴う遷移で用いられるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理に関わる依存関係を解析する依存関係解析ステップと、前記データ集合決定処理に関わる依存関係に基づいてバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いて再探索を行う再探索制御ステップと、探索結果に基づいて、前記検証内容の検証結果を出力する検証結果出力ステップと、をコンピュータ装置に実行させるモデル検査プログラムを記憶している。
【発明の効果】
【００３９】
本発明は、状態遷移モデルの遷移で利用されるデータ集合を決定しながら探索を行うモデル検査において、冗長な探索をより十分に削減する技術を提供することができる。
【図面の簡単な説明】
【００４０】
【図１】本発明の第１の実施の形態としてのモデル検査装置の機能ブロック構成を示す図である。
【図２】本発明の第１の実施の形態としてのモデル検査装置のハードウェア構成の一例を示す図である。
【図３】本発明の第１の実施の形態としてのモデル検査装置の動作を説明するフローチャートである。
【図４】本発明の第２の実施の形態としてのモデル検査装置の機能ブロック構成を示す図である。
【図５】本発明の第２の実施の形態としてのモデル検査装置の動作の概略を説明するフローチャートである。
【図６】本発明の第２の実施の形態としてのモデル検査装置の実行パス生成動作の詳細を説明するフローチャートである。
【図７】本発明の第２の実施の形態としてのモデル検査装置のバックトラック地点生成動作の概要を説明するフローチャートである。
【図８】本発明の第２の実施の形態としてのモデル検査装置のバックトラック地点生成のために行う前処理の詳細を説明するフローチャートである。
【図９】本発明の第２の実施の形態としてのモデル検査装置の依存関係解析動作の詳細を説明するフローチャートである。
【図１０】本発明の第２の実施の形態としてのモデル検査装置の通常依存関係解析動作の詳細を説明するフローチャートである。
【図１１】本発明の第２の実施の形態としてのモデル検査装置のｃｏｎｃｏｌｉｃ依存関係解析動作の詳細を説明するフローチャートである。
【図１２】本発明の第２の実施の形態としてのモデル検査装置の実行パス要素へのバックトラック地点生成動作の詳細を説明するフローチャートである。
【図１３】本発明の第２の実施の形態としてのモデル検査装置の他の実行パス要素へのバックトラック地点生成動作の詳細を説明するフローチャートである。
【図１４】本発明の第２の実施の形態としてのモデル検査装置のバックトラック地点からの再探索動作の詳細を説明するフローチャートである。
【図１５】関連技術における再探索を説明する模式図である。
【図１６】関連技術においてバックトラック地点からの最初の遷移列を規定しない場合の再探索を説明する模式図である。
【図１７】関連技術の課題を説明するための検査対象のネットワーク構成を示す図である。
【図１８】関連技術において発生する無駄な探索を説明するための模式図である。
【発明を実施するための形態】
【００４１】
以下、本発明の実施の形態について、図面を参照して詳細に説明する。
【００４２】
（第１の実施の形態）
本発明の第１の実施の形態としてのモデル検査装置１の機能ブロック構成を図１に示す。図１において、モデル検査装置１は、検証情報取得部１１と、モデル探索部１２と、データ集合決定処理部１３と、再探索制御部１４と、検証結果出力部１５とを備える。なお、図１において、機能ブロックを示す矩形間を結ぶ矢印の向きは、一例を示すものであり、機能ブロック間の信号の向きを限定するものではない。
【００４３】
ここで、モデル検査装置１は、図２に示すようなハードウェア要素によって構成可能である。図２において、モデル検査装置１は、ＣＰＵ（Central Processing Unit）１００１、メモリ１００２、出力装置１００３、および、入力装置１００４を含む。メモリ１００２は、ＲＡＭ（Random Access Memory）、ＲＯＭ（Read Only Memory）、補助記憶装置（ハードディスク等）等によって構成される。出力装置１００３は、ディスプレイ装置やプリンタ等のように、情報を出力する装置によって構成される。入力装置１００４は、キーボードやマウス等のように、ユーザ操作の入力を受け付ける装置によって構成される。
【００４４】
この場合、モデル検査装置１の各機能ブロックは、メモリ１００２に格納されるコンピュータ・プログラムを読み込んで実行するとともに出力装置１００３および入力装置１００４を制御するＣＰＵ１００１によって構成される。なお、モデル検査装置１およびその各機能ブロックのハードウェア構成は、上述の構成に限定されない。
【００４５】
次に、モデル検査装置１の各機能ブロックについて説明する。
【００４６】
検証情報取得部１１は、検証情報を取得する。検証情報は、状態遷移モデルおよびその検証内容を表す情報を含む。検証情報は、例えば、その検証内容を状態遷移モデルが満たすか否かが設定されるプロパティを含んでいてもよい。例えば、検証情報取得部１１は、検証情報として、あらかじめメモリ１００２に記憶された情報を取得してもよい。また、モデル探索部１２は、検証情報として、入力装置１００４または可搬型記憶媒体等を介して入力される情報を取得してもよい。
【００４７】
モデル探索部１２は、状態遷移モデルを遷移させて実行パスを得る。また、モデル探索部１２は、状態遷移モデルを遷移させることにより、検証内容を検査する。例えば、モデル探索部１２は、状態遷移モデルを遷移させる度に、その状態が検証内容を満たしているか否かを判定してもよい。また、モデル探索部１２は、検証内容を満たさないと判定した時点で、探索を終了してもよい。また、モデル探索部１２は、データ利用を伴う遷移を行う際には、後述のデータ集合決定処理部１３によって決定されるデータ集合から任意の１つを選んで遷移を行う。
【００４８】
データ集合決定処理部１３は、状態遷移モデルのデータ利用を伴う遷移において、利用されるデータの代表値の集合を決定する。以下、そのようなデータの代表値の集合を、単に「データ集合」とも記載する。このような代表値の集合は、その要素である代表値をそれぞれ入力としてその遷移を実行すると、その遷移に関する全ての動作パターンを実行できるような代表値の集合である。
【００４９】
再探索制御部１４は、実行パス上における遷移間でのデータ集合決定処理に関わる依存関係に基づいて、バックトラック地点から再探索を行う。そして、再探索制御部１４は、再探索でのデータ利用を伴う遷移において、データ集合決定処理結果の差分を用いる。ここで、データ集合処理結果の差分とは、データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合をいう。
【００５０】
また、データ集合決定処理に関わる依存関係のある遷移とは、それらの遷移間の順序を入れ替えると、少なくとも一方の遷移におけるデータ集合決定処理の結果が変わってくる関係をいう。例えば、再探索制御部１４は、実行パス上の次のような遷移の組合せ間に、データ集合決定処理に関わる依存関係があると判断してもよい。そのような遷移の組合せとは、すなわち、一方が、データ集合決定処理の結果に基づくデータを利用する遷移であり、他方が、そのデータ集合決定処理の結果に影響を与える遷移であってもよい。
【００５１】
このような場合、データ集合決定処理に関わる依存関係のある遷移の順序を仮に入れ替えて再探索を行うと、上述の一方の遷移において利用されるデータ集合決定処理の結果が、順序を入れ替えない場合とは異なってくる。そこで、この場合、再探索制御部１４は、実行パス上でデータ集合決定処理に関わる依存関係のある遷移のうち、データ集合決定処理の結果に基づくデータを利用する遷移の直前の状態を、バックトラック地点として決定してもよい。
【００５２】
そして、再探索制御部１４は、バックトラック地点からの再探索でのデータ利用を伴う遷移において利用するデータ集合として、次のような情報を用いる。すなわち、再探索制御部１４は、データ集合決定処理に関わる依存関係のある遷移間の順序を仮に入れ替えた場合のデータ集合処理結果の差分を用いる。具体的に、順序を仮に入れ替えた場合にデータ集合決定処理によって求められるデータ集合には、以前の探索において該当する遷移で既に利用済みのデータが含まれていることを考慮する。そこで、再探索制御部１４は、再探索におけるデータ利用を伴う遷移において、上述の順序を仮に入れ替えた場合のデータ集合決定処理によるデータ集合から、以前の探索において利用済みのデータを除外したデータ集合を求める。そして再探索制御部１４は、そのデータ集合を用いて、再探索を行えばよい。なお、再探索制御部１４は、このようなデータ集合処理結果の差分を求める処理を、データ集合決定処理に関わる依存関係を解析してバックトラック地点を決定する際に実行可能である。
【００５３】
検証結果出力部１５は、モデル探索部１２による検証内容の検証結果を、出力装置１００３等に出力する。例えば、検証結果出力部１５は、モデル探索部１２による探索の結果、検証内容が満たされると判定されたか否かを出力してもよい。また、検証結果出力部１５は、検証内容が満たされない場合、検証内容が満たされない反例を併せて出力してもよい。
【００５４】
以上のように構成されたモデル検査装置１の動作を、図３を参照して説明する。
【００５５】
図３では、まず、検証情報取得部１１は、検証情報を取得する（ステップＳ１）。
【００５６】
次に、モデル探索部１２は、検証情報に含まれる状態遷移モデルを遷移させて任意の実行パスを得る（ステップＳ２）。
【００５７】
このとき、前述のように、モデル探索部１２は、データ利用を伴う遷移を行う際には、データ集合決定処理部１３によって決定されるデータ集合から１つ選んで遷移を行う。また、前述のように、モデル探索部１２は、遷移を行いながら検証内容の検証を行う。
【００５８】
次に、再探索制御部１４は、ステップＳ２で得られた実行パス上の遷移間での、データ集合決定処理に関わる依存関係を解析する。そして、再探索制御部１４は、解析結果に基づいて、バックトラック地点を生成する（ステップＳ３）。
【００５９】
次に、モデル探索部１２は、実行パス上にバックトラック地点があれば（ステップＳ４でＹｅｓ）、最も深い（一番後ろの）バックトラック地点からの再探索を行う。そして、モデル探索部１２は、再探索による実行パスを得る（ステップＳ５）。なお、前述したように、再探索制御部１４は、再探索におけるデータ利用を伴う遷移において、データ集合処理結果の差分を用いるよう、モデル探索部１２を制御する。
【００６０】
そして、モデル検査装置１の動作は、再探索により得られた実行パスについて、ステップＳ３〜Ｓ５の動作を繰り返す。すなわち、再探索制御部１４は、再探索により得られた実行パス上の遷移間でのデータ集合決定処理に関わる依存関係に基づき、バックトラック地点を生成する。そして、再探索制御部１４は、最も深いバックトラック地点から再探索を行う。
【００６１】
そして、実行パス上に再探索していないバックトラック地点がなくなると（ステップＳ４でＮｏ）、検証結果出力部１５は、検証結果を出力する（ステップＳ６）。そして、モデル検査装置１は、動作を終了する。
【００６２】
次に、本発明の第１の実施の形態の効果について述べる。
【００６３】
本発明の第１の実施の形態としてのモデル検査装置は、状態遷移モデルの遷移で利用されるデータ集合を決定しながら探索を行うモデル検査において、冗長な探索をより十分に削減することができる。
【００６４】
その理由について述べる。本実施の形態では、モデル探索部が、状態遷移モデルを遷移させて実行パスを得る際に、データ利用を伴う遷移の際には、データ集合決定処理部により決定されたデータの代表値の集合（データ集合）を用いて探索を行う。そして、再探索制御部が、実行パス上の遷移間でのデータ集合決定処理に関わる依存関係に基づきバックトラック地点を決定し、バックトラック地点からの再探索を制御する。すなわち、再探索制御部が、再探索でのデータ利用を伴う遷移において、データ集合処理結果の差分を用いるよう、モデル探索部を制御するからである。このデータ集合処理結果の差分とは、再探索でのデータ利用を伴う遷移においてデータ集合決定処理により求まるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したものである。
【００６５】
このように、本発明の第１の実施の形態は、状態遷移モデルの遷移で利用されるデータ集合を決定しながら探索を行うモデル検査において、バックトラックによる再探索でデータ利用を伴う遷移を行う場合、上述のデータ集合処理結果の差分を用いる。これにより、本実施の形態は、検証の観点で、過去の探索と等価なデータを用いた無駄な探索を行わずに済む。
【００６６】
また、詳細には、本実施の形態では、再探索制御部が、次のような場合に実行パス上の遷移の組合せに、データ集合決定処理に関わる依存関係があると判断する。すなわち、一方がデータ集合決定処理の結果に基づくデータを利用する遷移であり、他方がそのデータ集合決定処理の結果に影響を与える遷移の場合である。このとき、本実施の形態では、再探索制御部が、そのような依存関係のある遷移の組合せのうち、データ集合決定処理の結果に基づくデータを利用する遷移の直前にバックトラック地点を生成する。そして、再探索制御部が、再探索でのデータ利用を伴う遷移において、依存関係のある遷移間の順序を仮に入れ替えた場合のデータ集合処理結果の差分を用いて、実際には遷移の順序を入れ替えずに再探索を行うよう、モデル探索部を制御する。つまり、このデータ集合処理結果の差分とは、データ集合決定処理に関わる依存関係のある遷移間の順序を仮に入れ替えた場合に、データ集合決定処理によって求まるデータ集合から、以前の探索で利用済みのデータを除外したデータ集合である。
【００６７】
ここで、データ集合決定処理に関わる依存関係のある遷移の組合せ間では、その順序を入れ替えた場合、データ集合決定処理の結果は変わるが、それ以外の結果に関しては違いがない。つまり、仮にその順序を入れ替えたとしても、データ集合決定処理に基づくデータ利用を伴う遷移は、データ集合決定処理の結果に影響を与える遷移の前で行っても、後で行っても、利用するデータ集合が異なるだけで、その他の結果に違いが出ない。したがって、このような遷移の順序を入れ替えて探索を行うことは、検証の観点からの意味はない。
【００６８】
このように、本実施の形態は、遷移の順序を入れ替えることなく、仮に順序を入れ替えた場合のデータ集合決定処理結果の差分を利用することにより、無駄な探索を削減しながら、探索処理を効率化している。
【００６９】
（第２の実施の形態）
次に、本発明の第２の実施の形態について図面を参照して詳細に説明する。なお、本実施の形態の説明において参照する各図面において、本発明の第１の実施の形態と同一の構成および同様に動作するステップには同一の符号を付して本実施の形態における詳細な説明を省略する。また、本実施の形態では、本発明のモデル検査装置の検査対象として、ネットワーク制御技術により制御されるネットワークを表すネットワークモデルを適用する例について説明する。なお、本実施の形態では、ネットワーク制御技術として、例えば、ＯｐｅｎＦｌｏｗを想定する。ただし、本実施の形態が検証対象とする状態遷移モデルが表すネットワークを制御する技術は、ＯｐｅｎＦｌｏｗに限定されるものではない。
【００７０】
［構成の説明］
まず、本発明の第２の実施の形態としてモデル検査装置２の構成を、図４に示す。図４において、モデル検査装置２は、本発明の第１の実施の形態としてのモデル検査装置１に対して、次の点で構成が異なる。すなわち、モデル検査装置２は、検証情報取得部１１に替えて検証情報取得部２１と、モデル探索部１２に替えてモデル探索部２２と、データ集合決定処理部１３に替えてデータ集合決定処理部２３と、再探索制御部１４に替えて再探索制御部２４とを備える。なお、図４において、機能ブロックを示す矩形間を結ぶ矢印の向きは、一例を示すものであり、機能ブロック間の信号の向きを限定するものではない。
【００７１】
また、モデル検査装置２および各機能ブロックは、図２を参照して説明した本発明の第１の実施の形態と同様のハードウェア要素によって構成可能である。なお、モデル検査装置２およびその各機能ブロックのハードウェア構成は、上述の構成に限定されない。
【００７２】
本実施の形態では、ネットワークモデルの仕様を、以下に示すものとして説明する。
【００７３】
まず、ネットワークモデルにおける状態の定義について説明する。状態は、（Ｔ，Ｓ，Ｃ，Ｐ，Ｍ，Ｑ）の六つ組として定義される。ここで、Ｔは、端末の集合を表す。Ｔの要素ｔ（ｔ∈Ｔ）は、その状態を表す変数ｓｖを持つ。また、Ｓは、スイッチの集合を表す。Ｓの要素ｓ（ｓ∈Ｓ）は、フローエントリの集合を表す変数Ｅを持つ。フローエントリは、スイッチにインストールされている転送規則である。また、Ｅの要素ｅ（ｅ∈Ｅ）は、フローエントリを表し、（ｍｒ，ａｆ）の組として定義される。ｍｒは、マッチングルールの内容を表す。ａｆは、アクションフィールドの内容を表す。また、Ｃは、コントローラの集合を表す。Ｃの要素ｃ（ｃ∈Ｃ）は、コントローラｃの各動作モデルが大域的に扱う変数の集合を表す変数Ｖを持つ。Ｖの要素ｖ（ｖ∈Ｖ）は、コントローラの動作モデルが大域的に扱う変数の１つである。ｖは、（ｖｎ， ｖｖ）の組として定義される。ｖｎは、変数の名前を表す。ｖｖは、その変数の内容を表す。また、Ｐは、パケットの集合を表す。Ｐの要素ｐ（ｐ∈Ｐ）は、パケットの内容を表す変数ｐｖを持つ。また、Ｍは、制御メッセージの集合を表す。例えば、ネットワークモデルが、ＯｐｅｎＦｌｏｗネットワークを表す場合、制御メッセージは、ＯｐｅｎＦｌｏｗメッセージである。制御メッセージＭの要素ｍ（ｍ∈Ｍ）は、制御メッセージの内容を表す変数ｍｖを持つ。Ｑは、通信ポートの集合を表す。Ｑの要素ｑ（ｑ∈Ｑ）は、パケットおよび制御メッセージを格納するＦＩＦＯ（First In, First Out）キューにより実現される通信ポートである。
【００７４】
また、検査対象のネットワークは、端末、スイッチ、および、コントローラの各装置を含む。各装置は、他の装置（端末、スイッチ、または、コントローラ）と通信するための通信ポートを持つ。通信ポートは、互いに通信可能な他の装置との間に、送信用および受信用に１つずつ設けられる。つまり、ある１つの端末、スイッチ、または、コントローラにとっての送信用通信ポートは、他の１つの端末、スイッチ、または、コントローラにとっての受信用通信ポートである。また、ある１つの端末、スイッチ、または、コントローラにとっての受信用通信ポートは、他の１つの端末、スイッチ、または、コントローラにとっての送信用通信ポートである。以降、パケットを送受信するための通信ポートを、パケット送信用通信ポート、パケット受信用通信ポートとも記載する。また、制御メッセージを送受信するための通信ポートを、制御メッセージ送信用通信ポート、制御メッセージ受信用通信ポートとも記載する。また、端末、スイッチ、および、コントローラを総称して、ノードと呼ぶ場合もある。
【００７５】
次に、ネットワークモデルにおける遷移の定義について説明する。遷移は、ネットワークモデルの示すネットワークに存在する端末、スイッチ、および、コントローラのいずれかが、特定の単位の動作を実行することにより、モデルの状態が変化する様子を表す。特定の単位の動作とは、例えば、以下の６種類であってもよい。
１：端末のパケット送信
２：端末のパケット受信
３：スイッチのフローエントリ適用
４：スイッチの問い合わせメッセージ送信
５：スイッチの制御メッセージ受信
６：コントローラのプログラム実行
上述の６種類の動作について、それぞれ詳しく説明する。
【００７６】
まず、端末のパケット送信動作について説明する。端末は、自身の状態ｓｖに応じて、パケット送信動作を実行可能である。端末のパケット送信動作では、端末ｔは、パケットｐを１つ生成して、端末ｔの送信用通信ポート（すなわち、あるスイッチｓの受信用通信ポート）にパケットｐを格納する。そして、この動作により、端末ｔの状態ｓｖの内容が変更される（変更されない場合もある）。
【００７７】
次に、端末のパケット受信動作について説明する。端末は、自身のパケット受信用通信ポートにパケットが１つ以上格納されている場合、パケット受信動作を実行可能である。端末のパケット受信動作では、端末ｔは、パケットが１つ以上格納されているパケット受信用通信ポートｑから、最初に格納されたパケットｐを取り出す。そして、この動作により、パケットｐの内容ｐｖに応じて、端末ｔの状態ｓｖの内容が変更される（変更されない場合もある）。
【００７８】
次に、スイッチのフローエントリ適用動作について説明する。スイッチは、自身のパケット受信用通信ポートにパケットが１つ以上格納されており、かつ、そのパケット受信用通信ポートに最初に格納されたパケットに適用可能なフローエントリを持つ場合、フローエントリ適用動作を実行することが可能である。スイッチのフローエントリ適用動作では、スイッチｓは、まずパケットが１つ以上格納されているパケット受信用通信ポートｑから、最初に格納されたパケットｐを取り出す。次に、スイッチｓは、そのスイッチｓが持つ各フローエントリのマッチングルールｍｒと、パケットｐの内容ｐｖとを比較することにより、パケットｐに適用可能なフローエントリｅを１つ選ぶ。最後に、スイッチｓは、選んだフローエントリｅのアクションフィールドａｆに従う動作を実行する。
【００７９】
次に、スイッチの問い合わせメッセージ送信動作について説明する。問い合わせメッセージは、制御メッセージの１つである。例えば、ネットワークモデルが、ＯｐｅｎＦｌｏｗネットワークを表す場合、問い合わせメッセージは、ｐａｃｋｅｔ＿ｉｎメッセージである。スイッチは、自身のパケット受信用通信ポートにパケットが１つ以上格納されており、かつ、そのパケット受信用通信ポートに最初に格納されたパケットに適用可能なフローエントリを持たない場合、問い合わせメッセージ送信動作を実行可能である。スイッチの問い合わせメッセージ送信動作では、スイッチｓは、まずパケットが１つ以上格納されているパケット受信用通信ポートｑ１から、最初に格納されたパケットｐを取り出す。次に、スイッチｓは、パケットｐの情報を含めた問い合わせメッセージｍを、コントローラとの間の制御メッセージ送信用通信ポートｑ２に格納する。
【００８０】
次に、スイッチの制御メッセージ受信動作について説明する。スイッチは、自身の制御メッセージ受信用通信ポートに制御メッセージが１つ以上格納されている場合、制御メッセージ受信動作を実行可能である。スイッチの制御メッセージ受信動作では、スイッチｓは、まず制御メッセージが１つ以上格納されている制御メッセージ受信用通信ポートｑから、最初に格納された制御メッセージｍを取り出す。次に、スイッチｓは、取り出した制御メッセージｍの内容ｍｖに従い動作を実行する。
【００８１】
次に、コントローラのプログラム実行動作について説明する。コントローラは、自身の制御メッセージ受信用通信ポートに制御メッセージが１つ以上格納されている場合、プログラム実行動作を実行可能である。コントローラのプログラム実行動作では、コントローラｃは、まず制御メッセージが１つ以上格納されている制御メッセージ受信用通信ポートｑから、最初に格納された制御メッセージｍを１つ取り出す。次に、コントローラｃは、ネットワークモデルにおいて定義されているコントローラの動作のうち、取り出した制御メッセージｍの内容ｍｖに対応する動作を実行する。もし、ｍｖに対応する動作が定義されていない場合、コントローラｃは、ネットワーク制御技術の仕様により規定されているデフォルトの動作を実行すればよい。
【００８２】
検証情報取得部２１は、本発明の第１の実施の形態と同様に構成される。ただし、検証情報取得部２１は、検査対象の検証情報として、上述したようなネットワークモデルおよびそれに対する検証内容を表す情報を取得する点が異なる。なお、ネットワークモデルは、上述の定義に限らず、各種公知のネットワーク制御技術の仕様に則った状態遷移系であれば何でもよい。また、検証情報は、ネットワークモデルに対する検証プロパティを含んでいてもよい。検証プロパティは、例えば、「パケット転送ループが発生しない」ことや、「パケット落ちが発生しない」ことであってもよい。なお、取得した検証情報には、検証プロパティが必ずしも含まれていなくてよい。検証情報に検証プロパティが含まれていない場合、検証情報取得部２１は、そのネットワークモデルに典型的な検証プロパティを検証してもよい。
【００８３】
モデル探索部２２は、検証情報に含まれるネットワークモデルの状態を、上述したような各ノードの動作により遷移させて実行パスを得る。また、モデル探索部２２は、ネットワークモデルの状態を遷移させるにあたり、遷移後の状態において、検証プロパティの成否を判断する。そして、モデル探索部２２は、検証プロパティが満たされない場合には、その時点でモデル検査を終了してもよい。また、モデル探索部２２は、検証プロパティが満たされないという結果と、それを示す具体例である反例とを含む結果情報を生成する。
【００８４】
次に、本実施の形態でモデル探索部２２が生成する実行パスのデータ構造について説明する。実行パスは、実行パス要素を要素とする配列（あるいはそれに準ずるデータ構造）によって構成される。実行パス要素は、（ｓｔ，ｔｒ，Ｂａｃｋｔｒａｃｋ，Ｄｏｎｅ）の四つ組で定義される。ｓｔは、ある時点でのネットワークモデルの状態を表す。また、ｔｒは、状態ｓｔから実行された遷移を表す。また、Ｂａｃｋｔｒａｃｋは、遷移の集合であり、バックトラックの際に状態ｓｔから実行される遷移の集合を表す。また、Ｄｏｎｅは、遷移の集合であり、過去の探索において状態ｓｔから実行した遷移の集合を表す。ＢａｃｋｔｒａｃｋからＤｏｎｅを引いた差集合は、状態ｓｔからバックトラックして実行される遷移であるが、まだされていない遷移の集合を表す。
【００８５】
次に、遷移のデータ構造について説明する。遷移は、（ｎｏｄｅ，ｔｙｐｅ，ｓｅｎｄ，ｒｅｃｖ，ｐｏｒｔ，ｉｎｓｔａｌｌ，ａｐｐｌｙ)の七つ組で定義される。ｎｏｄｅは、その遷移で動作した端末・スイッチ・コントローラを表す。また、ｔｙｐｅは、遷移の種類（上述の６種類の動作による遷移のいずれかを表す値）を表す。また、ｓｅｎｄは、その遷移で送信されたパケットあるいは制御メッセージの集合を表す。また、ｒｅｃｖは、その遷移で受信されたパケットあるいは制御メッセージを表す。また、ｐｏｒｔは、その遷移で受信されたパケットあるいは制御メッセージが格納されていた受信用通信ポートを表す。また、ｉｎｓｔａｌｌは、その遷移でインストールされたフローエントリを表す。また、ａｐｐｌｙは、その遷移で適用されたフローエントリを表す。このデータ構造に基づく遷移データは、モデル探索部２２による探索において、状態が遷移した際に、その遷移の内容に応じて、各フィールドの値が適切に設定された上で生成される。
【００８６】
データ集合決定処理部２３は、ｃｏｎｃｏｌｉｃ処理を行う。ｃｏｎｃｏｌｉｃ処理とは、ｃｏｎｃｏｌｉｃ手法を用いて、遷移で利用されるデータの代表値からなるデータ集合を決定する処理である。また、ｃｏｎｃｏｌｉｃ手法とは、遷移で用いられるデータの集合を、プログラムの記号実行（あるいはデータの範囲分割を行うその他の技術）に基づき決定する手法をいうものとする。データ集合決定処理部２３は、公知のｃｏｎｃｏｌｉｃ手法を採用してｃｏｎｃｏｌｉｃ処理を行えばよい。
【００８７】
具体的には、データ集合決定処理部２３は、例えば、パケットの送信を伴う遷移において、ｃｏｎｃｏｌｉｃ処理を用いてその遷移で用いられるパケットの代表値の集合を決定する。そのようなデータ集合は、その要素であるパケットをそれぞれ入力としてその遷移を実行すると、その遷移で動作するノードの動作パターンの全てに基づく遷移を実行できるようなパケットの集合である。
【００８８】
再探索制御部２４は、モデル探索部２２から実行パスを受け取り、実行パス上の２つの遷移間の依存関係およびｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する。そして、再探索制御部２４は、解析結果に基づいて、実行パス上にバックトラック地点を生成する。また、再探索制御部２４は、バックトラック地点からの再探索でのデータ利用を伴う遷移において、利用可能なデータ集合として、ｃｏｎｃｏｌｉｃ処理結果の差分を生成する。そして、再探索制御部２４は、バックトラック地点からｃｏｎｃｏｌｉｃ処理結果の差分を用いて再探索を行うよう、モデル探索部２２を制御する。
【００８９】
ここで、依存関係とは、２つの遷移間に成り立つ関係である。直感的には、２つの遷移の実行順序を変更すると、状態遷移系におけるそれらの遷移後の結果が変わる場合、２つの遷移間に依存関係が成り立つ（依存関係がある）という。あるいは、２つの遷移のうち片方の遷移を行うことで、もう片方の遷移が行えるようになったり行えなくなったりする場合、２つの遷移間に依存関係が成り立つ（依存関係がある）という。遷移ｔ１およびｔ２の間に依存関係が「成り立たない」条件は、一般的には以下のように定義される。
１：状態ｓ１において遷移ｔ１が実行可能であり、かつ、状態ｓ１から遷移ｔ１により状態ｓ２へ遷移する場合、遷移ｔ２は状態ｓ１およびｓ２の両方で実行可能か、両方で実行不可能かのいずれかである。
２：状態ｓ１において遷移ｔ１とｔ２が実行可能である場合、状態ｓ１から遷移ｔ１を実行した先の状態で遷移ｔ２を実行した先の状態がｓ２であるならば、状態ｓ１から遷移ｔ２を実行した先の状態で遷移ｔ１を実行した先の状態もｓ２である。
【００９０】
ただし、上記の一般的な依存関係の成否を解析するのはコストが高い。そこで、本実施の形態では、上述したネットワークモデルの仕様と、ＤＰＯＲのアルゴリズムとを考慮し、以下のように依存関係を定義する。
・遷移ｔ１で動作したノードと遷移ｔ２で動作したノードが同じノードである。
本実施の形態では、このような定義に基づく依存関係を「通常依存関係」と呼ぶことにする。再探索制御部２４は、この定義にしたがって、２つの遷移間の通常依存関係を解析する。
【００９１】
また、再探索制御部２４は、通常依存関係の解析に加えて、２つの遷移間のｃｏｎｃｏｌｉｃ依存関係を解析する。ｃｏｎｃｏｌｉｃ依存関係とは、ｃｏｎｃｏｌｉｃ処理の結果の変化を考慮した依存関係をさすものとする。データをｃｏｎｃｏｌｉｃに扱う（つまり、ｃｏｎｃｏｌｉｃ処理の発生する）モデル検査においては、上述した通常依存関係に加え、ｃｏｎｃｏｌｉｃ処理の結果の変化を考慮した依存関係を考える必要がある。ｃｏｎｃｏｌｉｃ依存関係が成り立つ条件は、以下のように定義される。
・遷移ｔ１および遷移ｔ２のいずれかが「ｃｏｎｃｏｌｉｃ処理の結果に基づくデータを利用する遷移」であり、もう一方が「ｃｏｎｃｏｌｉｃ処理の結果に影響を与える遷移」である。本実施の形態では、検証対象がネットワークモデルであるため、再探索制御部２４は、次の定義にしたがってｃｏｎｃｏｌｉｃ依存関係を解析する。
・遷移ｔ１および遷移ｔ２のいずれかが「端末のパケット送信による遷移」であり、もう一方が「コントローラのプログラム実行による状態遷移」である。
【００９２】
また、再探索制御部２４は、通常依存関係およびｃｏｎｃｏｌｉｃ依存関係に加えて、２つの遷移間のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する。ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係とは、あるモデル上で必ず成り立つ遷移間の実行順序関係である。例えば、上述したネットワークモデルで、あるメッセージｍの送受信を行う遷移を考える。このとき、メッセージｍの送信を行う遷移ｔ１は、メッセージｍの受信を行う遷移ｔ２より前に必ず起こる。このように、モデル上の因果関係から必ず成り立つ遷移間の実行順序関係を、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係という。遷移ｔ１が遷移ｔ２より必ず前に起こるｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を、「ｔ１→ｔ２」と記述するものとする。本実施の形態では、上述したネットワークモデルの仕様と、ＤＰＯＲのアルゴリズムとを考慮し、以下のようにｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を定義する。
１：遷移ｔ１で送信されるパケットあるいは制御メッセージと、遷移ｔ２で受信されるパケットあるいは制御メッセージが同じである場合、ｔ１→ｔ２
２：遷移ｔ１でインストールされるフローエントリと、遷移ｔ２で適用されるフローエントリが同じである場合、ｔ１→ｔ２
３：遷移ｔ１で受信されるパケットあるいは制御メッセージｐｍ１と、遷移ｔ２で受信されるパケットあるいは制御メッセージｐｍ２とが、同じ受信用通信ポートｑに格納されている。さらに、ｐｍ１をｑに格納した遷移ｔ３と、ｐｍ２をｑに格納した遷移ｔ４とがｔ３→ｔ４である場合、ｔ１→ｔ２
４：ｔ１→ｔ２であり、ｔ２→ｔ３である場合、ｔ１→ｔ３
再探索制御部２４は、以上のように定義される通常依存関係、ｃｏｎｃｏｌｉｃ依存関係、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する。そして、再探索制御部２４は、解析結果に基づいて、モデル探索部２２によるネットワークモデルの探索のバックトラックを制御する。
【００９３】
例えば、再探索制御部２４は、モデル探索部２２によるネットワークモデルの探索を、通常依存関係およびｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係に基づいてバックトラックさせながら制御する。ここで、通常依存関係およびｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係に基づく探索の制御については、公知の手法を採用すればよい。例えば、再探索制御部２４は、非特許文献２または３に記載されたＤＰＯＲまたはＤＰＯＲ−ＤＳ等の技術を採用すればよい。
【００９４】
また、再探索制御部２４は、モデル探索部２２によるネットワークモデルの探索を、ｃｏｎｃｏｌｉｃ依存関係およびｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係に基づいてバックトラックさせながら制御する。ここで、ｃｏｎｃｏｌｉｃ依存関係がある２つの遷移のうち、端末のパケット送信による遷移をｔ１とし、コントローラのプログラム実行による遷移をｔ２とする。この場合、再探索制御部２４は、遷移ｔ１の前の状態をバックトラック地点として決定する。そして、再探索制御部２４は、そのバックトラック地点からの再探索において遷移ｔ１と同じ端末によるパケット送信を表す遷移ｔ１’を行う際に、利用可能なパケットの集合として、ｃｏｎｃｏｌｉｃ処理結果の差分を次のように生成する。具体的には、再探索制御部２４は、遷移ｔ１およびｔ２の順序を仮に入れ替えた場合に、遷移ｔ１’についてｃｏｎｃｏｌｉｃ処理を行った結果のデータ集合をまず求める。そして、再探索制御部２４は、このデータ集合から、遷移ｔ１で既に利用したパケットを除外したデータ集合を、ｃｏｎｃｏｌｉｃ処理結果の差分として生成すればよい。
【００９５】
［動作の説明］
以上のように構成されたモデル検査装置２の動作について、図面を参照して説明する。まず、モデル検査装置２の動作の概略を図５に示す。
【００９６】
図５では、まず、検証情報取得部２１は、ネットワークモデルおよび検証プロパティを含む検証情報を取得する（ステップＳ１１）。
【００９７】
次に、モデル探索部２２は、ネットワークモデルを状態遷移させて、任意の実行パスを生成する（ステップＳ１２）。このステップの詳細については後述する。
【００９８】
次に、再探索制御部２４は、実行パス上の通常依存関係、ｃｏｎｃｏｌｉｃ依存関係、およびｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する。そして、再探索制御部２４は、解析結果に基づいて、実行パス上にバックトラック地点を生成し、バックトラック地点を含む実行パスを生成する（ステップＳ１３）。このステップの詳細については後述する。
【００９９】
次に、モデル探索部２２は、実行パス上にバックトラック地点があれば（ステップＳ１４でＹｅｓ）、一番深い（一番後ろの）バックトラック地点から、ネットワークモデルを再び状態遷移させる。そして、モデル探索部２２は、再探索により新たな実行パスを生成する（ステップＳ１５）。
【０１００】
次に、モデル探索部２２は、新たに生成した実行パスについて、ステップＳ１３〜Ｓ１５の動作を繰り返す。
【０１０１】
そして、実行パス上に再探索していないバックトラック地点がなくなると（ステップＳ１４でＮｏ）、検証結果出力部１５は、検証結果を出力する（ステップＳ１６）。具体的には、モデル探索部２２は、検証プロパティの成否と、検証プロパティが満たされない場合にはそれを示す反例とを含む検証結果を出力すればよい。
【０１０２】
以上で、モデル検査装置２は動作を終了する。
【０１０３】
次に、ステップＳ１２における実行パス生成動作の詳細について、図６を参照して説明する。
【０１０４】
図６では、まず、モデル探索部２２は、検証情報に含まれるネットワークモデルの初期状態ｓｔ０を生成し、状態ｓｔ＝ｓｔ０とする（ステップＡ１）。
【０１０５】
次に、モデル探索部２２は、状態ｓｔから実行可能な遷移が１つ以上あるか否かを判断する（ステップＡ２）。
【０１０６】
ここで、実行可能な遷移が１つ以上ある場合、モデル探索部２２は、状態ｓｔが実行可能な遷移の中から、遷移ｔｒ＿ｓｔを任意に１つ選ぶ（ステップＡ３）。
【０１０７】
次に、モデル探索部２２は、選んだ遷移ｔｒ＿ｓｔが「端末のパケット送信による遷移」であるか否かを判断する（ステップＡ４）。
【０１０８】
ここで、「端末のパケット送信による遷移」でない場合、モデル探索部２２は、状態ｓｔに遷移ｔｒ＿ｓｔを行わせて、次の状態ｓｔ’を生成する（ステップＡ５）。
【０１０９】
次に、モデル探索部２２は、新しい実行パス要素ｅ１＝（ｓｔ， ｔｒ＿ｓｔ，{  ｝，｛ｔｒ＿ｓｔ｝）を実行パススタックに積んで、ステップＡ１０に進む（ステップＡ６）。
【０１１０】
ここで、実行パススタックとは、現在探索中である実行パスの過程を保存するスタックであり、その要素は実行パス要素である。
【０１１１】
一方、ステップＡ４において、遷移ｔｒ＿ｓｔが「端末のパケット送信による遷移」である場合、データ集合決定処理部２３は、状態ｓｔに対してｃｏｎｃｏｌｉｃ処理を行う。これにより、データ集合決定処理部２３は、遷移ｔｒ＿ｓｔにおいて送信可能な代表パケットのデータ集合ｐ＿ｓｅｔを求める（ステップＡ７）。
【０１１２】
ここで、ｃｏｎｃｏｌｉｃ処理は、ネットワークモデルにおいて定義されるコントローラの動作のうち、スイッチからの問い合わせメッセージに対応する動作について全ての動作パターンを列挙可能なパケットの集合ｐ＿ｓｅｔを、記号実行により求める処理である。ただし、ｃｏｎｃｏｌｉｃ処理の内容は、これに限らない。例えば、データ集合決定処理部２３は、ネットワークモデル中の各スイッチにインストールされている全てのフローエントリを考慮し、データの範囲分割を行うことにより、全ての動作パターンを列挙可能なパケットの集合を求めてもよい。
【０１１３】
次に、モデル探索部２２は、データ集合ｐ＿ｓｅｔの要素ｐ１， ｐ２，・・・，ｐnの中から代表パケットｐｍを任意に１つ選ぶ。そして、モデル探索部２２は、選んだ代表パケットｐｍを利用する遷移ｔｒ＿ｓｔ＿ｍを状態ｓｔに行わせて、次の状態ｓｔ’を生成する（ステップＡ８）。ここで、遷移ｔｒ＿ｓｔ＿ｍは、代表パケットｐｍを送信する「端末のパケット送信による遷移」である。
【０１１４】
次に、モデル探索部２２は、新しい実行パス要素ｅ２＝（ｓｔ， ｔｒ＿ｓｔ＿ｍ，ｔｒ＿ｓｔ＿ｓｅｔ，｛ｔｒ＿ｓｔ＿ｍ｝）を実行パススタックに積んで、ステップＡ１０に進む（ステップＡ９）。
【０１１５】
このステップにおいて、モデル探索部２２は、新しい実行パス要素ｅ２のＢａｃｋｔｒａｃｋとしてのｔｒ＿ｓｔ＿ｓｅｔを、次のようにして生成する。具体的には、モデル探索部２２は、データ集合ｐ＿ｓｅｔから、利用済みのパケットｐｍを取り除いたデータ集合をｐ＿ｓｅｔ’とする。そして、モデル探索部２２は、遷移ｔｒ＿ｓｔ＿ｍのｓｅｎｄ（送信パケット）をｐ＿ｓｅｔ’の各要素（ｐ１， ｐ２，・・・， ｐｍ−１， ｐｍ＋１，・・・， ｐn）で置き換えた遷移の集合ｔｒ＿ｓｔ＿ｓｅｔを生成する。つまり、ｔｒ＿ｓｔ＿ｓｅｔの要素はｔｒ＿ｓｔ＿１， ｔｒ＿ｓｔ＿２，・・・， ｔｒ＿ｓｔ＿ｍ−１， ｔｒ＿ｓｔ＿ｍ＋１，・・・， ｔｒ＿ｓｔ＿nである。また、ｔｒ＿ｓｔ＿1のｓｅｎｄはｐ１、ｔｒ＿ｓｔ＿２のｓｅｎｄはｐ２、と続き、ｔｒ＿ｓｔ＿nのｓｅｎｄはｐｎである。
【０１１６】
次に、モデル探索部２２は、状態ｓｔ＝ｓｔ’として（ステップＡ１０）、ステップＡ２からの動作を繰り返す。
【０１１７】
また、ステップＡ２において、状態ｓｔから実行可能な遷移が１つもない場合、モデル探索部２２は、その時点での実行パススタックの内容を、実行パスとして（ステップＡ１１）、実行パス生成動作を終了する。
【０１１８】
ステップＳ１３におけるバックトラック地点生成動作の詳細について、図７を参照して説明する。
【０１１９】
図７では、まず、再探索制御部２４は、実行パスに対して、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析するための前処理を行う（ステップＢ１）。このステップの詳細については後述する。
【０１２０】
次に、再探索制御部２４は、通常依存関係、ｃｏｎｃｏｌｉｃ依存関係およびｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する。そして、再探索制御部２４は、解析結果に基づいて、実行パスにバックトラック地点を生成する（ステップＢ２）。このステップの詳細については後述する。
【０１２１】
次に、再探索制御部２４は、バックトラック地点を生成した実行パスをモデル探索部２２に返して（ステップＢ３）、バックトラック地点生成動作を終了する。
【０１２２】
次に、ステップＢ１における前処理の詳細について、図８を参照して説明する。
【０１２３】
この動作では、再探索制御部２４は、解析対象の実行パス中の各要素について、その要素の遷移とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にある（必ず先に起こる）遷移を持つ実行パス要素を求めていく。そのため、再探索制御部２４は、実行パス要素毎に、データ構造（ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合）を用意する。ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合は、実行パス要素の遷移に対してｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にある遷移を持つ実行パス要素の集合を保持する。
【０１２４】
図８では、まず、再探索制御部２４は、解析対象の実行パスから、ｉ番目の実行パス要素ｅ１を選び出す（ステップＣ１）。なお、このステップを最初に実行する場合のｉは２である。
【０１２５】
次に、再探索制御部２４は、ｊ番目の実行パス要素ｅ２を選び出す（ステップＣ２）。なお、このステップを最初に実行する場合のｊは１である。
【０１２６】
次に、再探索制御部２４は、実行パス要素ｅ１の遷移および実行パス要素ｅ２の遷移を比較し、「実行パス要素ｅ２の遷移→実行パス要素ｅ１の遷移」（ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係）であるか否かを確認する（ステップＣ３）。
【０１２７】
ここで、ステップＣ３の動作を詳細に説明する。ステップＣ３では、まず、再探索制御部２４は、実行パス要素ｅ１の遷移の受信メッセージｒｅｃｖが、実行パス要素ｅ２の送信メッセージ集合ｓｅｎｄに含まれるか否かを判断する。含まれる場合は、再探索制御部２４は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がある（ｅ２の遷移→ｅ１の遷移）とする。含まれない場合は、再探索制御部２４は、実行パス要素ｅ１の遷移で適用したフローエントリと、実行パス要素ｅ２の遷移でインストールしたフローエントリとが一致するか否かを判断する。一致する場合は、再探索制御部２４は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がある（ｅ２の遷移→ｅ１の遷移）とする。一致しない場合は、再探索制御部２４は、実行パス要素ｅ１およびｅ２の遷移で使用した受信用通信ポートｐｏｒｔが一致するか否かを判断する。一致しない場合は、再探索制御部２４は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がないとする。一致する場合は、再探索制御部２４は、解析対象の実行パスの中から、実行パス要素ｅ３および実行パス要素ｅ４を探す。実行パス要素ｅ３は、実行パス要素ｅ１の遷移の受信メッセージｒｅｃｖを含むｓｅｎｄを有する遷移を持つ。実行パス要素ｅ４は、実行パス要素ｅ２の遷移の受信メッセージｒｅｃｖを含むｓｅｎｄを有する遷移を持つ。そして、再探索制御部２４は、実行パス要素ｅ３のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合にｅ４が含まれるか否かを確認する。含まれる場合は、再探索制御部２４は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がある（ｅ２の遷移→ｅ１の遷移）とする。含まれない場合は、再探索制御部２４は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がないとする。
【０１２８】
このようにして、ステップＣ３において、「実行パス要素ｅ２の遷移→実行パス要素ｅ１の遷移」（ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係）であると判断した場合について説明する。この場合、再探索制御部２４は、実行パス要素ｅ１のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合（最初は空）に、実行パス要素ｅ２自身と、実行パス要素ｅ２のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に含まれる全ての実行パス要素とを追加する（ステップＣ４）。
【０１２９】
ステップＣ４の実行後、または、ステップＣ３においてｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係でないと判断した場合、再探索制御部２４は、ｊの値を1増やす（ステップＣ５）。
【０１３０】
そして、再探索制御部２４は、ｊの値がｉ以上でない場合（ステップＣ６でＮｏ）、ステップＣ２からＣ５を繰り返す。もし、ｊの値がｉ以上になったら（ステップＣ６でＹｅｓ）、再探索制御部２４は、ｉの値を1増やし、ｊの値を1にする（ステップＣ７）。
【０１３１】
そして、再探索制御部２４は、ｉの値が解析対象の実行パスの長さより大きくなければ（ステップＣ８でＮｏ）、ステップＣ１からＣ７を繰り返す。ｉの値が解析対象の実行パスの長さより大きくなれば（ステップＣ８でＹｅｓ）、再探索制御部２４は、前処理を終了する。
【０１３２】
次に、ステップＢ２における依存関係解析動作の詳細について、図９を参照して説明する。
【０１３３】
図９では、まず、再探索制御部２４は、解析対象の実行パスから、ｉ番目の実行パス要素ｅ１を選び出す（ステップＤ１）。なお、このステップを最初に実行する場合のｉは１である。
【０１３４】
次に、再探索制御部２４は、解析対象の実行パスから、ｊ番目の実行パス要素ｅ２を選び出す（ステップＤ２）。なお、このステップを最初に実行する場合のｊは２である。
【０１３５】
次に、再探索制御部２４は、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移とについて、通常依存関係の解析を行う。そして、再探索制御部２４は、通常依存関係の解析結果に基づいて、実行パスにバックトラック地点を生成する（ステップＤ３）。このステップの詳細については後述する。
【０１３６】
次に、再探索制御部２４は、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移とについて、ｃｏｎｃｏｌｉｃ依存関係の解析を行う。そして、再探索制御部２４は、ｃｏｎｃｏｌｉｃ依存関係の解析結果に基づいて、実行パスにバックトラック地点を生成する（ステップＤ４）。このステップの詳細については後述する。
【０１３７】
次に、再探索制御部２４は、ｊの値を1増やす（ステップＤ５）。そして、再探索制御部２４は、ｊの値が解析対象の実行パスの長さ以下の間（ステップＤ６でＮｏ）、ステップＤ２からＤ５を繰り返す。
【０１３８】
そして、再探索制御部２４は、ｊの値が解析対象の実行パスの長さより大きくなったら（ステップＤ６でＹｅｓ）、ｉの値を1増やし、ｊの値をｉ＋１とする（ステップＤ７）。
【０１３９】
そして、再探索制御部２４は、ｉの値が実行パスの長さ以下の間（ステップＤ８でＮｏ）、ステップＤ１からＤ７を繰り返す。ｉの値が実行パスの長さより大きくなったら（ステップＤ８でＹｅｓ）、再探索制御部２４は、依存関係解析動作を終了する。
【０１４０】
次に、ステップＤ３における通常依存関係の解析動作の詳細について、図１０を参照して説明する。
【０１４１】
図１０では、まず、再探索制御部２４は、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移とを比較し、それらの間に、通常依存関係およびｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係が、それぞれあるか否かをチェックする（ステップＥ１、Ｅ２）。
【０１４２】
具体的には、再探索制御部２４は、実行パス要素ｅ１およびｅ２の遷移の動作ノードｎｏｄｅが一致する場合、これらの間に通常依存関係があるとしてもよい。また、再探索制御部２４は、実行パス要素ｅ２のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に実行パス要素ｅ１が含まれていなければ、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がないとする。
【０１４３】
ここで、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移との間に、通常依存関係があり（ステップＥ１でＹｅｓ）、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がない（ステップＥ２でＮｏ）と判断された場合について説明する。この場合、再探索制御部２４は、実行パス要素ｅ１にバックトラック地点を生成する（ステップＥ３）。
【０１４４】
具体的には、再探索制御部２４は、実行パス要素ｅ２のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に含まれる実行パス要素のうち、解析対象の実行パス中で最前方にある実行パス要素ｅ３を選ぶ。そして、再探索制御部２４は、実行パス要素ｅ３の遷移を、実行パス要素ｅ１のバックトラック集合Ｂａｃｋｔｒａｃｋに追加することで、バックトラック地点を生成する。
【０１４５】
一方、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移との間に、通常依存関係がないか（ステップＥ１でＮｏ）、または、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がある（ステップＥ２でＹｅｓ）と判断された場合について説明する。この場合、再探索制御部２４は、バックトラック地点を生成する処理を行わない。
【０１４６】
以上で、再探索制御部２４は、通常依存関係の解析動作を終了する。
【０１４７】
次に、ステップＤ４におけるｃｏｎｃｏｌｉｃ依存関係の解析動作の詳細について、図１１を参照して説明する。
【０１４８】
図１１では、まず、再探索制御部２４は、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移とを比較し、それらの間に、ｃｏｎｃｏｌｉｃ依存関係およびｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係が、それぞれあるか否かをチェックする（ステップＦ１、Ｆ２）。
【０１４９】
具体的には、再探索制御部２４は、これらの２つの遷移のいずれか一方が「端末のパケット送信による遷移」であり、他方が「コントローラのプログラム実行による状態遷移」である場合、ｃｏｎｃｏｌｉｃ依存関係があるとする。また、再探索制御部２４は、実行パス要素ｅ２のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に実行パス要素ｅ１が含まれていなければ、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がないとする。
【０１５０】
ここで、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移との間に、ｃｏｎｃｏｌｉｃ依存関係があり（ステップＦ１でＹｅｓ）、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がない（ステップＦ２でＮｏ）と判断された場合について説明する。この場合、再探索制御部２４は、実行パス要素ｅ１の遷移が「端末のパケット送信による遷移」であるか否かを判断する（ステップＦ３）。
【０１５１】
ここで、ステップＦ３において、実行パス要素ｅ１の遷移が「端末のパケット送信による遷移」であると判断した場合、再探索制御部２４は、実行パス要素ｅ１にバックトラック地点を生成する（ステップＦ４）。このステップの詳細については後述する。
【０１５２】
一方、ステップＦ３において実行パス要素ｅ１の遷移が「端末のパケット送信による遷移」でないと判断した場合について説明する。この場合、実行パス要素ｅ２の遷移が「端末のパケット送信による遷移」である。この場合、再探索制御部２４は、実行パス要素ｅ２にバックトラック地点を生成する（ステップＦ５）。このステップの詳細については後述する。
【０１５３】
なお、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移との間に、ｃｏｎｃｏｌｉｃ依存関係がないか（ステップＦ１でＮｏ）、または、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がある（ステップＦ２でＹｅｓ）と判断された場合について説明する。この場合、再探索制御部２４は、バックトラック地点を生成する処理を行わない。
【０１５４】
以上で、再探索制御部２４は、ｃｏｎｃｏｌｉｃ依存関係の解析動作を終了する。
【０１５５】
次に、ステップＦ４における実行パス要素ｅ１へのバックトラック地点生成動作の詳細について、図１２を参照して説明する。
【０１５６】
ここでは、ステップＤ１で選び出した実行パス要素ｅ１（ｉ番目）の遷移ｔｒ１と、ステップＤ２で選び出した実行パス要素ｅ２（ｊ番目）の遷移ｔｒ２の間に、ｃｏｎｃｏｌｉｃ依存関係がある。また、遷移ｔｒ1は「端末のパケット送信による遷移」である。
【０１５７】
そこで、図１２では、まず、再探索制御部２４は、実行パス要素ｅ２の次の実行パス要素ｅ４（ｊ＋１番目）の状態ｓｔに対して、ｃｏｎｃｏｌｉｃ処理を行う。これにより、再探索制御部２４は、代表パケットの集合ｐ＿ｓｅｔを求める（ステップＧ１）。
【０１５８】
このようにして求められる代表パケットの集合ｐ＿ｓｅｔは、遷移ｔｒ２を実行した後の状態ｓｔに対するｃｏｎｃｏｌｉｃ処理結果である。すなわち、このようにして求められる代表パケットの集合ｐ＿ｓｅｔは、仮に遷移ｔｒ２を遷移ｔｒ１より前に実行した場合に、遷移ｔｒ１を行う前の状態に対するｃｏｎｃｏｌｉｃ処理結果の集合と等価である。
【０１５９】
次に、再探索制御部２４は、遷移の集合ｔｒ３＿ｓｅｔを生成する（ステップＧ２）。ここで、遷移の集合ｔ３＿ｓｅｔは、遷移ｔｒ１のｓｅｎｄ（送信パケット）をｐ＿ｓｅｔの各要素（ｐ１， ｐ２，・・・， ｐn）で置き換えた遷移の集合である。つまり、ｔｒ３＿ｓｅｔの要素は、ｔｒ３＿１，ｔｒ３＿２，・・・，ｔｒ３＿nであり、ｔｒ３＿1のｓｅｎｄはｐ１、ｔｒ３＿２のｓｅｎｄはｐ２、と続き、ｔｒ３＿nのｓｅｎｄはｐｎとなっている。
【０１６０】
次に、再探索制御部２４は、実行パス要素ｅ１に、バックトラック地点を生成する（ステップＧ３）。具体的には、再探索制御部２４は、実行パス要素ｅ１のバックトラック集合Ｂａｃｋｔｒａｃｋに、ｔｒ３＿ｓｅｔを足す（集合の和演算を行う）ことで、バックトラック地点を生成する。
【０１６１】
以上で、再探索制御部２４は、実行パス要素ｅ１へのバックトラック地点生成動作を終了する。
【０１６２】
次に、ステップＦ５における実行パス要素ｅ２へのバックトラック地点生成動作の詳細について、図１３を参照して説明する。
【０１６３】
ここでは、ステップＤ１で選び出した実行パス要素ｅ１（ｉ番目）の遷移ｔｒ１と、ステップＤ２で選び出した実行パス要素ｅ２（ｊ番目）の遷移ｔｒ２との間に、ｃｏｎｃｏｌｉｃ依存関係がある。また、遷移ｔｒ２は、「端末のパケット送信による遷移」である。
【０１６４】
そこで、図１３では、まず、再探索制御部２４は、実行パス要素ｅ１の状態ｓｔに対してｃｏｎｃｏｌｉｃ処理を行う。これにより、再探索制御部２４は、代表パケットの集合ｐ＿ｓｅｔを求める（ステップＨ１）。
【０１６５】
このようにして求められる代表パケットの集合ｐ＿ｓｅｔは、遷移ｔｒ１を実行する前の状態ｓｔに対するｃｏｎｃｏｌｉｃ処理結果である。すなわち、このようにして求められる代表パケットの集合ｐ＿ｓｅｔは、仮に遷移ｔｒ２を遷移ｔｒ１より前に実行した場合に、遷移ｔｒ２を行う前の状態に対するｃｏｎｃｏｌｉｃ処理結果の集合と等価である。
【０１６６】
次に、再探索制御部２４は、遷移の集合ｔｒ３＿ｓｅｔを生成する（ステップＨ２）。ここで、遷移の集合ｔｒ３＿ｓｅｔは、遷移ｔｒ２のｓｅｎｄ（送信パケット）をｐ＿ｓｅｔの各要素（ｐ１， ｐ２，・・・， ｐn）で置き換えた遷移の集合である。つまり、ｔｒ３＿ｓｅｔの要素はｔｒ３＿1， ｔｒ３＿２，・・・，ｔｒ３＿ｎである。また、ｔｒ３＿1のｓｅｎｄはｐ１、ｔｒ３＿２のｓｅｎｄはｐ２、と続き、ｔｒ３＿nのｓｅｎｄはｐｎとなっている。
【０１６７】
次に、再探索制御部２４は、実行パス要素ｅ２に、バックトラック地点を生成する（ステップＨ３）。具体的には、再探索制御部２４は、実行パス要素ｅ２のバックトラック集合Ｂａｃｋｔｒａｃｋに、ｔｒ３＿ｓｅｔを足す（集合の和演算を行う）ことで、バックトラック地点を生成する。
【０１６８】
以上で、再探索制御部２４は、実行パス要素ｅ２へのバックトラック地点生成動作を終了する。
【０１６９】
なお、ステップＧ１およびステップＨ１におけるｃｏｎｃｏｌｉｃ処理は、ステップＳ１２（ステップＡ７）におけるｃｏｎｃｏｌｉｃ処理と同様である。また、ステップＧ３およびステップＨ３では、バックトラック対象となる遷移を集合で扱い、和演算を行う。これにより、再探索制御部２４は、バックトラック対象となる遷移が重複して行われることのないように、モデル探索部２２を制御可能となる。
【０１７０】
次に、ステップＳ１５におけるバックトラック動作の詳細について、図１４を参照して説明する。
【０１７１】
図１４では、まず、モデル探索部２２は、実行パススタックの内容を、ステップＳ１３で取得した、バックトラック地点を含む実行パスに置き換える（ステップＩ１）。
【０１７２】
次に、モデル探索部２２は、実行パススタックにおいて、バックトラック地点を持つ実行パス要素のうち、一番後ろにある実行パス要素ｅ１を探し出す。そして、モデル探索部２２は、ｅ１より後ろの実行パス要素（ｅ１は含まない）を、実行パススタックから取り除く（ステップＩ２）。
【０１７３】
ここで、バックトラック地点を持つ実行パス要素とは、バックトラック集合ＢａｃｋｔｒａｃｋからＤｏｎｅを引いた差集合が空でない実行パス要素である。また、実行パススタックの最後の実行パス要素は、実行パス要素ｅ１となる。
【０１７４】
次に、モデル探索部２２は、実行パススタックの最後の実行パス要素ｅ１のバックトラック集合Ｂａｃｋｔｒａｃｋに含まれ、Ｄｏｎｅに含まれない遷移ｔｒを任意に１つ選ぶ。そして、モデル探索部２２は、実行パス要素ｅ１が持つ状態ｓｔに、遷移ｔｒを行わせ、次の状態ｓｔ’を生成する（ステップＩ３）。
【０１７５】
次に、モデル探索部２２は、実行パス要素ｅ１が持つ遷移をｔｒに置き換えるとともに、Ｄｏｎｅにｔｒを追加する（ステップＩ４）。
【０１７６】
以降、モデル探索部２２は、図６のステップＡ１０に進み、以降の動作を、図６に示した実行パス生成動作と同様に行う。
【０１７７】
以上で、モデル探索部２２のバックトラック動作の説明を終了する。
【０１７８】
［効果の説明］
次に、本発明の第２の実施の形態の効果について述べる。
【０１７９】
本発明の第２の実施の形態としてのモデル検査装置は、ネットワークモデルのモデル検査においてｃｏｎｃｏｌｉｃにデータを扱いつつＤＰＯＲ（またはその拡張技術）を適用する際、無駄な探索を発生させずに冗長な探索を削減し、効率的な探索を可能とする。
【０１８０】
その理由は、モデル探索部が、ネットワークモデルの状態を遷移させて任意の実行パスを得、再探索制御部が、ｃｏｎｃｏｌｉｃ依存関係を考慮したバックトラック地点からの再探索を制御するからである。具体的には、再探索制御部は、再探索でのｃｏｎｃｏｌｉｃ処理を伴う遷移において、ｃｏｎｃｏｌｉｃ処理結果の差分にあたるバックトラックの情報を生成する。このバックトラック情報は、ｃｏｎｃｏｌｉｃ依存関係のある遷移間の順序を仮に入れ替えた場合にｃｏｎｃｏｌｉｃ処理により求まるデータ集合を和演算したＢａｃｋｔｒａｃｋ集合と、利用済みのデータを示すＤｏｎｅ集合とからなる。そして、モデル探索部は、バックトラック地点からの再探索でのｃｏｎｃｏｌｉｃ処理を伴う遷移において、Ｂａｃｋｔｒａｃｋ集合からＤｏｎｅ集合を除いた中から任意に選択したデータを用いて再探索を行う。また、再探索制御部は、ｃｏｎｃｏｌｉｃ依存関係のある遷移のうち、ｃｏｎｃｏｌｉｃ処理を伴う遷移の直前の状態にバックトラック地点を生成し、遷移の順序は入れ替えない。
【０１８１】
これにより、本実施の形態は、ｃｏｎｃｏｌｉｃ依存関係を考慮したバックトラックを行いながらも、検証の観点で過去の探索と等価なデータを用いた無駄な探索を行わずに済む。したがって、探索の効率化が実現される。
【０１８２】
なお、本実施の形態において、ネットワークモデルの具体的な仕様、状態遷移の具体的な仕様、実行パスや遷移などを表す各種データの具体的なデータ構造を示して説明を行ったが、これらに限定されるものではない。本発明の実施の形態は、ネットワーク制御技術により制御されるネットワークを表すその他の状態遷移モデル、他の遷移の定義およびそれに伴う各種データ構造を用いた場合にも適用可能である。
【０１８３】
また、本実施の形態において、再探索制御部が、一方が、端末のパケット送信を伴う遷移であり、他方が、コントローラによるプログラム実行を伴う遷移である場合に、それらの間にｃｏｎｃｏｌｉｃ依存関係があると判断する例を説明した。これに限らず、再探索制御部は、その他の基準によりｃｏｎｃｏｌｉｃ依存関係を判断してもよい。
【０１８４】
また、上述した本発明の各実施の形態において、検証情報取得部は、検証情報のユーザによる入力を支援する雛形情報を提供する機能を有していてもよい。例えば、検証情報取得部は、検証情報に含まれる検証プロパティとして典型的な雛形を選択可能に出力装置に提示してもよい。これにより、ユーザは、所望の雛形を選択することで、検証情報を入力することができる。これにより、本実施の形態は、ユーザによる検証情報の作成負担を軽減することができ、結果として検証全体の効率を向上させる。
【０１８５】
また、上述した本発明の各実施の形態において、モデル検査装置の各機能ブロックが、メモリに記憶されたコンピュータ・プログラムを実行するＣＰＵによって実現される例を中心に説明した。これに限らず、各機能ブロックの一部、全部、または、それらの組み合わせが専用のハードウェアにより実現されていてもよい。
【０１８６】
また、上述した本発明の各実施の形態において、モデル検査装置の機能ブロックは、複数の装置に分散されて実現されてもよい。
【０１８７】
また、上述した本発明の各実施の形態において、各フローチャートを参照して説明したモデル検査装置の動作を、本発明のコンピュータ・プログラムとしてコンピュータの記憶装置（記憶媒体）に格納しておく。そして、係るコンピュータ・プログラムを当該ＣＰＵが読み出して実行するようにしてもよい。そして、このような場合において、本発明は、係るコンピュータ・プログラムのコードあるいは記憶媒体によって構成される。
【０１８８】
また、上述した各実施の形態は、適宜組み合わせて実施されることが可能である。
【０１８９】
以上、上述した各実施の形態を模範的な例として本発明を説明した。しかしながら、本発明は、上述した各実施の形態には限定されない。即ち、本発明は、本発明のスコープ内において、当業者が理解し得る様々な態様を適用することができる。
【０１９０】
この出願は、２０１４年１１月１７日に出願された日本出願特願２０１４−２３２８６５を基礎とする優先権を主張し、その開示の全てをここに取り込む。
【符号の説明】
【０１９１】
１    モデル検査装置
２    モデル検査装置
１１、２１    検証情報取得部
１２、２２    モデル探索部
１３、２３    データ集合決定処理部
１４、２４    再探索制御部
１５    検証結果出力部
１００１    ＣＰＵ
１００２    メモリ
１００３    出力装置
１００４    入力装置
【図１】
2016079962.tif 000003
【図２】
2016079962.tif 000004
【図３】
2016079962.tif 000005
【図４】
2016079962.tif 000006
【図５】
2016079962.tif 000007
【図６】
2016079962.tif 000008
【図７】
2016079962.tif 000009
【図８】
2016079962.tif 000010
【図９】
2016079962.tif 000011
【図１０】
2016079962.tif 000012
【図１１】
2016079962.tif 000013
【図１２】
2016079962.tif 000014
【図１３】
2016079962.tif 000015
【図１４】
2016079962.tif 000016
【図１５】
2016079962.tif 000017
【図１６】
2016079962.tif 000018
【図１７】
2016079962.tif 000019
【図１８】
2016079962.tif 000020
【手続補正書】
【提出日】平成29年4月20日(2017.4.20)
【手続補正２】
【補正対象書類名】明細書
【補正対象項目名】００３８
【補正方法】変更
【補正の内容】
【００３８】
また、本発明のモデル検査プログラムは、検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得する検証情報取得ステップと、前記状態遷移モデルを遷移させて実行パスを得るモデル探索ステップと、前記実行パス上の遷移間で、データ利用を伴う遷移で用いられるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理に関わる依存関係を解析する依存関係解析ステップと、前記データ集合決定処理に関わる依存関係に基づいてバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いて再探索を行う再探索制御ステップと、探索結果に基づいて、前記検証内容の検証結果を出力する検証結果出力ステップと、をコンピュータ装置に実行させる。
【手続補正３】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得する検証情報取得手段と、
前記状態遷移モデルを遷移させて実行パスを得るモデル探索手段と、
前記状態遷移モデルのデータ利用を伴う遷移で用いられるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理を行うデータ集合決定処理手段と、
前記実行パス上の遷移間での前記データ集合決定処理に関わる依存関係に基づきバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いるよう、前記モデル探索手段を制御する再探索制御手段と、
前記再探索制御手段の制御に基づく前記モデル探索手段の探索結果に基づいて、前記検証内容の検証結果を出力する検証結果出力手段と、
を備えたモデル検査装置。
【請求項２】
前記再探索制御手段は、前記再探索での前記データ利用を伴う遷移において、前記データ集合決定処理に関わる依存関係のある遷移間の順序を仮に入れ替えた場合の前記データ集合決定処理によるデータ集合から、前記利用済みのデータを除外したデータ集合を用いて、前記順序を入れ替えずに前記再探索を行うことを特徴とする請求項１に記載のモデル検査装置。
【請求項３】
前記再探索制御手段は、前記実行パス上の遷移間での前記データ集合決定処理に関わる依存関係を解析してバックトラック地点を生成する際に、前記バックトラック地点において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を求めることを特徴とする請求項１または請求項２に記載のモデル検査装置。
【請求項４】
前記再探索制御手段は、前記実行パス上の任意の遷移の組合せのうち、一方が前記データ集合決定処理の結果に基づくデータを利用する遷移であり、他方が前記データ集合決定処理の結果に影響を与える遷移である場合に、前記組合せ間に前記データ集合決定処理に関わる依存関係があると判断することを特徴とする請求項１から請求項３のいずれか１項に記載のモデル検査装置。
【請求項５】
前記状態遷移モデルが、端末間で送受信されるパケットを転送するスイッチおよび前記転送を制御するコントローラを含むネットワークを表すとき、
前記再探索制御手段は、前記実行パス上の任意の遷移の組合せのうち、一方が前記端末によるパケット送信を伴う遷移であり、他方が前記コントローラによるプログラム実行を伴う遷移である場合に、前記組合せ間に前記データ集合決定処理に関わる依存関係があると判断することを特徴とする請求項４に記載のモデル検査装置。
【請求項６】
コンピュータが、
検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得し、
前記状態遷移モデルを遷移させて実行パスを得、
前記実行パス上の遷移間で、データ利用を伴う遷移で用いるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理に関わる依存関係を解析し、
前記データ集合決定処理に関わる依存関係に基づいてバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いて再探索を行い、
探索結果に基づいて、前記検証内容の検証結果を出力するモデル検査方法。
【請求項７】
検査対象の状態遷移モデルおよび前記状態遷移モデルに対する検証内容を表す検証情報を取得する検証情報取得ステップと、
前記状態遷移モデルを遷移させて実行パスを得るモデル探索ステップと、
前記実行パス上の遷移間で、データ利用を伴う遷移で用いられるデータの代表値の集合であるデータ集合を決定するデータ集合決定処理に関わる依存関係を解析する依存関係解析ステップと、
前記データ集合決定処理に関わる依存関係に基づいてバックトラック地点から再探索を行う際に、前記データ利用を伴う遷移において、前記データ集合決定処理によるデータ集合から、該遷移で以前の探索において利用済みのデータを除外したデータ集合を用いて再探索を行う再探索制御ステップと、
探索結果に基づいて、前記検証内容の検証結果を出力する検証結果出力ステップと、
をコンピュータ装置に実行させるモデル検査プログラム。
【国際調査報告】
2016079962.tif 000021
2016079962.tif 000022
2016079962.tif 000023
2016079962.tif 000024