(57)【要約】【課題】変数選択のランダム性に変化を与えずに探索領域を低減することができるモデル検査装置を提供することを課題とする。【解決手段】モデル検査を行う検査対象および検査項目がＣＮＦ変換されたＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索するモデル検査装置において、ランダムに選定された独立変数、および、当該独立変数と当該独立変数以外の依存変数との関係式を用いて、ＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する。【選択図】図３
2010231289.tif 000002
【特許請求の範囲】
【請求項１】
モデル検査を行う検査対象および検査項目がＣＮＦ変換されたＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する探索手段を少なくとも備えたモデル検査装置において、
前記探索手段は、
ランダムに選定された独立変数、および、当該独立変数と当該独立変数以外の依存変数との関係式を用いて、前記ＣＮＦ式を真にする前記２進変数の組み合わせを網羅的に探索することを特徴とする、モデル検査装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査装置に関する。
【背景技術】
【０００２】
近年、ソフトウェアの網羅的な検査手法として形式検証への関心が高まっている。従来のモデル検査手法（形式検査手法）は、図１に示すように、ソフトウェアを２進変数から構成されたＢｏｏｌｅａｎ演算式の一種であるＣＮＦ（Ｃｏｎｊｕｎｃｔｉｖｅ  Ｎｏｒｍａｌ  Ｆｏｒｍ）に置き換え、そのブール演算式を真（ＴＲＵＥ）にする２進変数の組み合わせの存在性を主にランダム探索手法を用いて証明している。
【０００３】
しかし、従来のモデル検査手法では、ランダム探索手法を用いて各２進変数をランダム的に割り振ることで非常に早い時間でブール演算式を真（ＴＲＵＥ）にする２進変数の組み合わせを見つけていたものの、近年、システムの大規模化に伴い、２進変数の数が数百万ある場合など、いかにランダム探索領域数を低減するかが重要となってきており、ランダム探索領域を低減する手法の開発が望まれていた。
【０００４】
そこで、ランダム探索領域を低減する技術として、特許文献１および特許文献２が開示されている。
【０００５】
例えば、特許文献１に記載のクロス検証装置では、マップにおける各軸の代表点の数だけ繰り返さず、軸の比較や補間に必要な２進変数の数を効果的に減らしている。具体的には、動作仕様ならびにＣコードおよびＧＵＩロジックに含まれる変数を論理ゲートを用いて並列的に２進変数へ変換し、２進変数へ変換した後の動作仕様ならびにＣコードおよびＧＵＩロジックを例えばＴｓｅｉｔｉｎ手法でＣＮＦへ変換することにより、エンジンの制御ソフトウェアの開発における当該ソフトウェアのＣＮＦへの変換（具体的には、マップ変数のＣＮＦへの変換）の計算量を減らして効率よく行っている。
【０００６】
また、特許文献２に記載の形式検証システムでは、システムが大きくなると形式検証システムの探索領域が膨大になり、実時間内に検査ができなくなっていたが、２つの順序回路（内部状態を持つ回路）の等価性を判断することにより、回路の等価性を効率よく検証している。
【０００７】
一例として、従来の一般的なランダム探索領域を低減するプログラム（ＳａｔＥｌｉｔｅ，２００５，ｈｔｔｐ：／／ｍｉｎｉｓａｔ．ｓｅ／ＳａｔＥＬｉｔｅ．ｈｔｍｌ）を用いてＣＮＦ式を観察することにより、変数同士の関係式を見つける場合を説明する。例えば、下記の数式１に示すＣＮＦ式の中で、次のようなパターン（下線部分）がある場合、数式１の下線部分は、「ｘ１」，「ｘ２」，「ｙ」の変数同士に下記の数式２に示す関係があることを示している。
【数１】
2010231289.tif 000003
ｙ＝ｘ１∨ｘ２  （数式２）
そこで、上記数式１に示すＣＮＦ式から「ｙ」の代わりに（ｘ１∨ｘ２）を代入することで、解かなければならない変数を「３」から「２」に減らすことにより、ランダム探索領域の数を低減している。
【先行技術文献】
【特許文献】
【０００８】
【特許文献１】特開２００８−２７６５５６号公報
【特許文献２】特開平０９−１２８４３１号公報
【発明の概要】
【発明が解決しようとする課題】
【０００９】
しかしながら、従来技術では、変数選択のランダム性に変化を与えずに探索領域を低減することができないという問題点を有していた。例えば、従来技術においては、変数同士の依存関係「ｙ＝ｆ（ｘ）」を検出した場合、強制的に「ｙ」を削除して探索領域を低減していたが、ランダムな変数の数をコントロールするものではないため、この場合、探索のランダム性（先に探索する変数選択のランダム性）に変化を与えてしまい、問題によっては解きにくくなるという問題点を有していた。
【００１０】
すなわち、従来技術においては、図２に示すように、ＣＮＦ式を真（ＴＲＵＥ）にする２進変数の組み合わせを探索するＳＡＴソルバーが、各２進変数をランダム的に割り振ることで非常に早い時間で組み合わせを見つけることができるものの、人為的に「ｙ」を削除しているため、ランダム性に変化を与えており、それが原因になり問題によってはＣＮＦを解きにくくしてしまうという問題点を有していた。
【００１１】
本発明は、上記問題点に鑑みてなされたもので、変数選択のランダム性に変化を与えずに探索領域を低減することができるモデル検査装置を提供することを目的とする。
【課題を解決するための手段】
【００１２】
このような目的を達成するため、本発明に係るモデル検査装置は、モデル検査を行う検査対象および検査項目がＣＮＦ変換されたＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する探索手段を少なくとも備えたモデル検査装置において、前記探索手段は、ランダムに選定された独立変数、および、当該独立変数と当該独立変数以外の依存変数との関係式を用いて、前記ＣＮＦ式を真にする前記２進変数の組み合わせを網羅的に探索することを特徴とする。
【発明の効果】
【００１３】
この発明によれば、変数選択のランダム性に変化を与えずに探索領域を低減することができるという効果を奏する。
【図面の簡単な説明】
【００１４】
【図１】図１は、従来の形式検査手法の一例を示す図である。
【図２】図２は、従来手法の問題点の一例を示す図である。
【図３】図３は、モデル検査装置１０の構成の一例を示すブロック図である。
【図４】図４は、論理ゲートの一例を示す図である。
【図５】図５は、真理テーブルの一例を示す図である。
【図６】図６は、真理テーブルの一例を示す図である。
【図７】図７は、モデル検査を行う検査対象および検査項目の一例を示す図である。
【図８】図８は、モデル検査装置１０の実施例を示す図である。
【図９】図９は、モデル検査装置１０の実施例を示す図である。
【図１０】図１０は、従来手法で解を見つける確率の一例を説明する図である。
【図１１】図１１は、本発明で解を見つける確率の一例を説明する図である。
【発明を実施するための形態】
【００１５】
以下に、本発明にかかるモデル検査装置の実施の形態を図面に基づいて詳細に説明する。なお、この実施の形態によりこの発明が限定されるものではない。
【００１６】
［１．本実施の形態の構成］
まず、本実施の形態にかかるモデル検査装置１０の構成について、図３を参照して説明する。ここで、図３は、モデル検査装置１０の構成の一例を示すブロック図であり、該構成のうち本発明に関係する部分のみを概念的に示している。
【００１７】
図３において、モデル検査装置１０は、入力部１２と、テーブル作成部１４と、変換部１６と、探索部１８と、出力部２０と、を備えて構成されており、これら各部は任意の通信路を介して通信可能に接続されている。
【００１８】
このうち、入力部１２は、ＣＮＦ化された問題・検査項目をユーザにより入力させる入力装置である。具体的には、入力部１２は、モデル検査を行う検査対象および検査項目をＣＮＦ変換したＣＮＦ式を入力させる。ここで、ＣＮＦ化は、モデル検査を行う検査対象および検査項目をＣＮＦ式に変換する既存のＣＮＦ変換手段により行われる。
【００１９】
また、テーブル作成部１４は、ＣＮＦを分析し、ｙ＝ｆ（ｘ）等の変数同士の依存関係を分析し、テーブル化するテーブル作成手段である。具体的には、テーブル作成部１４は、入力部１２により入力されたＣＮＦ式に基づいて、検査対象ごとに検査項目となる独立変数と依存変数を含む変数の依存関係を示す関係式を抽出し、当該関係式に基づいて２進変数の組み合わせを示すテーブルを作成する。
【００２０】
ここで、独立変数とは、変数のうち独立的に割り振ることができる変数を意味する。また、依存変数とは、変数のうち独立変数以外の残りの変数を意味する。
【００２１】
また、変換部１６は、後述する探索部１８がランダムに解（ＣＮＦ式を真にする２進変数の組み合わせ）を探索する際、割り振られた独立変数を用いて、テーブル作成部１４により作成されたテーブルから依存変数の変数値（２進変数）を探し変換する変換手段である。具体的には、変換部１６は、ランダムに選定された独立変数以外の依存変数を、テーブル作成部１４により作成されたテーブルを参照することにより探索し、当該依存変数の変数値となる２進変数に変換する。
【００２２】
また、探索部１８は、本発明における探索手段に相当するものであり、ＣＮＦ変換されたＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索し、探索の際、ＣＮＦ式中の２進変数をランダムに割り振るランダム探索器である。本発明において、探索部１８は、変数（独立変数と依存変数）同士が依存関係を持つ場合、独立変数をランダムに選定し、独立変数以外の残りの依存変数は変換部１６を用いてテーブルから取得するメカニズムを用いている。具体的には、探索部１８は、ランダムに選定された独立変数、および、当該独立変数と当該独立変数以外の依存変数との関係式を用いて、ＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する。より具体的には、探索部１８は、ランダムに選定された独立変数の変数値となる２進変数と、変換部１６により変換された依存変数の変数値となる２進変数とを用いて、入力部１２により入力されたＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する。このように、探索部１８は、ＣＮＦ式を観察し、変数（独立変数および依存変数）同士の関係式を見つけた際、それらの変数から独立的に割り振ることができる独立変数を選び、この独立変数の変数値（２進変数）をランダムに割り振り、依存変数の変数値（２進変数）は変換部１６によりテーブルから取得する。
【００２３】
また、出力部２０は、求めた解（ＣＮＦ式を真にする２進変数の組み合わせ）をユーザに提示する出力装置である。具体的には、出力部２０は、探索部１８により探索された、検査対象および検索項目に対応付けられた２進変数の組み合わせを少なくとも含む探索結果を出力させる。
【００２４】
［２．本実施の形態の処理］
つぎに、モデル検査装置１０で実行するモデル検査処理の一例を図４から図６を参照して説明する。図４は、論理ゲートの一例を示す図である。図５および図６は、真理テーブルの一例を示す図である。
【００２５】
まず、入力部１２は、モデル検査を行う検査対象および検査項目をＣＮＦ変換したＣＮＦ式をユーザに入力させる。ここで、一例として、下記の数式３に示すＣＮＦ式が入力されるとする。
【数２】
2010231289.tif 000004
【００２６】
そして、テーブル作成部１４は、入力部１２により入力されたＣＮＦ式に基づいて、検査対象ごとに検査項目となる独立変数と依存変数を含む変数の依存関係を示す関係式（ｙ＝ｘ１∨ｘ２）を抽出する。上記数式３の場合、下線部分では、図４の論理ゲートに示すように、「ｘ１」，「ｘ２」，「ｙ」がＯＲ関係にあり、「ｙ＝ｘ１∨ｘ２」の関係式が成立する。そして、テーブル作成部１４は、当該関係式に基づいて、図５に示すような２進変数の組み合わせを示すテーブル（真理表）を作成する。
【００２７】
そして、変換部１６は、探索部１８によりランダムに選定される独立変数（例えば、図５において、「ｘ１」，「ｘ２」）以外の依存変数（例えば、図５において、「ｙ」）を、テーブル作成部１４により作成されたテーブルを参照することにより探索し、当該依存変数の変数値となる２進変数（図５において、「Ｆ」または「Ｔ」のいずれか）に変換する。
【００２８】
そして、探索部１８は、ＣＮＦ式を真にする変数「ｘ１」，「ｘ２」，「ｙ」をランダムに探索する。探索の際、いずれか２つの変数を先に探索し、残りの１個の変数はＣＮＦ式を参照して決める。すなわち、探索部１８は、変数「ｘ１」，「ｘ２」，「ｙ」のうちいずれかの２つの変数（独立変数）をランダム的に割り振った後、残りの１個の変数（依存変数）はランダム的に割り振るのではなく、変換部１６にて、テーブル作成部１４により作成された関係式を表すテーブルを参照してその変数値（依存変数の２進変数）を取得する。
【００２９】
例えば、図６に示すように、「ｘ１」，「ｙ」（独立変数）が先に割り振られた場合、変換部１６によりテーブルから返される「ｘ２」（依存変数）の変数値は、「ＦまたはＴまたは＊」のいずれか（依存変数の２進変数）になる。図６において、「不存在」は、上記数式３を満たさない（Ｔｒｕｅにならない）ことを意味し、図６では、このような「ｘ１」，「ｙ」の組み合わせは探索空間から外している。また、「＊」は、「ｄｏｎ’ｔ  ｃａｒｅ」を意味し、ＴｒｕｅまたはＦａｌｓｅのどちらでもよいことを意味する。
【００３０】
このように、探索部１８は、ランダムに選定された独立変数、および、当該独立変数と当該独立変数以外の依存変数との関係式を用いて、ＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する。具体的には、探索部１８は、ランダムに選定された独立変数の変数値となる２進変数と、変換部１６により変換された依存変数の変数値となる２進変数とを用いて、入力部１２により入力されたＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する。
【００３１】
そして、出力部２０は、探索部１８により探索された、検査対象および検索項目に対応付けられた２進変数の組み合わせを少なくとも含む探索結果を出力させる。
【００３２】
以上の方法で、本発明のモデル検査装置１０は、変数選択のランダム性に変化を与えることなく、ランダム探索領域数を低減することができる。
【００３３】
［３．実施例］
続いて、本モデル検査装置１０における実施例を図７から図１１を参照して説明する。図７は、モデル検査を行う検査対象および検査項目の一例を示す図である。図８および図９は、モデル検査装置１０の実施例を示す図である。図１０は、従来手法で解を見つける確率の一例を説明する図である。図１１は、本発明で解を見つける確率の一例を説明する図である。
【００３４】
本実施例においては、図７に示す例題についてモデル検査処理を行う例を説明する。図７において、「Ｓｕｂ  ｓｙｓｔｅｍ１，Ｓｕｂ  ｓｙｓｔｅｍ２，Ｓｕｂ  ｓｙｓｔｅｍ３」から構成されるソフトウェアを検査対象とし、「Ｐｏｒｔ１，Ｐｏｒｔ２，ｘ１，ｘ２，ｙ」を検査項目とする。ここで、Ｓｕｂ  ｓｙｓｔｅｍ１は、前提条件１（Ｓｕｂ  ｓｙｓｔｅｍ２の外部制約条件１）として、Ｓｕｂ  ｓｙｓｔｅｍ１が正常であるためには「Ｐｏｒｔ１」は「Ｔ」で、「Ｐｏｒｔ２」は「Ｆ」でなければならない。また、Ｓｕｂ  ｓｙｓｔｅｍ３は、前提条件２（Ｓｕｂ  ｓｙｓｔｅｍ２の外部制約条件２）として、Ｓｕｂ  ｓｙｓｔｅｍ３が正常であるためには「Ｐｏｒｔ１」，「Ｐｏｒｔ２」は共に「Ｔ」でなければならない。したがって、Ｓｕｂ  ｓｙｓｔｅｍ２の課題として、Ｓｕｂ  ｓｙｓｔｅｍ１，Ｓｕｂ  ｓｙｓｔｅｍ３の両方が正常であるための「ｘ１」，「ｘ２」，「ｙ」を見つけなければならない。
【００３５】
まず、入力部１２は、モデル検査を行う検査対象（例えば、Ｓｕｂ  ｓｙｓｔｅｍ１，Ｓｕｂ  ｓｙｓｔｅｍ２，Ｓｕｂ  ｓｙｓｔｅｍ３等）および検査項目（例えば、「ｘ１」，「ｘ２」，「ｙ」等）をＣＮＦ変換したＣＮＦ式（図８に示すＣＮＦ式）を入力させる。図８に示すように、Ｓｕｂ  ｓｙｓｔｅｍ２の詳細なＣＮＦ式は、｛（¬ｙ∨ｘ１∨ｘ２）∧（ｙ∨¬ｘ１）∧（ｙ∨¬ｘ２）｝と表現される。なお、図８において、全ｓｙｓｔｅｍ（Ｓｕｂ  ｓｙｓｔｅｍ１，Ｓｕｂ  ｓｙｓｔｅｍ２，Ｓｕｂ  ｓｙｓｔｅｍ３）のＣＮＦ式のうち、Ｓｕｂ  ｓｙｓｔｅｍ１およびＳｕｂ  ｓｙｓｔｅｍ３の詳細なＣＮＦ式は省略している。以下、Ｓｕｂ  ｓｙｓｔｅｍ２のＣＮＦ式に注目し説明する。
【００３６】
そして、テーブル作成部１４は、入力部１２により入力されたＣＮＦ式（図８に示す全ｓｙｓｔｅｍのＣＮＦ式）に基づいて、検査対象（図９において、Ｓｕｂ  ｓｙｓｔｅｍ２）ごとに検査項目となる独立変数（図９において、「ｘ１」，「ｘ２」）と依存変数（（図９において、「ｙ」）を含む変数の依存関係を示す関係式（図９において、「ｙ＝ｘ１∨ｘ２」）を抽出する。そして、テーブル作成部１４は、当該関係式に基づいて、図９のＴ１に示すような２進変数の組み合わせを示すテーブル（真理表）を作成する。ここで、図９のＴ１のテーブルにおいて、独立変数「ｘ１」の２進変数は上から順に「Ｆ，Ｆ，Ｔ，Ｔ」、独立変数「ｘ２」の２進変数は上から順に「Ｆ，Ｔ，Ｆ，Ｔ」であり、依存変数「ｙ」の２進変数は上から順に「Ｆ，Ｔ，Ｔ，Ｔ」となる。
【００３７】
そして、変換部１６は、探索部１８によりランダムに選定された独立変数（独立的に割り振られた変数）以外の依存変数を、テーブル作成部１４により作成されたテーブルを参照することにより探索し、当該依存変数の変数値となる２進変数（テーブルから取得する依存変数値）に変換する。ここで、図９において、独立変数として「ｘ１」，「ｘ２」が選定された場合の依存変数「ｙ」のｙ値変換テーブル（図９のＴ２のテーブル）と、独立変数として「ｘ１」，「ｙ」が選定された場合の依存変数「ｘ２」のｘ２値変換テーブル（図９のＴ３のテーブル）と、独立変数として「ｘ２」，「ｙ」が選定された場合の依存変数「ｘ１」のｘ１値変換テーブル（図９のＴ４のテーブル）が示される。
【００３８】
ここで、図９のＴ２のｙ値テーブルは、図９のＴ１のテーブルに対応する。また、図９のＴ３のｘ２値テーブルにおいて、独立変数「ｘ１」の２進変数は上から順に「Ｆ，Ｆ，Ｔ，Ｔ」、独立変数「ｙ」の２進変数は上から順に「Ｆ，Ｔ，Ｆ，Ｔ」であり、依存変数「ｘ２」の２進変数は上から順に「Ｆ，Ｔ，不存在，＊」となる。図９のＴ４のｘ１値テーブルにおいて、独立変数「ｘ２」の２進変数は上から順に「Ｆ，Ｆ，Ｔ，Ｔ」、独立変数「ｙ」の２進変数は上から順に「Ｆ，Ｔ，Ｆ，Ｔ」であり、依存変数「ｘ１」の２進変数は上から順に「Ｆ，Ｔ，不存在，＊」となる。なお、図９において、「不存在」は、図８に示したＣＮＦ式を満たさない（Ｔｒｕｅにならない）ことを意味し、「＊」は、ＴｒｕｅまたはＦａｌｓｅのどちらでもよいことを意味する。
【００３９】
そして、探索部１８は、ランダムに選定された独立変数（図９のＴ２のテーブルにおいて、「ｘ１」，「ｘ２」）、および、当該独立変数と当該独立変数以外の依存変数（図９のＴ２のテーブルにおいて、「ｙ」）との関係式（図９にＴ２のテーブルおいて、「ｙ＝ｘ１∨ｘ２」）を用いて、ＣＮＦ式（図８に示す、Ｓｕｂ  ｓｙｓｔｅｍ２の詳細のＣＮＦ式）を真にする２進変数の組み合わせを網羅的に探索する。具体的には、探索部１８は、ランダムに選定された独立変数の変数値となる２進変数（図９のＴ２のテーブルにおいて、「Ｆ」または「Ｔ」のいずれか）と、変換部１６により変換された依存変数の変数値となる２進変数（図９のＴ２のテーブルにおいて、「Ｆ」または「Ｔ」のいずれか）とを用いて、入力部１２により入力されたＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する。
【００４０】
そして、出力部２０は、図９のＴ５のテーブルに示すように、探索部１８により探索された、検査対象（Ｓｕｂ  ｓｙｓｔｅｍ１，Ｓｕｂ  ｓｙｓｔｅｍ２，Ｓｕｂ  ｓｙｓｔｅｍ３）および検索項目（Ｐｏｒｔ１，Ｐｏｒｔ２，ｘ１，ｘ２，ｙ）に対応付けられた２進変数の組み合わせを少なくとも含む探索結果（求めた解：ＣＮＦ式を真にする２進変数の組み合わせ）を出力させる。
【００４１】
このように、本実施例におけるモデル検査装置１０は、モデル検査において、変数選択のランダム性に変化を与えずに探索領域を低減することができるので、以下に示すように探索部１８が解（ＣＮＦ式を真にする２進変数の組み合わせ）を求める確率を従来手法よりも高くすることができる。
【００４２】
ここで、図１０および図１１を参照し、従来手法で解を見つける確率と、本発明で解を見つける確率とを比較して説明する。
【００４３】
図１０に示すように、従来の探索部は、ＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索することで、変数「ｘ１」，「ｘ２」，「ｙ」のうちの「ｘ１」，「ｘ２」を割り振り、Ｓｕｂ  ｓｙｓｔｅｍ２が正常でありながら、外部制約条件１と外部制約条件２（Ｓｕｂ  ｓｙｓｔｅｍ１とＳｕｂ  ｓｙｓｔｅｍ３の各ポートの条件）を満たす「ｘ１」と「ｘ２」の組み合わせを見つける。
【００４４】
したがって、図１０のＴ１のテーブルに示すように、従来手法で解（組み合わせ）を見つける確率は、「１／４」となる。
【００４５】
一方、図１１に示すように、本発明の探索部１８は、ランダムに選定された独立変数、および、当該独立変数と当該独立変数以外の依存変数との関係式を用いて、ＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する。すなわち、探索部１８は、変数「ｘ１」，「ｘ２」，「ｙ」のうち２つの変数（独立変数）をランダムに選定し、残りの１個の変数（依存変数）はランダム的に割り振るのではなく、変換部１６にて、テーブル作成部１４により作成された関係式を表すテーブルを参照してその変数値（依存変数の２進変数）を取得する。図１１において、ｉ）「ｘ１」，「ｘ２」が選定された場合、ｉｉ）「ｘ１」，「ｙ」が選定された場合、ｉｉｉ）「ｘ２」，「ｙ」が選定された場合に分け、各パターンにおける解を探す確率を求める。そして、これらｉ）〜ｉｉｉ）の確率を合計することにより、本発明で解（組み合わせ）を見つける確率を求める。
【００４６】
まず、ｉ）「ｘ１」，「ｘ２」が選定された場合における解（組み合わせ）を見つける確率は、図１１のＴ２のテーブルに示すように、「ｘ１，ｘ２が選ばれる確率（１／３）×その際解が存在する確率（１／４）」として計算され、「１／１２」となる。
【００４７】
次に、ｉｉ）「ｘ１」，「ｙ」が選定された場合における解（組み合わせ）を見つける確率は、図１１のＴ３のテーブルに示すように、「ｘ１，ｙが選ばれる確率（１／３）×その際解が存在する確率（１／３）」として計算され、「１／９」となる。
【００４８】
次に、ｉｉｉ）「ｘ２」，「ｙ」が選定された場合における解（組み合わせ）を見つける確率は、図１１のＴ４のテーブルに示すように、「ｘ２，ｙが選ばれる確率（１／３）×その際解が存在する確率（１／３）」として計算され、「１／９」となる。
【００４９】
したがって、これらｉ）〜ｉｉｉ）の確率を合計すると（「１／１２」＋「１／９」＋「１／９」）、本発明で解（組み合わせ）を見つける確率は、「１１／３６」となる。
【００５０】
図１０において従来手法で解（組み合わせ）を見つける確率は、「１／４＝９／３６」であるため、図１１において本発明で解（組み合わせ）を見つける確率「１１／３６」と比較すると、本発明の探索部１８で解を求める確率のほうが高いことがわかる。なお、大規模システムの場合、確率の積み重ねにより従来手法と本発明との総確率の差はさらに大きくなる。
【００５１】
このように、本モデル検査装置１０は、従来手法に比べ高い確率で解（組み合わせ）を求めることができ、より早い時間で解を求めることができる。
【００５２】
［４．本実施の形態のまとめ、およびその他の実施の形態］
以上、詳細に説明したように、本実施の形態にかかるモデル検査装置１０によれば、モデル検査を行う検査対象および検査項目がＣＮＦ変換されたＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索するモデル検査装置１０において、ランダムに選定された独立変数、および、当該独立変数と当該独立変数以外の依存変数との関係式を用いて、ＣＮＦ式を真にする２進変数の組み合わせを網羅的に探索する。これにより、従来とは異なり、変数選択のランダム性に変化を与えずに探索領域を低減することができる。
【００５３】
さらに、本発明は、上述した実施の形態以外にも、特許請求の範囲の書類に記載した技術的思想の範囲内において種々の異なる実施の形態にて実施されてよいものである。例えば、本実施の形態において説明した各処理のうち、自動的に行なわれるものとして説明した処理の全部または一部を手動的に行うこともでき、あるいは、手動的に行なわれるものとして説明した処理の全部または一部を公知の方法で自動的に行うこともできる。また、この他、上記文書中や図面中で示した処理手順、制御手順、具体的名称、各種の情報、データベース構成については、特記する場合を除いて任意に変更することができる。
【００５４】
また、モデル検査装置１０の分散・統合の具体的形態は図示のものに限られず、その全部または一部を、各種の負荷等に応じた任意の単位で、機能的または物理的に分散・統合して構成することができる。例えば、各データベースを独立したデータベース装置として独立に構成してもよく、また、処理の一部をＣＧＩ（Ｃｏｍｍｏｎ  Ｇａｔｅｗａｙ  Ｉｎｔｅｒｆａｃｅ）を用いて実現してもよい。
【００５５】
また、図示の各構成要素は機能概念的なものであり、必ずしも物理的に図示の如く構成されていることを要しない。例えば、モデル検査装置１０に含まれる各装置またはその各部が備える処理機能については、その全部または任意の一部を、ＣＰＵおよび当該ＣＰＵにて解釈実行されるプログラムにて実現することができ、あるいはワイヤードロジックによるハードウェアとして実現することも可能である。なお、プログラムは、後述する記録媒体に記録されており、必要に応じて制御装置に機械的に読み取られる。
【００５６】
また、モデル検査装置１０に含まれる各装置におけるＲＯＭやＨＤなどの記憶装置には、ＯＳと協働してＣＰＵに命令を与え、各種処理を行うためのコンピュータプログラムが記録されている。このコンピュータプログラムは、ＲＡＭ等にロードされることによって実行され、クロス検証装置１０に含まれる各装置の機能をＣＰＵと協働して実現する。また、このコンピュータプログラムは、任意のネットワークを介して接続されたアプリケーションプログラムサーバに記録されてもよく、必要に応じてその全部または一部をダウンロードすることも可能である。
【００５７】
また、このプログラムを、コンピュータ読み取り可能な記録媒体に格納することもできる。ここで、「記録媒体」とは、フレキシブルディスク、光磁気ディスク、ＲＯＭ、ＥＰＲＯＭ、ＥＥＰＲＯＭ、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等の任意の「可搬用の物理媒体」や、各種コンピュータシステムに内蔵されるＲＯＭ、ＲＡＭ、ＨＤ等の任意の「固定用の物理媒体」、あるいは、ＬＡＮ、ＷＡＮ、インターネットに代表されるネットワークを介してプログラムを送信する場合の通信回線や搬送波のように、短期にプログラムを保持する「通信媒体」を含むものとする。「プログラム」とは、任意の言語や記述方法にて記述されたデータ処理方法であり、ソースコードやバイナリコード等の形式を問わない。なお、「プログラム」は必ずしも単一的に構成されるものに限られず、複数のモジュールやライブラリとして分散構成されるものや、ＯＳに代表される別個のプログラムと協働してその機能を達成するものをも含む。なお、本実施の形態に示した各装置において記録媒体を読み取るための具体的な構成、読み取り手順、あるいは、読み取り後のインストール手順等については、周知の構成や手順を用いることができる。
【産業上の利用可能性】
【００５８】
以上詳述に説明したように、本発明によれば、変数選択のランダム性に変化を与えずに探索領域を低減することができるモデル検査装置を提供することができるので、ソフトウェア分野において有用である。
【符号の説明】
【００５９】
１０  モデル検査装置
１２  入力部
１４  テーブル作成部
１６  変換部
１８  探索部
２０  出力部
【図１】
2010231289.tif 000005
【図２】
2010231289.tif 000006
【図３】
2010231289.tif 000007
【図４】
2010231289.tif 000008
【図５】
2010231289.tif 000009
【図６】
2010231289.tif 000010
【図７】
2010231289.tif 000011
【図８】
2010231289.tif 000012
【図９】
2010231289.tif 000013
【図１０】
2010231289.tif 000014
【図１１】
2010231289.tif 000015