JP6428768B2 - モデル検査装置、方法及びプログラムを記憶した記憶媒体 - Google Patents

Description

本発明は、モデル検査装置、方法及びプログラムを記憶した記憶媒体に関する。

近年、システムやソフトウェアの複雑化・巨大化が進んでいる。これに対する一つの解決手段として、例えばモデル検査（model checking）による検証手法が知られている。モデル検査とは、検証対象を状態遷移系としてモデル化する。そして、モデル化した状態遷移系を例えば網羅的に探索する。これにより、検証対象が例えば仕様を満たすか否かを検証する。モデル検査は、システムの設計段階から適用することができる。また、検証対象が仕様を満たすか否かを保証、検証することができる。このため、システムやソフトウェアの信頼性を向上させるための技術として注目されている。

また、最近では、モデル検査はネットワークの検証への適用も試みられている。例えば、非特許文献１は、ＯｐｅｎＦｌｏｗにより制御されたネットワークをモデル検査によりテストするシステムを開示している。なお、非特許文献２、３が開示しているように、ＯｐｅｎＦｌｏｗでは、スイッチ（OpenFlow Switch: OFS）は、コントローラ(OpenFlow Controller: OFC)から設定されたフローエントリに基づき処理を行う。フローエントリは、例えば、パケットヘッダの所定フィールドと照合する条件、照合時の動作を規定したルール、統計情報等を規定する。スイッチは、受信パケットに対して当該受信パケットのヘッダ情報と照合するフローエントリが存在しない場合、例えばｐａｃｋｅｔ−ｉｎメッセージをコントローラに送信してフローの計算を依頼する。そして、コントローラは、ネットワークトポロジ等に基づきフローを導出し、該フローに対応するフローエントリを該フロー上のスイッチに設定する。

非特許文献１では、ＯｐｅｎＦｌｏｗのネットワークを状態探索する際に、ＯｐｅｎＦｌｏｗコントローラのプログラムの記号実行(symbolic execution)を行い、全てのコードパスを実行するためのパケットの代表値の集合を求め、それを用いて状態探索を行う。ここで、非特許文献１に開示されているモデル検査の概要について非特許文献１の記載に基づき説明しておく。システム状態を要素（component）の状態の組み合わせとし、遷移はメッセージ送信のようにある状態から他の状態への変化を表す。各状態で各要素（component）は可能な遷移の集合を保持する。与えられた状態空間モデルに対して探索するにあたり、モデル検査器（model checker）は、まず、状態のスタックを初期化したあと、以下の処理を状態スタックが空となるまで繰り返す。スタックから１つの状態とその状態が可能な遷移の１つを選択し、当該遷移を実行後、新たに到達した状態に関して例えば正しさのプロパティ（correctness property）をテストする。当該新たな状態が正しさのプロパティに違反していない場合、この新たな状態を探索された状態集合に追加し、この状態で可能とされる全ての遷移の実行をスケジュールする。非特許文献１では、ＯｐｅｎＦｌｏｗコントローラのプログラムは、イベントハンドラの集合として構成され、プログラムの状態をグローバル変数の値とし、各イベントハンドラを遷移として扱う。遷移を実行するには、対応するイベントハンドラを起動する。例えばスイッチからのｐａｃｋｅｔ−ｉｎメッセージの受信は、ｐａｃｋｅｔ−ｉｎ遷移を可能とし、モデル検査器は当該遷移に対応するイベントハンドラを起動することで当該遷移を実行する。イベントハンドラの動作がデータ依存である点を考慮して記号実行を行う。

モデル検査は、上記のような特長を持つ一方、計算に必要なメモリや時間が、検証対象の規模に対して指数的に増大する。そのため、実践的なシステムやソフトウェアの検証を目的としたモデル検査においては、探索の効率化が不可欠である。

例えば非特許文献４では、マルチスレッド環境モデルに対するモデル検査において、検証の観点で冗長な探索を枝刈りする技術であるＤＰＯＲ（Dynamic Partial Order Reduction：動的半順序縮約）を開示している。

ＤＰＯＲでは、モデル検査対象の状態遷移系を探索（例えばdepth-first-search：深さ優先探索）する際、
（A）最初に適当なパスを１つ実行する。
（B）そして、当該パスの遷移系列の中に、互いの実行順序が実行結果に影響を及ぼす遷移のペアが存在するか確認する。このような遷移のペアを「依存関係のある遷移」と呼ぶ。
（C）遷移のペアに依存関係のある遷移が存在する場合、当該ペアの遷移の実行順序を入れ替えたパスを探索するために、当該ペアのうち先に行った遷移の直前の状態を、先程実行したパスから探す。そして、当該状態（先に行った遷移の直前の状態）から、先程の実行パスとは異なる遷移（前記ペアのうち、先に行った遷移とは異なる遷移）を行うところから、探索を始めるバックトラック地点を生成する。
（D）当該先程の実行パスから、依存関係のある遷移を全て検出し終えたら、当該先程の実行パス上で、最後方（最も深い位置）にあるバックトラック地点から、探索を再開する。
（E）バックトラック地点がなくなるまで、この手順（上記（B）乃至（D））を繰り返す。

これにより、検証対象の全ての実行パターンのうち、実行結果が異なるパスのみを探索することが可能である。言い換えると、検証結果が異ならないパス、つまり、検証の観点で冗長なパスの探索を枝刈りすることができ、探索の効率化が可能である。

非特許文献５では、ＤＰＯＲを改良した技術であるＳＤＰＯＲ（Stateful Dynamic Partial Ordering Reduction）を開示している。モデル検査では、一般的に、過去に探索した状態（探索済み状態）に再度到達した場合、その状態以降の探索は当然ながら冗長であるため、探索を打ち切る。しかし、ＤＰＯＲにおいては、安易に探索を打ち切ると、実行パス上の依存関係のある遷移の解析に影響し、正しい結果が得られない。そのため、ＤＰＯＲでは、探索済み状態に到達した場合でも、探索を打ち切らずに続ける。ＳＤＰＯＲは、探索済み状態に到達した場合に、探索を打ち切ることが可能なように改良したＤＰＯＲである。ＳＤＰＯＲでは、過去の探索で行われた遷移をグラフで管理し、依存関係の解析に利用する。グラフは、各ノードに遷移が紐付けられ、各有向エッジが、過去の探索で行った遷移の実行順序を表すものである。

例えば、探索中に行った遷移ｔ１の直後の状態をｓ１とすると、さらにｓ１から遷移ｔ２を行った場合、前記グラフ中の遷移ｔ１に対応するノードｎ１から、遷移ｔ２に対応するノードｎ２に有向エッジが引かれる。ここで、ノードｎ１やｎ２が前記グラフ中に存在しなければ作成されるＳＤＰＯＲでは、過去に探索した状態S₂に到達すると、状態S₂から行うことのできる遷移を調べる。さらに、ＳＤＰＯＲでは、当該遷移に対応するノードを前記グラフ中から探し、当該ノードから有向エッジを辿って到達可能なノードを全て抽出する。ここで、先程抽出したノードに対応する遷移は、S₂以降の状態遷移において実行され得る遷移を表している。これらの遷移と、現在の実行パス上の遷移とを用いて、依存関係を解析し、バックトラック地点を生成する。これらの手順により、探索済みの状態以降の探索を打ち切っても、正しく依存関係を解析することができ、探索の打ち切りが可能な分効率化されるのが、ＳＤＰＯＲの特長である。

非特許文献６では、マルチスレッドシステム（multi-threaded system）向けに設計されたＤＰＯＲを分散環境システム（Distributed System）のモデル検査向けに修正した技術であるＤＰＯＲ−ＤＳ（Dynamic Partial Ordering Reduction in Distributed Systems）を開示している。検証対象のモデルの環境の違いを吸収するため、ＤＰＯＲ−ＤＳでは、バックトラック地点を生成する方法を変更している。ＤＰＯＲ−ＤＳでは、実行パス上の遷移間の関係について、依存関係(dependency relation)とは別に、分散環境モデルにおけるｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を定義し、バックトラック地点の生成の判断に利用する。ここで、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係とは、あるモデル上で必ず成り立つ遷移間の実行順序関係である。例えば、あるパケットｐの送受信を行う遷移を考えたとき、パケットｐの送信を行う遷移は、パケットｐの受信を行う遷移よりも必ず先に起こる。このように、モデル上の因果関係から、必ず成り立つ遷移間の順序関係が、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係である（非特許文献６参照）。

ＤＰＯＲ−ＤＳでは、実行パス上の遷移について、依存関係に加えて、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の有無も解析する。ある遷移間に依存関係があったとしても、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係が成り立つ場合には、バックトラック地点を生成しない。また、バックトラック地点から探索を再開する際、依存関係のあった２つの遷移のペア（先に行われたものをｔ１、後に行われたものをｔ２とする）の間に行われた遷移の中で、遷移ｔ２に対し、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にあった遷移と、遷移ｔ２と、を再開する探索の最初に連続して行わせる。

図１を参照しながら、具体例を用いて説明する。最初の探索において、ｔａ、ｔｂ、ｔｃ、ｔｄの順に遷移が実行されたとする。そして、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析の結果、
・ｔａとｔｄに依存関係があること、及び、
・ｔｃとｔｄにｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がある（ｔｃはｔｄより先に必ず行われる）こと、
が分かったとする。

すると、ＤＰＯＲ−ＤＳでは、遷移ｔａを行う直前の状態S₀にバックトラック地点ｂ１を生成する。

そして、当該バックトラック地点ｂ１から探索を再開する際に、最初に、
・ｔｃ（依存関係のある２つの遷移のペア（ｔａとｔｄ）の間に行われた遷移（ｔｂとｔｃ）の中で、前記ペアのうち後に行われた遷移（ｔｄ）に対しｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にあった遷移）と、
・ｔｄ（依存関係のある２つの遷移のペアのうち後に行われた遷移）
を行う。

その後は、遷移の順序の規定はなく適当なパスが実行される。つまり、図１の例では、バックトラック地点ｂ１から、例えばｔｃ、ｔｄ、ｔａ、ｔｂという順に遷移が実行される。このうち、最初のｔｃ、ｔｄは、前述の通り、ＤＰＯＲ−ＤＳの探索アルゴリズムによって実行の順番が規定されている部分である。残りのｔａ、ｔｂは、適当に実行の順番が決められた部分である。ここでは、依存関係のある遷移のペア（ｔａとｔｄ）の順序を入れ替えている。このバックトラック地点における、最初の部分の順番（ｔｃ、ｔｄ）の設定は、冗長な探索を削減することを目的とする工夫である。

この工夫が行われない場合、どうなるかに関して、図２を参照しながら具体例を用いて説明する。図１の例において、バックトラックにより探索を再開する際に、最初に行う遷移を単に一つだけ（ｔｃだけ）規定する場合、図２に示すように、例えばバックトラック地点ｂ１から、ｔｃ、ｔａ、ｔｂ、ｔｄという順に遷移が実行され得る。

図１のバックトラックは、依存関係のあるｔａとｔｄの順序を入れ替えた探索を行うことが目的であったが、図２の例では、バックトラックにおいて、依存関係のあるｔａとｔｄの順序の入れ替えは行われない。

図２に示すように、改めて、ｔｃ、ｔａ、ｔｂ、ｔｄのパスに対して依存関係の解析を行い、遷移ｔａを行う直前の状態ｓ５に、バックトラック地点ｂ２を生成する。これにより、次の探索において、ｔｃ、ｔｄ、ｔａ、ｔｂという順に遷移が行われ、所望の順序で遷移が発生するパスの探索が可能である。しかしながら、２回目の探索（ｔｃ、ｔａ、ｔｂ、ｔｄのパスの探索）は、検証の観点からは冗長であり、効率の観点からは無駄である。この冗長な探索を削減するため、ＤＰＯＲ−ＤＳでは、バックトラックによる探索再開時の最初の遷移列を規定して（図１の例では、バックトラック地点ｂ１からの遷移列ｔｃ、ｔｄ）、冗長なパス（図２の例では、パスｔｃ、ｔａ、ｔｂ、ｔｄ）の探索を削減する、という工夫を行っている。これらの手順により、分散環境モデルのモデル検査においても、探索の枝刈りを可能としていることが、ＤＰＯＲ−ＤＳの特長である。

Canini，M. et al.: "A NICE Way to Test OpenFlow Applications"，Proc. of NSDI，2012. McKeown，N. et al.: "OpenFlow: enabling innovation in campus networks"，ACM SIGCOMM Computer Communication Review，Vol. 38，No. 2，pp. 69-74，2008. "OpenFlow Switch Specification Version 1.0.0 (Wire Protocol 0x01)"，2009. ＜インターネット検索＞http://www.openflow.org/documents/openflow-spec-v1.0.0.pdf Flanagan，C. et al.: "Dynamic partial-order reduction for model checking software"，Proc. of POPL ’05，pp. 110-121，2005. Yang, Y. et al.: "Efficient Stateful Dynamic Partial Order Reduction", Proc. of SPIN ’08, pp. 288-305, 2008. Yabandeh，M. et al.: "DPOR-DS: Dynamic Partial Order Reduction in Distributed Systems"，EPFL Technical Report NSL-REPORT-2009-005，2009.

以下に関連技術の分析を与える。

非特許文献６における問題点は、前述のバックトラックによる探索再開時に最初の遷移列を規定して冗長な探索を削減するという工夫において、前記最初の遷移列が必ずしも実行可能であるとは限らず、無駄な探索が生じる場合がある、ということである（本発明者の知見）。図３を参照しながら具体例を用いて説明する。

まず、適当なパスとしてｔａ、ｔｂ、ｔｃ、ｔｄという順序で遷移が行われるパスｐ１が探索されたとする。

そして、
・ｔａとｔｄ、ｔｂとｔｃに、それぞれ依存関係があること、及び、
・ｔｃとｔｄにｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がある（ｔｃはｔｄより先に必ず行われる）こと、
が分かったとする。

次に、ＤＰＯＲ−ＤＳでは、前述した方法に従い、遷移ｔａを行う直前の状態S₀に対し、最初に、ｔｃ、ｔｄの順序で遷移を行うバックトラック地点ｂ１を生成する。同様に、遷移ｔｂを行う直前の状態S₁に対し、最初にｔｃを行うバックトラック地点ｂ２を生成する。すなわち、依存関係のある２つの遷移のペア（ｔｂとｔｃ）に関して、ｔｂとｔｃの間に行われた遷移の中で該ペアのうち、後に行われた遷移ｔｃに対してｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にあった遷移（無し）と、後に行われた遷移ｔｃを最初に行うバックトラック地点ｂ２が生成される。

バックトラック地点の生成が完了したので、次に、探索を実行したパス（実行パス）ｐ１上で最後方にあるバックトラック地点から探索を再開する。ここでは、遷移ｔｂを行う直前の状態にあるバックトラック地点ｂ２が最後方であるため、バックトラック地点ｂ２から遷移ｔｃをまず行い、その後、適当に遷移を実行する。ここでは、ｔｃにつづいてｔｂが実行される。その結果、全体としてｔａ、ｔｃ、ｔｂ、ｔｅというパスｐ２の探索（２回目の探索）が行われたとする。

パスｐ２で、最初の探索のパスｐ１では行われていない遷移ｔｅが行われている。これは、依存関係のあるｔｂとｔｃの実行順序を入れ替えた結果、ｔｃの遷移の内容が変わり、最初の探索のパスｐ１ではｔｃの後に行われた遷移ｔｄが行われなくなり、代わりに、ｔｅが行われるようになったためである。

次に、２回目の探索のパスｐ２において、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行った結果、
・ｔｃとｔｂ、ｔａとｔｅにそれぞれ依存関係があること、及び、
・ｔｃとｔｅにｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係があること、
が分かったとする。

そしてバックトラック地点の生成を行うが、ｔｃとｔｂの依存関係に関しては、既にバックトラック済みである。このため、再度、バックトラック地点は生成されない。結果として、ｔａが行われる直前の状態S₀に対し、最初にｔｃ、ｔｅの順序で遷移を行うバックトラック地点ｂ３を生成する。すなわち、依存関係のある２つの遷移のペア（ｔａとｔｅ）に関して、ｔａとｔｅの間に行われた遷移の中で該ペアのうち後に行われた遷移ｔｅに対してｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にあった遷移（ｔｃ）と、遷移ｔｅを最初に行うバックトラック地点ｂ３が生成される。

先程と同じように、バックトラック地点ｂ３の生成が完了したので、次に実行パス上で最後方にあるバックトラック地点から探索を再開する。ここでは、最後方のバックトラック地点はｂ１とｂ３の２つが存在する。先に生成されたｂ１を選択してバックトラックを行う。

そして、ｔｃ、ｔｄの順番で遷移を行おうとする。しかし、ｔｃは実行できるが、ｔｄは実行できない。なぜならば、前述したように、ｔｃをｔｂより先に行う場合、その後に実行できるのはｔｄではなく、ｔｅだからである。

従って、このバックトラック地点ｂ１から行おうとしていた遷移ｔｃ、ｔｄの探索は、そもそも行うことができず、無駄な探索に終わる。

上記の通り、ＤＰＯＲ−ＤＳでは、冗長な探索を削減するための工夫として、バックトラックによる探索の再開時の最初の遷移列を規定している。しかしながら、当該最初の遷移列が必ずしも実行可能であるとは限らず、無駄な探索が生じる場合があるという問題があることが判明した。

本発明の目的は、上記の問題を解決し、冗長な探索を削減するにあたり、無駄な探索を回避し効率的な探索を可能とする装置、プログラム及び方法を提供することにある。

上記の目的を達成するため、本発明の１つの側面によれば、モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら、前記探索を行う分散環境モデル探索部と、
前記分散環境モデル探索部が探索したパス上の複数の遷移に関して、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成する分散環境モデル依存関係解析部と、
少なくとも前記分散環境モデル依存関係解析部が生成した情報に基づき、前記分散環境モデル探索部が行うバックトラック後の前記探索において、実行を後回しにすべき前記所定の遷移に関する情報を生成する遅延遷移情報付与部と、を備える分散環境モデル用モデル検査装置が提供される。

本発明の別の側面によれば、モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら前記探索を行い、
前記探索したパス上の複数の遷移に関して、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成し、
少なくとも前記生成された情報に基づき、前記分散環境モデルのバックトラック後の探索にあたり、実行を後回しにすべき前記所定の遷移に関する情報を生成する、分散環境モデル用モデル検査方法が提供される。

本発明のさらに別の側面によれば、モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら、前記探索を行う分散環境モデル探索処理と、
前記分散環境モデル探索処理が探索したパス上の複数の遷移に関して、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成する分散環境モデル依存関係解析処理と、
少なくとも前記分散環境モデル依存関係解析処理が生成した情報に基づき、前記分散環境モデル探索部が行うバックトラック後の前記探索において、実行を後回しにすべき前記所定の遷移に関する情報を生成する遅延遷移情報付与処理と、
をコンピュータに実行させるプログラムが提供される。本発明のさらに別の側面によれば、該プログラムを記録したコンピュータ読み出し可能な半導体メモリや磁気／光ディスク等の記録媒体（non-transitory storage medium）が提供される。

本発明によれば、モデル検査において冗長な探索を削減するにあたり、無駄な探索を生じず、効率的な探索を可能にすることできる。

関連技術を説明する図である。 関連技術を説明する図である。 関連技術を説明する図である。 本発明の第１の実施の形態の構成を説明する図である。 本発明の第１の実施の形態の全体の動作の一例を説明する流れ図である。 図５のステップＳ１２の動作の詳細の一例を説明する流れ図である。 図５のステップＳ１３の動作の詳細の一例を説明する流れ図である。 図７のステップＳ１３＿３の動作の詳細の一例を説明する流れ図である。 図７のステップＳ１３＿４の動作の詳細の一例を説明する流れ図である。 図５のステップＳ１４の動作の詳細の一例を説明する流れ図である。 図５のステップＳ１５の動作の詳細の一例を説明する流れ図である。 図５のステップＳ１６の動作の詳細の一例を説明する流れ図である。 本発明の第３の実施の形態の構成の一例を説明する図である。 本発明の第３の実施の形態の全体の動作の一例を説明する流れ図である。 図１４のステップＳ３２の動作の詳細の一例を説明する流れ図である。 図１４のステップＳ３２の動作の詳細の一例を説明する流れ図である。 図１６のステップＳ３２＿１７の動作の詳細の一例を説明する流れ図である。 図１４のステップＳ３３の動作の詳細の一例を説明する流れ図である。 図１４のステップＳ３６の動作の詳細の一例を説明する流れ図である。 本発明の第４の実施の形態の構成を説明する図である。 本発明の動作原理の一例を説明する図である。 本発明の基本概念を説明する図である。

以下では、本発明の基本的な実施形態を説明する。図２２を参照すると、本発明の基本的な実施形態に係る装置は、分散環境モデル探索部（以下、部は、工程、処理、手段ともいう）１１と、分散環境モデル依存関係解析部１２と、遅延遷移情報付与部１３とを備える。分散環境モデル探索部１１は、モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら、前記探索を行う。分散環境モデル依存関係解析部１２は、分散環境モデル探索部１１が探索したパス上の複数の遷移に関して、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成する。遅延遷移情報付与部１３は、少なくとも分散環境モデル依存関係解析部１２が生成した前記情報に基づき、分散環境モデル探索部１１で行う分散環境モデルの今後の探索（バックトラック後の探索）において、実行を後回しにすべき当該所定の遷移に関する情報を生成する。なお、図２２において、各部１１乃至１３をそれぞれ、工程（step）、処理(processing)と読み替えることで、本発明の基本的な実施形態に係る方法、プログラムに対応する。 また、本発明の基本的な実施形態に係る装置は、ＬＳＩ（Large Scale Integration）等のハードウェア部品である回路部品を実装することにより、その動作をハードウェア的に実現することができる。あるいは、その機能を提供するプログラムを、図示しないソフトウェア記憶媒体に格納し、そのプログラムを主記憶部にロードしてＣＰＵにおいて実行することにより、ソフトウェア的に実現することも可能である。以下、各部について詳細に説明する。

分散環境モデル探索部１１は、モデル検査対象の分散環境モデルの状態を遷移させて探索を行い、実行パスを生成して分散環境モデル依存関係解析部１２に受け渡す。分散環境モデル依存関係解析部１２は、実行パス上の依存関係及びｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析し、探索したパス上にバックトラック地点を生成して分散環境モデル探索部１１に返す。分散環境モデル探索部１１は、分散環境モデル依存関係解析部１２から受け渡された当該パス上でバックトラックを特定し変更を加えたパスを遅延遷移情報付与部１３に与え、遅延遷移情報付与部１３は、当該パスを解析し、分散環境モデル探索部１１での今後の探索（バックトラックの探索）において実行を後回しにすべき遷移に関する情報を分散環境モデル探索部１１に返し、分散環境モデル探索部１１は、バックトラックの探索において、遅延遷移情報付与部１３からの設定に基づき、実行を後回しにすべき遷移を後回しにして、分散環境モデルの探索を行う。

本発明の基本的な実施形態によれば、モデル検査においてバックトラックにより探索を再開する際、前述したＤＰＯＲ−ＤＳのように、最初に実行する遷移列を規定するのではなく、探索中に実行を後回しにする遷移を規定する。

ＤＲＯＰ−ＤＳも本発明の基本的な実施形態も、以前の探索で検出された依存関係のある遷移のペアの実行順序をバックトラック後の探索で入れ替えることができる。ただし、ＤＰＯＲ−ＤＳの方法では、図３を参照して説明した通り、実行可能でない遷移を実行しようとする無駄な探索が発生し得る。

これに対して、本発明の基本的な実施形態によれば、以前の探索で検出された、依存関係のある遷移のペアのうち先に行われた遷移を、バックトラック後の探索では、後回しにする。図２１を参照して、本発明の基本的な実施形態の動作原理を詳細に説明する。

最初に、適当なパスとしてｔａ、ｔｂ、ｔｃ、ｔｄという順序で遷移が行われるパスｐ１が探索されたとする。そして、
・ｔａとｔｄ、ｔｂとｔｃにそれぞれ依存関係があること、及び、
・ｔｃとｔｄにｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係があること（ｔｃはｔｄより先に必ず行われること）
が分かったとする。

次に、ｔａを行う直前の状態S₀にバックトラック地点ｂ１を生成する。また、そのバックトラック地点ｂ１から探索を再開する際、最初に、
ｔｃ（依存関係のある２つの遷移のペア（ｔａとｔｄ）の間に行われた遷移（ｔｂとｔｃ）の中で、当該遷移のペア（ｔａとｔｄ）のうち、後に行われた遷移（ｔｄ）に対してｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にあった遷移）を行う。加えて、状態S₀から探索を再開する場合、当該探索では、
ｔａ（以前の探索で検出された依存関係のある２つの遷移のペア（ｔａとｔｄ）のうち、先に行われた遷移）の実行を後回しにする。

同様の方法により、遷移ｔｂを行う直前の状態S₁に対し、最初にｔｃを行うバックトラック地点ｂ２を生成する。状態S₁から再開する探索では、
ｔｂ（以前の探索で検出された依存関係のある２つの遷移のペア（ｔｂとｔｃ）のうち、先に行われた遷移）の実行を後回しにする。

バックトラック地点の生成が完了したので、次に実行パス上で最後方にあるバックトラック地点から探索を再開する。ここでは、ｔｂを行う直前の状態S₁にあるバックトラック地点ｂ２が最後方であるため、バックトラック地点ｂ２から、遷移ｔｃをまず行い、その後、適当に遷移を実行する。ただし、遷移ｔｂの実行だけは、後回しにする。その結果、全体として、ｔａ、ｔｃ、ｔｅ、ｔｂというパスｐ２が行われたとする。ここで、最初のパスｐ１では行われていない遷移ｔｅが行われているのは、依存関係のあるｔｂとｔｃの実行順序を入れ替えた結果、ｔｃの遷移の内容が変わり、最初のパスｐ１ではｔｃの後に行われるｔｄが行われなくなり、代わりにｔｅが行われるようになったためである。

次に、２回目の探索パスｐ２において、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、
・ｔｃとｔｂ、ｔａとｔｅにそれぞれ依存関係があること、及び、
・ｔｃとｔｅにｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係があること、
が分かったとする。

そしてバックトラック地点の生成を行う。しかし、ｔｃとｔｂの依存関係に関しては、既にバックトラック済みであるため、再度バックトラック地点は生成されない。

また、ｔａとｔｅの依存関係の解析結果からは、前述の方法に従い、状態S₀から遷移ｔｃを最初に行うバックトラック地点ｂ３の作成が試みられる。しかしながら、この場合、既に同じ内容のバックトラック地点ｂ１が生成されているため、新たなバックトラック地点は生成されない。

バックトラック地点の生成が完了したので、次に、実行パス上で最後方にあるバックトラック地点から探索を再開する。ここでは、ｔａを行う直前の状態S₀にあるバックトラック地点ｂ１が最後方である。バックトラック地点ｂ１から遷移ｔｃをまず行い、その後、適当に遷移を実行する。ただし、ｔａの実行だけは、後回しにする。その結果、全体としてｔｃ、ｔｅ、ｔｂ、ｔａというパスｐ３が行われる。

このように、本発明の基本的な実施形態によれば、依存関係のある遷移を後回しにして探索する。これにより、ＤＰＯＲ−ＤＳとは異なり、実行されない遷移（具体例としては、図３の３回目の探索におけるｔｄ）を実行しようとする無駄な探索は行われない。

また、本発明の基本的な実施形態によれば、ＤＰＯＲのように、依存関係のある遷移の順序が入れ替わっていない無駄な探索（具体例としては、図２の２回目の探索のｔｃ、ｔａ、ｔｂ、ｔｄのパスの探索）が行われることもない。結果として、本発明の基本的な実施形態によれば、モデル検査を効率化することができる。

上記のとおり、本発明の基本的な実施形態によれば、バックトラック後の探索において、以前の探索とは内容が変わってしまう遷移があったとしても、特定の遷移の実行を、後回しにするだけである。ＤＰＯＲ−ＤＳでは、実行可能でない遷移を行おうとしてしまうという無駄な探索が発生する場合があるが、本発明の基本的な実施形態によれば、このような無駄な探索が発生することはない。
その結果、本発明の基本的な実施形態によれば、モデル検査における探索の効率化を実現することができる。

本発明の基本的な実施形態によれば、分散環境モデルに対するモデル検査において、ＤＰＯＲを適用する際、無駄な探索を発生させずに、冗長な探索を削減し、探索を効率化することができる。以下の例示的な実施の形態では、分散環境のモデル検査に本発明の基本的な実施形態を適用した例に即して説明する。

＜第１の実施の形態＞
図４は、本発明の第１の実施の形態の構成を例示する図である。図４を参照して、本発明の第１の実施の形態の構成について詳細に説明する。図４を参照すると、本発明の第１の実施の形態の分散環境モデル用モデル検査装置１は、分散環境モデル探索部１１、分散環境モデル依存関係解析部１２、遅延遷移情報付与部１３、入力装置２１、出力装置２２、及び、記憶装置２３を含む。このうち、分散環境モデル探索部１１、分散環境モデル依存関係解析部１２、遅延遷移情報付与部１３は、図２２の各要素にそれぞれ対応する。なお、分散環境モデル探索部１１、分散環境モデル依存関係解析部１２、遅延遷移情報付与部１３はコンピュータ上で実行されるプログラムにより、その処理・機能を実現するようにしてもよい。

また、分散環境モデル探索部１１は、ユーザから入力装置２１を介して、
・分散環境モデル（状態空間の記述）と、
・分散環境モデルが満たすべきプロパティと
を含む検証情報Ｄ１１を受け取る。検証情報Ｄ１１を用いて、モデル検査（状態の探索）を実行する。分散環境モデル探索部１１は、前記プロパティの成否と、前記プロパティが満たされない場合には、それを示す反例と、を含む検証結果Ｄ１６を出力装置２２を介して、ユーザに返す。

分散環境モデル（分散システムの状態空間の記述）の仕様は、後述する依存関係及びｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係が適切に定義でき、これらの関係が機械的に解析可能な状態遷移系でありさえすればよく、特定の仕様に制限されるものではない。また、前記分散環境モデルの記述形式（状態空間の記述形式）も、分散環境モデル探索部１１で機械的に処理可能（例えばコンピュータ、ＣＰＵ（Central Processing Unit）等データ処理装置による分散環境モデルの読み込み、解析、探索の実行等）でありさえすればよく、特定の形式に制限されるものではない。

第１の実施の形態では、前記分散環境モデルの仕様を以下に示すものとして説明する。
第１の実施の形態では、分散環境モデルにおける状態を例えば以下のように定義する（ただし、本発明において、状態は以下に制限されない）。

状態は、三つの集合の組（Ｎ，Ｍ，Ｑ）として定義される。

Ｎは分散環境中の動作主体であるノードの集合である。Ｎの要素ｎ（ｎ∈Ｎ）はその状態を表す変数ｓｖを持つ。

Ｍはノード間でやり取りされるメッセージの集合である。Ｍの要素ｍ（ｍ∈Ｍ）はメッセージの内容を表す変数ｍｖを持つ。

Ｑは通信チャネルの集合である。Ｑの要素ｑ（ｑ∈Ｑ）は複数のメッセージを格納する変数により実現される通信チャネルである。

ノードは、通信チャネルにメッセージが格納された順番とは無関係に通信チャネルからメッセージを取り出せるものとする。各ノードは、その他のノードと通信するための通信チャネルを互いに通信可能な各ノードに対し送信用と受信用とを１つずつ持つ。ある１つのノードにとっての送信用通信チャネルは、それ以外の１つのノードにとっての受信用通信チャネルであり、その逆も然りである。

第１の実施の形態の分散環境モデルにおける遷移の定義について説明する。

遷移は、分散環境モデルに存在するノードのいずれかが、特定の単位の動作を実行することで、モデルの状態が変化する様子を表すものとする。特定の単位の動作とは、具体的には、例えば、以下の３種類である。

１． ノードのメッセージ送信
２． ノードのメッセージ受信
３． ノードの内部動作

以下では、前記３種類の動作についてそれぞれ詳しく説明する。

まず、ノードのメッセージ送信による遷移について説明する。ノードは、自身の状態ｓｖに応じて、メッセージ送信動作を実行することが可能である。ノードのメッセージ送信による遷移では、ノードｎがメッセージｍを１つ生成して、ノードｎのメッセージ送信用通信チャネル（＝ノードｎ以外のあるノードにとっての受信用通信チャネル）にメッセージｍを格納し、ノードｎの状態ｓｖの内容を変更する（変更しない場合もある）。

次に、ノードのメッセージ受信による遷移について説明する。ノードは、自身のメッセージ受信用通信チャネルにメッセージが１つ以上格納されている場合、メッセージ受信動作を実行することが可能である。ノードのメッセージ受信による遷移では、メッセージが１つ以上格納されているノードｎのメッセージ受信用通信チャネルｑから、任意のメッセージｍを１つ取り出す。そして、該メッセージｍの内容ｍｖに応じて、ノードｎの状態ｓｖの内容を変更する（変更しない場合もある）。

次に、ノードの内部動作による遷移について説明する。ノードは、自身の状態ｓｖに応じて、内部動作を実行することが可能である。ノードの内部動作による遷移では、ノードｎが自身の状態ｓｖの内容を変更する（変更しない場合もある）。

分散環境モデル探索部１１は、状態を遷移させるにあたり、上記のモデルの動作（１、２、３）に加えて、遷移後の状態における、検証情報Ｄ１１に含まれるプロパティの成否を確認する。分散環境モデル探索部１１は、該プロパティが満たされない場合には、その場で、モデル検査の処理を終了し、検証プロパティが満たされないという結果と、それを示す具体例である反例と、を含む検証結果Ｄ１６を、出力装置２２を介してユーザに返す。

なお、検証情報Ｄ１１において、プロパティは必ずしも含まれていなくてよい。プロパティが定義されていない場合、典型的なプロパティを検証することとし、以降は、分散環境モデル用モデル検査装置１全体が、検証情報Ｄ１１に、前記典型的なプロパティが含まれているかのように動作する。

分散環境モデル依存関係解析部１２は、分散環境モデル探索部１１から、分散環境モデル探索部１１で実行した実行パスＤ１２を受け取る。

分散環境モデル依存関係解析部１２は、前記実行パスＤ１２上の２つの遷移間の依存関係及びｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する。

分散環境モデル依存関係解析部１２は、実行パスＤ１２上にバックトラック地点を生成する。分散環境モデル依存関係解析部１２は、その結果（バックトラック地点が生成された実行パス）Ｄ１３を分散環境モデル探索部１１に返す。

依存関係とは、２つの遷移間に成り立つ関係である。例えば、状態遷移系の２つの遷移の実行順序を変更するとそれらの遷移後の結果が変わる場合、又は、２つの遷移の一方を行うと他方の遷移の実行可否に影響を与える場合、２つの遷移間に依存関係が成り立つ（依存関係がある）という。

遷移ｔ１とｔ２の間に依存関係が「成り立たない」条件は、一般的には、例えば、以下のように定義される。

１．状態S₁において遷移ｔ１が実行可能であり、状態S₁から遷移ｔ１により状態S₂へ遷移する場合、遷移ｔ２は状態S₁とS₂との両方で実行可能か、両方で実行不可能かのいずれかである。

２．状態S₁において遷移ｔ１とｔ２が実行可能である場合、状態S₁から遷移ｔ１を実行した先の状態で遷移ｔ２を実行した先の状態がS₂であるならば、状態S₁から遷移ｔ２を実行した先の状態で遷移ｔ１を実行した先の状態もS₂である。

ただし、上記の一般的な依存関係の成否を解析することはコストが高い。このため、本発明の第１の実施の形態においては、用いる分散環境モデルの仕様と、ＤＰＯＲのアルゴリズムと、を考慮し、以下のように依存関係を定義する。

遷移ｔ１で動作したノードと遷移ｔ２で動作したノードが同じノードであり、いずれの遷移でも前記ノードの状態ｓｖの内容を変更している。

ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係とは、あるモデル上で必ず成り立つ遷移間の実行順序関係である。例えば、第１の実施の形態における分散環境モデルで、あるメッセージｍの送受信を行う遷移を考えたとき、メッセージｍの送信を行う遷移ｔ１は、メッセージｍの受信を行う遷移ｔ２より必ず先に起こる。

このように、モデル上の因果関係から必ず成り立つ遷移間の実行順序関係をｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係といい、ｔ１→ｔ２と記述する。

本発明の第１の実施の形態においては、用いる分散環境モデルの仕様と、ＤＰＯＲのアルゴリズムと、を考慮し、以下のように、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を定義する。

１．遷移ｔ１がノードのメッセージ送信による遷移であり、遷移ｔ２がノードのメッセージ受信による遷移であり、遷移ｔ１で送信されるメッセージと遷移ｔ２で受信されるメッセージが同じメッセージである場合、ｔ１→ｔ２

２．ｔ１→ｔ２であり、ｔ２→ｔ３である場合、ｔ１→ｔ３

次に、実行パスＤ１２のデータ構造について説明する。

実行パスＤ１２は、（ｓｔ，ｔｒ，Ｂａｃｋｔｒａｃｋ，Ｄｏｎｅ，Ｄｅｌａｙ，Ｄｅｐｅｎｄｅｎｃｙ）の六つ組（＝実行パス要素）を要素とする配列（又はそれに準ずるデータ構造）である。

ｓｔは、ある時点での分散環境モデルの状態である。

ｔｒは、状態ｓｔから実行された遷移である。

Ｂａｃｋｔｒａｃｋは、モデル検査による探索においてバックトラックするにあたり、バックトラックの際に状態ｓｔから実行されるべき遷移の集合を表す。

Ｄｏｎｅは、過去の探索において状態ｓｔから実行した遷移の集合を表す。

Ｄｅｌａｙは、状態ｓｔ以降の探索において実行を後回しにすべき遷移（＝遅延遷移）の集合を表す。

ＢａｃｋｔｒａｃｋからＤｏｎｅを引いた差集合は、状態ｓｔからバックトラックして実行されるべきであるが、未だ実行されていない遷移の集合を表す。

Ｄｅｐｅｎｄｅｎｃｙは、分散環境モデル依存関係解析部１２により依存関係があると判明した遷移を記憶しておくハッシュ表（又はそれに準ずるデータ構造）である。キーは遷移、値はその前記遷移と依存関係にある遷移の集合である。

本明細書では、Ｄｅｐｅｎｄｅｎｃｙを用いて遷移ｔｒ１をキーとして取得できる遷移集合ｔｒ＿ｓｅｔに遷移ｔｒ２を加えることを、「ｔｒ１をキーとしてｔｒ２をＤｅｐｅｎｄｅｎｃｙに登録する」と表現する。ただし、Ｄｅｐｅｎｄｅｎｃｙを用いてｔｒ１をキーとして取得できる値がない場合は、｛ｔｒ２｝（ｔｒ２を要素として持つ集合）をキーｔｒ１に対応する値として設定することとする。

実行パスＤ１３は、実行パスＤ１２と同様のデータ構造から成る。

次に、遷移のデータ構造について説明する。遷移は、五つの要素からなる組（ｎｏｄｅ，ｔｙｐｅ，ｓｅｎｄ，ｒｅｃｖ，ｃｈａｎｇｅ＿ｆｌａｇ）で表される。

ｎｏｄｅは、当該遷移で動作したノードである。

ｔｙｐｅは、当該遷移の種類（ノードのメッセージ送信、ノードのメッセージ受信、ノードの内部動作のいずれかであるかを表す値）である。

ｓｅｎｄは、当該遷移で送信したメッセージを表す。

ｒｅｃｖは、当該遷移で受信したメッセージを表す。

ｃｈａｎｇｅ＿ｆｌａｇは、当該遷移でノードの状態ｓｖが変更されたか否かを表すフラグである。ｃｈａｎｇｅ＿ｆｌａｇには、状態ｓｖが変更された場合はｔｒｕｅ、変更されていない場合はｆａｌｓｅが格納される。

このデータ構造に基づく遷移データは、分散環境モデル探索部１１による探索において、状態が遷移した際に、その遷移の内容に応じて、各フィールドの値が適切に設定された上で生成される。

遅延遷移情報付与部１３は、分散環境モデル探索部１１から、実行パスＤ１４を受け取ると、分散環境モデル探索部１１が今後行う探索において、実行を後回しにすべき遷移の情報を実行パスＤ１４に付与する。その結果（実行パスＤ１５）を、分散環境モデル探索部１１に返す。実行パスＤ１４、Ｄ１５のデータ構造は、前述した実行パスＤ１２のデータ構造と同様である。

図５は、本発明の第１の実施の形態の全体の動作を説明するための流れ図である。図５を参照して、図４に示した本発明の第１の実施の形態の動作について詳細に説明する。

（ステップＳ１１）
ユーザは、検証情報Ｄ１１を作成し、入力装置２１を介して分散環境モデル探索部１１に検証情報Ｄ１１を入力する。

（ステップＳ１２）
分散環境モデル探索部１１は、検証情報Ｄ１１を受け取ると、検証情報Ｄ１１に含まれる分散環境モデルを状態遷移させて適当な実行パスを１つ行う。分散環境モデル探索部１１は、実行パスＤ１２を生成して分散環境モデル依存関係解析部１２に受け渡す。

（ステップＳ１３）
分散環境モデル依存関係解析部１２は、実行パスＤ１２上の依存関係及びｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する。分散環境モデル依存関係解析部１２は、実行パスＤ１２上にバックトラック地点を生成する。分散環境モデル依存関係解析部１２は、バックトラック地点が生成された実行パスＤ１３を分散環境モデル探索部１１に返す。

（ステップＳ１４）
分散環境モデル探索部１１は、実行パスＤ１３上で一番深い（最後方の）バックトラック地点を特定し、該特定したバックトラック地点に基づき実行パスＤ１３に変更を加える。分散環境モデル探索部１１は、該変更を加えた実行パスＤ１４を、遅延遷移情報付与部１３に受け渡す。

（ステップＳ１５）
遅延遷移情報付与部１３は、分散環境モデル探索部１１から受け取った実行パスＤ１４を解析する。遅延遷移情報付与部１３は、今後の探索において実行を後回しにすべき遷移に関する情報を実行パスＤ１４に付与する。そして、遅延遷移情報付与部１３は、実行を後回しにすべき遷移に関する情報を付与した実行パスＤ１５を分散環境モデル探索部１１に返す。

（ステップＳ１６）
分散環境モデル探索部１１は、実行パスＤ１５上で一番深いバックトラック地点から分散環境モデルを再び状態遷移させ、新たな実行パス（Ｄ１２’）を得る。分散環境モデル探索部１１は、新たな実行パス（Ｄ１２’）を、図４の実行パスＤ１２として、分散環境モデル依存関係解析部１２に受け渡す。

（ステップＳ１７）
分散環境モデル依存関係解析部１２では、実行パスＤ１２を受け取り、バックトラックすべきか否かを判断する。バックトラック地点がある場合（ステップＳ１７のＹｅｓ分岐）、上記したステップＳ１４に進む。バックトラック地点がない場合（ステップＳ１７のＮｏ分岐）、ステップＳ１８（検証結果出力）に進む。ステップＳ１７の判定により、バックトラック地点がなくなるまで、ステップＳ１３〜１６の手順を繰り返す。

（ステップＳ１８）
分散環境モデル探索部１１は、検証結果Ｄ１６を出力装置２２へ出力する。分散環境モデル探索部１１は、検証結果Ｄ１６として、例えば、プロパティの成否と、プロパティが満たされない場合にはそれを示す反例とを出力する。

（ステップＳ１９）
ユーザは、出力装置２２から出力された検証結果を確認する。

（図５のステップＳ１２の詳細）
図６は、図５のステップＳ１２の動作の詳細を説明する流れ図である。以下では、図６を参照して、該ステップＳ１２についてより詳細に説明する。

（ステップＳ１２＿１）
分散環境モデル探索部１１は、検証情報Ｄ１１から、分散環境モデルを抽出する。分散環境モデル探索部１１は、分散環境モデルの初期状態ｓｔ０を生成し、状態ｓｔ ＝ ｓｔ０とする。

（ステップＳ１２＿５）
次に、分散環境モデル探索部１１は、状態ｓｔから、実行可能な遷移が１つ以上あるか否かをチェックする。状態ｓｔが遷移可能である場合には（ステップＳ１２＿５のＹｅｓ分岐）、ステップＳ１２＿６に移行する。状態ｓｔが遷移可能でない場合には（ステップＳ１２＿５のＮｏ分岐）、ステップＳ１２＿１９に移行する。

（ステップＳ１２＿６）
分散環境モデル探索部１１は、実行パススタックの一番上にある実行パス要素ｅ１のＤｅｌａｙから、
・実行パス要素ｅ１のＤｅｐｅnｄｅｎｃｙを用いて、実行パス要素ｅ１の持つ遷移ｔｒ＿ｅ１をキーとして取得できる遷移集合ｔｒ＿ｓｅｔ（遷移ｔｒ＿ｅ１と依存関係にある遷移の集合）に含まれる各遷移と、
・前記遷移ｔｒ＿ｅ１と、
を取り除いた（実行パス要素ｅ１のＤｅｌａｙとｔｒ＿ｓｅｔの差集合からｔｒ＿ｅ１を取り除いた）Ｄｅｌａｙ’（＝Ｄｅｌａｙ−ｔｒ＿ｓｅｔ−ｔｒ＿ｅ１）を計算する。

分散環境モデル探索部１１は、状態ｓｔが実行可能な遷移の中から、Ｄｅｌａｙ’に含まれない遷移ｔｒ＿ｓｔ（状態ｓｔ以降、実行を後回しにすべき遷移集合に含まれない遷移）を１つ選ぶ。

分散環境モデル探索部１１は、状態ｓｔに遷移ｔｒ＿ｓｔを行わせて、次の状態ｓｔ’を生成する。ここで、実行パススタックとは、現在探索中である実行パスの過程を保存するスタック（Last-In-First-Out）である。その要素は実行パス要素である。スタックは図示されないメモリ等の記憶装置に設けられる。

分散環境モデル探索部１１は、実行パススタックが空である（＝ｅ１がない）場合、
Ｄｅｌａｙ’＝｛ ｝（空集合）
とする。そして、分散環境モデル探索部１１は、状態ｓｔから実行可能な遷移の中から任意の遷移ｔｒ＿ｓｔを選ぶ。分散環境モデル探索部１１は、状態ｓｔが実行可能な遷移として、Ｄｅｌａｙ’に含まれない遷移が存在していない場合にも、状態ｓｔが実行可能な遷移の中から任意の遷移ｔｒ＿ｓｔを選ぶ。以上がステップＳ１２＿６の処理である。

（ステップＳ１２＿７）
次に、分散環境モデル探索部１１は、新しい実行パス要素ｅ２ ＝（ｓｔ，ｔｒ＿ｓｔ，｛ ｝，｛ｔｒ＿ｓｔ｝，Ｄｅｌａｙ，Ｄｅｐｅｎｄｅｎｃｙ）を生成し、実行パススタックに積む。ここで、実行パス要素ｅ２のＤｅｌａｙの内容は前記Ｄｅｌａｙ’である。また、実行パス要素ｅ２のＤｅｐｅｎｄｅｎｃｙの内容は、実行パス要素ｅ１のＤｅｐｅnｄｅｎｃｙから、前記遷移ｔｒ＿ｅ１と前記遷移集合ｔｒ＿ｓｅｔのペアを取り除いたものである。

（ステップＳ１２＿１１）
次いで、分散環境モデル探索部１１は、ｓｔ ＝ ｓｔ’とし、ステップＳ１２＿５に戻る。

（ステップＳ１２＿１９）
ステップＳ１２＿５において、状態ｓｔが実行可能な遷移が１つもない場合（ステップＳ１２＿５のＮｏ分岐）、分散環境モデル探索部１１は、その時点での実行パススタックの内容を、実行パスＤ１２として、分散環境モデル依存関係解析部１２に受け渡して、ステップＳ１２を終了する。

（図５のステップＳ１３の詳細）
図７は、図５のステップＳ１３の動作の詳細を説明する流れ図である。図７を参照して、該ステップＳ１３についてより詳細に説明する。

（ステップＳ１３＿３）
分散環境モデル依存関係解析部１２は、まず、実行パスＤ１２に対しｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析するための前処理を行う。

（ステップＳ１３＿４）
次に、分散環境モデル依存関係解析部１２は、依存関係及びｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析と、バックトラック地点の生成を行う。

（ステップＳ１３＿６）
最後に、分散環境モデル依存関係解析部１２は、バックトラック地点を生成した実行パスＤ１３を、分散環境モデル探索部１１に返す。以上で、ステップＳ１３を終了する。

（図７のステップＳ１３＿３の詳細）
図８は、図７のステップＳ１３＿３の動作の詳細を説明する流れ図である。図８を参照して、該ステップＳ１３＿３についてより詳細に説明する。図７のステップＳ１３＿３では、分散環境モデル依存関係解析部１２は、解析対象の実行パス中の各要素について、その要素の遷移とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にある（必ず先に起こる）遷移を持つ実行パス要素を求めていく。そのため、各実行パス要素毎に、その要素の遷移とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係にある遷移を持つ実行パス要素の集合を保持するデータ構造（ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合）を用意する。

（ステップＳ１３＿３＿１）
分散環境モデル依存関係解析部１２は、まず、解析対象の実行パスから、ｉ番目（ｉは最初は２）の実行パス要素ｅ１を選び出す。

（ステップＳ１３＿３＿２）
次に、分散環境モデル依存関係解析部１２は、ｊ番目（ｊは最初は１）の実行パス要素ｅ２を選び出す。

（ステップＳ１３＿３＿３）
さらに、分散環境モデル依存関係解析部１２は、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移と、を比較する。分散環境モデル依存関係解析部１２は、「実行パス要素ｅ２の遷移→実行パス要素ｅ１の遷移」でない場合、ステップＳ１３＿３＿５へ移る。

（ステップＳ１３＿３＿４）
分散環境モデル依存関係解析部１２は、「実行パス要素ｅ２の遷移→実行パス要素ｅ１の遷移」（ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係）である場合、実行パス要素ｅ１のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合（最初は空）に、
・実行パス要素ｅ２自身と、
・実行パス要素ｅ２のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に含まれる全ての実行パス要素と、
を追加する。

ステップＳ１３＿３＿３における比較は、具体的には、分散環境モデル依存関係解析部１２は、実行パス要素ｅ１の遷移の受信メッセージｒｅｃｖと、実行パス要素ｅ２の送信メッセージｓｅｎｄと、が一致するか否か比較する。一致すれば、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係有りとする。

（ステップＳ１３＿３＿５）
次に、分散環境モデル依存関係解析部１２は、ｊの値を１増やす。

（ステップＳ１３＿３＿６）
分散環境モデル依存関係解析部１２では、ｊの値がｉ以上であるか判定し、ｊの値がｉ未満の場合（ステップＳ１３＿３＿６のＮｏ分岐）、ステップＳ１３＿３＿２からＳ１３＿３＿５を繰り返す。

（ステップＳ１３＿３＿７）
分散環境モデル依存関係解析部１２は、ｊの値がｉ以上になったら、ｉの値を１増やし、ｊの値を１にする。

（ステップＳ１３＿３＿８）
分散環境モデル依存関係解析部１２は、ｉの値が解析対象の実行パスの長さより大きいいか否かを判定する。ｉの値が解析対象の実行パスの長さ以下の場合（ステップＳ１３＿３＿８のＮｏ分岐）、ステップＳ１３＿３＿１からＳ１３＿３＿７を繰り返す。ｉの値が解析対象の実行パスの長さを超える場合（ステップＳ１３＿３＿８のＹｅｓ分岐）、ステップＳ１３＿３を終了する。

（図７のステップＳ１３＿４の詳細）
図９は、図７のステップＳ１３＿４の動作の詳細を説明する流れ図である。図９を参照して、該ステップＳ１３＿４についてより詳細に説明する。

（ステップＳ１３＿４＿１）
分散環境モデル依存関係解析部１２は、まず、解析対象の実行パスから、ｉ番目（ｉは最初は１）の実行パス要素ｅ１を選び出す。

（ステップＳ１３＿４＿２）
次に、分散環境モデル依存関係解析部１２は、解析対象の実行パスから、ｊ番目（ｊは最初はｉ＋１）の実行パス要素ｅ２を選び出す。

（ステップＳ１３＿４＿３）
さらに、分散環境モデル依存関係解析部１２は、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移と、を比較し、実行パス要素ｅ１とｅ２の遷移に、「依存関係があり、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がない」か否かをチェックする。

分散環境モデル依存関係解析部１２において、ステップＳ１３＿４＿３の比較のうち、依存関係に関しては、
実行パス要素ｅ１及びｅ２の遷移の動作ノードｎｏｄｅが等しく、且つ、
ｅ１及びｅ２の遷移の状態変更フラグｃｈａｎｇｅ＿ｆｌａｇのいずれかがｔｒｕｅ、
であれば、
依存関係がある、とする。

分散環境モデル依存関係解析部１２において、ステップＳ１３＿４＿３の比較のうち、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係に関しては、
実行パス要素ｅ２のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に実行パス要素ｅ１の遷移が含まれていれば、実行パス要素ｅ１とｅ２の遷移にｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係があるとする。ここで、実行パス要素ｅ１及びｅ２の遷移に「依存関係があり、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がない」という条件を満たさない場合、分散環境モデル依存関係解析部１２は、ステップＳ１３＿４＿７へ移る。

（ステップＳ１３＿４＿４）
分散環境モデル依存関係解析部１２は、ステップＳ１３＿４＿３で、実行パス要素ｅ１及びｅ２の遷移に「依存関係があり、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がない」ことが分かった場合、実行パス要素ｅ２の遷移が、実行パス要素ｅ１のＤｅｌａｙに含まれているか否かチェックする。実行パス要素ｅ２の遷移が、実行パス要素ｅ１のＤｅｌａｙに含まれていれば、分散環境モデル依存関係解析部１２は、ステップＳ１３＿４＿６へ移る。

（ステップＳ１３＿４＿５）
実行パス要素ｅ２の遷移が、実行パス要素ｅ１のＤｅｌａｙに含まれていなければ、分散環境モデル依存関係解析部１２は、実行パス要素ｅ２のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に含まれる実行パス要素のうち、解析対象の実行パスに中で最前方にある実行パス要素（これを「ｅ３」とする）を選び、実行パス要素ｅ１のバックトラック集合Ｂａｃｋｔｒａｃｋに、実行パス要素ｅ３の遷移を追加することで、バックトラック地点を生成する。

（ステップＳ１３＿４＿６）
次いで、分散環境モデル依存関係解析部１２は、実行パス要素ｅ１のＤｅｐｅｎｄｅｎｃｙに、実行パス要素ｅ２の遷移をキーとして、実行パス要素ｅ１の遷移を登録する。

（ステップＳ１３＿４＿７）
次に、分散環境モデル依存関係解析部１２は、ｊの値を１増やす。

（ステップＳ１３＿４＿８）
分散環境モデル依存関係解析部１２は、ｊの値が解析対象の実行パスの長さより大きいか判定し、ｊが実行パスの長さ以下の場合（ステップＳ１３＿４＿８のＮｏ分岐）、ステップＳ１３＿４＿２からＳ１３＿４＿７を繰り返す。

（ステップＳ１３＿４＿９）
分散環境モデル依存関係解析部１２は、ｊの値が解析対象の実行パスの長さより大きくなったら（ステップＳ１３＿４＿８のＹｅｓ分岐）、ｉの値を１増やし、ｊの値をｉ＋１とし、ステップＳ１３＿４＿１０に移る。

（ステップＳ１３＿４＿１０）
分散環境モデル依存関係解析部１２は、ｉの値が実行パスの長さよりも大きいか否か判定する。ｉの値が実行パスの長さ以下の場合（ステップＳ１３＿４＿１０のＮｏ分岐）、ステップＳ１３＿４＿１からＳ１３＿４＿９を繰り返す。ｉの値が実行パスの長さよりも大きい場合（ステップＳ１３＿４＿１０のＹｅｓ分岐）、ステップＳ１３＿４を終了する。

（図５のステップＳ１４の詳細）
図１０は、図５のステップＳ１４（実行パスの変更）の動作の詳細を説明する流れ図である。図１０を参照して、該ステップＳ１４についてより詳細に説明する。

（ステップＳ１４＿１）
分散環境モデル探索部１１は、まず、図５のステップＳ１３、Ｓ１７を介して、分散環境モデル依存関係解析部１２から取得した実行パスＤ１３において、
・バックトラック地点を持つ（＝バックトラック集合ＢａｃｋｔｒａｃｋからＤｏｎｅを引いた差集合が空でない）実行パス要素のうち、最後方にある実行パス要素ｅ１を探し出し、
・実行パス要素ｅ１以降の実行パス要素（ｅ１は含まない）を、実行パスＤ１３から取り除き、それを実行パスＤ１４とする。つまり、実行パスＤ１４の最後の実行パス要素は、当該実行パス要素ｅ１となる。

（ステップＳ１４＿２）
次に、分散環境モデル探索部１１は、実行パスＤ１４を遅延遷移情報付与部１３へ受け渡す。

（図５のステップＳ１５の詳細）
図１１は、図５のステップＳ１５（遅延遷移情報付与部１３による遅延遷移情報の付与）を説明する流れ図である。図１１を参照して、該ステップＳ１５について、より詳細に説明する。前述したように、遅延遷移情報付与部１３は分散環境モデル探索部１１から受け取った実行パスＤ１４を解析し、分散環境モデル探索部１１が今後の探索において実行を後回しにすべき遷移に関する情報を付与し実行パスＤ１５とする。

（ステップＳ１５＿１）
遅延遷移情報付与部１３は、分散環境モデル探索部１１から受け取った実行パスＤ１４の最後の実行パス要素ｅ１の遷移ｔｒを、実行パス要素ｅ１のＤｅｌａｙに追加する。遅延遷移情報付与部１３は、実行パスＤ１４の最後の実行パス要素ｅ１の遷移ｔｒを当該ｅ１のＤｅｌａｙに追加したものを実行パスＤ１５とする。

（ステップＳ１５＿２）。

次に、遅延遷移情報付与部１３は実行パスＤ１５を分散環境モデル探索部１１に返す。

（図５のステップＳ１６の詳細）
図１２は、図５のステップＳ１６（バックトラック実行）の動作の詳細を説明する流れ図である。図１２を参照して、該ステップＳ１６について、より詳細に説明する。

（ステップＳ１６＿１）
分散環境モデル探索部１１は、まず、実行パススタックの内容を、図５のステップＳ１５で取得した実行パスＤ１５に置き換える。

（ステップＳ１６＿３）
次に、分散環境モデル探索部１１は、実行パススタックの最後の実行パス要素ｅ１のバックトラック集合Ｂａｃｋｔｒａｃｋに含まれ、Ｄｏｎｅに含まれない任意の遷移ｔｒを１つ選び、実行パス要素ｅ１が持つ状態ｓｔに遷移ｔｒを行わせ、次の状態ｓｔ’を生成する。

（ステップＳ１６＿４）
さらに、分散環境モデル探索部１１は、実行パス要素ｅ１が持つ遷移をｔｒに置き換え、Ｄｏｎｅに遷移ｔｒを追加する。その後、図６のステップＳ１２＿５に進む。以降の手順は、図６を参照して説明したステップＳ１２と同様であるため、説明は省略する。

次に、第１の実施の形態の効果について説明する。第１の実施の形態の分散環境モデル用モデル検査装置１は、ＤＰＯＲを用いるモデル検査において、バックトラックにより探索を再開する際、ＤＰＯＲ−ＤＳとは異なり、最初に実行する遷移列を規定するのではなく、探索中に実行を後回しにする遷移（遅延遷移）を規定する。

第１の実施の形態によれば、バックトラック後の探索において、以前の探索とは内容が変わってしまう遷移があったとしても、特定の遷移の実行を後回しにするだけである。このため、前述のＤＰＯＲ−ＤＳの方法のように、実行可能でない遷移を行おうとしてしまう無駄な探索が発生することはない。

結果として、第１の実施の形態によれば、分散環境モデルに対するモデル検査においてＤＰＯＲを適用する際の探索の効率化が実現される。

＜第２の実施の形態＞
次に、本発明の第２の実施の形態について図面を参照して詳細に説明する。第２の実施の形態の基本構成は、図４の通りである。以下では、前記第１の実施の形態と同様の部分は省略し、異なる部分についてのみ説明する。まず、図４を参照して、本発明の第２の実施の形態の構成について詳細に説明する。

分散環境モデル探索部１１は、ユーザから入力装置を介して、分散環境モデルと、前記分散環境モデルが満たすべきプロパティと、を含む検証情報Ｄ１１を受け取ると、検証情報Ｄ１１を用いてモデル検査を実行する。そして、分散環境モデル探索部１１は、前記プロパティの成否と、前記プロパティが満たされない場合にはそれを示す反例と、を含む検証結果Ｄ１６を、出力装置を介してユーザに返す。前記分散環境モデルは、ＯｐｅｎＦｌｏｗによって制御されるネットワーク（ＯｐｅｎＦｌｏｗネットワーク）環境を表すモデルであるとし、その仕様は、ＯｐｅｎＦｌｏｗの仕様に則った状態遷移系であればよく、特定の仕様に限定されるものでない。前記分散環境モデルの記述形式は、機械的に処理可能であればよく、特定の形式に限定されるものでない。第２の実施の形態では、前記分散環境モデルの仕様を以下に示すものとして説明する。

第２の実施の形態の分散環境モデルにおける状態の定義について説明する。前記状態は、六つの集合の組（Ｔ，Ｓ，Ｃ，Ｐ，Ｍ，Ｑ）として定義される。

Ｔは、端末の集合である。Ｔの要素ｔ（ｔ∈Ｔ）は、その状態を表す変数ｓｖを持つ。

Ｓは、スイッチの集合である。Ｓの要素ｓ（ｓ∈Ｓ）は、スイッチにインストールされているフローエントリの集合を表す変数Ｅを持つ。Ｅの要素ｅ（ｅ∈Ｅ）は、フローエントリである。Ｅの要素ｅは、マッチングルールの内容を表す値ｍｒとアクションフィールドの内容を表す値ａｆの組（ｍｒ，ａｆ）として定義される。

Ｃは、コントローラの集合である。Ｃの要素ｃ（ｃ∈Ｃ）は、コントローラｃの各動作モデルが大域的に扱う変数の集合を表す変数Ｖを持つ。Ｖの要素ｖ（ｖ∈Ｖ）はコントローラの動作モデルが大域的に扱う変数の１つであり、変数の名前を表す値ｖｎとその変数の内容を表す値ｖｖの組（ｖｎ，ｖｖ）として定義される。

Ｐは、パケットの集合である。Ｐの要素ｐ（ｐ∈Ｐ）はパケットの内容を表す変数ｐｖを持つ。

Ｍは、ＯｐｅｎＦｌｏｗメッセージの集合である。Ｍの要素ｍ（ｍ∈Ｍ）はＯｐｅｎＦｌｏｗメッセージの内容を表す変数ｍｖを持つ。

Ｑは、通信ポートの集合である。Ｑの要素ｑ（ｑ∈Ｑ）はパケット及びＯｐｅｎＦｌｏｗメッセージを格納するＦＩＦＯ（First In,First Out）キューにより実現される通信ポートである。

各端末、スイッチ、コントローラは、その他の端末、スイッチ、コントローラと通信するための通信ポートを、互いに通信可能な各端末、スイッチ、コントローラに対し送信用と受信用とを１つずつ持つ。ある１つの端末、スイッチ、コントローラにとっての送信用通信ポートは、それ以外の１つの端末、スイッチ、コントローラにとっての受信用通信ポートであり、その逆も然りである。また、端末、スイッチ、コントローラを総称し、ノードと呼ぶ場合もある。

第２の実施の形態の分散環境モデルにおける遷移の定義について説明する。

遷移は、分散環境モデル（ＯｐｅｎＦｌｏｗネットワーク）に存在する端末、スイッチ、コントローラのいずれかが、特定の単位の動作を実行することでモデルの状態が変化する様子を表すものとする。特定の単位の動作とは、具体的には、以下の６種類である。

１． 端末のパケット送信
２． 端末のパケット受信
３． スイッチのフローエントリ適用
４． スイッチのＰａｃｋｅｔ−Ｉｎメッセージ送信
５． スイッチのＯｐｅｎＦｌｏｗメッセージ受信
６． コントローラのプログラム実行

以下では前記６種類の動作についてそれぞれ詳しく説明する。

端末のパケット送信による遷移について説明する。端末は、自身の状態ｓｖに応じて、パケット送信動作を実行することが可能である。端末のパケット送信による遷移では、端末ｔがパケットｐを１つ生成して、端末ｔの送信用通信ポート（＝あるスイッチｓにとってのパケット受信用通信ポート）にパケットｐを格納し、端末ｔの状態ｓｖの内容を変更する（変更しない場合もある）。

次に、端末のパケット受信による遷移について説明する。端末は、自身のパケット受信用通信ポートにパケットが１つ以上格納されている場合、パケット受信動作を実行することが可能である。端末のパケット受信による遷移では、パケットが１つ以上格納されている端末ｔのパケット受信用通信ポートｑから、最初に格納されたパケットｐを取り出す。
そして、パケットｐの内容ｐｖに応じて端末ｔの状態ｓｖの内容を変更する（変更しない場合もある）。

次に、スイッチのフローエントリ適用による状態遷移について説明する。スイッチは、自身のパケット受信用通信ポートにパケットが１つ以上格納されており、前記パケット受信用ポートに最初に格納されたパケットに適用可能なフローエントリを持つ場合、フローエントリ適用動作を実行することが可能である。スイッチのフローエントリ適用動作では、まずパケットが１つ以上格納されているスイッチｓのパケット受信用通信ポートｑから、最初に格納されたパケットｐを取り出す。次に、スイッチｓが持つ各フローエントリのマッチングルールｍｒと、パケットｐの内容ｐｖと、を比較し、パケットｐに適用可能なフローエントリｅを１つ選ぶ。最後に、フローエントリｅのアクションフィールドａｆに従い動作を実行する。

次に、スイッチのＰａｃｋｅｔ−Ｉｎメッセージ（ＯｐｅｎＦｌｏｗメッセージの１つ）送信による状態遷移について説明する。スイッチは、自身のパケット受信用通信ポートにパケットが１つ以上格納されており、前記パケット受信用ポートに最初に格納されたパケットに適用可能なフローエントリを持たない場合、Ｐａｃｋｅｔ−Ｉｎメッセージ送信動作を実行することが可能である。スイッチのＰａｃｋｅｔ−Ｉｎメッセージ送信動作では、まずパケットが１つ以上格納されているスイッチｓのパケット受信用通信ポートｑ１から、最初に格納されたパケットｐを取り出す。次いで、スイッチは、パケットｐの情報を含めたＰａｃｋｅｔ−Ｉｎメッセージｍを、コントローラに対応するＯｐｅｎＦｌｏｗメッセージ送信用通信ポートｑ２に格納する。

次に、スイッチのＯｐｅｎＦｌｏｗメッセージ受信による状態遷移について説明する。
スイッチは、自身のＯｐｅｎＦｌｏｗメッセージ受信用通信ポートにＯｐｅｎＦｌｏｗメッセージが１つ以上格納されている場合、ＯｐｅｎＦｌｏｗメッセージ受信動作を実行することが可能である。スイッチのＯｐｅｎＦｌｏｗメッセージ受信動作では、まずＯｐｅｎＦｌｏｗメッセージが１つ以上格納されているスイッチｓのＯｐｅｎＦｌｏｗメッセージ受信用通信ポートｑから、最初に格納されたＯｐｅｎＦｌｏｗメッセージｍを取り出す。次いで、スイッチは、ＯｐｅｎＦｌｏｗメッセージｍの内容ｍｖに従い動作を実行する。

次に、コントローラのプログラム実行による状態遷移について説明する。コントローラは、自身のＯｐｅｎＦｌｏｗメッセージ受信用通信ポートにＯｐｅｎＦｌｏｗメッセージが１つ以上格納されている場合、プログラム実行動作を実行することが可能である。コントローラのプログラム実行動作では、まずＯｐｅｎＦｌｏｗメッセージが１つ以上格納されているコントローラｃのＯｐｅｎＦｌｏｗメッセージ受信用通信ポートｑから、最初に格納されたＯｐｅｎＦｌｏｗメッセージｍを１つ取り出す。次に、ＯｐｅｎＦｌｏｗメッセージｍの内容ｍｖを参照し、検証情報Ｄ１１に含まれる分散環境モデルにおいて定義されているコントローラの動作のうち、ｍｖに対応するものを実行する（定義されていない場合はＯｐｅｎＦｌｏｗ仕様で規定されているデフォルトの動作を実行する）。

本発明の第２の実施の形態においては、第２の実施の形態で用いる分散環境モデルの仕様と、ＤＰＯＲのアルゴリズムと、を考慮し、以下のように依存関係を定義する。

遷移ｔ１で動作したノードと遷移ｔ２で動作したノードが同じノードである。

本発明の第２の実施の形態においては、第２の実施の形態で分散環境モデルの仕様と、ＤＰＯＲのアルゴリズムと、を考慮し、以下のようにｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を定義する。

１．遷移ｔ１で送信されるパケット又はメッセージと、遷移ｔ２で受信されるパケット又はＯｐｅｎＦｌｏｗメッセージが同じである場合、ｔ１→ｔ２

２．遷移ｔ１でインストールされるフローエントリと、遷移ｔ２で適用されるフローエントリが同じである場合、ｔ１→ｔ２

３．遷移ｔ１で受信されるパケット又はＯｐｅｎＦｌｏｗメッセージｐｍ１と、遷移ｔ２で受信されるパケット又はＯｐｅｎＦｌｏｗメッセージｐｍ２と、は同じ受信用通信ポートｑに格納されており、ｐｍ１をｑに格納した遷移ｔ３と、ｐｍ２をｑに格納した遷移ｔ４と、がｔ３→ｔ４である場合、ｔ１→ｔ２

４．ｔ１→ｔ２であり、ｔ２→ｔ３である場合、ｔ１→ｔ３

次に、本発明の第２の実施の形態における遷移のデータ構造について説明する。遷移は、七つの要素の組（ｎｏｄｅ，ｔｙｐｅ，ｓｅｎｄ，ｒｅｃｖ，ｐｏｒｔ，ｉｎｓｔａｌｌ，ａｐｐｌｙ）で表される。

ｎｏｄｅは、当該遷移で動作した端末、スイッチ、コントローラである。
ｓｅｎｄは、当該遷移で送信したパケット又はＯｐｅｎＦｌｏｗメッセージの集合を表す。

ｒｅｃｖは、当該遷移で受信したパケット又はＯｐｅｎＦｌｏｗメッセージを表す。

ｐｏｒｔは、当該遷移で受信したパケット又はＯｐｅｎＦｌｏｗメッセージが格納されていた受信用通信ポートを表す。

ｉｎｓｔａｌｌは、当該遷移でインストールされたフローエントリを表す。

ａｐｐｌｙは、当該遷移で適用されたフローエントリを表す。

このデータ構造に基づく遷移データは、分散環境モデル探索部１１による探索において、状態が遷移した際に、該遷移の内容に応じて、各フィールドの値が適切に設定された上で生成される。

次に、本発明の第２の実施の形態の動作について詳細に説明する。

図７のステップＳ１３＿３について、図８を参照してより詳細に説明する。ステップＳ１３＿３の手順の流れは第１の実施の形態と同様であるが、図８のステップＳ１３＿３＿３の内容が異なるため、ステップＳ１３＿３＿３の内容ついてのみ説明し、それ以外は省略する。

分散環境モデル依存関係解析部１２は、ステップＳ１３＿３＿３では、実行パス要素ｅ１の遷移と実行パス要素ｅ２の遷移を比較し、「実行パス要素ｅ２の遷移→実行パス要素ｅ１の遷移」（ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係）であるか否か確認する。

具体的には、分散環境モデル依存関係解析部１２は、まず、実行パス要素ｅ１の遷移の受信メッセージｒｅｃｖが、実行パス要素ｅ２の送信メッセージ集合ｓｅｎｄに含まれるか否か確認する。

実行パス要素ｅ１の遷移の受信メッセージｒｅｃｖが、実行パス要素ｅ２の送信メッセージ集合ｓｅｎｄに含まれる場合、分散環境モデル依存関係解析部１２は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係があるとする。一方、含まれない場合には、分散環境モデル依存関係解析部１２は、実行パス要素ｅ１の遷移で適用したフローエントリと、実行パス要素ｅ２の遷移でインストールしたフローエントリとが一致するか否か比較する。

実行パス要素ｅ１の遷移で適用したフローエントリと、実行パス要素ｅ２の遷移でインストールしたフローエントリとが一致する場合、分散環境モデル依存関係解析部１２は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係があるとする。一致しない場合には、分散環境モデル依存関係解析部１２は、実行パス要素ｅ１及び実行パス要素ｅ２の遷移で使用した受信用通信ポートｐｏｒｔが互いに一致するか否か比較する。

実行パス要素ｅ１及び実行パス要素ｅ２の遷移で使用した受信用通信ポートｐｏｒｔが一致しない場合、分散環境モデル依存関係解析部１２は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がないとする。一致する場合は、分散環境モデル依存関係解析部１２は、解析対象の実行パスの中から、実行パス要素ｅ１の遷移の受信メッセージｒｅｃｖを含むｓｅｎｄを持つ遷移を持つ実行パス要素ｅ３と、実行パス要素ｅ２の遷移の受信メッセージｒｅｃｖを含むｓｅｎｄを持つ遷移を持つ実行パス要素ｅ４と、を探し、実行パス要素ｅ３のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に実行パス要素ｅ４が含まれるか否かを確認する。

実行パス要素ｅ３のｈａｐｐｅｎｓ−ｂｅｆｏｒｅ集合に実行パス要素ｅ４が含まれる場合、分散環境モデル依存関係解析部１２は、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係があるとし、含まれない場合には、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がないとする。

（図７のステップＳ１３＿４の詳細）
図９は、図７のステップＳ１３＿４の動作の詳細について説明する図である。図９を参照して、ステップＳ１３＿４についてより詳細に説明する。

図９のステップＳ１３＿４の手順の流れは、前記第１の実施の形態と同様であるが、ステップＳ１３＿４＿３の内容が異なるため、ステップＳ１３＿４＿３の内容についてのみ説明し、それ以外の説明は省略する。

（ステップＳ１３＿４＿３）
分散環境モデル依存関係解析部１２は、実行パス要素ｅ１の遷移と、実行パス要素ｅ２の遷移と、を比較し、それらに「依存関係があり、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係がない」か否か確認する。

分散環境モデル依存関係解析部１２は、ステップＳ１３＿４＿３の比較のうち、依存関係に関しては、実行パス要素ｅ１及びｅ２の遷移の動作ノードｎｏｄｅが一致する場合、依存関係があるとする。ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係に関しては、前記第１の実施の形態におけるステップＳ１３＿４＿３と同様であるため、説明は省略する。

本発明の第２の実施の形態の効果について以下に説明する。第２の実施の形態の分散環境モデル用モデル検査装置１は、ＤＰＯＲを用いるモデル検査において、バックトラックにより探索を再開する際、ＤＰＯＲ−ＤＳとは異なり、最初に実行する遷移列を規定するのではなく、探索中に実行を後回しにする遷移（遅延遷移）を規定する。

本発明の第２の実施の形態によれば、バックトラック後の探索において、以前の探索とは内容が変わってしまう遷移があったとしても、特定の遷移の実行を後回しにする。前述のＤＰＯＲ−ＤＳの方法では、実行可能でない遷移を行おうとしてしまう無駄な探索が発生する場合がある。第２の実施の形態では、このようなことはない。その結果、第２の実施の形態によれば、ＯｐｅｎＦｌｏｗネットワーク環境を表す分散環境モデルに対するモデル検査において、ＤＰＯＲを適用する際の探索の効率化が実現される。

なお、第２の実施の形態の分散環境モデル用モデル検査装置１において、以下の第３の実施の形態と同様に、モデル検査による探索の際、探索した状態を記憶管理する。そして、分散環境モデル用モデル検査装置１は、探索において行われた遷移の内容とその順序を履歴として表すグラフ（例えば有向グラフ）を用いて、探索した遷移をパス毎に記憶管理するようにしてもよい。また、前記探索した状態及び遷移の記憶管理にあたり、探索済み状態からどの遷移が行われたかを紐付け（関連付け）しておくようにしてもよい（詳細は、以下の第３の実施の形態で説明される）。そして、モデル検査による探索中に、探索済み状態に到達したら、該探索済み状態と、探索済み状態から行われた遷移の履歴情報が紐付けて保存・管理されていることから、当該履歴情報を取得する。そして、到達した状態以降は疑似的にその履歴情報と同様の遷移を行ったものとみなし、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析して、バックトラック地点を生成し探索を打ち切るようにしてもよい。探索済み状態以降を、再度探索することなく、依存関係及びｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析することを可能としている。この結果、ＯｐｅｎＦｌｏｗネットワーク環境を表した分散環境モデルに対するモデル検査においてＤＰＯＲを適用する場合でも、探索済み状態以降の探索を打ち切ることが可能となる。その結果、探索の効率化が実現される。

＜第３の実施の形態＞
次に、本発明の第３の実施の形態について図面を参照して詳細に説明する。以下では、前述した第１の実施の形態と同様の部分は省略し、主に、相違点について説明する。なお、第３の実施の形態では、モデル検査による探索の際、探索した状態を記憶管理するとともに、探索において行われた遷移の内容とその順序を履歴として表すグラフ（例えば有向グラフ）を用いて、探索した遷移をパス毎に記憶管理する。図１３を参照して、本発明の第３の実施の形態の構成について詳細に説明する。

図１３を参照すると、本発明の第３の実施の形態における分散環境モデル用モデル検査装置３は、分散環境モデル探索部１１と、分散環境モデル依存関係解析部１２と、遅延遷移情報付与部１３と、探索済み状態管理部３４と、探索済み遷移履歴管理部３５と、探索済み状態遷移対応情報管理部３６と、を含む。分散環境モデル探索部１１は、分散環境モデル依存関係解析部１２、遅延遷移情報付与部１３、探索済み状態管理部３４、探索済み遷移履歴管理部３５、探索済み状態遷移対応情報管理部３６のそれぞれと、情報をやり取りするように構成されている。また、分散環境モデル用モデル検査装置３は、ＬＳＩ（Large Scale Integration）等のハードウェア部品である回路部品を実装することにより、その動作をハードウェア的に実現することができる。あるいは、その機能を提供するプログラムを、図示しないソフトウェア記憶媒体に格納し、そのプログラムを主記憶部にロードしてＣＰＵにおいて実行することにより、ソフトウェア的に実現することも可能である。

探索済み状態遷移対応情報管理部３６は、探索済み状態管理部３４が記憶管理する探索済み状態と、探索済み遷移履歴管理部３５が記憶管理する遷移と、を紐付け（関係付け）るため、その対応関係を管理する。

分散環境モデル依存関係解析部１２は、分散環境モデル探索部１１から、
・前半部分実行パスと、
・後半部分実行パスと、を含む実行パス情報Ｄ３２を受け取る。分散環境モデル依存関係解析部１２は、前半部分実行パスと、後半部分実行パスと、を結合してできる実行パス上の２つの遷移間の依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析し、前半部分実行パス上に、バックトラック地点を生成する。分散環境モデル依存関係解析部１２は、その結果（バックトラック地点が生成された前半部分実行パス）Ｄ３３を分散環境モデル探索部１１に返す。

実行パス情報Ｄ３２のデータ構造について説明する。実行パス情報Ｄ３２に含まれる前半部分実行パスは、６つの実行パス要素（ｓｔ，ｔｒ，Ｂａｃｋｔｒａｃｋ，Ｄｏｎｅ，Ｄｅｌａｙ，Ｄｅｐｅｎｄｅｎｃｙ）を要素とする配列（又はそれに準ずるデータ構造）である。

ｓｔは、ある時点での分散環境モデルの状態である。

ｔｒは、状態ｓｔから実行された遷移である。

Ｂａｃｋｔｒａｃｋは、モデル検査による探索においてバックトラックするにあたり、バックトラックの際に状態ｓｔから実行されるべき遷移の集合を表す。

Ｄｏｎｅは、過去の探索において状態ｓｔから実行した遷移の集合を表す。

Ｄｅｌａｙは、状態ｓｔ以降の探索において実行を後回しにすべき遷移（＝遅延遷移）の集合を表す。ＢａｃｋｔｒａｃｋからＤｏｎｅを引いた差集合は、状態ｓｔからバックトラックして実行されるべきであるが、まだされていない遷移の集合を表す。

Ｄｅｐｅｎｄｅｎｃｙは、分散環境モデル依存関係解析部１２により依存関係があると判明した遷移を記憶しておくハッシュ表（あるいは、ハッシュ表に準ずるデータ構造）である。キーは遷移、値はその前記遷移と依存関係にある遷移の集合である。

本明細書では、Ｄｅｐｅｎｄｅｎｃｙを用いて遷移ｔｒ１をキーとして取得できる遷移集合ｔｒ＿ｓｅｔに遷移ｔｒ２を加えることを、「ｔｒ１をキーとしてｔｒ２をＤｅｐｅｎｄｅｎｃｙに登録する」と表現する。ただし、Ｄｅｐｅｎｄｅｎｃｙを用いてｔｒ１をキーとして取得できる値がない場合は、｛ｔｒ２｝（ｔｒ２を要素として持つ集合）をキーｔｒ１に対応する値として設定することとする。実行パス情報Ｄ３２に含まれる後半部分実行パスは、遷移の配列（あるいはそれに準ずるデータ構造）である。

「実行パス要素の遷移」と表現した場合、
・前半部分実行パスの要素の場合、ｔｒのことを表し、
・後半部分実行パスの要素の場合、その要素そのもの（＝遷移）を表す。

実行パス情報Ｄ３２に含まれる前半部分実行パスは１つでなければならない。これに対して、後半部分実行パスは複数あってもよく、あるいは、なくてもよい。

なお、後半部分実行パスの要素は、後述されるように、分散環境モデル探索部１１の探索中に、探索済み状態に到達したら、該探索済み状態から行われた遷移の履歴情報を探索済み遷移履歴管理部３５から取得し、当該到達した状態以降を、疑似的にその履歴情報と同様の遷移を行ったものとみなして設定されたパスに相当する。

前半部分実行パスＤ３３のデータ構造は、前述した実行パス情報Ｄ３２に含まれる前半部分実行パスのデータ構造と同様である。

遅延遷移情報付与部１３は、分散環境モデル探索部１１から、前半部分実行パスＤ３４を受け取ると、分散環境モデル探索部１１が今後行う探索において、実行を後回しにすべき遷移の情報を前半部分実行パスＤ３４に付与し、その結果（前半部分実行パスＤ３５）を、分散環境モデル探索部１１に返す。

前半部分実行パスＤ３４、Ｄ３５のデータ構造は、前述した実行パス情報Ｄ３２に含まれる前半部分実行パスのデータ構造と同様である。

探索済み状態管理部３４は、分散環境モデル探索部１１から、探索が行われた状態を受け取り保存（記憶）する。状態を保存する方法は、
・受け取った状態をそのまま保存（記憶）してもよいし、あるいは、
・何らかの変換を施したもの（例えば記憶容量削減のため圧縮されたもの）を保存（記憶）してもよい。

また、探索済み状態管理部３４は、分散環境モデル探索部１１から、これから探索する状態が過去に探索済みの状態であるか否かの問い合わせを受け付けると、当該状態と一致するものが、探索済み状態管理部３４で記憶している状態の中に存在するか否か検索する。探索済み状態管理部３４は、
・当該状態と一致するものが存在する場合には、「探索済み」、
・当該状態と一致するものが存在しない場合には、「未探索」
という回答を、分散環境モデル探索部１１に返す。

探索済み遷移履歴管理部３５は、分散環境モデル探索部１１から、探索が行われた遷移を受け取り、以下で説明するグラフ構造により保存する。

グラフの全てのノードは遷移を表している。ノード間には有向エッジが引かれる。有向エッジは、分散環境モデルにおける特定の実行パス上での遷移の実行順序を表す。ただし、根ノードと呼ばれる特別なノードだけは遷移ではなく実行パスの出発点を表す。

分散環境モデルの初期状態から行われる遷移を表すノードには、根ノードから有向エッジが引かれる。

ＳＤＰＯＲにおいては、互いに異なる実行パス上で行われる遷移ｔｒに関して、管理するグラフ中で遷移ｔｒを表すノードは常に１つである。これに対し、本発明の第３の実施形態の探索済み遷移履歴管理部３５においては、互いに異なる実行パス上で行われる遷移ｔｒに関して、実行パス毎に異なるノードを作成し、各実行パス上の遷移ｔｒを個別に表す。

本発明の第３の実施の形態によれば、このようなグラフ構造を用いることで、根ノードから有向エッジを辿ることにより、特定の実行パス上で行われた遷移の列が取得できる形で遷移を保存するのが、ＳＤＰＯＲとの差異である。

ＳＤＰＯＲでは、ＤＰＯＲ−ＤＳが定義しているｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行わない。ＳＤＰＯＲが管理するグラフも、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を目的としていず、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析に必要な情報を保持しない。

本発明の第３の実施の形態において管理するグラフは、前述した差異（ＳＤＰＯＲとの差異）のため、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析に必要な情報を保持できる。これにより、ＤＰＯＲ−ＤＳのように、探索のバックトラックの要否にｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を考慮する場合でも、ＳＤＰＯＲのように、探索済み状態以降を再探索することは必要とされず、探索を打ち切ることが可能になる。結果として、探索の効率化が実現される。

分散環境モデル探索部１１による探索の開始時点では、グラフは空である。分散環境モデル探索部１１から新しいノード及び有向エッジを生成する操作を受け付け、グラフが構築されていく。

探索済み状態遷移対応情報管理部３６は、分散環境モデル探索部１１により過去に探索された状態と、前記状態から行われた遷移と、を紐付ける情報を保存する。探索済み状態遷移対応情報管理部３６は、分散環境モデル探索部１１から、状態を入力として与えられ、該状態から行われた遷移の問い合わせが行われると、探索済み遷移履歴管理部３５に登録されている、該状態から行われた遷移を表すノードを、分散環境モデル探索部１１に返す。該状態から行われた遷移が複数ある場合には、それらの遷移を表すノードを全て返す。

また、探索済み状態遷移対応情報管理部３６は、分散環境モデル探索部１１から、状態と遷移を入力として与えられ、該状態と該遷移を紐付ける操作を受け付けると、当該状態と、探索済み遷移履歴管理部３５に保存されている前記遷移を表すノードと、を紐付ける情報を保存する。

図１４は、本発明の第３の実施の形態の全体の動作を説明するための流れ図である。図１３及び図１４を参照して、本発明の第３の実施の形態の動作について詳細に説明する。

（ステップＳ３２）
分散環境モデル探索部１１は、検証情報Ｄ１１を受け取ると、検証情報Ｄ１１に含まれる分散環境モデルを状態遷移させて適当なパスの１つについて探索を行い、実行パス情報Ｄ３２を生成し、実行パス情報Ｄ３２を分散環境モデル依存関係解析部１２に受け渡す。

（ステップＳ３３）
分散環境モデル依存関係解析部１２は、実行パス情報Ｄ３２に含まれる、前半部分実行パスと、後半部分実行パスと、を結合してできる実行パス上の依存関係及びｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する。分散環境モデル依存関係解析部１２は、前記前半部分実行パス上にバックトラック地点を生成し、その結果（バックトラック地点が生成された前半部分実行パス）Ｄ３３を、分散環境モデル探索部１１に返す。

（ステップＳ３４）
分散環境モデル探索部１１は、前半部分実行パスＤ３３上で一番深い（最後方の）バックトラック地点を特定して、当該バックトラック地点に基づき、前半部分実行パスＤ３３に変更を加える。分散環境モデル探索部１１は、前記変更を加えた前半部分実行パスＤ３４を遅延遷移情報付与部１３に受け渡す。

（ステップＳ３５）
遅延遷移情報付与部１３は、前半部分実行パスＤ３４を解析して、今後の探索において実行を後回しにすべき遷移に関する情報を前半部分実行パスＤ３４に付与する。遅延遷移情報付与部１３は、前記情報を付与した前半部分実行パスＤ３５を分散環境モデル探索部１１に返す。

（ステップＳ３６）
分散環境モデル探索部１１は、前半部分実行パスＤ３５上で一番深いバックトラック地点から分散環境モデルを再び状態遷移させ（バックトラック実行）、新たな実行パス情報Ｄ３２’を得る。分散環境モデル探索部１１は、新たな実行パス情報Ｄ３２’を分散環境モデル依存関係解析部１２に受け渡す。

（ステップＳ３７）
分散環境モデル探索部１１では、実行パス情報Ｄ３２に含まれる前半部分実行パスのバックトラック地点の有無を判定する。実行パス情報Ｄ３２に含まれる前半部分実行パス上から、バックトラック地点が存在する場合（ステップＳ３７のＹｅｓ分岐）、ステップＳ３４〜３６の手順を繰り返す。パス情報Ｄ３２に含まれる前半部分実行パス上にバックトラック地点がなくなると（ステップＳ３７のＮｏ分岐）、分散環境モデル探索部１１はモデル検証結果を出力する。

（図１４のステップＳ３２の詳細）
図１５、図１６は、図１４のステップＳ３２の動作の詳細を説明する図である。図１３及び図１５、図１６を参照して、ステップＳ３２についてより詳細に説明する。

（ステップＳ３２＿１）
分散環境モデル探索部１１は、検証情報Ｄ１１から分散環境モデルを抽出し、その初期状態ｓｔ０を生成して状態ｓｔ ＝ ｓｔ０とする。

（ステップＳ３２＿２）
次に、分散環境モデル探索部１１は、探索済み遷移履歴管理部３５が管理するグラフに根ノードを生成させる。

（ステップＳ３２＿３）
さらに、分散環境モデル探索部１１は、初期状態ｓｔ０と前記根ノードを、探索済み状態遷移対応情報管理部３６に紐付けさせる。

（ステップＳ３２＿４）
次いで、分散環境モデル探索部１１は、初期状態ｓｔ０を探索済み状態管理部３４に登録する。

（ステップＳ３２＿５）
次に、分散環境モデル探索部１１は、状態ｓｔが実行可能な遷移が１つ以上あるかチェックする。

（ステップＳ３２＿６）
状態ｓｔが実行可能な遷移が１つ以上ある場合（ｓｔは遷移可能：ステップＳ３２＿５のＹｅｓ分岐）、実行パススタックの一番上にある実行パス要素ｅ１のＤｅｌａｙから、実行パス要素ｅ１のＤｅｐｅnｄｅｎｃｙを用いて実行パス要素ｅ１の持つ遷移ｔｒ＿ｅ１をキーとして取得できる遷移集合ｔｒ＿ｓｅｔに含まれる各遷移と、前記遷移ｔｒ＿ｅ１と、を取り除いた（実行パス要素ｅ１のＤｅｌａｙとｔｒ＿ｓｅｔの差集合から遷移ｔｒ＿ｅ１を取り除いた）Ｄｅｌａｙ’を計算する。そして、分散環境モデル探索部１１は、状態ｓｔが実行可能な遷移の中から、Ｄｅｌａｙ’に含まれない遷移ｔｒ＿ｓｔを１つ選び、状態ｓｔに遷移ｔｒ＿ｓｔを行わせて、次の状態ｓｔ’を生成する。

分散環境モデル探索部１１は、実行パススタックが空である（＝実行パス要素ｅ１がない）場合、Ｄｅｌａｙ’を｛ ｝（空集合）とし、状態ｓｔから実行可能な遷移の中から任意の遷移ｔｒ＿ｓｔを選ぶ。

状態ｓｔが実行可能な遷移に、該Ｄｅｌａｙ’（実行パス要素ｅ１のＤｅｌａｙとｔｒ＿ｓｅｔの差集合から遷移ｔｒ＿ｅ１を取り除いた集合）に含まれない遷移が存在しない場合にも、状態ｓｔが実行可能な遷移の中から、任意の遷移ｔｒ＿ｓｔを選び、状態ｓｔに遷移ｔｒ＿ｓｔを行わせて、次の状態ｓｔ’を生成する。以上はステップＳ３２＿６の処理である。

（ステップＳ３２＿７）
次に、分散環境モデル探索部１１は、新しい実行パス要素ｅ２ ＝（ｓｔ，ｔｒ＿ｓｔ，｛ ｝，｛ｔｒ＿ｓｔ｝，Ｄｅｌａｙ，Ｄｅｐｅｎｄｅｎｃｙ）を生成し、実行パススタックに積む。ここで、新しい実行パス要素ｅ２のＤｅｌａｙの内容は、ステップＳ３２＿６で計算されたＤｅｌａｙ’である。また、新しい実行パス要素ｅ２のＤｅｐｅｎｄｅｎｃｙの内容は、実行パス要素ｅ１のＤｅｐｅnｄｅｎｃｙから、前記遷移ｔｒ＿ｅ１と前記遷移集合ｔｒ＿ｓｅｔのペアを取り除いたものである。

（ステップＳ３２＿８）
次いで、分散環境モデル探索部１１は、探索済み遷移履歴管理部３５が管理するグラフに遷移ｔｒ＿ｓｔを表すノードｎｄ１を生成させ、遷移ｔｒ＿ｓｔの直前に行った遷移を表すノード（ｔｒ＿ｓｔが初期状態からの遷移であれば根ノード）からノードｎｄ１への有向エッジを引く。

（ステップＳ３２＿９）
次に、分散環境モデル探索部１１は、状態ｓｔ’と、ノードｎｄ１と、を探索済み状態遷移対応情報管理部３６に紐付けさせる。

（ステップＳ３２＿１０）
さらに、分散環境モデル探索部１１は、状態ｓｔ’が探索済み状態管理部３４に登録済みか否かチェックする。

（ステップＳ３２＿１１）
分散環境モデル探索部１１は、ステップＳ３２＿１０で、登録済みでなければ（図１５のステップＳ３２＿１０のＮｏ分岐）、状態ｓｔ’を探索済み状態管理部３４に登録する。その後、ステップＳ３２＿５へ戻る（戻る際にｓｔ＝ｓｔ’とする）。

（ステップＳ３２＿１９）
図１５のステップＳ３２＿５の遷移可能の判定において、状態ｓｔから実行可能な遷移が１つもない場合（図１５のステップＳ３２＿５のＮｏ分岐）、分散環境モデル探索部１１は、その時点での実行パススタックの内容が前半部分実行パスであり、後半部分実行パスが空の実行パスである実行パス情報Ｄ３２を生成し、分散環境モデル依存関係解析部１２に受け渡し、ステップＳ３２を終了する。

（図１６のステップＳ３２＿１２）
図１５のステップＳ３２＿１０で状態ｓｔ’が登録済みである場合（ステップＳ３２＿１０のＹｅｓ分岐）、まず、探索済み状態遷移対応情報管理部３６において、状態ｓｔ’と紐付いているノードを全て取得する。

（図１６のステップＳ３２＿１５）
分散環境モデル探索部１１は、選んでいないノードが存在するか否か判定する。選んでいないノードが存在する場合（図１６のステップＳ３２＿１５のＹｅｓ分岐）、ステップＳ３２＿１３で全てのノードが選び出されるまで、ステップＳ３２＿１３からＳ３２＿１４を繰り返す。

（図１６のステップＳ３２＿１３）
分散環境モデル探索部１１は、状態ｓｔ’と紐付いているノードの中から任意のノードｎｄ２を選び出す。

（図１６のステップＳ３２＿１４）
分散環境モデル探索部１１は、探索済み遷移履歴管理部３５が管理するグラフにおいて、ノードｎｄ２から有向エッジを１つだけ辿って到達できるノードｎｄ３を全て列挙する。

（図１６のステップＳ３２＿１６）
図１６のステップＳ３２＿１５の判定で、選んでいないノードが存在しない場合、分散環境モデル探索部１１は、図１５のステップＳ３２＿８で生成したノードｎｄ１から、図１６のステップＳ３２＿１４で列挙したノードｎｄ３のそれぞれに対し、有向エッジを引く。

（図１６のステップＳ３２＿１７）
次に、分散環境モデル探索部１１は、状態ｓｔ’を起点状態とし、後半部分実行パスを取得する。

（図１６のステップＳ３２＿１８）
最後に、分散環境モデル探索部１１は、その時点での実行パススタックの内容が前半部分実行パスであり、図１６のステップＳ３２＿１７で取得したものが後半部分実行パスである実行パス情報Ｄ３２を生成し、分散環境モデル依存関係解析部１２に受け渡して、ステップＳ３２を終了する。

（図１６のステップＳ３２＿１７の詳細）
図１７は、図１６のステップＳ３２＿１７の動作の詳細を説明する図である。図１７を参照して、ステップＳ３２＿１７についてより詳細に説明する。

（ステップＳ３２＿１７＿１）
探索済み状態遷移対応情報管理部３６は、起点状態ｓｔと紐付けられている全てのノードを抽出する。

（ステップＳ３２＿１７＿４）
分散環境モデル探索部１１は、ステップＳ３２＿１７＿１で抽出したノードが全て選び出されるまで、ステップＳ３２＿１７＿２からＳ３２＿１７＿３を繰り返す。

（ステップＳ３２＿１７＿２）
次に、分散環境モデル探索部１１は、起点状態ｓｔと紐付けられている全てのノードの中から任意のノードｎｄを選び出す。

（ステップＳ３２＿１７＿３）
分散環境モデル探索部１１は、探索済み遷移履歴管理部３５が管理するグラフにおいて、ノードｎｄから有向エッジを最後まで（＝他のノードへの有向エッジがないノードに到達するまで）たどって得られる実行パスを取得する。

ステップＳ３２＿１７＿２の途中で分岐が生じる（＝他のノードへの有向エッジが複数あるノードに到達する）場合、分散環境モデル探索部１１は、有向エッジの辿り方の全てのパターンを網羅し、全ての実行パスを取得する。

（ステップＳ３２＿１７＿５）
分散環境モデル探索部１１は、上記手順で取得した実行パス全てを後半部分実行パスとし、ステップＳ３２＿１７を終了する。

（図１４のステップＳ３３の詳細）
図１８は、図１４のステップＳ３３の動作の詳細を説明する流れ図である。図１８を参照して、ステップＳ３３についてより詳細に説明する。

（ステップＳ３３＿１）
分散環境モデル依存関係解析部１２は、まず、実行パス情報Ｄ３２に含まれる後半部分実行パスから、任意のものを１つ選び出す。

（ステップＳ３３＿２）
次に、分散環境モデル依存関係解析部１２は、実行パス情報Ｄ３２に含まれる、前半部分実行パスと、ステップＳ３３＿１で選んだ後半部分実行パスと、を結合してできる実行パスを解析の対象とする。

（ステップＳ３３＿３）
次に、分散環境モデル依存関係解析部１２は、解析の対象の実行パスに対して、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析するための前処理を行う。

（ステップＳ３３＿４）
さらに、分散環境モデル依存関係解析部１２は、前処理を行った解析の対象の実行パスから、依存関係及びｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析とバックトラック地点の生成を行う。

（ステップＳ３３＿５）
実行パス情報Ｄ３２に含まれる後半部分実行パスが複数ある場合、その全てがステップＳ３３＿１で選び出されるまで、分散環境モデル依存関係解析部１２は、ステップＳ３３＿１からＳ３３＿４を繰り返す。

（ステップＳ３３＿６）
最後に、分散環境モデル依存関係解析部１２は、バックトラック地点を生成した前半部分実行パスＤ３３を分散環境モデル探索部１１に返し、ステップＳ３３を終了する。

なお、ステップＳ３３＿３の動作は、前述した本発明の第２の実施の形態におけるステップ１３＿３と同様であるため、説明は省略する。

（図１８のステップＳ３３＿４の詳細）
図１８のステップＳ３３＿４について、図９を参照してより詳細に説明する。図１８のステップＳ３３＿４の手順の流れは、前述した第２の実施の形態において図９を参照して説明したステップＳ１３＿４と基本的に同様とされるが、図９のステップＳ１３＿４＿１０の処理内容が異なる。このため、以下では、図９のステップＳ１３＿４＿１０の内容についてのみ説明し、それ以外の説明は省略する。

本発明の第３の実施の形態におけるステップＳ１３＿４＿１０では、ｉの値が前半部分実行パスの長さよりも大きくなるまで、ステップＳ１３＿４＿１からＳ１３＿４＿９を繰り返す。

（図１４のステップＳ３４の詳細）
次に、図１４のステップＳ３４について、図１０を参照して、より詳細に説明する。なお、以下では、図１０における実行パスＤ１３、Ｄ１４は、それぞれ前半部分実行パスＤ３３、Ｄ３４に置き換え（読み替え）られる。

（ステップＳ３４＿１）
分散環境モデル探索部１１は、まず、ステップＳ３３で取得した前半部分実行パスＤ３３において、バックトラック地点を持つ（＝バックトラック集合ＢａｃｋｔｒａｃｋからＤｏｎｅを引いた差集合が空でない）実行パス要素のうち、最後方にある実行パス要素ｅ１を探し出し、それ以降の実行パス要素（ｅ１は含まない）を前半部分実行パスＤ３３から取り除き、それを前半部分実行パスＤ３４とする（図１０のステップＳ１４＿１）。つまり、前半部分実行パスＤ３４の最後の実行パス要素は前記実行パス要素ｅ１となる。

（ステップＳ３４＿２）
次に、前半部分実行パスＤ３４を遅延遷移情報付与部１３へ受け渡す（図１０のステップＳ１４＿２）。

（図１４のステップＳ３５の詳細）
次に、図１４のステップＳ３５について、図１１を参照して、より詳細に説明する。なお、以下では、図１１における実行パスＤ１４は、前半部分実行パスＤ３４に置き換え（読み替え）られる。

（ステップＳ３５＿１）
遅延遷移情報付与部１３は、まず、前半部分実行パスＤ３４の最後の実行パス要素ｅ１の遷移ｔｒを、ｅ１のＤｅｌａｙに追加し、それを前半部分実行パスＤ３５とする（図１１のステップＳ１５＿１）。

（ステップＳ３５＿２）
次に、遅延遷移情報付与部１３は、前半部分実行パスＤ３５を分散環境モデル探索部１１に返す（図１１のステップＳ１５＿２）。

（図１４のステップＳ３６の詳細）
図１９は、図１４のステップＳ３６の動作の詳細を説明する流れ図である。図１９を参照して、ステップＳ３６についてより詳細に説明する。

（ステップＳ３６＿１）
分散環境モデル探索部１１は、まず、実行パススタックの内容を、ステップＳ３５で取得した前半部分実行パスＤ３５に置き換える。

（ステップＳ３６＿３）
次に、分散環境モデル探索部１１は、実行パススタックの最後の実行パス要素ｅ１のバックトラック集合Ｂａｃｋｔｒａｃｋに含まれ、Ｄｏｎｅに含まれない任意の遷移ｔｒを１つ選び、実行パス要素ｅ１が持つ状態ｓｔに遷移ｔｒを行わせ、次の状態ｓｔ’を生成する。

（ステップＳ３６＿４）
さらに、分散環境モデル探索部１１は、実行パス要素ｅ１が持つ遷移をｔｒに置き換え、Ｄｏｎｅに遷移ｔｒを追加する。

（ステップＳ３６＿５）
次いで、分散環境モデル探索部１１は、探索済み遷移履歴管理部３５が管理するグラフに、遷移ｔｒを表すノードｎｄ１を生成させる。

（ステップＳ３６＿６）
次に、探索済み状態遷移対応情報管理部３６において、状態ｓｔと紐付いているノードを全て列挙し、探索済み遷移履歴管理部３５が管理するグラフにおいて、そのそれぞれからｎｄ１への有向エッジを引く。

（ステップＳ３６＿７）
さらに、分散環境モデル探索部１１は、状態ｓｔ’とノードｎｄ１を、探索済み状態遷移対応情報管理部３６に紐付けさせる。

その後、分散環境モデル探索部１１は、ステップＳ３２＿１０に進み、以降の手順は、ステップＳ３２の説明で述べたものと同様なので省略する。

第３の実施の形態の効果について以下に説明する。第３の実施の形態の分散環境モデル用モデル検査装置３は、ＤＰＯＲを用いたモデル検査による探索の際、探索した状態を記憶して管理するとともに、探索において行われた遷移の内容とその順序をパス毎に区別して取得可能な履歴を表すグラフ構造を用いて、探索した遷移を記憶管理する。また、探索した状態及び遷移の管理にあたり、探索済みの状態からどの遷移が行われたかを紐付けておく。モデル検査による探索中に探索済みの状態に到達したら、前記探索済みの状態及び、前記探索済みの状態から行われた遷移の履歴情報が紐付けて保存・管理されているため、前記履歴情報を取得する。そして、前記探索済みの状態以降は、疑似的に、当該履歴情報と同様の遷移を行ったものとみなして、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析し、バックトラック地点を生成し探索を打ち切ることができる。

これにより、探索済みの状態以降を再度探索することなく、ｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析が可能である。このため、例えばＯｐｅｎＦｌｏｗネットワーク環境を表す分散環境モデルに対するモデル検査において、ＤＰＯＲを適用する場合でも、探索済み状態以降の探索の打ち切りが可能になる。結果として、探索の効率化が実現される。

＜第４の実施の形態＞
次に、本発明の第４の実施の形態について図面を参照して詳細に説明する。以下では、前記第３の実施の形態と同様の部分は省略し、異なる部分についてのみ説明する。図２０は、本発明の第４の実施の形態の構成を示す図である。図２０を参照すると、本発明の第４の実施の形態における分散環境モデル用モデル検査装置４は、分散環境モデル探索部１１と、分散環境モデル依存関係解析部１２と、遅延遷移情報付与部１３と、探索済み状態管理部３４と、探索済み遷移履歴管理部３５と、探索済み状態遷移対応情報管理部３６と、検証情報雛形提供部４７と、を含む。分散環境モデル探索部１１は、分散環境モデル依存関係解析部１２、遅延遷移情報付与部１３、探索済み状態管理部３４、探索済み遷移履歴管理部３５、探索済み状態遷移対応情報管理部３６、検証情報雛形提供部４７のそれぞれと、情報をやり取りするように構成されている。探索済み状態遷移対応情報管理部３６は、探索済み状態管理部３４が管理する探索済み状態と、探索済み遷移履歴管理部３５が管理する遷移と、を紐付けるため、その対応関係を管理する。また、分散環境モデル用モデル検査装置４は、ＬＳＩ（Large Scale Integration）等のハードウェア部品である回路部品を実装することにより、その動作をハードウェア的に実現することができる。あるいは、その機能を提供するプログラムを、図示しないソフトウェア記憶媒体に格納し、そのプログラムを主記憶部にロードしてＣＰＵにおいて実行することにより、ソフトウェア的に実現することも可能である。

検証情報雛形提供部４７は、ユーザが検証情報を入力する際、検証情報Ｄ１１に含まれるプロパティに対して典型的な雛形（Ｄ１１'）を提供する。さらに、検証情報雛形提供部４７は、ユーザが前記雛形を選択することで、それを前記プロパティの定義の一部又は全部に利用し、分散環境モデル探索部１１に入力することが可能な機能を備える。

次に、第４の実施形態の動作について説明する。ユーザは、図５のステップＳ１１において、検証情報Ｄ１１を作成する際、検証情報雛形提供部４７から所望の雛形をいくつか選択し、それらを用いて検証情報Ｄ１１を完成させ、分散環境モデル探索部１１に入力する。ただし、ユーザは、雛形を全く用いずに、検証情報Ｄ１１を作成してもよい。その他の動作は、本発明の第３の実施の形態と同様のため省略する。

次に、第４の実施形態の効果について説明する。ユーザが本発明の分散環境モデル用モデル検査装置を利用するにあたり、検証情報Ｄ１１を作成する負担を軽減することができるため、結果として検証全体の効率を向上させることができる。

本発明は、分散環境、例えばＯｐｅｎＦｌｏｗネットワーク環境を構築したり、その環境に変更を加える際に、それらの妥当性を検証するツール等に適用して好適とされる。ただし、適用は上記に制限されるものでない。

なお、上記の非特許文献の各開示を、本書に引用をもって繰り込むものとする。本発明の全開示（請求の範囲を含む）の枠内において、さらにその基本的技術思想に基づいて、実施の形態ないし実施例の変更・調整が可能である。また、本発明の請求の範囲の枠内において種々の開示要素（各請求項の各要素、各実施例の各要素、各図面の各要素等を含む）の多様な組み合わせ乃至選択が可能である。すなわち、本発明は、請求の範囲を含む全開示、技術的思想にしたがって当業者であればなし得るであろう各種変形、修正を含むことは勿論である。

特に制限されないが、上記した実施形態は以下のように付記される。
（付記１）
モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら、前記探索を行う分散環境モデル探索部と、
前記分散環境モデル探索部が探索したパス上の複数の遷移に関して依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成する分散環境モデル依存関係解析部と、
前記分散環境モデル依存関係解析部が生成した前記情報と前記解析結果に基づき、前記分散環境モデル探索部が行うバックトラック後の前記探索において、実行を後回しにすべき前記所定の遷移に関する情報を生成する遅延遷移情報付与部と、
を備える分散環境モデル用モデル検査装置。

（付記２）
前記分散環境モデル探索部は、前記モデル検査の対象として、ＯｐｅｎＦｌｏｗネットワーク環境を表す分散環境モデルの探索を行う、ことを特徴とする付記１に記載の分散環境モデル用モデル検査装置。

（付記３）
前記分散環境モデル探索部で探索した状態を探索済み状態として記憶管理する探索済み状態管理部と、
前記探索したパス上の遷移について前記遷移が行われた順序を、探索済みの遷移の履歴としてパス毎に区別して記憶管理する探索済み遷移履歴管理部と、
前記探索済み状態管理部が記憶保持する前記探索済みの状態と、前記探索済み遷移履歴管理部が保持する前記遷移との対応情報を管理する探索済み状態遷移対応情報管理部と、 を備え、
前記分散環境モデル探索部は、モデル検査により分散環境モデルを探索する際に、探索した状態と遷移をそれぞれ前記探索済み状態管理部と前記探索済み遷移履歴管理部に登録し、前記探索済み状態遷移対応情報管理部に登録した前記探索した状態と前記遷移の対応付けを行わせる、ことを特徴とする、付記１又は２に記載の分散環境モデル用モデル検査装置。

（付記４）
前記分散環境モデル探索部は、前記モデル検査の探索で到達した状態が、前記探索済み状態管理部で記憶管理されている探索済みの状態である場合、前記探索済み状態遷移対応情報管理部及び前記探索済み遷移履歴管理部を参照し、前記探索済みの状態から行われた探索済みの遷移の履歴情報を取得し、
前記探索済みの状態以降の遷移は前記履歴情報と同様の遷移を行ったとみなしたパスを生成し、
前記分散環境モデル依存関係解析部は、前記履歴情報と同様の遷移を行ったとみなしたパスに基づき、遷移の依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する、ことを特徴とする、付記３に記載の分散環境モデル用モデル検査装置。

（付記５）
前記分散環境モデル探索部は、前記分散環境モデル用モデル検査装置により検証するプロパティを受け付ける手段を備える、ことを特徴とする付記１乃至４のいずれか１に記載の分散環境モデル用モデル検査装置。

（付記６）
前記プロパティを入力する際に、前記プロパティの少なくとも一部について典型的な雛形を提供する検証情報雛形提供部を備えていることを特徴とする付記５に記載の分散環境モデル用モデル検査装置。

（付記７）
実行を後回しにすべき前記所定の遷移として、以前の探索で検出された、依存関係のある遷移のペアのうち先に行われた遷移を、バックトラック後の探索では、後回しにする、ことを特徴とする付記１乃至６のいずれか１に記載の分散環境モデル用モデル検査装置。

（付記８）
モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら前記探索を行い、
前記探索したパス上の複数の遷移に関して、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成し、
前記解析結果と前記生成された情報に基づき、前記分散環境モデルのバックトラック後の探索にあたり、実行を後回しにすべき前記所定の遷移に関する情報を生成する、分散環境モデル用モデル検査方法。

（付記９）
前記分散環境モデルのモデル検査で探索した状態を探索済み状態として第１の記憶部で記憶管理し、
前記探索したパス上の遷移について前記遷移が行われた順序を、探索済みの遷移の履歴としてパス毎に区別した形態で、第２の記憶部で記憶管理し、
前記探索済みの状態と、探索済みの遷移との対応情報を第３の記憶部で記憶管理することを特徴とする、付記８に記載の分散環境モデル用モデル検査方法。

（付記１０）
前記分散環境モデルのモデル検査において、探索で到達した状態が、前記第１の記憶部で記憶管理されている前記探索済みの状態である場合、前記第２及び第３の記憶部を参照して、探索済みの状態から行われた探索済みの遷移の履歴情報を取得し、
前記探索済みの状態以降の遷移は前記履歴情報と同様の遷移を行ったとみなしたパスを生成し、
前記履歴情報と同様の遷移を行ったとみなしたパスに基づき、遷移の依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する、ことを特徴とする、付記９に記載の分散環境モデル用モデル検査方法。

（付記１１）
検証するプロパティを入力する、ことを特徴とする付記８又は９に記載の分散環境モデル用モデル検査方法。

（付記１２）
前記プロパティの少なくとも一部について典型的な雛形を提供する、ことを特徴とする付記８又は９に記載の分散環境モデル用モデル検査方法。

（付記１３）
実行を後回しにすべき前記所定の遷移として、以前の探索で検出された、依存関係のある遷移のペアのうち先に行われた遷移を、バックトラック後の探索では、後回しにする、ことを特徴とする付記８乃至１２のいずれか１に記載の分散環境モデル用モデル検査方法。

（付記１４）
モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら、前記探索を行う分散環境モデル探索処理と、
前記分散環境モデル探索処理が探索したパス上の複数の遷移に関して、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成する分散環境モデル依存関係解析処理と、
前記分散環境モデル依存関係解析処理が生成した情報と前記解析結果に基づき、前記分散環境モデル探索部が行うバックトラック後の前記探索において、実行を後回しにすべき前記所定の遷移に関する情報を生成する遅延遷移情報付与処理と、
をコンピュータに実行させるプログラム。

（付記１５）
前記分散環境モデル探索処理は、前記モデル検査の対象として、ＯｐｅｎＦｌｏｗネットワーク環境を表す分散環境モデルの探索を行う、ことを特徴とする付記１４に記載のプログラム。

（付記１６）
前記分散環境モデル探索処理で探索した状態を探索済み状態として記憶管理する探索済み状態管理処理と、
前記探索したパス上の遷移について前記遷移が行われた順序を、探索済みの遷移の履歴としてパス毎に区別して記憶管理する探索済み遷移履歴管理処理と、
前記探索済み状態管理処理が記憶保持する前記探索済みの状態と、前記探索済み遷移履歴管理処理が保持する前記遷移との対応情報を管理する探索済み状態遷移対応情報管理処理と、
を備え、
前記分散環境モデル探索処理は、モデル検査により分散環境モデルを探索する際に、探索した状態と遷移をそれぞれ前記探索済み状態管理処理と前記探索済み遷移履歴管理処理に登録し、前記探索済み状態遷移対応情報管理処理に登録した前記探索した状態と前記遷移の対応付けを行わせる、ことを特徴とする、付記１４又は１５に記載のプログラム。

（付記１７）
前記分散環境モデル探索処理は、前記モデル検査の探索で到達した状態が、前記探索済み状態管理処理で記憶管理されている探索済みの状態である場合、前記探索済み状態遷移対応情報管理処理及び前記探索済み遷移履歴管理処理を参照し、前記探索済みの状態から行われた探索済みの遷移の履歴情報を取得し、
前記探索済みの状態以降の遷移は前記履歴情報と同様の遷移を行ったとみなしたパスを生成し、
前記分散環境モデル依存関係解析処理は、前記履歴情報と同様の遷移を行ったとみなしたパスに基づき、遷移の依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する、ことを特徴とする、付記１６に記載のプログラム。

（付記１８）
前記分散環境モデル探索処理は、検証するプロパティを受け付ける、ことを特徴とする付記１４乃至１７のいずれか１に記載のプログラム。

（付記１９）
前記プロパティを入力する際に、前記プロパティの少なくとも一部について典型的な雛形を提供する検証情報雛形提供処理を含むことを特徴とする付記１７に記載のプログラム。

（付記２０）
実行を後回しにすべき前記所定の遷移として、以前の探索で検出された、依存関係のある遷移のペアのうち先に行われた遷移を、バックトラック後の探索では、後回しにする、ことを特徴とする付記１４乃至１９のいずれか１に記載のプログラム。

以上、上述した実施形態を模範的な例として本発明を説明した。しかしながら、本発明は、上述した実施形態には限定されない。即ち、本発明は、本発明のスコープ内において、当業者が理解し得る様々な態様を適用することができる。

この出願は、２０１４年４月１８日に出願された日本出願特願２０１４−０８６６４３を基礎とする優先権を主張し、その開示の全てをここに取り込む。

１ 分散環境モデル用モデル検査装置
１１ 分散環境モデル探索部
１２ 分散環境モデル依存関係解析部
１３ 遅延遷移情報付与部
２１ 入力装置
２２ 出力装置
２３ 記憶装置
３ 分散環境モデル用モデル検査装置
３４ 探索済み状態管理部
３５ 探索済み遷移履歴管理部
３６ 探索済み状態遷移対応情報管理部
４ 分散環境モデル用モデル検査装置
４７ 検証情報雛形提供部

Claims (10)

1. モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら、前記探索を行う分散環境モデル探索手段と、
   前記分散環境モデル探索手段が探索したパス上の複数の遷移に関して依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成する分散環境モデル依存関係解析手段と、
   少なくとも前記分散環境モデル依存関係解析手段が生成した前記情報に基づき、前記分散環境モデル探索手段が行うバックトラック後の前記探索において、実行を後回しにすべき前記所定の遷移に関する情報を生成する遅延遷移情報付与手段と、
   を備える分散環境モデル用モデル検査装置。
2. 前記分散環境モデル探索手段は、前記モデル検査の対象として、ＯｐｅｎＦｌｏｗネットワーク環境を表す分散環境モデルの探索を行う、ことを特徴とする請求項１に記載の分散環境モデル用モデル検査装置。
3. 前記分散環境モデル探索手段で探索した状態を探索済み状態として記憶管理する探索済み状態管理手段と、
   前記探索したパス上の遷移について前記遷移が行われた順序を、探索済みの遷移の履歴としてパス毎に区別して記憶管理する探索済み遷移履歴管理手段と、
   前記探索済み状態管理手段が記憶保持する前記探索済みの状態と、前記探索済み遷移履歴管理手段が保持する前記遷移との対応情報を管理する探索済み状態遷移対応情報管理手段と、 を備え、
   前記分散環境モデル探索手段は、モデル検査により分散環境モデルを探索する際に、探索した状態と遷移をそれぞれ前記探索済み状態管理手段と前記探索済み遷移履歴管理手段に登録し、前記探索済み状態遷移対応情報管理手段に登録した前記探索した状態と前記遷移の対応付けを行わせる、ことを特徴とする、請求項１又は２に記載の分散環境モデル用モデル検査装置。
4. 前記分散環境モデル探索手段は、前記モデル検査の探索で到達した状態が、前記探索済み状態管理手段で記憶管理されている探索済みの状態である場合、前記探索済み状態遷移対応情報管理手段及び前記探索済み遷移履歴管理手段を参照し、前記探索済みの状態から行われた探索済みの遷移の履歴情報を取得し、
   前記探索済みの状態以降の遷移は前記履歴情報と同様の遷移を行ったとみなしたパスを生成し、
   前記分散環境モデル依存関係解析手段は、前記履歴情報と同様の遷移を行ったとみなしたパスに基づき、遷移の依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する、ことを特徴とする、請求項３に記載の分散環境モデル用モデル検査装置。
5. 前記分散環境モデル探索手段は、前記分散環境モデル用モデル検査装置により検証するプロパティを受け付ける手段を備える、ことを特徴とする請求項１乃至４のいずれか１項に記載の分散環境モデル用モデル検査装置。
6. 前記プロパティを入力する際に、前記プロパティの少なくとも一部について典型的な雛形を提供する検証情報雛形提供手段を備えていることを特徴とする請求項５に記載の分散環境モデル用モデル検査装置。
7. モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら前記探索を行い、
   前記探索したパス上の複数の遷移に関して、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成し、
   少なくとも前記生成された情報に基づき、前記分散環境モデルのバックトラック後の探索にあたり、実行を後回しにすべき前記所定の遷移に関する情報を生成する、分散環境モデル用モデル検査方法。
8. 前記分散環境モデルのモデル検査で探索した状態を探索済み状態として第１の記憶手段で記憶管理し、
   前記探索したパス上の遷移について前記遷移が行われた順序を、探索済みの遷移の履歴としてパス毎に区別した形態で、第２の記憶手段で記憶管理し、
   前記探索済みの状態と、探索済みの遷移との対応情報を第３の記憶手段で記憶管理し、
   前記分散環境モデルのモデル検査において、探索で到達した状態が、前記第１の記憶手段で記憶管理されている前記探索済みの状態である場合、前記第２及び第３の記憶手段を参照して、探索済みの状態から行われた探索済みの遷移の履歴情報を取得し、
   前記探索済みの状態以降の遷移は前記履歴情報と同様の遷移を行ったとみなしたパスを生成し、
   前記履歴情報と同様の遷移を行ったとみなしたパスに基づき、遷移の依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係を解析する、ことを特徴とする、請求項７に記載の分散環境モデル用モデル検査方法。
9. 検証するプロパティを入力するか、又は、
   前記プロパティの少なくとも一部について典型的な雛形を提供する、ことを特徴とする請求項７又は８に記載の分散環境モデル用モデル検査方法。
10. モデル検査により分散環境モデルを探索する際に、所定の遷移に関して実行を後回しにするか否か判断しながら、前記探索を行う分散環境モデル探索処理と、
    前記分散環境モデル探索処理が探索したパス上の複数の遷移に関して、依存関係とｈａｐｐｅｎｓ−ｂｅｆｏｒｅ関係の解析を行い、前記パスに対するバックトラックに関する情報を生成する分散環境モデル依存関係解析処理と、
    少なくとも前記分散環境モデル依存関係解析処理が生成した情報に基づき、前記分散環境モデル探索処理が行うバックトラック後の前記探索において、実行を後回しにすべき前記所定の遷移に関する情報を生成する遅延遷移情報付与処理と、
    をコンピュータに実行させるプログラム。

Images