"モデル検査において任意のテスト項目に対してプログラムのテストベクタを生成できない場合にテストベクタを生成できない要因を解析するプログラム解析装置であって、前記テストベクタを生成できないテスト項目を段階的に分解し、サブテスト項目を生成するサブテスト項目生成手段と、前記サブテスト項目生成手段でサブテスト項目を生成する毎に、該サブテスト項目に対してモデル検査を行い、該サブテスト項目に対するテストベクタを生成するモデル検査手段と、前記モデル検査手段でテストベクタを生成できない場合に該テストベクタを生成できないサブテスト項目に基づいてテストベクタを生成できない要因の箇所を特定する要因特定手段と、を備えることを特徴とするプログラム解析装置。前記モデル検査手段は、サブテスト項目をアサーションとして論理表現に変換し、サブテスト項目に対応する箇所にフラグを挿入してプログラムを加工し、該加工済みのプログラムとサブテスト項目に対応するアサーションをモデル検査にかけることを特徴とする請求項1に記載のプログラム解析装置。データベースを備え、前記モデル検査手段でテストベクタを生成できる場合に該テストベクタを生成できるサブテスト項目をデータベースに登録することを特徴とする請求項1又は請求項2に記載のプログラム解析装置。前記モデル検査手段でテストベクタを生成できない場合に該テストベクタを生成できないサブテスト項目を前記要因特定手段で特定した要因の箇所としてデータベースに登録することを特徴とする請求項3に記載のプログラム解析装置。モデル検査において任意のテスト項目に対してプログラムのテストベクタを生成できない場合にテストベクタを生成できない要因を解析するプログラム解析方法であって、前記テストベクタを生成できないテスト項目を段階的に分解し、サブテスト項目を生成するサブテスト項目生成ステップと、前記サブテスト項目生成ステップでサブテスト項目を生成する毎に、該サブテスト項目に対してモデル検査を行い、該サブテスト項目に対するテストベクタを生成するモデル検査ステップと、前記モデル検査ステップでテストベクタを生成できない場合に該テストベクタを生成できないサブテスト項目に基づいてテストベクタを生成できない要因の箇所を特定する要因特定ステップと、を含むことを特徴とするプログラム解析方法。モデル検査において任意のテスト項目に対してプログラムのテストベクタを生成できない場合にテストベクタを生成できない要因を解析するためのプログラム解析プログラムであって、コンピュータに、前記テストベクタを生成できないテスト項目を段階的に分解し、サブテスト項目を生成するサブテスト項目生成機能と、前記サブテスト項目生成機能でサブテスト項目を生成する毎に、該サブテスト項目に対してモデル検査を行い、該サブテスト項目に対するテストベクタを生成するモデル検査機能と、前記モデル検査機能でテストベクタを生成できない場合に該テストベクタを生成できないサブテスト項目に基づいてテストベクタを生成できない要因の箇所を特定する要因特定機能と、を実現させることを特徴とするプログラム解析プログラム。テスト項目をモデル検査にかけても、テストベクタを生成できない場合がある。このようにテストベクタが見つからないのは、テスト項目における分岐の切り替えの組み合わせの中に分岐の切り替え側に入れないものがあり例えば、ある分岐Aの切り替えとある分岐Bの切り替えとが論理的に衝突している、プログラム内の分岐の設定において論理的な矛盾論理的な不整合がある。そのようなプログラム内の矛盾要因箇所を特定しておく必要があるが、特定するためには人手でプログラムを解析する必要がある。しかし、この解析作業はプログラムが大きくなるほど困難な作業となり、大規模プログラムに対しては人手で解析を行うのは実質的に不可能である。そこで、本発明は、任意のテスト項目に対してテストベクタを生成できない場合にその要因箇所を自動的に特定するプログラム解析装置、プログラム解析方法及びプログラム解析プログラムを提供することを課題とする。本発明に係るプログラム解析装置は、モデル検査において任意のテスト項目に対してプログラムのテストベクタを生成できない場合にテストベクタを生成できない要因を解析するプログラム解析装置であって、テストベクタを生成できないテスト項目を段階的に分解し、サブテスト項目を生成するサブテスト項目生成手段と、サブテスト項目生成手段でサブテスト項目を生成する毎に、該サブテスト項目に対してモデル検査を行い、該サブテスト項目に対するテストベクタを生成するモデル検査手段と、モデル検査手段でテストベクタを生成できない場合に該テストベクタを生成できないサブテスト項目に基づいてテストベクタを生成できない要因の箇所を特定する要因特定手段とを備えることを特徴とする。テスト項目は、プログラム分岐を1つ以上含むプログラム内に存在する分岐の切り替えの組み合わせである。テストベクタは、テスト項目における分岐の切り替えの組み合わせを満たすテスト入力である。任意のテスト項目でテストベクタを生成できない場合、そのテスト項目における分岐の切り替えの組み合わせの中に分岐の切り替え側に入れないものが含まれている。そこで、プログラム解析装置では、テストベクタを生成できないテスト項目が入力されると、サブテスト項目生成手段によりそのテスト項目を段階的に分解してサブテスト項目を順次生成する。サブテスト項目は、テスト項目の分岐の切り替えの組み合わせを分解して一部を取り出し、テスト項目よりも条件を緩和したテスト項目である。プログラム解析装置では、サブテスト項目が生成される毎に、モデル検査手段によりそのサブテスト項目に対してモデル検査を行う。このモデル検査でサブテスト項目に対するテストベクタを生成できる場合、そのサブテスト項目の分岐の切り替えの組み合わせについては論理的な矛盾論理的な不整合がない。一方、テストベクタを生成できない場合、そのサブテスト項目の分岐の切り替えの組み合わせについては論理的な矛盾を含んでいる。そこで、プログラム解析装置では、モデル検査手段でテストベクタを生成できない場合、要因特定手段によりそのテストベクタを生成できないサブテスト項目に基づいてテストベクタを生成できない要因の箇所を特定する。このように、プログラム解析装置は、任意のテスト項目に対してテストベクタを生成できない場合に、その任意のテスト項目よりも条件を緩和したサブテスト項目に対してモデル検査を繰り返し行い、テストベクタを生成できないサブテスト項目を探索することにより、プログラム内の論理的な矛盾要因箇所を自動的に特定することができる。人手では解析不可能な大規模プログラムに対しても自動で解析でき、大規模プログラム内の論理的な矛盾要因箇所を特定できる。この特定できた矛盾要因箇所により、プログラムの潜在的な不備や不具合を未然に防止するのに役立てることができる。本発明の上記プログラム解析装置では、モデル検査手段は、サブテスト項目をアサーションとして論理表現に変換し、サブテスト項目に対応する箇所にフラグを挿入してプログラムを加工し、該加工済みのプログラムとサブテスト項目に対応するアサーションをモデル検査にかける。このプログラム解析装置のモデル検査手段では、サブテスト項目における各分岐の切り替えをアサーションとして論理表現に変換するとともにサブテスト項目における各分岐の切り替え側の箇所にフラグを挿入してプログラムを加工し、その加工済みのプログラムとサブテスト項目に対応するアサーションをモデル検査にかける。これによって、プログラム解析装置は、サブテスト項目に対するモデル検査を自動かつ効率的にできる。本発明の上記プログラム解析装置では、データベースを備え、モデル検査手段でテストベクタを生成できる場合に該テストベクタを生成できるサブテスト項目をデータベースに登録する。このプログラム解析装置では、データベースを備えており、モデル検査手段でサブテスト項目に対するテストベクタを生成できる場合にはデータベースにそのテストベクタを生成できるサブテスト項目を登録する。このように、プログラム解析装置は、データベースにテストベクタを生成できるサブテスト項目を登録しておくことにより、テスト項目からサブテスト項目を生成する際にデータベースを参照して、データベースに登録されているサブテスト項目を除外してサブテスト項目を生成することにより、サブテスト項目を効率良く生成できる。本発明の上記プログラム解析装置では、モデル検査手段でテストベクタを生成できない場合に該テストベクタを生成できないサブテスト項目を要因特定手段で特定した要因の箇所としてデータベースに登録する。このプログラム解析装置では、データベースを備えており、モデル検査手段でサブテスト項目に対するテストベクタを生成できない場合にはデータベースにそのテストベクタを生成できないサブテスト項目をテストベクタを生成できない要因の箇所として登録する。このように、プログラム解析装置は、データベースにテストベクタを生成できないサブテスト項目すなわち、矛盾要因箇所を登録しておくことにより、データベースにプログラム内の論理的な矛盾要因箇所が自動的に蓄積され、その矛盾要因箇所を含むテスト項目に対する不要な解析を防止できる。本発明に係るプログラム解析方法は、モデル検査において任意のテスト項目に対してプログラムのテストベクタを生成できない場合にテストベクタを生成できない要因を解析するプログラム解析方法であって、テストベクタを生成できないテスト項目を段階的に分解し、サブテスト項目を生成するサブテスト項目生成ステップと、サブテスト項目生成ステップでサブテスト項目を生成する毎に、該サブテスト項目に対してモデル検査を行い、該サブテスト項目に対するテストベクタを生成するモデル検査ステップと、モデル検査ステップでテストベクタを生成できない場合に該テストベクタを生成できないサブテスト項目に基づいてテストベクタを生成できない要因の箇所を特定する要因特定ステップとを含むことを特徴とする。このプログラム解析方法によれば、各ステップの処理を行うことにより、上記プログラム解析装置の作用及び効果を奏する。本発明に係るプログラム解析プログラムは、モデル検査において任意のテスト項目に対してプログラムのテストベクタを生成できない場合にテストベクタを生成できない要因を解析するためのプログラム解析プログラムであって、コンピュータに、テストベクタを生成できないテスト項目を段階的に分解し、サブテスト項目を生成するサブテスト項目生成機能と、サブテスト項目生成機能でサブテスト項目を生成する毎に、該サブテスト項目に対してモデル検査を行い、該サブテスト項目に対するテストベクタを生成するモデル検査機能と、モデル検査機能でテストベクタを生成できない場合に該テストベクタを生成できないサブテスト項目に基づいてテストベクタを生成できない要因の箇所を特定する要因特定機能とを実現させることを特徴とする。このプログラム解析プログラムによれば、このプログラムをコンピュータに実行させることによって、上記プログラム解析装置の作用及び効果を奏する。本発明によれば、任意のテスト項目に対してテストベクタを生成できない場合に、その任意のテスト項目よりも条件を緩和したサブテスト項目に対してモデル検査を繰り返し行い、テストベクタを生成できないサブテスト項目を探索することにより、プログラム内の論理的な矛盾要因箇所を自動的に特定することができる。以下、図面を参照して、本発明に係るプログラム解析装置及びプログラム解析方法並びにプログラム解析プログラムの実施の形態を説明する。なお、各図において同一又は相当する要素については同一の符号を付し、重複する説明を省略する。本実施の形態では、本発明を、プログラムの要因解析装置に適用する。本実施の形態に係る要因解析装置は、モデル検査においてテスト項目に対してプログラムのテストベクタを生成できない場合に、プログラム内におけるテストベクタを生成できない要因を解析する装置である。なお、プログラムは、コンピュータを動作させるためのプログラムであり、1つ以上の分岐を含むプログラムである。テスト項目は、プログラム内に存在する分岐の切り替えの組み合わせで表される。テストベクタは、テスト項目における分岐の切り替えの組み合わせを満たすテスト入力テストデータであり、モデル検査によって探し出される。図1及び図2を参照して、本実施の形態に係る要因解析装置1について説明する。図1は、本実施の形態に係る要因解析装置の構成図である。図2は、分岐を含むプログラムの一例であり、aが加工無しのプログラムであり、bがモデル検査にかける加工済みのプログラムである。要因解析装置1は、プログラムPとそのプログラムPのテストベクタを生成できなかったテスト項目TIすなわち、論理的な矛盾要因を含むテスト項目が入力されると、そのテスト項目TIの条件を段階的に緩和しながらサブテスト項目STIを順次生成し、サブテスト項目STIが生成される毎にモデル検査を行い、テストベクタを生成できないサブテスト項目を探し出し、プログラムの論理的な矛盾要因箇所Cを特定する。そのために、要因解析装置1は、テスト項目データベース2、テスト項目制御部3、プログラム制御部4、モデル検査部5、結果判定部6、要因制御部7、テスト項目データベース制御部8から構成される。要因解析装置1は、要因解析だけを行う専用装置でもよいし、あるいは、汎用コンピュータで要因解析用のアプリケーションを実行することによって構成されてもよい。なお、本実施の形態では、テスト項目データベース2が特許請求の範囲に記載するデータベースに相当し、テスト項目制御部3が特許請求の範囲に記載するサブテスト項目生成手段に相当し、モデル検査部5モデル検査の手法によりテスト項目制御部3、プログラム制御部4を含む場合があるが特許請求の範囲に記載するモデル検査手段に相当し、結果判定部6及び要因制御部7が特許請求の範囲に記載する要因特定手段に相当する。テスト項目データベース2は、要因解析装置1の記憶装置に構築され、テスト項目の情報、サブテスト項目の情報、矛盾要因箇所の情報が登録されるデータベースである。登録されるテスト項目の情報は、要因解析装置1に入力されたテストベクタを生成できなかったテスト項目の情報である。テスト項目は、プログラム内に含まれる分岐の切り替えの組み合わせである。分岐は、例えば、図2に示すようなifとelseを用いたものがあり、この例の場合、ifの条件式を満たすTrue真への切り替えと条件式を満たさないFalse偽への切り替えの2つの切り替えパターンがある。例えば、プログラム中に4つの分岐が少なくとも存在する場合、1番目の分岐がTrueと2番目の分岐がTrueと3番目の分岐がFalseと4番目の分岐がTrueとからなるT1,T2,F3,T4とする組み合わせがテスト項目である。登録されるサブテスト項目の情報は、要因解析装置1におけるモデル検査においてテストベクタを生成できたサブテスト項目の情報である。サブテスト項目は、テスト項目の分岐の切り替えの組み合わせを分解した一部でありテスト項目の真部分集合であり、テスト項目よりも組み合わされる分岐の条件を緩和したテスト項目である。したがって、サブテスト項目に含まれる分岐の個数は、1個以上かつ元のテスト項目に含まれる分岐の個数-1個以下である。例えば、上記の例で示した元のテスト項目TIがT1,T2,F3,T4の場合、サブテスト項目としては、1番目の分岐のTrueと2番目の分岐のTrueと3番目の分岐のFalseからなるT1,T2,F3、1番目の分岐のTrueと2番目の分岐のTrueからなるT1,T2、1番目の分岐のTrueだけからなるT1等がある。登録される矛盾要因箇所の情報は、要因解析装置1におけるモデル検査においてテストベクタを生成できなかったサブテスト項目の情報すなわち、このサブテスト項目に含まれる分岐の切り替え側の箇所が矛盾要因箇所であり、その分岐の切り替え側の箇所を通過できないである。テスト項目制御部3では、入力されたテスト項目TIを段階的に分解洗練し、サブテスト項目STIを生成する。この際、テスト項目制御部3では、テスト項目データベース2に登録されているサブテスト項目を探索するためにテスト項目データベース制御部8に指令を出し、テスト項目データベース2のサブテスト項目の情報を参照する。サブテスト項目STIを生成する毎に、テスト項目制御部3では、そのサブテスト項目STIに含まれる各分岐の切り替えに対応するアサーションとして論理表現に変換する。サブテスト項目を段階的に分解する場合、サブテスト項目に含まれる分岐の切り替えの組み合わせが元のテスト項目の真部分集合になっていれば、どのような順に分解してもよい。例えば、サブテスト項目に含まれる分岐の個数については、1個から順に増やしていってもよいし、元のテスト項目に含まれる分岐の数-1個から順に少なくしていってもよいし、あるいは、分岐の個数についてはランダムに又は所定の条件に従って変更していってもよい。プログラム制御部4では、テスト項目制御部3でサブテスト項目STIを生成する毎に、入力されたプログラムPを加工し、サブテスト項目STIに含まれる各分岐の切り替えで通過する箇所にフラグを挿入する。モデル検査部5では、テスト項目制御部3でサブテスト項目STIを生成する毎に、サブテスト項目STIに対するテストベクタ反例を自動生成するために、サブテスト項目STIに対してモデル検査を行う。ここでは、プログラム制御部4で加工したプログラムとテスト項目制御部3で論理表現したサブテスト項目STIに対応するアサーションをモデル検査にかける。そして、モデル検査部5では、そのサブテスト項目STIに対するテストベクタの有無を判断する。図2aには、ifとelseによる分岐を含むプログラムの一部を示しており、ifの条件式gvar1grar2>10がTrueの場合にはtemp=1を実行し、条件式gvar1grar2>10がFalseの場合にはtemp=2を実行する。この分岐の切り替えがサブテスト項目に含まれており、切り替え側がFalseだったとする。この場合、図2bに示すように、プログラム制御部4によってelse{}の中にflag=1が挿入されるとともに、テスト項目制御部3によってアサーションの論理表現としてassertflag==1flag=1になるパスを探せというアサーションが設定され、モデル検査部5でflagを1にする入力データを探索する。その入力データテストベクタの一部としては、例えば、gvar1=2,gvar2=4である。なお、本実施の形態では、モデル検査として、サブテスト項目をアサーションとして論理表現に変換するとともにサブテスト項目に対向する通過する箇所にフラグを挿入してプログラムを加工してモデル検査を行う手法の一例を示したが、モデル検査についてはどのような手法で行ってもよい。結果判定部6では、モデル検査部5でモデル検査を行う毎に、モデル検査部5での出力結果テストベクタの有無に基づいて、そのサブテスト項目STIに対してテストベクタを生成できたか否かを判定する。テストベクタを生成できたと判定した場合、結果判定部6では、テストベクタを生成できたサブテスト項目STIの情報をテスト項目データベース2に登録するようにテスト項目データベース制御部8に指令を出す。要因制御部7では、結果判定部6で判定を行う毎に、結果判定部6でテストベクタを生成できなかったと判定している場合、そのテストベクタを生成できなかったサブテスト項目に含まれる分岐の切り替え箇所を論理的な矛盾要因箇所Cの情報としてテスト項目データベース2に登録するようにテスト項目データベース制御部8に指令を出すとともに、その矛盾要因箇所Cの情報を出力する。テスト項目データベース制御部8では、結果判定部6からの指令を受けて、テストベクタを生成できたサブテスト項目STIの情報をテスト項目データベース2に登録する。また、テスト項目データベース制御部8では、要因制御部7からの指令を受けて、矛盾要因箇所Cの情報をテスト項目データベース2に登録する。また、テスト項目データベース制御部8では、テスト項目制御部3からの指令を受けて、テスト項目データベース2に登録されているサブテスト項目の情報を探索する。次に、要因解析装置1の処理の流れについて図3のフローチャートに沿って説明する。図3は、図1の要因解析装置における処理の流れを示すフローチャートである。ここでは、サブテスト項目に含まれる分岐の個数として、1個から順に増やしていく場合である。なお、各処理についての説明において、テストベクタを生成できなかったテスト項目TIとして上記の例で示したT1,T2,F3,T4の場合のサブテスト項目の例を適宜挿入する。要因解析装置1には、テストベクタを生成できなかった解析対象のテスト項目TIとプログラムPが入力される。まず、要因解析装置1では、テスト項目データベース2に登録されている矛盾要因箇所の情報テストベクタを生成できなかったサブテスト項目の情報を参照し、解析対象のテスト項目TIが既知の矛盾要因を含んでいるか否かを判定するS1。S1にてテスト項目TIが既知の矛盾要因を含んでいると判定した場合、矛盾要因箇所を探索する必要がないので、要因解析装置1では、その矛盾要因を特定し、処理を終了する。S1にてテスト項目TIが既知の矛盾要因を含んでいないと判定した場合、要因解析装置1では、テスト項目TIから初期サブテスト項目STI0を設定するS2。初期サブテスト項目STI0は、テスト項目TIの真部分集合STI0⊂TIであれば、任意のものを選んでよい。ここでは、処理の効率化を図るために、テスト項目データベース2に登録されているテストベクタを生成できたサブテスト項目矛盾要因の無いサブテスト項目を除外した中で上記の条件を満たすものを選んでもよい。例えば、テスト項目TIのT1,T2,F3,T4の中から、1番目の分岐のTrueだけからなるT1を初期サブテスト項目STI0⊂TIとする。サブテスト項目STI0∪∪STIi⊂TIを生成する毎に、要因解析装置1では、サブテスト項目STI0∪∪STIi⊂TIに対してアサーションへの変換を行うとともにサブテスト項目STI0∪∪STIi⊂TIに対応してフラグを挿入してプログラムを加工するS3。そして、要因解析装置1では、サブテスト項目STI0∪∪STIi⊂TIのモデル検査を行い、サブテスト項目STI0∪∪STIi⊂TIに対するテストベクタ反例が見つかったか否かを判定するS3。S3にてサブテスト項目STI0∪∪STIi⊂TIに対してテストベクタが見つかったと判定した場合、要因解析装置1では、テストベクタを生成できたサブテスト項目STI0∪∪STIi⊂TIをテスト項目データベース2に登録するS4。さらに、要因解析装置1では、新たなサブテスト項目STIi1を追加する。追加するサブテスト項目STIi1は、現在のサブテスト項目STI0∪∪STIi⊂TIをさらに詳細化するために追加されるが、STI0∪∪STIi∪STIi1⊂TIを満たすものを任意選んでよい。例えば、サブテスト項目STI0∪∪STIi⊂TIが1番目の分岐のTrueと2番目の分岐のTrueからなるT1,T2の場合、3番目の分岐のFalseを追加し、T1,T2,F3を追加後のサブテスト項目STI0∪∪STIi∪STIi1⊂TIとする。そして、要因解析装置1では、このサブテスト項目STI0∪∪STIi∪STIi1⊂TIに対してモデル検査を行うS3。S3にてサブテスト項目STI0∪∪STIi∪STIi1⊂TIに対してテストベクタが見つからなかったと判定した場合、要因解析装置1では、最後に追加したサブテスト項目STIi1のみに対してアサーションへの変換を行うとともにサブテスト項目STIi1に対応してフラグを挿入してプログラムを加工するS6。そして、要因解析装置1では、サブテスト項目STIi1のモデル検査を行い、サブテスト項目STIi1に対するテストベクタが見つかったか否かを判定するS6。S6にて最後に追加したサブテスト項目STIi1に対してテストベクタが見つかったと判定した場合、要因解析装置1では、最後に追加したサブテスト項目STIi1とそれ以外の登録済みのサブテスト項目{STI0,,STIi}との組み合わせによって表現されるサブテスト項目を生成する。例えば、サブテスト項目STI0∪∪STIi⊂TIが1番目の分岐のTrueと2番目の分岐のTrueからなるT1,T2であり、最後に追加したサブテスト項目STIi1が3番目の分岐のFalseのF3だった場合、2番目の分岐のTrueと3番目の分岐のFalseとを組み合わせたT2,F3となるサブテスト項目を生成する。ここでも、処理の効率化を図るために、テスト項目データベース2に登録されているテストベクタを生成できたサブテスト項目を除外した中でサブテスト項目を生成するとよい。そして、要因解析装置1では、その組み合わせサブテスト項目に対してアサーションへの変換を行うとともに組み合わせサブテスト項目に対応してフラグを挿入してプログラムを加工するS8。そして、要因解析装置1では、その組み合わせサブテスト項目のモデル検査を行い、その組み合わせサブテスト項目に対するテストベクタが見つかったか否かを判定するS8。S8には組み合わせサブテスト項目に対してテストベクタが見つかったと判定した場合、要因解析装置1では、その組み合わせサブテスト項目をテスト項目データベース2に登録するS9。さらに、要因解析装置1では、最後に追加したサブテスト項目STIi1と既に組み合わせた以外のサブテスト項目{STI0,,STIi}との組み合わせによって表現されるサブテスト項目を生成する。ここでは、テスト項目データベース2に登録した組み合わせ済みのサブテスト項目を除外して組み合わせを行う。そして、要因解析装置1では、その組み合わせサブテスト項目に対してモデル検査を行うS8。S6にて最後に追加したサブテスト項目STIi1に対してテストベクタが見つらなかったと判定した場合又はS8には組み合わせサブテスト項目に対してテストベクタが見つからなかったと判定した場合、要因解析装置1では、そのサブテスト項目に含まれる分岐の切り替え箇所を論理的な矛盾要因箇所Cの情報としてテスト項目データベース2に登録するとともに、矛盾要因箇所Cの情報を出力するS10。そして、要因解析装置1では、処理を終了する。プログラムの開発者は、テスト項目データベース2に登録されている矛盾要因箇所Cの情報を参照し、プログラム内のその論理的な矛盾箇所を把握し、修正する必要がある場合にはプログラムを修正する。この要因解析装置1によれば、テストベクタを生成できなかったテスト項目が入力されると、そのテスト項目よりも条件を段階的に分解したサブテスト項目に対してモデル検査を繰り返し行い、テストベクタを生成できないサブテスト項目を探索することにより、プログラム内の論理的な矛盾要因箇所を自動的に特定することができる。これによって、人手では解析不可能な大規模プログラムに対しても自動で解析でき、大規模プログラム内の論理的な矛盾要因箇所を特定できる。この特定できた矛盾要因箇所により、プログラムの潜在的な不備や不具合を未然に防止するのに役立てることができる。また、要因解析装置1によれば、サブテスト項目に対してアサーションへの変換を行うとともにサブテスト項目に対応してフラグを挿入してプログラムを加工してモデル検査を行うことにより、サブテスト項目に対するモデル検査を自動かつ効率的にできる。また、要因解析装置1によれば、テスト項目データベース2を構築し、テストベクタを生成できるサブテスト項目の情報を登録しておくことにより、登録されているサブテスト項目を除外して新たなサブテスト項目を生成でき、解析効率が向上する。また、要因解析装置1によれば、テスト項目データベース2を構築し、矛盾要因箇所の情報テストベクタを生成できないサブテスト項目の情報を登録しておくことにより、その矛盾要因箇所を含むテスト項目に対する不要な解析を防止でき、解析効率が向上する。以上、本発明に係る実施の形態について説明したが、本発明は上記実施の形態に限定されることなく様々な形態で実施される。例えば、本実施の形態ではプログラムの矛盾要因箇所を特定する要因解析装置に適用したが、CD-ROM等の記憶媒体に格納されたプログラムやインタネット等のネットワークを介して利用可能なプログラム等に適用し、このようなプログラムをコンピュータ上で実行することによってプログラムの矛盾要因箇所を特定する構成としてもよい。また、本実施の形態では要因解析装置にデータベースを備える構成としたが、データベースが無くても構成可能である。また、上記したようにモデル検査についてどのような手法を適用してもよい。"